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/json_irep.h>
14 #include <util/message.h>
15 #include <util/namespace.h>
16 #include <util/replace_expr.h>
17 #include <util/std_expr.h>
18 #include <util/std_types.h>
19 #include <util/ui_message.h>
20 
21 #include <solvers/prop/prop.h>
22 
23 #ifdef DEBUG
24 #include <iostream>
25 #endif
26 
27 #include <unordered_set>
28 
30  const namespacet &_ns,
31  propt &_prop,
32  message_handlert &_message_handler,
33  bool _get_array_constraints)
34  : equalityt(_prop, _message_handler),
35  ns(_ns),
36  log(_message_handler),
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
42  get_array_constraints = _get_array_constraints;
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 
70  array_equalities.push_back(array_equalityt());
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  forall_operands(op, expr) collect_indices(*op);
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=
120  to_array_type(array_op_type);
121 
122  if(is_unbounded_array(array_type))
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  {
136  const with_exprt &with_expr=to_with_expr(a);
137 
139  array_type == with_expr.old().type(),
140  "collect_arrays got 'with' without matching types",
142 
143  arrays.make_union(a, with_expr.old());
144  collect_arrays(with_expr.old());
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]);
150  record_array_index(index_expr);
151  }
152  }
153  else if(a.id()==ID_update)
154  {
155  const update_exprt &update_expr=to_update_expr(a);
156 
158  array_type == update_expr.old().type(),
159  "collect_arrays got 'update' without matching types",
161 
162  arrays.make_union(a, update_expr.old());
163  collect_arrays(update_expr.old());
164 
165 #if 0
166  // make sure this shows as an application
167  index_exprt index_expr(update_expr.old(), update_expr.index());
168  record_array_index(index_expr);
169 #endif
170  }
171  else if(a.id()==ID_if)
172  {
173  const if_exprt &if_expr=to_if_expr(a);
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.id()==ID_constant ||
206  a.id()==ID_array ||
207  a.id()==ID_string_constant)
208  {
209  }
210  else if(a.id()==ID_array_of)
211  {
212  }
213  else if(a.id()==ID_byte_update_little_endian ||
214  a.id()==ID_byte_update_big_endian)
215  {
217  false,
218  "byte_update should be removed before collect_arrays");
219  }
220  else if(a.id()==ID_typecast)
221  {
222  const auto &typecast_op = to_typecast_expr(a).op();
223 
224  // cast between array types?
226  typecast_op.type().id() == ID_array,
227  "unexpected array type cast from " + typecast_op.type().id_string());
228 
229  arrays.make_union(a, typecast_op);
230  collect_arrays(typecast_op);
231  }
232  else if(a.id()==ID_index)
233  {
234  // nested unbounded arrays
235  const auto &array_op = to_index_expr(a).array();
236  arrays.make_union(a, array_op);
237  collect_arrays(array_op);
238  }
239  else if(a.id() == ID_array_comprehension)
240  {
241  }
242  else
243  {
245  false,
246  "unexpected array expression (collect_arrays): '" + a.id_string() + "'");
247  }
248 }
249 
252 {
253  if(lazy_arrays && refine)
254  {
255  // lazily add the constraint
257  {
258  if(expr_map.find(lazy.lazy) == expr_map.end())
259  {
260  lazy_array_constraints.push_back(lazy);
261  expr_map[lazy.lazy] = true;
262  }
263  }
264  else
265  {
266  lazy_array_constraints.push_back(lazy);
267  }
268  }
269  else
270  {
271  // add the constraint eagerly
273  }
274 }
275 
277 {
278  collect_indices();
279  // at this point all indices should in the index set
280 
281  // reduce initial index map
282  update_index_map(true);
283 
284  // add constraints for if, with, array_of, lambda
285  std::set<std::size_t> roots_to_process, updated_roots;
286  for(std::size_t i=0; i<arrays.size(); i++)
287  roots_to_process.insert(arrays.find_number(i));
288 
289  while(!roots_to_process.empty())
290  {
291  for(std::size_t i = 0; i < arrays.size(); i++)
292  {
293  if(roots_to_process.count(arrays.find_number(i)) == 0)
294  continue;
295 
296  // take a copy as arrays may get modified by add_array_constraints
297  // in case of nested unbounded arrays
298  exprt a = arrays[i];
299 
301 
302  // we have to update before it gets used in the next add_* call
303  for(const std::size_t u : update_indices)
304  updated_roots.insert(arrays.find_number(u));
305  update_index_map(false);
306  }
307 
308  roots_to_process = std::move(updated_roots);
309  updated_roots.clear();
310  }
311 
312  // add constraints for equalities
313  for(const auto &equality : array_equalities)
314  {
317  equality);
318 
319  // update_index_map should not be necessary here
320  }
321 
322  // add the Ackermann constraints
324 }
325 
327 {
328  // this is quadratic!
329 
330 #ifdef DEBUG
331  std::cout << "arrays.size(): " << arrays.size() << '\n';
332 #endif
333 
334  // iterate over arrays
335  for(std::size_t i=0; i<arrays.size(); i++)
336  {
337  const index_sett &index_set=index_map[arrays.find_number(i)];
338 
339 #ifdef DEBUG
340  std::cout << "index_set.size(): " << index_set.size() << '\n';
341 #endif
342 
343  // iterate over indices, 2x!
344  for(index_sett::const_iterator
345  i1=index_set.begin();
346  i1!=index_set.end();
347  i1++)
348  for(index_sett::const_iterator
349  i2=i1;
350  i2!=index_set.end();
351  i2++)
352  if(i1!=i2)
353  {
354  if(i1->is_constant() && i2->is_constant())
355  continue;
356 
357  // index equality
358  const equal_exprt indices_equal(
359  *i1, typecast_exprt::conditional_cast(*i2, i1->type()));
360 
361  literalt indices_equal_lit=convert(indices_equal);
362 
363  if(indices_equal_lit!=const_literal(false))
364  {
365  const typet &subtype = arrays[i].type().subtype();
366  index_exprt index_expr1(arrays[i], *i1, subtype);
367 
368  index_exprt index_expr2=index_expr1;
369  index_expr2.index()=*i2;
370 
371  equal_exprt values_equal(index_expr1, index_expr2);
372 
373  // add constraint
375  implies_exprt(literal_exprt(indices_equal_lit), values_equal));
376  add_array_constraint(lazy, true); // added lazily
378 
379 #if 0 // old code for adding, not significantly faster
380  prop.lcnf(!indices_equal_lit, convert(values_equal));
381 #endif
382  }
383  }
384  }
385 }
386 
388 void arrayst::update_index_map(std::size_t i)
389 {
390  if(arrays.is_root_number(i))
391  return;
392 
393  std::size_t root_number=arrays.find_number(i);
394  INVARIANT(root_number!=i, "is_root_number incorrect?");
395 
396  index_sett &root_index_set=index_map[root_number];
397  index_sett &index_set=index_map[i];
398 
399  root_index_set.insert(index_set.begin(), index_set.end());
400 }
401 
402 void arrayst::update_index_map(bool update_all)
403 {
404  // iterate over non-roots
405  // possible reasons why update is needed:
406  // -- there are new equivalence classes in arrays
407  // -- there are new indices for arrays that are not the root
408  // of an equivalence class
409  // (and we cannot do that in record_array_index())
410  // -- equivalence classes have been merged
411  if(update_all)
412  {
413  for(std::size_t i=0; i<arrays.size(); i++)
414  update_index_map(i);
415  }
416  else
417  {
418  for(const auto &index : update_indices)
419  update_index_map(index);
420 
421  update_indices.clear();
422  }
423 
424 #ifdef DEBUG
425  // print index sets
426  for(const auto &index_entry : index_map)
427  for(const auto &index : index_entry.second)
428  std::cout << "Index set (" << index_entry.first << " = "
429  << arrays.find_number(index_entry.first) << " = "
430  << format(arrays[arrays.find_number(index_entry.first)])
431  << "): " << format(index) << '\n';
432  std::cout << "-----\n";
433 #endif
434 }
435 
437  const index_sett &index_set,
438  const array_equalityt &array_equality)
439 {
440  // add constraints x=y => x[i]=y[i]
441 
442  for(const auto &index : index_set)
443  {
444  const typet &subtype1 = array_equality.f1.type().subtype();
445  index_exprt index_expr1(array_equality.f1, index, subtype1);
446 
447  const typet &subtype2 = array_equality.f2.type().subtype();
448  index_exprt index_expr2(array_equality.f2, index, subtype2);
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;
458  equal_exprt equality_expr(index_expr1, index_expr2);
459 
460  // add constraint
461  // equality constraints are not added lazily
462  // convert must be done to guarantee correct update of the index_set
463  prop.lcnf(!array_equality.l, convert(equality_expr));
465  }
466 }
467 
469  const index_sett &index_set,
470  const exprt &expr)
471 {
472  if(expr.id()==ID_with)
473  return add_array_constraints_with(index_set, to_with_expr(expr));
474  else if(expr.id()==ID_update)
475  return add_array_constraints_update(index_set, to_update_expr(expr));
476  else if(expr.id()==ID_if)
477  return add_array_constraints_if(index_set, to_if_expr(expr));
478  else if(expr.id()==ID_array_of)
479  return add_array_constraints_array_of(index_set, to_array_of_expr(expr));
480  else if(expr.id() == ID_array)
481  return add_array_constraints_array_constant(index_set, to_array_expr(expr));
482  else if(expr.id() == ID_array_comprehension)
483  {
485  index_set, to_array_comprehension_expr(expr));
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 ||
501  expr.id()==ID_byte_update_big_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 &subtype = expr.type().subtype();
514  index_exprt index_expr1(expr, index, subtype);
515  index_exprt index_expr2(expr_typecast_op, index, subtype);
516 
518  index_expr1.type()==index_expr2.type(),
519  "array elements should all have same type");
520 
521  // add constraint
523  equal_exprt(index_expr1, index_expr2));
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 
554  index_exprt index_expr(expr, index, expr.type().subtype());
555 
557  index_expr.type() == value.type(),
558  "with-expression operand should match array element type",
560 
562  lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
563  add_array_constraint(lazy, false); // added immediately
565 
566  updated_indices.insert(index);
567  }
568 
569  // For all other indices use the existing value, i.e., add constraints
570  // x[I]=y[I] for I!=i,j,...
571 
572  for(auto other_index : index_set)
573  {
574  if(updated_indices.find(other_index) == updated_indices.end())
575  {
576  // we first build the guard
577  exprt::operandst disjuncts;
578  disjuncts.reserve(updated_indices.size());
579  for(const auto &index : updated_indices)
580  {
581  disjuncts.push_back(equal_exprt{
582  index, typecast_exprt::conditional_cast(other_index, index.type())});
583  }
584 
585  literalt guard_lit = convert(disjunction(disjuncts));
586 
587  if(guard_lit!=const_literal(true))
588  {
589  const typet &subtype = expr.type().subtype();
590  index_exprt index_expr1(expr, other_index, subtype);
591  index_exprt index_expr2(expr.old(), other_index, subtype);
592 
593  equal_exprt equality_expr(index_expr1, index_expr2);
594 
595  // add constraint
597  literal_exprt(guard_lit)));
598 
599  add_array_constraint(lazy, false); // added immediately
601 
602 #if 0 // old code for adding, not significantly faster
603  {
604  literalt equality_lit=convert(equality_expr);
605 
606  bvt bv;
607  bv.reserve(2);
608  bv.push_back(equality_lit);
609  bv.push_back(guard_lit);
610  prop.lcnf(bv);
611  }
612 #endif
613  }
614  }
615  }
616 }
617 
619  const index_sett &,
620  const update_exprt &)
621 {
622  // we got x=UPDATE(y, [i], v)
623  // add constaint x[i]=v
624 
625 #if 0
626  const exprt &index=expr.where();
627  const exprt &value=expr.new_value();
628 
629  {
630  index_exprt index_expr(expr, index, expr.type().subtype());
631 
633  index_expr.type()==value.type(),
634  "update operand should match array element type",
636 
637  set_to_true(equal_exprt(index_expr, value));
638  }
639 
640  // use other array index applications for "else" case
641  // add constraint x[I]=y[I] for I!=i
642 
643  for(auto other_index : index_set)
644  {
645  if(other_index!=index)
646  {
647  // we first build the guard
648 
649  other_index = typecast_exprt::conditional_cast(other_index, index.type());
650 
651  literalt guard_lit=convert(equal_exprt(index, other_index));
652 
653  if(guard_lit!=const_literal(true))
654  {
655  const typet &subtype=expr.type().subtype();
656  index_exprt index_expr1(expr, other_index, subtype);
657  index_exprt index_expr2(expr.op0(), other_index, subtype);
658 
659  equal_exprt equality_expr(index_expr1, index_expr2);
660 
661  literalt equality_lit=convert(equality_expr);
662 
663  // add constraint
664  bvt bv;
665  bv.reserve(2);
666  bv.push_back(equality_lit);
667  bv.push_back(guard_lit);
668  prop.lcnf(bv);
669  }
670  }
671  }
672 #endif
673 }
674 
676  const index_sett &index_set,
677  const array_of_exprt &expr)
678 {
679  // we got x=array_of[v]
680  // get other array index applications
681  // and add constraint x[i]=v
682 
683  for(const auto &index : index_set)
684  {
685  const typet &subtype = expr.type().subtype();
686  index_exprt index_expr(expr, index, subtype);
687 
689  index_expr.type() == expr.what().type(),
690  "array_of operand type should match array element type");
691 
692  // add constraint
694  lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.what()));
695  add_array_constraint(lazy, false); // added immediately
697  }
698 }
699 
701  const index_sett &index_set,
702  const array_exprt &expr)
703 {
704  // we got x = { v, ... } - add constraint x[i] = v
705  const exprt::operandst &operands = expr.operands();
706 
707  for(const auto &index : index_set)
708  {
709  const typet &subtype = expr.type().subtype();
710  const index_exprt index_expr{expr, index, subtype};
711 
712  if(index.is_constant())
713  {
714  // We have a constant index - just pick the element at that index from the
715  // array constant.
716 
717  const std::size_t i =
718  numeric_cast_v<std::size_t>(to_constant_expr(index));
719  // if the access is out of bounds, we leave it unconstrained
720  if(i >= operands.size())
721  continue;
722 
723  const exprt v = operands[i];
725  index_expr.type() == v.type(),
726  "array operand type should match array element type");
727 
728  // add constraint
730  equal_exprt{index_expr, v}};
731  add_array_constraint(lazy, false); // added immediately
733  }
734  else
735  {
736  // We have a non-constant index into an array constant. We need to build a
737  // case statement testing the index against all possible values. Whenever
738  // neighbouring array elements are the same, we can test the index against
739  // the range rather than individual elements. This should be particularly
740  // helpful when we have arrays of zeros, as is the case for initializers.
741 
742  std::vector<std::pair<std::size_t, std::size_t>> ranges;
743 
744  for(std::size_t i = 0; i < operands.size(); ++i)
745  {
746  if(ranges.empty() || operands[i] != operands[ranges.back().first])
747  ranges.emplace_back(i, i);
748  else
749  ranges.back().second = i;
750  }
751 
752  for(const auto &range : ranges)
753  {
754  exprt index_constraint;
755 
756  if(range.first == range.second)
757  {
758  index_constraint =
759  equal_exprt{index, from_integer(range.first, index.type())};
760  }
761  else
762  {
763  index_constraint = and_exprt{
765  from_integer(range.first, index.type()), ID_le, index},
767  index, ID_le, from_integer(range.second, index.type())}};
768  }
769 
772  implies_exprt{index_constraint,
773  equal_exprt{index_expr, operands[range.first]}}};
774  add_array_constraint(lazy, true); // added lazily
776  }
777  }
778  }
779 }
780 
782  const index_sett &index_set,
783  const array_comprehension_exprt &expr)
784 {
785  // we got x=lambda(i: e)
786  // get all other array index applications
787  // and add constraints x[j]=e[i/j]
788 
789  for(const auto &index : index_set)
790  {
791  index_exprt index_expr{expr, index};
792  exprt comprehension_body = expr.body();
793  replace_expr(expr.arg(), index, comprehension_body);
794 
795  // add constraint
798  equal_exprt(index_expr, comprehension_body));
799 
800  add_array_constraint(lazy, false); // added immediately
802  }
803 }
804 
806  const index_sett &index_set,
807  const if_exprt &expr)
808 {
809  // we got x=(c?a:b)
810  literalt cond_lit=convert(expr.cond());
811 
812  // get other array index applications
813  // and add c => x[i]=a[i]
814  // !c => x[i]=b[i]
815 
816  // first do true case
817 
818  for(const auto &index : index_set)
819  {
820  const typet subtype = expr.type().subtype();
821  index_exprt index_expr1(expr, index, subtype);
822  index_exprt index_expr2(expr.true_case(), index, subtype);
823 
824  // add implication
826  or_exprt(literal_exprt(!cond_lit),
827  equal_exprt(index_expr1, index_expr2)));
828  add_array_constraint(lazy, false); // added immediately
830 
831 #if 0 // old code for adding, not significantly faster
832  prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
833 #endif
834  }
835 
836  // now the false case
837  for(const auto &index : index_set)
838  {
839  const typet subtype = expr.type().subtype();
840  index_exprt index_expr1(expr, index, subtype);
841  index_exprt index_expr2(expr.false_case(), index, subtype);
842 
843  // add implication
846  or_exprt(literal_exprt(cond_lit),
847  equal_exprt(index_expr1, index_expr2)));
848  add_array_constraint(lazy, false); // added immediately
850 
851 #if 0 // old code for adding, not significantly faster
852  prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
853 #endif
854  }
855 }
856 
858 {
859  switch(type)
860  {
862  return "arrayAckermann";
864  return "arrayWith";
866  return "arrayIf";
868  return "arrayOf";
870  return "arrayTypecast";
872  return "arrayConstant";
874  return "arrayComprehension";
876  return "arrayEquality";
877  default:
878  UNREACHABLE;
879  }
880 }
881 
883 {
884  json_objectt json_result;
885  json_objectt &json_array_theory =
886  json_result["arrayConstraints"].make_object();
887 
888  size_t num_constraints = 0;
889 
890  array_constraint_countt::iterator it = array_constraint_count.begin();
891  while(it != array_constraint_count.end())
892  {
893  std::string contraint_type_string = enum_to_string(it->first);
894  json_array_theory[contraint_type_string] =
895  json_numbert(std::to_string(it->second));
896 
897  num_constraints += it->second;
898  it++;
899  }
900 
901  json_result["numOfConstraints"] =
902  json_numbert(std::to_string(num_constraints));
903  log.status() << ",\n" << json_result;
904 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2172
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
json_numbert
Definition: json.h:291
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:3076
format
static format_containert< T > format(const T &o)
Definition: format.h:37
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2421
arrayst::constraint_typet::ARRAY_WITH
@ ARRAY_WITH
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1788
arrayst::constraint_typet::ARRAY_COMPREHENSION
@ ARRAY_COMPREHENSION
arrayst::array_equalityt::f1
exprt f1
Definition: arrays.h:66
arrayst::constraint_typet::ARRAY_IF
@ ARRAY_IF
typet::subtype
const typet & subtype() const
Definition: type.h:47
arrayst::constraint_typet
constraint_typet
Definition: arrays.h:117
arrayst::array_comprehension_args
std::unordered_set< irep_idt > array_comprehension_args
Definition: arrays.h:161
arrayst::record_array_equality
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:55
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:1411
arrayst::log
messaget log
Definition: arrays.h:55
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1333
arrayst::lazy_constraintt
Definition: arrays.h:98
typet
The type of an expression, extends irept.
Definition: type.h:28
update_exprt::old
exprt & old()
Definition: std_expr.h:2368
bvt
std::vector< literalt > bvt
Definition: literal.h:201
arrayst::index_map
index_mapt index_map
Definition: arrays.h:83
messaget::status
mstreamt & status() const
Definition: message.h:414
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
arrayst::collect_arrays
void collect_arrays(const exprt &a)
Definition: arrays.cpp:130
and_exprt
Boolean AND.
Definition: std_expr.h:1834
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:1361
exprt
Base class for all expressions.
Definition: expr.h:54
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:1323
array_comprehension_exprt::arg
const symbol_exprt & arg() const
Definition: std_expr.h:3037
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:83
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
arrayst::array_equalityt::l
literalt l
Definition: arrays.h:65
arrayst::update_indices
std::set< std::size_t > update_indices
Definition: arrays.h:157
jsont::make_object
json_objectt & make_object()
Definition: json.h:438
arrayst::array_constraint_count
array_constraint_countt array_constraint_count
Definition: arrays.h:129
namespace.h
equal_exprt
Equality.
Definition: std_expr.h:1139
arrayst::constraint_typet::ARRAY_ACKERMANN
@ ARRAY_ACKERMANN
arrayst::lazy_typet::ARRAY_IF
@ ARRAY_IF
json_irep.h
Util.
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2123
json_objectt
Definition: json.h:300
arrayst::constraint_typet::ARRAY_OF
@ ARRAY_OF
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
union_find::number
size_type number(const T &a)
Definition: union_find.h:235
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
array_exprt::type
const array_typet & type() const
Definition: std_expr.h:1388
with_exprt::old
exprt & old()
Definition: std_expr.h:2182
arrayst::add_array_constraints_with
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition: arrays.cpp:540
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:110
arrayst::lazy_typet::ARRAY_OF
@ ARRAY_OF
union_find::find_number
size_type find_number(const_iterator it) const
Definition: union_find.h:201
DATA_INVARIANT_WITH_DIAGNOSTICS
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:512
or_exprt
Boolean OR.
Definition: std_expr.h:1942
union_find::make_union
bool make_union(const T &a, const T &b)
Definition: union_find.h:155
arrayst::add_array_constraints
void add_array_constraints()
Definition: arrays.cpp:276
arrayst::lazy_array_constraints
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:112
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:2557
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:643
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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:1316
std_types.h
Pre-defined types.
arrayst::array_equalities
array_equalitiest array_equalities
Definition: arrays.h:73
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
array_comprehension_exprt::body
const exprt & body() const
Definition: std_expr.h:3047
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:79
index_exprt::index
exprt & index()
Definition: std_expr.h:1268
arrayst::lazy_typet::ARRAY_WITH
@ ARRAY_WITH
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
arrayst::expr_map
std::map< exprt, bool > expr_map
Definition: arrays.h:114
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
union_find::is_root_number
bool is_root_number(size_type a) const
Definition: union_find.h:216
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
arrayst::record_array_index
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:45
equalityt
Definition: equality.h:20
arrayst::constraint_typet::ARRAY_CONSTANT
@ ARRAY_CONSTANT
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
arrayst::add_array_Ackermann_constraints
void add_array_Ackermann_constraints()
Definition: arrays.cpp:326
arrayst::array_equalityt::f2
exprt f2
Definition: arrays.h:66
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:154
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:2234
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2356
arrayst::display_array_constraint_count
void display_array_constraint_count()
Definition: arrays.cpp:882
irep_pretty_diagnosticst
Definition: irep.h:514
arrayst::add_array_constraints_update
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition: arrays.cpp:618
format_expr.h
arrays.h
Theory of Arrays with Extensionality.
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
union_find::size
size_t size() const
Definition: union_find.h:268
arrayst::array_equalityt
Definition: arrays.h:64
array_typet
Arrays with given size.
Definition: std_types.h:757
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2113
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:100
arrayst::add_array_constraints_comprehension
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
Definition: arrays.cpp:781
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
arrayst::lazy_typet::ARRAY_CONSTANT
@ ARRAY_CONSTANT
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2103
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:807
arrayst::add_array_constraints_array_constant
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
Definition: arrays.cpp:700
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:675
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
arrayst::update_index_map
void update_index_map(bool update_all)
Definition: arrays.cpp:402
implies_exprt
Boolean implication.
Definition: std_expr.h:1897
replace_expr.h
exprt::operands
operandst & operands()
Definition: expr.h:96
arrayst::arrays
union_find< exprt, irep_hash > arrays
Definition: arrays.h:76
arrayst::lazy_typet::ARRAY_ACKERMANN
@ ARRAY_ACKERMANN
index_exprt
Array index operator.
Definition: std_expr.h:1242
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
arrayst::lazy_arrays
bool lazy_arrays
Definition: arrays.h:109
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3013
arrayst::constraint_typet::ARRAY_EQUALITY
@ ARRAY_EQUALITY
message.h
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:251
arrayst::get_array_constraints
bool get_array_constraints
Definition: arrays.h:111
arrayst::lazy_typet::ARRAY_COMPREHENSION
@ ARRAY_COMPREHENSION
std_expr.h
API to expression classes.
arrayst::constraint_typet::ARRAY_TYPECAST
@ ARRAY_TYPECAST
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1381
arrayst::add_array_constraints_equality
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition: arrays.cpp:436
arrayst::arrayst
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition: arrays.cpp:29
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
arrayst::enum_to_string
std::string enum_to_string(constraint_typet)
Definition: arrays.cpp:857
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:128
ui_message.h
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700
arrayst::add_array_constraints_if
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition: arrays.cpp:805