cprover
Loading...
Searching...
No Matches
arrays.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "arrays.h"
10
11#include <util/arith_tools.h>
12#include <util/json.h>
13#include <util/message.h>
14#include <util/replace_expr.h>
15#include <util/std_expr.h>
16
18#include <solvers/prop/prop.h>
19
20#ifdef DEBUG
21# include <util/format_expr.h>
22
23# include <iostream>
24#endif
25
26#include <unordered_set>
27
29 const namespacet &_ns,
30 propt &_prop,
34 ns(_ns),
36 message_handler(_message_handler)
37{
38 lazy_arrays = false; // will be set to true when --refine is used
39 incremental_cache = false; // for incremental solving
40 // get_array_constraints is true when --show-array-constraints is used
42}
43
45{
46 // we are not allowed to put the index directly in the
47 // entry for the root of the equivalence class
48 // because this map is accessed during building the error trace
49 std::size_t number=arrays.number(index.array());
50 if(index_map[number].insert(index.index()).second)
51 update_indices.insert(number);
52}
53
55 const equal_exprt &equality)
56{
57 const exprt &op0=equality.op0();
58 const exprt &op1=equality.op1();
59
61 op0.type() == op1.type(),
62 "record_array_equality got equality without matching types",
63 irep_pretty_diagnosticst{equality});
64
66 op0.type().id() == ID_array,
67 "record_array_equality parameter should be array-typed");
68
70
71 array_equalities.back().f1=op0;
72 array_equalities.back().f2=op1;
73 array_equalities.back().l=SUB::equality(op0, op1);
74
75 arrays.make_union(op0, op1);
76 collect_arrays(op0);
77 collect_arrays(op1);
78
79 return array_equalities.back().l;
80}
81
83{
84 for(std::size_t i=0; i<arrays.size(); i++)
85 {
87 }
88}
89
91{
92 if(expr.id()!=ID_index)
93 {
94 if(expr.id() == ID_array_comprehension)
96 to_array_comprehension_expr(expr).arg().get_identifier());
97
98 for(const auto &op : expr.operands())
100 }
101 else
102 {
103 const index_exprt &e = to_index_expr(expr);
104
105 if(
106 e.index().id() == ID_symbol &&
108 to_symbol_expr(e.index()).get_identifier()) != 0)
109 {
110 return;
111 }
112
113 collect_indices(e.index()); // necessary?
114
115 const typet &array_op_type = e.array().type();
116
117 if(array_op_type.id()==ID_array)
118 {
119 const array_typet &array_type=
121
123 {
125 }
126 }
127 }
128}
129
131{
132 const array_typet &array_type = to_array_type(a.type());
133
134 if(a.id()==ID_with)
135 {
137
139 array_type == with_expr.old().type(),
140 "collect_arrays got 'with' without matching types",
142
145
146 // make sure this shows as an application
147 for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
148 {
149 index_exprt index_expr(with_expr.old(), with_expr.operands()[i]);
151 }
152 }
153 else if(a.id()==ID_update)
154 {
156
158 array_type == update_expr.old().type(),
159 "collect_arrays got 'update' without matching types",
161
164
165#if 0
166 // make sure this shows as an application
169#endif
170 }
171 else if(a.id()==ID_if)
172 {
174
176 array_type == if_expr.true_case().type(),
177 "collect_arrays got if without matching types",
179
181 array_type == if_expr.false_case().type(),
182 "collect_arrays got if without matching types",
184
185 arrays.make_union(a, if_expr.true_case());
186 arrays.make_union(a, if_expr.false_case());
187 collect_arrays(if_expr.true_case());
188 collect_arrays(if_expr.false_case());
189 }
190 else if(a.id()==ID_symbol)
191 {
192 }
193 else if(a.id()==ID_nondet_symbol)
194 {
195 }
196 else if(a.id()==ID_member)
197 {
198 const auto &struct_op = to_member_expr(a).struct_op();
199
201 struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
202 "unexpected array expression: member with '" + struct_op.id_string() +
203 "'");
204 }
205 else if(a.is_constant() || a.id() == ID_array || a.id() == ID_string_constant)
206 {
207 }
208 else if(a.id()==ID_array_of)
209 {
210 }
211 else if(a.id()==ID_byte_update_little_endian ||
213 {
215 false,
216 "byte_update should be removed before collect_arrays");
217 }
218 else if(a.id()==ID_typecast)
219 {
220 const auto &typecast_op = to_typecast_expr(a).op();
221
222 // cast between array types?
224 typecast_op.type().id() == ID_array,
225 "unexpected array type cast from " + typecast_op.type().id_string());
226
229 }
230 else if(a.id()==ID_index)
231 {
232 // nested unbounded arrays
233 const auto &array_op = to_index_expr(a).array();
236 }
237 else if(a.id() == ID_array_comprehension)
238 {
239 }
240 else
241 {
243 false,
244 "unexpected array expression (collect_arrays): '" + a.id_string() + "'");
245 }
246}
247
250{
251 if(lazy_arrays && refine)
252 {
253 // lazily add the constraint
255 {
256 if(expr_map.find(lazy.lazy) == expr_map.end())
257 {
258 lazy_array_constraints.push_back(lazy);
259 expr_map[lazy.lazy] = true;
260 }
261 }
262 else
263 {
264 lazy_array_constraints.push_back(lazy);
265 }
266 }
267 else
268 {
269 // add the constraint eagerly
271 }
272}
273
275{
277 // at this point all indices should in the index set
278
279 // reduce initial index map
280 update_index_map(true);
281
282 // add constraints for if, with, array_of, lambda
283 std::set<std::size_t> roots_to_process, updated_roots;
284 for(std::size_t i=0; i<arrays.size(); i++)
286
287 while(!roots_to_process.empty())
288 {
289 for(std::size_t i = 0; i < arrays.size(); i++)
290 {
291 if(roots_to_process.count(arrays.find_number(i)) == 0)
292 continue;
293
294 // take a copy as arrays may get modified by add_array_constraints
295 // in case of nested unbounded arrays
296 exprt a = arrays[i];
297
299
300 // we have to update before it gets used in the next add_* call
301 for(const std::size_t u : update_indices)
303 update_index_map(false);
304 }
305
306 roots_to_process = std::move(updated_roots);
308 }
309
310 // add constraints for equalities
311 for(const auto &equality : array_equalities)
312 {
315 equality);
316
317 // update_index_map should not be necessary here
318 }
319
320 // add the Ackermann constraints
322}
323
325{
326 // this is quadratic!
327
328#ifdef DEBUG
329 std::cout << "arrays.size(): " << arrays.size() << '\n';
330#endif
331
332 // iterate over arrays
333 for(std::size_t i=0; i<arrays.size(); i++)
334 {
336
337#ifdef DEBUG
338 std::cout << "index_set.size(): " << index_set.size() << '\n';
339#endif
340
341 // iterate over indices, 2x!
342 for(index_sett::const_iterator
343 i1=index_set.begin();
344 i1!=index_set.end();
345 i1++)
346 for(index_sett::const_iterator
347 i2=i1;
348 i2!=index_set.end();
349 i2++)
350 if(i1!=i2)
351 {
352 if(i1->is_constant() && i2->is_constant())
353 continue;
354
355 // index equality
358
360
362 {
363 const typet &subtype =
364 to_array_type(arrays[i].type()).element_type();
365 index_exprt index_expr1(arrays[i], *i1, subtype);
366
368 index_expr2.index()=*i2;
369
371
372 // add constraint
375 add_array_constraint(lazy, true); // added lazily
377
378#if 0 // old code for adding, not significantly faster
380#endif
381 }
382 }
383 }
384}
385
387void arrayst::update_index_map(std::size_t i)
388{
390 return;
391
392 std::size_t root_number=arrays.find_number(i);
393 INVARIANT(root_number!=i, "is_root_number incorrect?");
394
397
398 root_index_set.insert(index_set.begin(), index_set.end());
399}
400
402{
403 // iterate over non-roots
404 // possible reasons why update is needed:
405 // -- there are new equivalence classes in arrays
406 // -- there are new indices for arrays that are not the root
407 // of an equivalence class
408 // (and we cannot do that in record_array_index())
409 // -- equivalence classes have been merged
410 if(update_all)
411 {
412 for(std::size_t i=0; i<arrays.size(); i++)
414 }
415 else
416 {
417 for(const auto &index : update_indices)
418 update_index_map(index);
419
420 update_indices.clear();
421 }
422
423#ifdef DEBUG
424 // print index sets
425 for(const auto &index_entry : index_map)
426 for(const auto &index : index_entry.second)
427 std::cout << "Index set (" << index_entry.first << " = "
428 << arrays.find_number(index_entry.first) << " = "
430 << "): " << format(index) << '\n';
431 std::cout << "-----\n";
432#endif
433}
434
436 const index_sett &index_set,
438{
439 // add constraints x=y => x[i]=y[i]
440
441 for(const auto &index : index_set)
442 {
443 const typet &element_type1 =
444 to_array_type(array_equality.f1.type()).element_type();
446
447 const typet &element_type2 =
448 to_array_type(array_equality.f2.type()).element_type();
450
452 index_expr1.type()==index_expr2.type(),
453 "array elements should all have same type");
454
455 array_equalityt equal;
456 equal.f1 = index_expr1;
457 equal.f2 = index_expr2;
458 equal.l = array_equality.l;
460
461 // add constraint
462 // equality constraints are not added lazily
463 // convert must be done to guarantee correct update of the index_set
466 }
467}
468
470 const index_sett &index_set,
471 const exprt &expr)
472{
473 if(expr.id()==ID_with)
475 else if(expr.id()==ID_update)
477 else if(expr.id()==ID_if)
479 else if(expr.id()==ID_array_of)
481 else if(expr.id() == ID_array)
483 else if(expr.id() == ID_array_comprehension)
484 {
487 }
488 else if(
489 expr.id() == ID_symbol || expr.id() == ID_nondet_symbol ||
490 expr.is_constant() || expr.id() == "zero_string" ||
491 expr.id() == ID_string_constant)
492 {
493 }
494 else if(
495 expr.id() == ID_member &&
496 (to_member_expr(expr).struct_op().id() == ID_symbol ||
497 to_member_expr(expr).struct_op().id() == ID_nondet_symbol))
498 {
499 }
500 else if(expr.id()==ID_byte_update_little_endian ||
502 {
503 INVARIANT(false, "byte_update should be removed before arrayst");
504 }
505 else if(expr.id()==ID_typecast)
506 {
507 // we got a=(type[])b
508 const auto &expr_typecast_op = to_typecast_expr(expr).op();
509
510 // add a[i]=b[i]
511 for(const auto &index : index_set)
512 {
513 const typet &element_type = to_array_type(expr.type()).element_type();
514 index_exprt index_expr1(expr, index, element_type);
515 index_exprt index_expr2(expr_typecast_op, index, element_type);
516
518 index_expr1.type()==index_expr2.type(),
519 "array elements should all have same type");
520
521 // add constraint
524 add_array_constraint(lazy, false); // added immediately
526 }
527 }
528 else if(expr.id()==ID_index)
529 {
530 }
531 else
532 {
534 false,
535 "unexpected array expression (add_array_constraints): '" +
536 expr.id_string() + "'");
537 }
538}
539
541 const index_sett &index_set,
542 const with_exprt &expr)
543{
544 // We got x=(y with [i:=v, j:=w, ...]).
545 // First add constraints x[i]=v, x[j]=w, ...
546 std::unordered_set<exprt, irep_hash> updated_indices;
547
548 const exprt::operandst &operands = expr.operands();
549 for(std::size_t i = 1; i + 1 < operands.size(); i += 2)
550 {
551 const exprt &index = operands[i];
552 const exprt &value = operands[i + 1];
553
555 expr, index, to_array_type(expr.type()).element_type());
556
558 index_expr.type() == value.type(),
559 "with-expression operand should match array element type",
561
564 add_array_constraint(lazy, false); // added immediately
566
567 updated_indices.insert(index);
568 }
569
570 // For all other indices use the existing value, i.e., add constraints
571 // x[I]=y[I] for I!=i,j,...
572
573 for(auto other_index : index_set)
574 {
576 {
577 // we first build the guard
579 disjuncts.reserve(updated_indices.size());
580 for(const auto &index : updated_indices)
581 {
582 disjuncts.push_back(equal_exprt{
583 index, typecast_exprt::conditional_cast(other_index, index.type())});
584 }
585
587
588 if(guard_lit!=const_literal(true))
589 {
590 const typet &element_type = to_array_type(expr.type()).element_type();
591 index_exprt index_expr1(expr, other_index, element_type);
592 index_exprt index_expr2(expr.old(), other_index, element_type);
593
595
596 // add constraint
599
600 add_array_constraint(lazy, false); // added immediately
602
603#if 0 // old code for adding, not significantly faster
604 {
606
607 bvt bv;
608 bv.reserve(2);
609 bv.push_back(equality_lit);
610 bv.push_back(guard_lit);
611 prop.lcnf(bv);
612 }
613#endif
614 }
615 }
616 }
617}
618
620 const index_sett &,
621 const update_exprt &)
622{
623 // we got x=UPDATE(y, [i], v)
624 // add constaint x[i]=v
625
626#if 0
627 const exprt &index=expr.where();
628 const exprt &value=expr.new_value();
629
630 {
631 index_exprt index_expr(expr, index, expr.type().subtype());
632
634 index_expr.type()==value.type(),
635 "update operand should match array element type",
637
639 }
640
641 // use other array index applications for "else" case
642 // add constraint x[I]=y[I] for I!=i
643
644 for(auto other_index : index_set)
645 {
646 if(other_index!=index)
647 {
648 // we first build the guard
649
651
653
654 if(guard_lit!=const_literal(true))
655 {
656 const typet &subtype=expr.type().subtype();
657 index_exprt index_expr1(expr, other_index, subtype);
658 index_exprt index_expr2(expr.op0(), other_index, subtype);
659
661
663
664 // add constraint
665 bvt bv;
666 bv.reserve(2);
667 bv.push_back(equality_lit);
668 bv.push_back(guard_lit);
669 prop.lcnf(bv);
670 }
671 }
672 }
673#endif
674}
675
677 const index_sett &index_set,
678 const array_of_exprt &expr)
679{
680 // we got x=array_of[v]
681 // get other array index applications
682 // and add constraint x[i]=v
683
684 for(const auto &index : index_set)
685 {
686 const typet &element_type = expr.type().element_type();
687 index_exprt index_expr(expr, index, element_type);
688
690 index_expr.type() == expr.what().type(),
691 "array_of operand type should match array element type");
692
693 // add constraint
696 add_array_constraint(lazy, false); // added immediately
698 }
699}
700
702 const index_sett &index_set,
703 const array_exprt &expr)
704{
705 // we got x = { v, ... } - add constraint x[i] = v
706 const exprt::operandst &operands = expr.operands();
707
708 for(const auto &index : index_set)
709 {
710 const typet &element_type = expr.type().element_type();
711 const index_exprt index_expr{expr, index, element_type};
712
713 if(index.is_constant())
714 {
715 // We have a constant index - just pick the element at that index from the
716 // array constant.
717
718 const optionalt<std::size_t> i =
720 // if the access is out of bounds, we leave it unconstrained
721 if(!i.has_value() || *i >= operands.size())
722 continue;
723
724 const exprt v = operands[*i];
726 index_expr.type() == v.type(),
727 "array operand type should match array element type");
728
729 // add constraint
732 add_array_constraint(lazy, false); // added immediately
734 }
735 else
736 {
737 // We have a non-constant index into an array constant. We need to build a
738 // case statement testing the index against all possible values. Whenever
739 // neighbouring array elements are the same, we can test the index against
740 // the range rather than individual elements. This should be particularly
741 // helpful when we have arrays of zeros, as is the case for initializers.
742
743 std::vector<std::pair<std::size_t, std::size_t>> ranges;
744
745 for(std::size_t i = 0; i < operands.size(); ++i)
746 {
747 if(ranges.empty() || operands[i] != operands[ranges.back().first])
748 ranges.emplace_back(i, i);
749 else
750 ranges.back().second = i;
751 }
752
753 for(const auto &range : ranges)
754 {
756
757 if(range.first == range.second)
758 {
760 equal_exprt{index, from_integer(range.first, index.type())};
761 }
762 else
763 {
766 from_integer(range.first, index.type()), ID_le, index},
768 index, ID_le, from_integer(range.second, index.type())}};
769 }
770
774 equal_exprt{index_expr, operands[range.first]}}};
775 add_array_constraint(lazy, true); // added lazily
777 }
778 }
779 }
780}
781
783 const index_sett &index_set,
784 const array_comprehension_exprt &expr)
785{
786 // we got x=lambda(i: e)
787 // get all other array index applications
788 // and add constraints x[j]=e[i/j]
789
790 for(const auto &index : index_set)
791 {
792 index_exprt index_expr{expr, index};
794 replace_expr(expr.arg(), index, comprehension_body);
795
796 // add constraint
800
801 add_array_constraint(lazy, false); // added immediately
803 }
804}
805
807 const index_sett &index_set,
808 const if_exprt &expr)
809{
810 // we got x=(c?a:b)
812
813 // get other array index applications
814 // and add c => x[i]=a[i]
815 // !c => x[i]=b[i]
816
817 // first do true case
818
819 for(const auto &index : index_set)
820 {
821 const typet &element_type = to_array_type(expr.type()).element_type();
822 index_exprt index_expr1(expr, index, element_type);
823 index_exprt index_expr2(expr.true_case(), index, element_type);
824
825 // add implication
829 add_array_constraint(lazy, false); // added immediately
831
832#if 0 // old code for adding, not significantly faster
834#endif
835 }
836
837 // now the false case
838 for(const auto &index : index_set)
839 {
840 const typet &element_type = to_array_type(expr.type()).element_type();
841 index_exprt index_expr1(expr, index, element_type);
842 index_exprt index_expr2(expr.false_case(), index, element_type);
843
844 // add implication
849 add_array_constraint(lazy, false); // added immediately
851
852#if 0 // old code for adding, not significantly faster
854#endif
855 }
856}
857
859{
860 switch(type)
861 {
863 return "arrayAckermann";
865 return "arrayWith";
867 return "arrayIf";
869 return "arrayOf";
871 return "arrayTypecast";
873 return "arrayConstant";
875 return "arrayComprehension";
877 return "arrayEquality";
878 default:
880 }
881}
882
884{
887 json_result["arrayConstraints"].make_object();
888
889 size_t num_constraints = 0;
890
891 array_constraint_countt::iterator it = array_constraint_count.begin();
892 while(it != array_constraint_count.end())
893 {
894 std::string contraint_type_string = enum_to_string(it->first);
896 json_numbert(std::to_string(it->second));
897
898 num_constraints += it->second;
899 it++;
900 }
901
902 json_result["numOfConstraints"] =
903 json_numbert(std::to_string(num_constraints));
904 log.status() << ",\n" << json_result;
905}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Theory of Arrays with Extensionality.
virtual void clear()
Reset the abstract state.
Definition ai.h:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Boolean AND.
Definition std_expr.h:2071
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3358
const symbol_exprt & arg() const
Definition std_expr.h:3382
const exprt & body() const
Definition std_expr.h:3396
Array constructor from list of elements.
Definition std_expr.h:1563
const array_typet & type() const
Definition std_expr.h:1570
Array constructor from single element.
Definition std_expr.h:1498
const array_typet & type() const
Definition std_expr.h:1505
exprt & what()
Definition std_expr.h:1515
Arrays with given size.
Definition std_types.h:763
std::list< lazy_constraintt > lazy_array_constraints
Definition arrays.h:114
std::unordered_set< irep_idt > array_comprehension_args
Definition arrays.h:163
index_mapt index_map
Definition arrays.h:85
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition arrays.cpp:435
std::set< std::size_t > update_indices
Definition arrays.h:159
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
Definition arrays.cpp:676
void add_array_Ackermann_constraints()
Definition arrays.cpp:324
bool lazy_arrays
Definition arrays.h:111
void collect_indices()
Definition arrays.cpp:82
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition arrays.cpp:619
void collect_arrays(const exprt &a)
Definition arrays.cpp:130
union_find< exprt, irep_hash > arrays
Definition arrays.h:78
literalt record_array_equality(const equal_exprt &expr)
Definition arrays.cpp:54
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
Definition arrays.cpp:701
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition arrays.cpp:28
constraint_typet
Definition arrays.h:119
std::map< exprt, bool > expr_map
Definition arrays.h:116
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition arrays.cpp:806
std::string enum_to_string(constraint_typet)
Definition arrays.cpp:858
bool get_array_constraints
Definition arrays.h:113
void add_array_constraints()
Definition arrays.cpp:274
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
Definition arrays.cpp:782
virtual bool is_unbounded_array(const typet &type) const =0
void record_array_index(const index_exprt &expr)
Definition arrays.cpp:44
array_equalitiest array_equalities
Definition arrays.h:75
std::set< exprt > index_sett
Definition arrays.h:81
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
Definition arrays.cpp:249
array_constraint_countt array_constraint_count
Definition arrays.h:131
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition arrays.cpp:540
bool incremental_cache
Definition arrays.h:112
void display_array_constraint_count()
Definition arrays.cpp:883
void update_index_map(bool update_all)
Definition arrays.cpp:401
messaget log
Definition arrays.h:57
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:676
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
Equality.
Definition std_expr.h:1306
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition equality.cpp:17
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The trinary if-then-else operator.
Definition std_expr.h:2323
exprt & cond()
Definition std_expr.h:2340
exprt & false_case()
Definition std_expr.h:2360
exprt & true_case()
Definition std_expr.h:2350
Boolean implication.
Definition std_expr.h:2134
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
const std::string & id_string() const
Definition irep.h:399
const irep_idt & id() const
Definition irep.h:396
mstreamt & status() const
Definition message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Boolean OR.
Definition std_expr.h:2179
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
TO_BE_DOCUMENTED.
Definition prop.h:25
void l_set_to_true(literalt a)
Definition prop.h:52
void lcnf(literalt l0, literalt l1)
Definition prop.h:58
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
size_type number(const T &a)
Definition union_find.h:235
bool make_union(const T &a, const T &b)
Definition union_find.h:155
size_t size() const
Definition union_find.h:268
size_type find_number(const_iterator it) const
Definition union_find.h:201
bool is_root_number(size_type a) const
Definition union_find.h:216
Operator to update elements in structs and arrays.
Definition std_expr.h:2608
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
exprt & old()
Definition std_expr.h:2434
static format_containert< T > format(const T &o)
Definition format.h:37
auto lazy(funt fun) -> lazyt< decltype(fun())>
Delay the computation of fun to the next time the force method is called.
Definition lazy.h:49
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition invariant.h:535
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:51
API to expression classes.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1543
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3425
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1603
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2486
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2688
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844