cprover
arrays.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "arrays.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/format_expr.h>
13 #include <util/namespace.h>
14 #include <util/replace_expr.h>
15 #include <util/std_expr.h>
16 #include <util/std_types.h>
17 
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,
29  message_handlert &message_handler)
30  : equalityt(_prop, message_handler), ns(_ns)
31 {
32  lazy_arrays = false; // will be set to true when --refine is used
33  incremental_cache = false; // for incremental solving
34 }
35 
37 {
38  // we are not allowed to put the index directly in the
39  // entry for the root of the equivalence class
40  // because this map is accessed during building the error trace
41  std::size_t number=arrays.number(index.array());
42  if(index_map[number].insert(index.index()).second)
43  update_indices.insert(number);
44 }
45 
47  const equal_exprt &equality)
48 {
49  const exprt &op0=equality.op0();
50  const exprt &op1=equality.op1();
51 
53  op0.type() == op1.type(),
54  "record_array_equality got equality without matching types",
55  irep_pretty_diagnosticst{equality});
56 
58  op0.type().id() == ID_array,
59  "record_array_equality parameter should be array-typed");
60 
61  array_equalities.push_back(array_equalityt());
62 
63  array_equalities.back().f1=op0;
64  array_equalities.back().f2=op1;
65  array_equalities.back().l=SUB::equality(op0, op1);
66 
67  arrays.make_union(op0, op1);
68  collect_arrays(op0);
69  collect_arrays(op1);
70 
71  return array_equalities.back().l;
72 }
73 
75 {
76  for(std::size_t i=0; i<arrays.size(); i++)
77  {
79  }
80 }
81 
83 {
84  if(expr.id()!=ID_index)
85  {
86  if(expr.id() == ID_array_comprehension)
88  to_array_comprehension_expr(expr).arg().get_identifier());
89 
90  forall_operands(op, expr) collect_indices(*op);
91  }
92  else
93  {
94  const index_exprt &e = to_index_expr(expr);
95 
96  if(
97  e.index().id() == ID_symbol &&
99  to_symbol_expr(e.index()).get_identifier()) != 0)
100  {
101  return;
102  }
103 
104  collect_indices(e.index()); // necessary?
105 
106  const typet &array_op_type = e.array().type();
107 
108  if(array_op_type.id()==ID_array)
109  {
110  const array_typet &array_type=
111  to_array_type(array_op_type);
112 
113  if(is_unbounded_array(array_type))
114  {
116  }
117  }
118  }
119 }
120 
122 {
123  const array_typet &array_type = to_array_type(a.type());
124 
125  if(a.id()==ID_with)
126  {
127  const with_exprt &with_expr=to_with_expr(a);
128 
130  array_type == with_expr.old().type(),
131  "collect_arrays got 'with' without matching types",
133 
134  arrays.make_union(a, with_expr.old());
135  collect_arrays(with_expr.old());
136 
137  // make sure this shows as an application
138  for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
139  {
140  index_exprt index_expr(with_expr.old(), with_expr.operands()[i]);
141  record_array_index(index_expr);
142  }
143  }
144  else if(a.id()==ID_update)
145  {
146  const update_exprt &update_expr=to_update_expr(a);
147 
149  array_type == update_expr.old().type(),
150  "collect_arrays got 'update' without matching types",
152 
153  arrays.make_union(a, update_expr.old());
154  collect_arrays(update_expr.old());
155 
156 #if 0
157  // make sure this shows as an application
158  index_exprt index_expr(update_expr.old(), update_expr.index());
159  record_array_index(index_expr);
160 #endif
161  }
162  else if(a.id()==ID_if)
163  {
164  const if_exprt &if_expr=to_if_expr(a);
165 
167  array_type == if_expr.true_case().type(),
168  "collect_arrays got if without matching types",
170 
172  array_type == if_expr.false_case().type(),
173  "collect_arrays got if without matching types",
175 
176  arrays.make_union(a, if_expr.true_case());
177  arrays.make_union(a, if_expr.false_case());
178  collect_arrays(if_expr.true_case());
179  collect_arrays(if_expr.false_case());
180  }
181  else if(a.id()==ID_symbol)
182  {
183  }
184  else if(a.id()==ID_nondet_symbol)
185  {
186  }
187  else if(a.id()==ID_member)
188  {
189  const auto &struct_op = to_member_expr(a).struct_op();
190 
192  struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
193  "unexpected array expression: member with '" + struct_op.id_string() +
194  "'");
195  }
196  else if(a.id()==ID_constant ||
197  a.id()==ID_array ||
198  a.id()==ID_string_constant)
199  {
200  }
201  else if(a.id()==ID_array_of)
202  {
203  }
204  else if(a.id()==ID_byte_update_little_endian ||
205  a.id()==ID_byte_update_big_endian)
206  {
208  false,
209  "byte_update should be removed before collect_arrays");
210  }
211  else if(a.id()==ID_typecast)
212  {
213  const auto &typecast_op = to_typecast_expr(a).op();
214 
215  // cast between array types?
217  typecast_op.type().id() == ID_array,
218  "unexpected array type cast from " + typecast_op.type().id_string());
219 
220  arrays.make_union(a, typecast_op);
221  collect_arrays(typecast_op);
222  }
223  else if(a.id()==ID_index)
224  {
225  // nested unbounded arrays
226  const auto &array_op = to_index_expr(a).array();
227  arrays.make_union(a, array_op);
228  collect_arrays(array_op);
229  }
230  else if(a.id() == ID_array_comprehension)
231  {
232  }
233  else
234  {
236  false,
237  "unexpected array expression (collect_arrays): '" + a.id_string() + "'");
238  }
239 }
240 
243 {
244  if(lazy_arrays && refine)
245  {
246  // lazily add the constraint
248  {
249  if(expr_map.find(lazy.lazy) == expr_map.end())
250  {
251  lazy_array_constraints.push_back(lazy);
252  expr_map[lazy.lazy] = true;
253  }
254  }
255  else
256  {
257  lazy_array_constraints.push_back(lazy);
258  }
259  }
260  else
261  {
262  // add the constraint eagerly
264  }
265 }
266 
268 {
269  collect_indices();
270  // at this point all indices should in the index set
271 
272  // reduce initial index map
273  update_index_map(true);
274 
275  // add constraints for if, with, array_of, lambda
276  std::set<std::size_t> roots_to_process, updated_roots;
277  for(std::size_t i=0; i<arrays.size(); i++)
278  roots_to_process.insert(arrays.find_number(i));
279 
280  while(!roots_to_process.empty())
281  {
282  for(std::size_t i = 0; i < arrays.size(); i++)
283  {
284  if(roots_to_process.count(arrays.find_number(i)) == 0)
285  continue;
286 
287  // take a copy as arrays may get modified by add_array_constraints
288  // in case of nested unbounded arrays
289  exprt a = arrays[i];
290 
292 
293  // we have to update before it gets used in the next add_* call
294  for(const std::size_t u : update_indices)
295  updated_roots.insert(arrays.find_number(u));
296  update_index_map(false);
297  }
298 
299  roots_to_process = std::move(updated_roots);
300  updated_roots.clear();
301  }
302 
303  // add constraints for equalities
304  for(const auto &equality : array_equalities)
305  {
308  equality);
309 
310  // update_index_map should not be necessary here
311  }
312 
313  // add the Ackermann constraints
315 }
316 
318 {
319  // this is quadratic!
320 
321 #ifdef DEBUG
322  std::cout << "arrays.size(): " << arrays.size() << '\n';
323 #endif
324 
325  // iterate over arrays
326  for(std::size_t i=0; i<arrays.size(); i++)
327  {
328  const index_sett &index_set=index_map[arrays.find_number(i)];
329 
330 #ifdef DEBUG
331  std::cout << "index_set.size(): " << index_set.size() << '\n';
332 #endif
333 
334  // iterate over indices, 2x!
335  for(index_sett::const_iterator
336  i1=index_set.begin();
337  i1!=index_set.end();
338  i1++)
339  for(index_sett::const_iterator
340  i2=i1;
341  i2!=index_set.end();
342  i2++)
343  if(i1!=i2)
344  {
345  if(i1->is_constant() && i2->is_constant())
346  continue;
347 
348  // index equality
349  const equal_exprt indices_equal(
350  *i1, typecast_exprt::conditional_cast(*i2, i1->type()));
351 
352  literalt indices_equal_lit=convert(indices_equal);
353 
354  if(indices_equal_lit!=const_literal(false))
355  {
356  const typet &subtype = arrays[i].type().subtype();
357  index_exprt index_expr1(arrays[i], *i1, subtype);
358 
359  index_exprt index_expr2=index_expr1;
360  index_expr2.index()=*i2;
361 
362  equal_exprt values_equal(index_expr1, index_expr2);
363 
364  // add constraint
366  implies_exprt(literal_exprt(indices_equal_lit), values_equal));
367  add_array_constraint(lazy, true); // added lazily
368 
369 #if 0 // old code for adding, not significantly faster
370  prop.lcnf(!indices_equal_lit, convert(values_equal));
371 #endif
372  }
373  }
374  }
375 }
376 
378 void arrayst::update_index_map(std::size_t i)
379 {
380  if(arrays.is_root_number(i))
381  return;
382 
383  std::size_t root_number=arrays.find_number(i);
384  INVARIANT(root_number!=i, "is_root_number incorrect?");
385 
386  index_sett &root_index_set=index_map[root_number];
387  index_sett &index_set=index_map[i];
388 
389  root_index_set.insert(index_set.begin(), index_set.end());
390 }
391 
392 void arrayst::update_index_map(bool update_all)
393 {
394  // iterate over non-roots
395  // possible reasons why update is needed:
396  // -- there are new equivalence classes in arrays
397  // -- there are new indices for arrays that are not the root
398  // of an equivalence class
399  // (and we cannot do that in record_array_index())
400  // -- equivalence classes have been merged
401  if(update_all)
402  {
403  for(std::size_t i=0; i<arrays.size(); i++)
404  update_index_map(i);
405  }
406  else
407  {
408  for(const auto &index : update_indices)
409  update_index_map(index);
410 
411  update_indices.clear();
412  }
413 
414 #ifdef DEBUG
415  // print index sets
416  for(const auto &index_entry : index_map)
417  for(const auto &index : index_entry.second)
418  std::cout << "Index set (" << index_entry.first << " = "
419  << arrays.find_number(index_entry.first) << " = "
420  << format(arrays[arrays.find_number(index_entry.first)])
421  << "): " << format(index) << '\n';
422  std::cout << "-----\n";
423 #endif
424 }
425 
427  const index_sett &index_set,
428  const array_equalityt &array_equality)
429 {
430  // add constraints x=y => x[i]=y[i]
431 
432  for(const auto &index : index_set)
433  {
434  const typet &subtype1 = array_equality.f1.type().subtype();
435  index_exprt index_expr1(array_equality.f1, index, subtype1);
436 
437  const typet &subtype2 = array_equality.f2.type().subtype();
438  index_exprt index_expr2(array_equality.f2, index, subtype2);
439 
441  index_expr1.type()==index_expr2.type(),
442  "array elements should all have same type");
443 
444  array_equalityt equal;
445  equal.f1 = index_expr1;
446  equal.f2 = index_expr2;
447  equal.l = array_equality.l;
448  equal_exprt equality_expr(index_expr1, index_expr2);
449 
450  // add constraint
451  // equality constraints are not added lazily
452  // convert must be done to guarantee correct update of the index_set
453  prop.lcnf(!array_equality.l, convert(equality_expr));
454  }
455 }
456 
458  const index_sett &index_set,
459  const exprt &expr)
460 {
461  if(expr.id()==ID_with)
462  return add_array_constraints_with(index_set, to_with_expr(expr));
463  else if(expr.id()==ID_update)
464  return add_array_constraints_update(index_set, to_update_expr(expr));
465  else if(expr.id()==ID_if)
466  return add_array_constraints_if(index_set, to_if_expr(expr));
467  else if(expr.id()==ID_array_of)
468  return add_array_constraints_array_of(index_set, to_array_of_expr(expr));
469  else if(expr.id() == ID_array)
470  return add_array_constraints_array_constant(index_set, to_array_expr(expr));
471  else if(expr.id() == ID_array_comprehension)
472  {
474  index_set, to_array_comprehension_expr(expr));
475  }
476  else if(expr.id()==ID_symbol ||
477  expr.id()==ID_nondet_symbol ||
478  expr.id()==ID_constant ||
479  expr.id()=="zero_string" ||
480  expr.id()==ID_string_constant)
481  {
482  }
483  else if(
484  expr.id() == ID_member &&
485  (to_member_expr(expr).struct_op().id() == ID_symbol ||
486  to_member_expr(expr).struct_op().id() == ID_nondet_symbol))
487  {
488  }
489  else if(expr.id()==ID_byte_update_little_endian ||
490  expr.id()==ID_byte_update_big_endian)
491  {
492  INVARIANT(false, "byte_update should be removed before arrayst");
493  }
494  else if(expr.id()==ID_typecast)
495  {
496  // we got a=(type[])b
497  const auto &expr_typecast_op = to_typecast_expr(expr).op();
498 
499  // add a[i]=b[i]
500  for(const auto &index : index_set)
501  {
502  const typet &subtype = expr.type().subtype();
503  index_exprt index_expr1(expr, index, subtype);
504  index_exprt index_expr2(expr_typecast_op, index, subtype);
505 
507  index_expr1.type()==index_expr2.type(),
508  "array elements should all have same type");
509 
510  // add constraint
512  equal_exprt(index_expr1, index_expr2));
513  add_array_constraint(lazy, false); // added immediately
514  }
515  }
516  else if(expr.id()==ID_index)
517  {
518  }
519  else
520  {
522  false,
523  "unexpected array expression (add_array_constraints): '" +
524  expr.id_string() + "'");
525  }
526 }
527 
529  const index_sett &index_set,
530  const with_exprt &expr)
531 {
532  // We got x=(y with [i:=v, j:=w, ...]).
533  // First add constraints x[i]=v, x[j]=w, ...
534  std::unordered_set<exprt, irep_hash> updated_indices;
535 
536  const exprt::operandst &operands = expr.operands();
537  for(std::size_t i = 1; i + 1 < operands.size(); i += 2)
538  {
539  const exprt &index = operands[i];
540  const exprt &value = operands[i + 1];
541 
542  index_exprt index_expr(expr, index, expr.type().subtype());
543 
545  index_expr.type() == value.type(),
546  "with-expression operand should match array element type",
548 
550  lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
551  add_array_constraint(lazy, false); // added immediately
552 
553  updated_indices.insert(index);
554  }
555 
556  // For all other indices use the existing value, i.e., add constraints
557  // x[I]=y[I] for I!=i,j,...
558 
559  for(auto other_index : index_set)
560  {
561  if(updated_indices.find(other_index) == updated_indices.end())
562  {
563  // we first build the guard
564  exprt::operandst disjuncts;
565  disjuncts.reserve(updated_indices.size());
566  for(const auto &index : updated_indices)
567  {
568  disjuncts.push_back(equal_exprt{
569  index, typecast_exprt::conditional_cast(other_index, index.type())});
570  }
571 
572  literalt guard_lit = convert(disjunction(disjuncts));
573 
574  if(guard_lit!=const_literal(true))
575  {
576  const typet &subtype = expr.type().subtype();
577  index_exprt index_expr1(expr, other_index, subtype);
578  index_exprt index_expr2(expr.old(), other_index, subtype);
579 
580  equal_exprt equality_expr(index_expr1, index_expr2);
581 
582  // add constraint
584  literal_exprt(guard_lit)));
585  add_array_constraint(lazy, false); // added immediately
586 
587 #if 0 // old code for adding, not significantly faster
588  {
589  literalt equality_lit=convert(equality_expr);
590 
591  bvt bv;
592  bv.reserve(2);
593  bv.push_back(equality_lit);
594  bv.push_back(guard_lit);
595  prop.lcnf(bv);
596  }
597 #endif
598  }
599  }
600  }
601 }
602 
604  const index_sett &,
605  const update_exprt &)
606 {
607  // we got x=UPDATE(y, [i], v)
608  // add constaint x[i]=v
609 
610 #if 0
611  const exprt &index=expr.where();
612  const exprt &value=expr.new_value();
613 
614  {
615  index_exprt index_expr(expr, index, expr.type().subtype());
616 
618  index_expr.type()==value.type(),
619  "update operand should match array element type",
621 
622  set_to_true(equal_exprt(index_expr, value));
623  }
624 
625  // use other array index applications for "else" case
626  // add constraint x[I]=y[I] for I!=i
627 
628  for(auto other_index : index_set)
629  {
630  if(other_index!=index)
631  {
632  // we first build the guard
633 
634  other_index = typecast_exprt::conditional_cast(other_index, index.type());
635 
636  literalt guard_lit=convert(equal_exprt(index, other_index));
637 
638  if(guard_lit!=const_literal(true))
639  {
640  const typet &subtype=expr.type().subtype();
641  index_exprt index_expr1(expr, other_index, subtype);
642  index_exprt index_expr2(expr.op0(), other_index, subtype);
643 
644  equal_exprt equality_expr(index_expr1, index_expr2);
645 
646  literalt equality_lit=convert(equality_expr);
647 
648  // add constraint
649  bvt bv;
650  bv.reserve(2);
651  bv.push_back(equality_lit);
652  bv.push_back(guard_lit);
653  prop.lcnf(bv);
654  }
655  }
656  }
657 #endif
658 }
659 
661  const index_sett &index_set,
662  const array_of_exprt &expr)
663 {
664  // we got x=array_of[v]
665  // get other array index applications
666  // and add constraint x[i]=v
667 
668  for(const auto &index : index_set)
669  {
670  const typet &subtype = expr.type().subtype();
671  index_exprt index_expr(expr, index, subtype);
672 
674  index_expr.type() == expr.what().type(),
675  "array_of operand type should match array element type");
676 
677  // add constraint
679  lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.what()));
680  add_array_constraint(lazy, false); // added immediately
681  }
682 }
683 
685  const index_sett &index_set,
686  const array_exprt &expr)
687 {
688  // we got x = { v, ... } - add constraint x[i] = v
689  const exprt::operandst &operands = expr.operands();
690 
691  for(const auto &index : index_set)
692  {
693  const typet &subtype = expr.type().subtype();
694  const index_exprt index_expr{expr, index, subtype};
695 
696  if(index.is_constant())
697  {
698  // We have a constant index - just pick the element at that index from the
699  // array constant.
700 
701  const std::size_t i =
702  numeric_cast_v<std::size_t>(to_constant_expr(index));
703  // if the access is out of bounds, we leave it unconstrained
704  if(i >= operands.size())
705  continue;
706 
707  const exprt v = operands[i];
709  index_expr.type() == v.type(),
710  "array operand type should match array element type");
711 
712  // add constraint
714  equal_exprt{index_expr, v}};
715  add_array_constraint(lazy, false); // added immediately
716  }
717  else
718  {
719  // We have a non-constant index into an array constant. We need to build a
720  // case statement testing the index against all possible values. Whenever
721  // neighbouring array elements are the same, we can test the index against
722  // the range rather than individual elements. This should be particularly
723  // helpful when we have arrays of zeros, as is the case for initializers.
724 
725  std::vector<std::pair<std::size_t, std::size_t>> ranges;
726 
727  for(std::size_t i = 0; i < operands.size(); ++i)
728  {
729  if(ranges.empty() || operands[i] != operands[ranges.back().first])
730  ranges.emplace_back(i, i);
731  else
732  ranges.back().second = i;
733  }
734 
735  for(const auto &range : ranges)
736  {
737  exprt index_constraint;
738 
739  if(range.first == range.second)
740  {
741  index_constraint =
742  equal_exprt{index, from_integer(range.first, index.type())};
743  }
744  else
745  {
746  index_constraint = and_exprt{
748  from_integer(range.first, index.type()), ID_le, index},
750  index, ID_le, from_integer(range.second, index.type())}};
751  }
752 
755  implies_exprt{index_constraint,
756  equal_exprt{index_expr, operands[range.first]}}};
757  add_array_constraint(lazy, true); // added lazily
758  }
759  }
760  }
761 }
762 
764  const index_sett &index_set,
765  const array_comprehension_exprt &expr)
766 {
767  // we got x=lambda(i: e)
768  // get all other array index applications
769  // and add constraints x[j]=e[i/j]
770 
771  for(const auto &index : index_set)
772  {
773  index_exprt index_expr{expr, index};
774  exprt comprehension_body = expr.body();
775  replace_expr(expr.arg(), index, comprehension_body);
776 
777  // add constraint
780  equal_exprt(index_expr, comprehension_body));
781  add_array_constraint(lazy, false); // added immediately
782  }
783 }
784 
786  const index_sett &index_set,
787  const if_exprt &expr)
788 {
789  // we got x=(c?a:b)
790  literalt cond_lit=convert(expr.cond());
791 
792  // get other array index applications
793  // and add c => x[i]=a[i]
794  // !c => x[i]=b[i]
795 
796  // first do true case
797 
798  for(const auto &index : index_set)
799  {
800  const typet subtype = expr.type().subtype();
801  index_exprt index_expr1(expr, index, subtype);
802  index_exprt index_expr2(expr.true_case(), index, subtype);
803 
804  // add implication
806  or_exprt(literal_exprt(!cond_lit),
807  equal_exprt(index_expr1, index_expr2)));
808  add_array_constraint(lazy, false); // added immediately
809 
810 #if 0 // old code for adding, not significantly faster
811  prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
812 #endif
813  }
814 
815  // now the false case
816  for(const auto &index : index_set)
817  {
818  const typet subtype = expr.type().subtype();
819  index_exprt index_expr1(expr, index, subtype);
820  index_exprt index_expr2(expr.false_case(), index, subtype);
821 
822  // add implication
825  or_exprt(literal_exprt(cond_lit),
826  equal_exprt(index_expr1, index_expr2)));
827  add_array_constraint(lazy, false); // added immediately
828 
829 #if 0 // old code for adding, not significantly faster
830  prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
831 #endif
832  }
833 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
to_array_comprehension_expr
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:4485
format
static format_containert< T > format(const T &o)
Definition: format.h:35
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3299
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
arrayst::array_equalityt::f1
exprt f1
Definition: arrays.h:61
typet::subtype
const typet & subtype() const
Definition: type.h:47
arrayst::array_comprehension_args
std::unordered_set< irep_idt > array_comprehension_args
Definition: arrays.h:138
arrayst::record_array_equality
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:46
arith_tools.h
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1462
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1384
arrayst::lazy_constraintt
Definition: arrays.h:93
typet
The type of an expression, extends irept.
Definition: type.h:29
update_exprt::old
exprt & old()
Definition: std_expr.h:3246
bvt
std::vector< literalt > bvt
Definition: literal.h:201
arrayst::index_map
index_mapt index_map
Definition: arrays.h:78
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
union_find::size
size_t size() const
Definition: union_find.h:269
union_find::find_number
size_type find_number(typename numbering< T >::const_iterator it) const
Definition: union_find.h:202
union_find::is_root_number
bool is_root_number(size_type a) const
Definition: union_find.h:217
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
arrayst::collect_arrays
void collect_arrays(const exprt &a)
Definition: arrays.cpp:121
and_exprt
Boolean AND.
Definition: std_expr.h:2137
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1412
exprt
Base class for all expressions.
Definition: expr.h:53
decision_proceduret::set_to_true
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
Definition: decision_procedure.cpp:23
array_of_exprt::type
const array_typet & type() const
Definition: std_expr.h:1374
array_comprehension_exprt::arg
const symbol_exprt & arg() const
Definition: std_expr.h:4446
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:52
arrayst::collect_indices
void collect_indices()
Definition: arrays.cpp:74
arrayst::array_equalityt::l
literalt l
Definition: arrays.h:60
arrayst::update_indices
std::set< std::size_t > update_indices
Definition: arrays.h:134
namespace.h
equal_exprt
Equality.
Definition: std_expr.h:1190
arrayst::lazy_typet::ARRAY_IF
@ ARRAY_IF
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
union_find::number
size_type number(const T &a)
Definition: union_find.h:236
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
array_exprt::type
const array_typet & type() const
Definition: std_expr.h:1439
with_exprt::old
exprt & old()
Definition: std_expr.h:3060
arrayst::add_array_constraints_with
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition: arrays.cpp:528
disjunction
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:29
arrayst::incremental_cache
bool incremental_cache
Definition: arrays.h:105
arrayst::lazy_typet::ARRAY_OF
@ ARRAY_OF
DATA_INVARIANT_WITH_DIAGNOSTICS
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:512
or_exprt
Boolean OR.
Definition: std_expr.h:2245
arrayst::add_array_constraints
void add_array_constraints()
Definition: arrays.cpp:267
arrayst::lazy_array_constraints
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:106
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
lazy
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
literal_exprt
Definition: literal_expr.h:18
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1367
std_types.h
Pre-defined types.
arrayst::array_equalities
array_equalitiest array_equalities
Definition: arrays.h:68
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
array_comprehension_exprt::body
const exprt & body() const
Definition: std_expr.h:4456
prop.h
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
arrayst::is_unbounded_array
virtual bool is_unbounded_array(const typet &type) const =0
arrayst::index_sett
std::set< exprt > index_sett
Definition: arrays.h:74
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
arrayst::lazy_typet::ARRAY_WITH
@ ARRAY_WITH
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
arrayst::expr_map
std::map< exprt, bool > expr_map
Definition: arrays.h:108
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
arrayst::record_array_index
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:36
equalityt
Definition: equality.h:20
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
arrayst::add_array_Ackermann_constraints
void add_array_Ackermann_constraints()
Definition: arrays.cpp:317
arrayst::array_equalityt::f2
exprt f2
Definition: arrays.h:61
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
arrayst::lazy_typet::ARRAY_TYPECAST
@ ARRAY_TYPECAST
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3112
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3234
irep_pretty_diagnosticst
Definition: irep.h:524
arrayst::add_array_constraints_update
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition: arrays.cpp:603
union_find::make_union
bool make_union(const T &a, const T &b)
Definition: union_find.h:154
format_expr.h
arrays.h
Theory of Arrays with Extensionality.
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
arrayst::array_equalityt
Definition: arrays.h:59
array_typet
Arrays with given size.
Definition: std_types.h:965
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
arrayst::add_array_constraints_comprehension
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
Definition: arrays.cpp:763
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
arrayst::lazy_typet::ARRAY_CONSTANT
@ ARRAY_CONSTANT
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
literalt
Definition: literal.h:26
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
arrayst::add_array_constraints_array_constant
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
Definition: arrays.cpp:684
arrayst::add_array_constraints_array_of
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
Definition: arrays.cpp:660
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
arrayst::update_index_map
void update_index_map(bool update_all)
Definition: arrays.cpp:392
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
replace_expr.h
exprt::operands
operandst & operands()
Definition: expr.h:95
arrayst::lazy_typet::ARRAY_ACKERMANN
@ ARRAY_ACKERMANN
arrayst::arrays
union_find< exprt > arrays
Definition: arrays.h:71
index_exprt
Array index operator.
Definition: std_expr.h:1293
arrayst::lazy_arrays
bool lazy_arrays
Definition: arrays.h:104
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:4422
arrayst::add_array_constraint
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
Definition: arrays.cpp:242
arrayst::lazy_typet::ARRAY_COMPREHENSION
@ ARRAY_COMPREHENSION
std_expr.h
API to expression classes.
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
arrayst::add_array_constraints_equality
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition: arrays.cpp:426
arrayst::arrayst
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler)
Definition: arrays.cpp:26
propt::lcnf
void lcnf(literalt l0, literalt l1)
Definition: prop.h:58
equalityt::equality
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
arrayst::add_array_constraints_if
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition: arrays.cpp:785