CBMC
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/replace_symbol.h>
16#include <util/std_expr.h>
17
19#include <solvers/prop/prop.h>
20
21#ifdef DEBUG
22# include <util/format_expr.h>
23
24# include <iostream>
25#endif
26
27#include <unordered_set>
28
30 const namespacet &_ns,
31 propt &_prop,
35 ns(_ns),
37 message_handler(_message_handler)
38{
39 lazy_arrays = false; // will be set to true when --refine is used
40 incremental_cache = false; // for incremental solving
41 // get_array_constraints is true when --show-array-constraints is used
43}
44
46{
47 // we are not allowed to put the index directly in the
48 // entry for the root of the equivalence class
49 // because this map is accessed during building the error trace
50 std::size_t number=arrays.number(index.array());
51 if(index_map[number].insert(index.index()).second)
52 update_indices.insert(number);
53}
54
56 const equal_exprt &equality)
57{
58 const exprt &op0=equality.op0();
59 const exprt &op1=equality.op1();
60
62 op0.type() == op1.type(),
63 "record_array_equality got equality without matching types",
64 irep_pretty_diagnosticst{equality});
65
67 op0.type().id() == ID_array,
68 "record_array_equality parameter should be array-typed");
69
71
72 array_equalities.back().f1=op0;
73 array_equalities.back().f2=op1;
74 array_equalities.back().l=SUB::equality(op0, op1);
75
76 arrays.make_union(op0, op1);
77 collect_arrays(op0);
78 collect_arrays(op1);
79
80 return array_equalities.back().l;
81}
82
84{
85 for(std::size_t i=0; i<arrays.size(); i++)
86 {
88 }
89}
90
92{
93 if(expr.id()!=ID_index)
94 {
95 if(expr.id() == ID_array_comprehension)
97 to_array_comprehension_expr(expr).arg().get_identifier());
98
99 for(const auto &op : expr.operands())
100 collect_indices(op);
101 }
102 else
103 {
104 const index_exprt &e = to_index_expr(expr);
105
106 if(
107 e.index().id() == ID_symbol &&
109 to_symbol_expr(e.index()).get_identifier()) != 0)
110 {
111 return;
112 }
113
114 collect_indices(e.index()); // necessary?
115
116 const typet &array_op_type = e.array().type();
117
118 if(array_op_type.id()==ID_array)
119 {
120 const array_typet &array_type=
122
124 {
126 }
127 }
128 }
129}
130
132{
133 const array_typet &array_type = to_array_type(a.type());
134
135 if(a.id()==ID_with)
136 {
138
140 array_type == with_expr.old().type(),
141 "collect_arrays got 'with' without matching types",
143
146
147 // make sure this shows as an application
150 }
151 else if(a.id()==ID_update)
152 {
154
156 array_type == update_expr.old().type(),
157 "collect_arrays got 'update' without matching types",
159
162
163#if 0
164 // make sure this shows as an application
167#endif
168 }
169 else if(a.id()==ID_if)
170 {
172
174 array_type == if_expr.true_case().type(),
175 "collect_arrays got if without matching types",
177
179 array_type == if_expr.false_case().type(),
180 "collect_arrays got if without matching types",
182
183 arrays.make_union(a, if_expr.true_case());
184 arrays.make_union(a, if_expr.false_case());
185 collect_arrays(if_expr.true_case());
186 collect_arrays(if_expr.false_case());
187 }
188 else if(a.id()==ID_symbol)
189 {
190 }
191 else if(a.id()==ID_nondet_symbol)
192 {
193 }
194 else if(a.id()==ID_member)
195 {
196 const auto &struct_op = to_member_expr(a).struct_op();
197
199 struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
200 "unexpected array expression: member with '" + struct_op.id_string() +
201 "'");
202 }
203 else if(a.is_constant() || a.id() == ID_array || a.id() == ID_string_constant)
204 {
205 }
206 else if(a.id()==ID_array_of)
207 {
208 }
209 else if(a.id()==ID_byte_update_little_endian ||
211 {
213 false,
214 "byte_update should be removed before collect_arrays");
215 }
216 else if(a.id()==ID_typecast)
217 {
218 const auto &typecast_op = to_typecast_expr(a).op();
219
220 // cast between array types?
222 typecast_op.type().id() == ID_array,
223 "unexpected array type cast from " + typecast_op.type().id_string());
224
227 }
228 else if(a.id()==ID_index)
229 {
230 // nested unbounded arrays
231 const auto &array_op = to_index_expr(a).array();
234 }
235 else if(a.id() == ID_array_comprehension)
236 {
237 }
239 {
240 arrays.make_union(a, let_expr->where());
241 collect_arrays(let_expr->where());
242 }
243 else
244 {
246 false,
247 "unexpected array expression (collect_arrays): '" + a.id_string() + "'");
248 }
249}
250
253{
254 if(lazy_arrays && refine)
255 {
256 // lazily add the constraint
258 {
259 if(expr_map.find(lazy.lazy) == expr_map.end())
260 {
261 lazy_array_constraints.push_back(lazy);
262 expr_map[lazy.lazy] = true;
263 }
264 }
265 else
266 {
267 lazy_array_constraints.push_back(lazy);
268 }
269 }
270 else
271 {
272 // add the constraint eagerly
274 }
275}
276
278{
280 // at this point all indices should in the index set
281
282 // reduce initial index map
283 update_index_map(true);
284
285 // add constraints for if, with, array_of, lambda
286 std::set<std::size_t> roots_to_process, updated_roots;
287 for(std::size_t i=0; i<arrays.size(); i++)
289
290 while(!roots_to_process.empty())
291 {
292 for(std::size_t i = 0; i < arrays.size(); i++)
293 {
294 if(roots_to_process.count(arrays.find_number(i)) == 0)
295 continue;
296
297 // take a copy as arrays may get modified by add_array_constraints
298 // in case of nested unbounded arrays
299 exprt a = arrays[i];
300
302
303 // we have to update before it gets used in the next add_* call
304 for(const std::size_t u : update_indices)
306 update_index_map(false);
307 }
308
309 roots_to_process = std::move(updated_roots);
311 }
312
313 // add constraints for equalities
314 for(const auto &equality : array_equalities)
315 {
318 equality);
319
320 // update_index_map should not be necessary here
321 }
322
323 // add the Ackermann constraints
325}
326
328{
329 // this is quadratic!
330
331#ifdef DEBUG
332 std::cout << "arrays.size(): " << arrays.size() << '\n';
333#endif
334
335 // iterate over arrays
336 for(std::size_t i=0; i<arrays.size(); i++)
337 {
339
340#ifdef DEBUG
341 std::cout << "index_set.size(): " << index_set.size() << '\n';
342#endif
343
344 // iterate over indices, 2x!
345 for(index_sett::const_iterator
346 i1=index_set.begin();
347 i1!=index_set.end();
348 i1++)
349 for(index_sett::const_iterator
350 i2=i1;
351 i2!=index_set.end();
352 i2++)
353 if(i1!=i2)
354 {
355 if(i1->is_constant() && i2->is_constant())
356 continue;
357
358 // index equality
361
363
365 {
366 const typet &subtype =
367 to_array_type(arrays[i].type()).element_type();
368 index_exprt index_expr1(arrays[i], *i1, subtype);
369
371 index_expr2.index()=*i2;
372
374
375 // add constraint
378 add_array_constraint(lazy, true); // added lazily
380
381#if 0 // old code for adding, not significantly faster
383#endif
384 }
385 }
386 }
387}
388
390void arrayst::update_index_map(std::size_t i)
391{
393 return;
394
395 std::size_t root_number=arrays.find_number(i);
396 INVARIANT(root_number!=i, "is_root_number incorrect?");
397
400
401 root_index_set.insert(index_set.begin(), index_set.end());
402}
403
405{
406 // iterate over non-roots
407 // possible reasons why update is needed:
408 // -- there are new equivalence classes in arrays
409 // -- there are new indices for arrays that are not the root
410 // of an equivalence class
411 // (and we cannot do that in record_array_index())
412 // -- equivalence classes have been merged
413 if(update_all)
414 {
415 for(std::size_t i=0; i<arrays.size(); i++)
417 }
418 else
419 {
420 for(const auto &index : update_indices)
421 update_index_map(index);
422
424 }
425
426#ifdef DEBUG
427 // print index sets
428 for(const auto &index_entry : index_map)
429 for(const auto &index : index_entry.second)
430 std::cout << "Index set (" << index_entry.first << " = "
431 << arrays.find_number(index_entry.first) << " = "
433 << "): " << format(index) << '\n';
434 std::cout << "-----\n";
435#endif
436}
437
439 const index_sett &index_set,
441{
442 // add constraints x=y => x[i]=y[i]
443
444 for(const auto &index : index_set)
445 {
446 const typet &element_type1 =
447 to_array_type(array_equality.f1.type()).element_type();
449
450 const typet &element_type2 =
451 to_array_type(array_equality.f2.type()).element_type();
453
455 index_expr1.type()==index_expr2.type(),
456 "array elements should all have same type");
457
458 array_equalityt equal;
459 equal.f1 = index_expr1;
460 equal.f2 = index_expr2;
461 equal.l = array_equality.l;
463
464 // add constraint
465 // equality constraints are not added lazily
466 // convert must be done to guarantee correct update of the index_set
469 }
470}
471
473 const index_sett &index_set,
474 const exprt &expr)
475{
476 if(expr.id()==ID_with)
478 else if(expr.id()==ID_update)
480 else if(expr.id()==ID_if)
482 else if(expr.id()==ID_array_of)
484 else if(expr.id() == ID_array)
486 else if(expr.id() == ID_array_comprehension)
487 {
490 }
491 else if(
492 expr.id() == ID_symbol || expr.id() == ID_nondet_symbol ||
493 expr.is_constant() || expr.id() == "zero_string" ||
494 expr.id() == ID_string_constant)
495 {
496 }
497 else if(
498 expr.id() == ID_member &&
499 (to_member_expr(expr).struct_op().id() == ID_symbol ||
500 to_member_expr(expr).struct_op().id() == ID_nondet_symbol))
501 {
502 }
503 else if(expr.id()==ID_byte_update_little_endian ||
505 {
506 INVARIANT(false, "byte_update should be removed before arrayst");
507 }
508 else if(expr.id()==ID_typecast)
509 {
510 // we got a=(type[])b
511 const auto &expr_typecast_op = to_typecast_expr(expr).op();
512
513 // add a[i]=b[i]
514 for(const auto &index : index_set)
515 {
516 const typet &element_type = to_array_type(expr.type()).element_type();
517 index_exprt index_expr1(expr, index, element_type);
518 index_exprt index_expr2(expr_typecast_op, index, element_type);
519
521 index_expr1.type()==index_expr2.type(),
522 "array elements should all have same type");
523
524 // add constraint
527 add_array_constraint(lazy, false); // added immediately
529 }
530 }
531 else if(expr.id()==ID_index)
532 {
533 }
534 else if(auto let_expr = expr_try_dynamic_cast<let_exprt>(expr))
535 {
536 // we got x=let(a=e, A)
537 // add x[i]=A[a/e][i]
538
539 exprt where = let_expr->where();
540 replace_symbolt replace_symbol;
541 for(const auto &binding :
542 make_range(let_expr->variables()).zip(let_expr->values()))
543 {
544 replace_symbol.insert(binding.first, binding.second);
545 }
546 replace_symbol(where);
547
548 for(const auto &index : index_set)
549 {
550 index_exprt index_expr{expr, index};
551 index_exprt where_indexed{where, index};
552
553 // add constraint
556
557 add_array_constraint(lazy, false); // added immediately
559 }
560 }
561 else
562 {
564 false,
565 "unexpected array expression (add_array_constraints): '" +
566 expr.id_string() + "'");
567 }
568}
569
571 const index_sett &index_set,
572 const with_exprt &expr)
573{
574 // We got x=(y with [i:=v]).
575 // First add constraint x[i]=v
576 std::unordered_set<exprt, irep_hash> updated_indices;
577
579 expr, expr.where(), to_array_type(expr.type()).element_type());
580
582 index_expr.type() == expr.new_value().type(),
583 "with-expression operand should match array element type",
585
588 add_array_constraint(lazy, false); // added immediately
590
591 updated_indices.insert(expr.where());
592
593 // For all other indices use the existing value, i.e., add constraints
594 // x[I]=y[I] for I!=i,j,...
595
596 for(auto other_index : index_set)
597 {
599 {
600 // we first build the guard
602 disjuncts.reserve(updated_indices.size());
603 for(const auto &index : updated_indices)
604 {
605 disjuncts.push_back(equal_exprt{
606 index, typecast_exprt::conditional_cast(other_index, index.type())});
607 }
608
610
611 if(guard_lit!=const_literal(true))
612 {
613 const typet &element_type = to_array_type(expr.type()).element_type();
614 index_exprt index_expr1(expr, other_index, element_type);
615 index_exprt index_expr2(expr.old(), other_index, element_type);
616
618
619 // add constraint
622
623 add_array_constraint(lazy, false); // added immediately
625
626#if 0 // old code for adding, not significantly faster
627 {
629
630 bvt bv;
631 bv.reserve(2);
632 bv.push_back(equality_lit);
633 bv.push_back(guard_lit);
634 prop.lcnf(bv);
635 }
636#endif
637 }
638 }
639 }
640}
641
643 const index_sett &,
644 const update_exprt &)
645{
646 // we got x=UPDATE(y, [i], v)
647 // add constaint x[i]=v
648
649#if 0
650 const exprt &index=expr.where();
651 const exprt &value=expr.new_value();
652
653 {
654 index_exprt index_expr(expr, index, expr.type().subtype());
655
657 index_expr.type()==value.type(),
658 "update operand should match array element type",
660
662 }
663
664 // use other array index applications for "else" case
665 // add constraint x[I]=y[I] for I!=i
666
667 for(auto other_index : index_set)
668 {
669 if(other_index!=index)
670 {
671 // we first build the guard
672
674
676
677 if(guard_lit!=const_literal(true))
678 {
679 const typet &subtype=expr.type().subtype();
680 index_exprt index_expr1(expr, other_index, subtype);
681 index_exprt index_expr2(expr.op0(), other_index, subtype);
682
684
686
687 // add constraint
688 bvt bv;
689 bv.reserve(2);
690 bv.push_back(equality_lit);
691 bv.push_back(guard_lit);
692 prop.lcnf(bv);
693 }
694 }
695 }
696#endif
697}
698
700 const index_sett &index_set,
701 const array_of_exprt &expr)
702{
703 // we got x=array_of[v]
704 // get other array index applications
705 // and add constraint x[i]=v
706
707 for(const auto &index : index_set)
708 {
709 const typet &element_type = expr.type().element_type();
710 index_exprt index_expr(expr, index, element_type);
711
713 index_expr.type() == expr.what().type(),
714 "array_of operand type should match array element type");
715
716 // add constraint
719 add_array_constraint(lazy, false); // added immediately
721 }
722}
723
725 const index_sett &index_set,
726 const array_exprt &expr)
727{
728 // we got x = { v, ... } - add constraint x[i] = v
729 const exprt::operandst &operands = expr.operands();
730
731 for(const auto &index : index_set)
732 {
733 const typet &element_type = expr.type().element_type();
734 const index_exprt index_expr{expr, index, element_type};
735
736 if(index.is_constant())
737 {
738 // We have a constant index - just pick the element at that index from the
739 // array constant.
740
741 const std::optional<std::size_t> i =
743 // if the access is out of bounds, we leave it unconstrained
744 if(!i.has_value() || *i >= operands.size())
745 continue;
746
747 const exprt v = operands[*i];
749 index_expr.type() == v.type(),
750 "array operand type should match array element type");
751
752 // add constraint
755 add_array_constraint(lazy, false); // added immediately
757 }
758 else
759 {
760 // We have a non-constant index into an array constant. We need to build a
761 // case statement testing the index against all possible values. Whenever
762 // neighbouring array elements are the same, we can test the index against
763 // the range rather than individual elements. This should be particularly
764 // helpful when we have arrays of zeros, as is the case for initializers.
765
766 std::vector<std::pair<std::size_t, std::size_t>> ranges;
767
768 for(std::size_t i = 0; i < operands.size(); ++i)
769 {
770 if(ranges.empty() || operands[i] != operands[ranges.back().first])
771 ranges.emplace_back(i, i);
772 else
773 ranges.back().second = i;
774 }
775
776 for(const auto &range : ranges)
777 {
779
780 if(range.first == range.second)
781 {
783 equal_exprt{index, from_integer(range.first, index.type())};
784 }
785 else
786 {
789 from_integer(range.first, index.type()), ID_le, index},
791 index, ID_le, from_integer(range.second, index.type())}};
792 }
793
797 equal_exprt{index_expr, operands[range.first]}}};
798 add_array_constraint(lazy, true); // added lazily
800 }
801 }
802 }
803}
804
806 const index_sett &index_set,
807 const array_comprehension_exprt &expr)
808{
809 // we got x=lambda(i: e)
810 // get all other array index applications
811 // and add constraints x[j]=e[i/j]
812
813 for(const auto &index : index_set)
814 {
815 index_exprt index_expr{expr, index};
817 replace_expr(expr.arg(), index, comprehension_body);
818
819 // add constraint
823
824 add_array_constraint(lazy, false); // added immediately
826 }
827}
828
830 const index_sett &index_set,
831 const if_exprt &expr)
832{
833 // we got x=(c?a:b)
835
836 // get other array index applications
837 // and add c => x[i]=a[i]
838 // !c => x[i]=b[i]
839
840 // first do true case
841
842 for(const auto &index : index_set)
843 {
844 const typet &element_type = to_array_type(expr.type()).element_type();
845 index_exprt index_expr1(expr, index, element_type);
846 index_exprt index_expr2(expr.true_case(), index, element_type);
847
848 // add implication
852 add_array_constraint(lazy, false); // added immediately
854
855#if 0 // old code for adding, not significantly faster
857#endif
858 }
859
860 // now the false case
861 for(const auto &index : index_set)
862 {
863 const typet &element_type = to_array_type(expr.type()).element_type();
864 index_exprt index_expr1(expr, index, element_type);
865 index_exprt index_expr2(expr.false_case(), index, element_type);
866
867 // add implication
872 add_array_constraint(lazy, false); // added immediately
874
875#if 0 // old code for adding, not significantly faster
877#endif
878 }
879}
880
882{
883 switch(type)
884 {
886 return "arrayAckermann";
888 return "arrayWith";
890 return "arrayIf";
892 return "arrayOf";
894 return "arrayTypecast";
896 return "arrayConstant";
898 return "arrayComprehension";
900 return "arrayEquality";
902 return "arrayLet";
903 default:
905 }
906}
907
909{
912 json_result["arrayConstraints"].make_object();
913
914 size_t num_constraints = 0;
915
916 array_constraint_countt::iterator it = array_constraint_count.begin();
917 while(it != array_constraint_count.end())
918 {
919 std::string contraint_type_string = enum_to_string(it->first);
921 json_numbert(std::to_string(it->second));
922
923 num_constraints += it->second;
924 it++;
925 }
926
927 json_result["numOfConstraints"] =
928 json_numbert(std::to_string(num_constraints));
929 log.status() << ",\n" << json_result;
930}
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:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3544
const symbol_exprt & arg() const
Definition std_expr.h:3568
const exprt & body() const
Definition std_expr.h:3582
Array constructor from list of elements.
Definition std_expr.h:1621
const array_typet & type() const
Definition std_expr.h:1628
Array constructor from single element.
Definition std_expr.h:1558
const array_typet & type() const
Definition std_expr.h:1565
exprt & what()
Definition std_expr.h:1575
Arrays with given size.
Definition std_types.h:807
std::list< lazy_constraintt > lazy_array_constraints
Definition arrays.h:115
std::unordered_set< irep_idt > array_comprehension_args
Definition arrays.h:165
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:438
std::set< std::size_t > update_indices
Definition arrays.h:161
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
Definition arrays.cpp:699
void add_array_Ackermann_constraints()
Definition arrays.cpp:327
bool lazy_arrays
Definition arrays.h:112
void collect_indices()
Definition arrays.cpp:83
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition arrays.cpp:642
void collect_arrays(const exprt &a)
Definition arrays.cpp:131
union_find< exprt, irep_hash > arrays
Definition arrays.h:78
literalt record_array_equality(const equal_exprt &expr)
Definition arrays.cpp:55
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
Definition arrays.cpp:724
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition arrays.cpp:29
constraint_typet
Definition arrays.h:120
std::map< exprt, bool > expr_map
Definition arrays.h:117
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition arrays.cpp:829
std::string enum_to_string(constraint_typet)
Definition arrays.cpp:881
bool get_array_constraints
Definition arrays.h:114
void add_array_constraints()
Definition arrays.cpp:277
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
Definition arrays.cpp:805
virtual bool is_unbounded_array(const typet &type) const =0
void record_array_index(const index_exprt &expr)
Definition arrays.cpp:45
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:252
array_constraint_countt array_constraint_count
Definition arrays.h:133
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition arrays.cpp:570
bool incremental_cache
Definition arrays.h:113
void display_array_constraint_count()
Definition arrays.cpp:908
void update_index_map(bool update_all)
Definition arrays.cpp:404
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:731
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
Equality.
Definition std_expr.h:1366
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:212
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:2502
exprt & cond()
Definition std_expr.h:2519
exprt & false_case()
Definition std_expr.h:2539
exprt & true_case()
Definition std_expr.h:2529
Boolean implication.
Definition std_expr.h:2230
Array index operator.
Definition std_expr.h:1470
exprt & index()
Definition std_expr.h:1510
exprt & array()
Definition std_expr.h:1500
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
mstreamt & status() const
Definition message.h:406
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:2275
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
Replace a symbol expression by a given expression.
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
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:2783
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
exprt & new_value()
Definition std_expr.h:2633
exprt & where()
Definition std_expr.h:2623
exprt & old()
Definition std_expr.h:2613
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
double log(double x)
Definition math.c:2449
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
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:71
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:1603
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3611
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1665
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2582
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3173
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2661
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2866
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888