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 <iostream>
22#endif
23
24#include <unordered_set>
25
27 const namespacet &_ns,
28 propt &_prop,
32 ns(_ns),
34 message_handler(_message_handler)
35{
36 lazy_arrays = false; // will be set to true when --refine is used
37 incremental_cache = false; // for incremental solving
38 // get_array_constraints is true when --show-array-constraints is used
40}
41
43{
44 // we are not allowed to put the index directly in the
45 // entry for the root of the equivalence class
46 // because this map is accessed during building the error trace
47 std::size_t number=arrays.number(index.array());
48 if(index_map[number].insert(index.index()).second)
49 update_indices.insert(number);
50}
51
53 const equal_exprt &equality)
54{
55 const exprt &op0=equality.op0();
56 const exprt &op1=equality.op1();
57
59 op0.type() == op1.type(),
60 "record_array_equality got equality without matching types",
61 irep_pretty_diagnosticst{equality});
62
64 op0.type().id() == ID_array,
65 "record_array_equality parameter should be array-typed");
66
68
69 array_equalities.back().f1=op0;
70 array_equalities.back().f2=op1;
71 array_equalities.back().l=SUB::equality(op0, op1);
72
73 arrays.make_union(op0, op1);
74 collect_arrays(op0);
75 collect_arrays(op1);
76
77 return array_equalities.back().l;
78}
79
81{
82 for(std::size_t i=0; i<arrays.size(); i++)
83 {
85 }
86}
87
89{
90 if(expr.id()!=ID_index)
91 {
92 if(expr.id() == ID_array_comprehension)
95
96 forall_operands(op, expr) collect_indices(*op);
97 }
98 else
99 {
100 const index_exprt &e = to_index_expr(expr);
101
102 if(
103 e.index().id() == ID_symbol &&
106 {
107 return;
108 }
109
110 collect_indices(e.index()); // necessary?
111
112 const typet &array_op_type = e.array().type();
113
114 if(array_op_type.id()==ID_array)
115 {
116 const array_typet &array_type=
118
120 {
122 }
123 }
124 }
125}
126
128{
129 const array_typet &array_type = to_array_type(a.type());
130
131 if(a.id()==ID_with)
132 {
134
136 array_type == with_expr.old().type(),
137 "collect_arrays got 'with' without matching types",
139
142
143 // make sure this shows as an application
144 for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
145 {
146 index_exprt index_expr(with_expr.old(), with_expr.operands()[i]);
148 }
149 }
150 else if(a.id()==ID_update)
151 {
153
155 array_type == update_expr.old().type(),
156 "collect_arrays got 'update' without matching types",
158
161
162#if 0
163 // make sure this shows as an application
166#endif
167 }
168 else if(a.id()==ID_if)
169 {
171
173 array_type == if_expr.true_case().type(),
174 "collect_arrays got if without matching types",
176
178 array_type == if_expr.false_case().type(),
179 "collect_arrays got if without matching types",
181
182 arrays.make_union(a, if_expr.true_case());
183 arrays.make_union(a, if_expr.false_case());
184 collect_arrays(if_expr.true_case());
185 collect_arrays(if_expr.false_case());
186 }
187 else if(a.id()==ID_symbol)
188 {
189 }
190 else if(a.id()==ID_nondet_symbol)
191 {
192 }
193 else if(a.id()==ID_member)
194 {
195 const auto &struct_op = to_member_expr(a).struct_op();
196
198 struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
199 "unexpected array expression: member with '" + struct_op.id_string() +
200 "'");
201 }
202 else if(a.id()==ID_constant ||
203 a.id()==ID_array ||
204 a.id()==ID_string_constant)
205 {
206 }
207 else if(a.id()==ID_array_of)
208 {
209 }
210 else if(a.id()==ID_byte_update_little_endian ||
212 {
214 false,
215 "byte_update should be removed before collect_arrays");
216 }
217 else if(a.id()==ID_typecast)
218 {
219 const auto &typecast_op = to_typecast_expr(a).op();
220
221 // cast between array types?
223 typecast_op.type().id() == ID_array,
224 "unexpected array type cast from " + typecast_op.type().id_string());
225
228 }
229 else if(a.id()==ID_index)
230 {
231 // nested unbounded arrays
232 const auto &array_op = to_index_expr(a).array();
235 }
236 else if(a.id() == ID_array_comprehension)
237 {
238 }
239 else
240 {
242 false,
243 "unexpected array expression (collect_arrays): '" + a.id_string() + "'");
244 }
245}
246
249{
250 if(lazy_arrays && refine)
251 {
252 // lazily add the constraint
254 {
255 if(expr_map.find(lazy.lazy) == expr_map.end())
256 {
257 lazy_array_constraints.push_back(lazy);
258 expr_map[lazy.lazy] = true;
259 }
260 }
261 else
262 {
263 lazy_array_constraints.push_back(lazy);
264 }
265 }
266 else
267 {
268 // add the constraint eagerly
270 }
271}
272
274{
276 // at this point all indices should in the index set
277
278 // reduce initial index map
279 update_index_map(true);
280
281 // add constraints for if, with, array_of, lambda
282 std::set<std::size_t> roots_to_process, updated_roots;
283 for(std::size_t i=0; i<arrays.size(); i++)
285
286 while(!roots_to_process.empty())
287 {
288 for(std::size_t i = 0; i < arrays.size(); i++)
289 {
290 if(roots_to_process.count(arrays.find_number(i)) == 0)
291 continue;
292
293 // take a copy as arrays may get modified by add_array_constraints
294 // in case of nested unbounded arrays
295 exprt a = arrays[i];
296
298
299 // we have to update before it gets used in the next add_* call
300 for(const std::size_t u : update_indices)
302 update_index_map(false);
303 }
304
305 roots_to_process = std::move(updated_roots);
307 }
308
309 // add constraints for equalities
310 for(const auto &equality : array_equalities)
311 {
314 equality);
315
316 // update_index_map should not be necessary here
317 }
318
319 // add the Ackermann constraints
321}
322
324{
325 // this is quadratic!
326
327#ifdef DEBUG
328 std::cout << "arrays.size(): " << arrays.size() << '\n';
329#endif
330
331 // iterate over arrays
332 for(std::size_t i=0; i<arrays.size(); i++)
333 {
335
336#ifdef DEBUG
337 std::cout << "index_set.size(): " << index_set.size() << '\n';
338#endif
339
340 // iterate over indices, 2x!
341 for(index_sett::const_iterator
342 i1=index_set.begin();
343 i1!=index_set.end();
344 i1++)
345 for(index_sett::const_iterator
346 i2=i1;
347 i2!=index_set.end();
348 i2++)
349 if(i1!=i2)
350 {
351 if(i1->is_constant() && i2->is_constant())
352 continue;
353
354 // index equality
357
359
361 {
362 const typet &subtype =
364 index_exprt index_expr1(arrays[i], *i1, subtype);
365
367 index_expr2.index()=*i2;
368
370
371 // add constraint
374 add_array_constraint(lazy, true); // added lazily
376
377#if 0 // old code for adding, not significantly faster
379#endif
380 }
381 }
382 }
383}
384
387{
389 return;
390
391 std::size_t root_number=arrays.find_number(i);
392 INVARIANT(root_number!=i, "is_root_number incorrect?");
393
396
397 root_index_set.insert(index_set.begin(), index_set.end());
398}
399
401{
402 // iterate over non-roots
403 // possible reasons why update is needed:
404 // -- there are new equivalence classes in arrays
405 // -- there are new indices for arrays that are not the root
406 // of an equivalence class
407 // (and we cannot do that in record_array_index())
408 // -- equivalence classes have been merged
409 if(update_all)
410 {
411 for(std::size_t i=0; i<arrays.size(); i++)
413 }
414 else
415 {
416 for(const auto &index : update_indices)
417 update_index_map(index);
418
420 }
421
422#ifdef DEBUG
423 // print index sets
424 for(const auto &index_entry : index_map)
425 for(const auto &index : index_entry.second)
426 std::cout << "Index set (" << index_entry.first << " = "
427 << arrays.find_number(index_entry.first) << " = "
429 << "): " << format(index) << '\n';
430 std::cout << "-----\n";
431#endif
432}
433
435 const index_sett &index_set,
437{
438 // add constraints x=y => x[i]=y[i]
439
440 for(const auto &index : index_set)
441 {
442 const typet &element_type1 =
445
446 const typet &element_type2 =
449
451 index_expr1.type()==index_expr2.type(),
452 "array elements should all have same type");
453
454 array_equalityt equal;
455 equal.f1 = index_expr1;
456 equal.f2 = index_expr2;
457 equal.l = array_equality.l;
459
460 // add constraint
461 // equality constraints are not added lazily
462 // convert must be done to guarantee correct update of the index_set
465 }
466}
467
469 const index_sett &index_set,
470 const exprt &expr)
471{
472 if(expr.id()==ID_with)
474 else if(expr.id()==ID_update)
476 else if(expr.id()==ID_if)
478 else if(expr.id()==ID_array_of)
480 else if(expr.id() == ID_array)
482 else if(expr.id() == ID_array_comprehension)
483 {
486 }
487 else if(expr.id()==ID_symbol ||
488 expr.id()==ID_nondet_symbol ||
489 expr.id()==ID_constant ||
490 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 std::size_t i =
720 // if the access is out of bounds, we leave it unconstrained
721 if(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:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Boolean AND.
Definition std_expr.h:1974
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3182
const symbol_exprt & arg() const
Definition std_expr.h:3206
const exprt & body() const
Definition std_expr.h:3220
Array constructor from list of elements.
Definition std_expr.h:1476
const array_typet & type() const
Definition std_expr.h:1483
Array constructor from single element.
Definition std_expr.h:1411
const array_typet & type() const
Definition std_expr.h:1418
exprt & what()
Definition std_expr.h:1428
Arrays with given size.
Definition std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:777
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:434
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:323
bool lazy_arrays
Definition arrays.h:111
void collect_indices()
Definition arrays.cpp:80
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:127
union_find< exprt, irep_hash > arrays
Definition arrays.h:78
literalt record_array_equality(const equal_exprt &expr)
Definition arrays.cpp:52
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:26
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:273
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:42
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:248
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:400
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:643
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
Equality.
Definition std_expr.h:1225
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition equality.cpp:17
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
The trinary if-then-else operator.
Definition std_expr.h:2226
exprt & cond()
Definition std_expr.h:2243
exprt & false_case()
Definition std_expr.h:2263
exprt & true_case()
Definition std_expr.h:2253
Boolean implication.
Definition std_expr.h:2037
Array index operator.
Definition std_expr.h:1328
exprt & index()
Definition std_expr.h:1363
exprt & array()
Definition std_expr.h:1353
const std::string & id_string() const
Definition irep.h:399
const irep_idt & id() const
Definition irep.h:396
const exprt & struct_op() const
Definition std_expr.h:2697
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:2082
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
TO_BE_DOCUMENTED.
Definition prop.h:24
void l_set_to_true(literalt a)
Definition prop.h:51
void lcnf(literalt l0, literalt l1)
Definition prop.h:57
const irep_idt & get_identifier() const
Definition std_expr.h:109
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
const exprt & op() const
Definition std_expr.h:293
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:2496
Operator to update elements in structs and arrays.
Definition std_expr.h:2312
exprt & old()
Definition std_expr.h:2322
#define forall_operands(it, expr)
Definition expr.h:18
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)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#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:511
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:22
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:1456
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3249
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1506
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2374
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2561
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832