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/json.h>
13 #include <util/message.h>
14 #include <util/replace_expr.h>
15 #include <util/std_expr.h>
16 
18 #include <solvers/prop/prop.h>
19 
20 #ifdef DEBUG
21 #include <iostream>
22 #endif
23 
24 #include <unordered_set>
25 
27  const namespacet &_ns,
28  propt &_prop,
29  message_handlert &_message_handler,
30  bool _get_array_constraints)
31  : equalityt(_prop, _message_handler),
32  ns(_ns),
33  log(_message_handler),
34  message_handler(_message_handler)
35 {
36  lazy_arrays = false; // will be set to true when --refine is used
37  incremental_cache = false; // for incremental solving
38  // get_array_constraints is true when --show-array-constraints is used
39  get_array_constraints = _get_array_constraints;
40 }
41 
43 {
44  // we are not allowed to put the index directly in the
45  // entry for the root of the equivalence class
46  // because this map is accessed during building the error trace
47  std::size_t number=arrays.number(index.array());
48  if(index_map[number].insert(index.index()).second)
49  update_indices.insert(number);
50 }
51 
53  const equal_exprt &equality)
54 {
55  const exprt &op0=equality.op0();
56  const exprt &op1=equality.op1();
57 
59  op0.type() == op1.type(),
60  "record_array_equality got equality without matching types",
61  irep_pretty_diagnosticst{equality});
62 
64  op0.type().id() == ID_array,
65  "record_array_equality parameter should be array-typed");
66 
67  array_equalities.push_back(array_equalityt());
68 
69  array_equalities.back().f1=op0;
70  array_equalities.back().f2=op1;
71  array_equalities.back().l=SUB::equality(op0, op1);
72 
73  arrays.make_union(op0, op1);
74  collect_arrays(op0);
75  collect_arrays(op1);
76 
77  return array_equalities.back().l;
78 }
79 
81 {
82  for(std::size_t i=0; i<arrays.size(); i++)
83  {
85  }
86 }
87 
89 {
90  if(expr.id()!=ID_index)
91  {
92  if(expr.id() == ID_array_comprehension)
95 
96  forall_operands(op, expr) collect_indices(*op);
97  }
98  else
99  {
100  const index_exprt &e = to_index_expr(expr);
101 
102  if(
103  e.index().id() == ID_symbol &&
105  to_symbol_expr(e.index()).get_identifier()) != 0)
106  {
107  return;
108  }
109 
110  collect_indices(e.index()); // necessary?
111 
112  const typet &array_op_type = e.array().type();
113 
114  if(array_op_type.id()==ID_array)
115  {
116  const array_typet &array_type=
117  to_array_type(array_op_type);
118 
119  if(is_unbounded_array(array_type))
120  {
122  }
123  }
124  }
125 }
126 
128 {
129  const array_typet &array_type = to_array_type(a.type());
130 
131  if(a.id()==ID_with)
132  {
133  const with_exprt &with_expr=to_with_expr(a);
134 
136  array_type == with_expr.old().type(),
137  "collect_arrays got 'with' without matching types",
139 
140  arrays.make_union(a, with_expr.old());
141  collect_arrays(with_expr.old());
142 
143  // make sure this shows as an application
144  for(std::size_t i = 1; i < with_expr.operands().size(); i += 2)
145  {
146  index_exprt index_expr(with_expr.old(), with_expr.operands()[i]);
147  record_array_index(index_expr);
148  }
149  }
150  else if(a.id()==ID_update)
151  {
152  const update_exprt &update_expr=to_update_expr(a);
153 
155  array_type == update_expr.old().type(),
156  "collect_arrays got 'update' without matching types",
158 
159  arrays.make_union(a, update_expr.old());
160  collect_arrays(update_expr.old());
161 
162 #if 0
163  // make sure this shows as an application
164  index_exprt index_expr(update_expr.old(), update_expr.index());
165  record_array_index(index_expr);
166 #endif
167  }
168  else if(a.id()==ID_if)
169  {
170  const if_exprt &if_expr=to_if_expr(a);
171 
173  array_type == if_expr.true_case().type(),
174  "collect_arrays got if without matching types",
176 
178  array_type == if_expr.false_case().type(),
179  "collect_arrays got if without matching types",
181 
182  arrays.make_union(a, if_expr.true_case());
183  arrays.make_union(a, if_expr.false_case());
184  collect_arrays(if_expr.true_case());
185  collect_arrays(if_expr.false_case());
186  }
187  else if(a.id()==ID_symbol)
188  {
189  }
190  else if(a.id()==ID_nondet_symbol)
191  {
192  }
193  else if(a.id()==ID_member)
194  {
195  const auto &struct_op = to_member_expr(a).struct_op();
196 
198  struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
199  "unexpected array expression: member with '" + struct_op.id_string() +
200  "'");
201  }
202  else if(a.id()==ID_constant ||
203  a.id()==ID_array ||
204  a.id()==ID_string_constant)
205  {
206  }
207  else if(a.id()==ID_array_of)
208  {
209  }
210  else if(a.id()==ID_byte_update_little_endian ||
211  a.id()==ID_byte_update_big_endian)
212  {
214  false,
215  "byte_update should be removed before collect_arrays");
216  }
217  else if(a.id()==ID_typecast)
218  {
219  const auto &typecast_op = to_typecast_expr(a).op();
220 
221  // cast between array types?
223  typecast_op.type().id() == ID_array,
224  "unexpected array type cast from " + typecast_op.type().id_string());
225 
226  arrays.make_union(a, typecast_op);
227  collect_arrays(typecast_op);
228  }
229  else if(a.id()==ID_index)
230  {
231  // nested unbounded arrays
232  const auto &array_op = to_index_expr(a).array();
233  arrays.make_union(a, array_op);
234  collect_arrays(array_op);
235  }
236  else if(a.id() == ID_array_comprehension)
237  {
238  }
239  else
240  {
242  false,
243  "unexpected array expression (collect_arrays): '" + a.id_string() + "'");
244  }
245 }
246 
249 {
250  if(lazy_arrays && refine)
251  {
252  // lazily add the constraint
254  {
255  if(expr_map.find(lazy.lazy) == expr_map.end())
256  {
257  lazy_array_constraints.push_back(lazy);
258  expr_map[lazy.lazy] = true;
259  }
260  }
261  else
262  {
263  lazy_array_constraints.push_back(lazy);
264  }
265  }
266  else
267  {
268  // add the constraint eagerly
270  }
271 }
272 
274 {
275  collect_indices();
276  // at this point all indices should in the index set
277 
278  // reduce initial index map
279  update_index_map(true);
280 
281  // add constraints for if, with, array_of, lambda
282  std::set<std::size_t> roots_to_process, updated_roots;
283  for(std::size_t i=0; i<arrays.size(); i++)
284  roots_to_process.insert(arrays.find_number(i));
285 
286  while(!roots_to_process.empty())
287  {
288  for(std::size_t i = 0; i < arrays.size(); i++)
289  {
290  if(roots_to_process.count(arrays.find_number(i)) == 0)
291  continue;
292 
293  // take a copy as arrays may get modified by add_array_constraints
294  // in case of nested unbounded arrays
295  exprt a = arrays[i];
296 
298 
299  // we have to update before it gets used in the next add_* call
300  for(const std::size_t u : update_indices)
301  updated_roots.insert(arrays.find_number(u));
302  update_index_map(false);
303  }
304 
305  roots_to_process = std::move(updated_roots);
306  updated_roots.clear();
307  }
308 
309  // add constraints for equalities
310  for(const auto &equality : array_equalities)
311  {
314  equality);
315 
316  // update_index_map should not be necessary here
317  }
318 
319  // add the Ackermann constraints
321 }
322 
324 {
325  // this is quadratic!
326 
327 #ifdef DEBUG
328  std::cout << "arrays.size(): " << arrays.size() << '\n';
329 #endif
330 
331  // iterate over arrays
332  for(std::size_t i=0; i<arrays.size(); i++)
333  {
334  const index_sett &index_set=index_map[arrays.find_number(i)];
335 
336 #ifdef DEBUG
337  std::cout << "index_set.size(): " << index_set.size() << '\n';
338 #endif
339 
340  // iterate over indices, 2x!
341  for(index_sett::const_iterator
342  i1=index_set.begin();
343  i1!=index_set.end();
344  i1++)
345  for(index_sett::const_iterator
346  i2=i1;
347  i2!=index_set.end();
348  i2++)
349  if(i1!=i2)
350  {
351  if(i1->is_constant() && i2->is_constant())
352  continue;
353 
354  // index equality
355  const equal_exprt indices_equal(
356  *i1, typecast_exprt::conditional_cast(*i2, i1->type()));
357 
358  literalt indices_equal_lit=convert(indices_equal);
359 
360  if(indices_equal_lit!=const_literal(false))
361  {
362  const typet &subtype =
363  to_array_type(arrays[i].type()).element_type();
364  index_exprt index_expr1(arrays[i], *i1, subtype);
365 
366  index_exprt index_expr2=index_expr1;
367  index_expr2.index()=*i2;
368 
369  equal_exprt values_equal(index_expr1, index_expr2);
370 
371  // add constraint
373  implies_exprt(literal_exprt(indices_equal_lit), values_equal));
374  add_array_constraint(lazy, true); // added lazily
376 
377 #if 0 // old code for adding, not significantly faster
378  prop.lcnf(!indices_equal_lit, convert(values_equal));
379 #endif
380  }
381  }
382  }
383 }
384 
386 void arrayst::update_index_map(std::size_t i)
387 {
388  if(arrays.is_root_number(i))
389  return;
390 
391  std::size_t root_number=arrays.find_number(i);
392  INVARIANT(root_number!=i, "is_root_number incorrect?");
393 
394  index_sett &root_index_set=index_map[root_number];
395  index_sett &index_set=index_map[i];
396 
397  root_index_set.insert(index_set.begin(), index_set.end());
398 }
399 
400 void arrayst::update_index_map(bool update_all)
401 {
402  // iterate over non-roots
403  // possible reasons why update is needed:
404  // -- there are new equivalence classes in arrays
405  // -- there are new indices for arrays that are not the root
406  // of an equivalence class
407  // (and we cannot do that in record_array_index())
408  // -- equivalence classes have been merged
409  if(update_all)
410  {
411  for(std::size_t i=0; i<arrays.size(); i++)
412  update_index_map(i);
413  }
414  else
415  {
416  for(const auto &index : update_indices)
417  update_index_map(index);
418 
419  update_indices.clear();
420  }
421 
422 #ifdef DEBUG
423  // print index sets
424  for(const auto &index_entry : index_map)
425  for(const auto &index : index_entry.second)
426  std::cout << "Index set (" << index_entry.first << " = "
427  << arrays.find_number(index_entry.first) << " = "
428  << format(arrays[arrays.find_number(index_entry.first)])
429  << "): " << format(index) << '\n';
430  std::cout << "-----\n";
431 #endif
432 }
433 
435  const index_sett &index_set,
436  const array_equalityt &array_equality)
437 {
438  // add constraints x=y => x[i]=y[i]
439 
440  for(const auto &index : index_set)
441  {
442  const typet &element_type1 =
443  to_array_type(array_equality.f1.type()).element_type();
444  index_exprt index_expr1(array_equality.f1, index, element_type1);
445 
446  const typet &element_type2 =
447  to_array_type(array_equality.f2.type()).element_type();
448  index_exprt index_expr2(array_equality.f2, index, element_type2);
449 
451  index_expr1.type()==index_expr2.type(),
452  "array elements should all have same type");
453 
454  array_equalityt equal;
455  equal.f1 = index_expr1;
456  equal.f2 = index_expr2;
457  equal.l = array_equality.l;
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 &element_type = to_array_type(expr.type()).element_type();
514  index_exprt index_expr1(expr, index, element_type);
515  index_exprt index_expr2(expr_typecast_op, index, element_type);
516 
518  index_expr1.type()==index_expr2.type(),
519  "array elements should all have same type");
520 
521  // add constraint
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(
555  expr, index, to_array_type(expr.type()).element_type());
556 
558  index_expr.type() == value.type(),
559  "with-expression operand should match array element type",
561 
563  lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
564  add_array_constraint(lazy, false); // added immediately
566 
567  updated_indices.insert(index);
568  }
569 
570  // For all other indices use the existing value, i.e., add constraints
571  // x[I]=y[I] for I!=i,j,...
572 
573  for(auto other_index : index_set)
574  {
575  if(updated_indices.find(other_index) == updated_indices.end())
576  {
577  // we first build the guard
578  exprt::operandst disjuncts;
579  disjuncts.reserve(updated_indices.size());
580  for(const auto &index : updated_indices)
581  {
582  disjuncts.push_back(equal_exprt{
583  index, typecast_exprt::conditional_cast(other_index, index.type())});
584  }
585 
586  literalt guard_lit = convert(disjunction(disjuncts));
587 
588  if(guard_lit!=const_literal(true))
589  {
590  const typet &element_type = to_array_type(expr.type()).element_type();
591  index_exprt index_expr1(expr, other_index, element_type);
592  index_exprt index_expr2(expr.old(), other_index, element_type);
593 
594  equal_exprt equality_expr(index_expr1, index_expr2);
595 
596  // add constraint
598  literal_exprt(guard_lit)));
599 
600  add_array_constraint(lazy, false); // added immediately
602 
603 #if 0 // old code for adding, not significantly faster
604  {
605  literalt equality_lit=convert(equality_expr);
606 
607  bvt bv;
608  bv.reserve(2);
609  bv.push_back(equality_lit);
610  bv.push_back(guard_lit);
611  prop.lcnf(bv);
612  }
613 #endif
614  }
615  }
616  }
617 }
618 
620  const index_sett &,
621  const update_exprt &)
622 {
623  // we got x=UPDATE(y, [i], v)
624  // add constaint x[i]=v
625 
626 #if 0
627  const exprt &index=expr.where();
628  const exprt &value=expr.new_value();
629 
630  {
631  index_exprt index_expr(expr, index, expr.type().subtype());
632 
634  index_expr.type()==value.type(),
635  "update operand should match array element type",
637 
638  set_to_true(equal_exprt(index_expr, value));
639  }
640 
641  // use other array index applications for "else" case
642  // add constraint x[I]=y[I] for I!=i
643 
644  for(auto other_index : index_set)
645  {
646  if(other_index!=index)
647  {
648  // we first build the guard
649 
650  other_index = typecast_exprt::conditional_cast(other_index, index.type());
651 
652  literalt guard_lit=convert(equal_exprt(index, other_index));
653 
654  if(guard_lit!=const_literal(true))
655  {
656  const typet &subtype=expr.type().subtype();
657  index_exprt index_expr1(expr, other_index, subtype);
658  index_exprt index_expr2(expr.op0(), other_index, subtype);
659 
660  equal_exprt equality_expr(index_expr1, index_expr2);
661 
662  literalt equality_lit=convert(equality_expr);
663 
664  // add constraint
665  bvt bv;
666  bv.reserve(2);
667  bv.push_back(equality_lit);
668  bv.push_back(guard_lit);
669  prop.lcnf(bv);
670  }
671  }
672  }
673 #endif
674 }
675 
677  const index_sett &index_set,
678  const array_of_exprt &expr)
679 {
680  // we got x=array_of[v]
681  // get other array index applications
682  // and add constraint x[i]=v
683 
684  for(const auto &index : index_set)
685  {
686  const typet &element_type = expr.type().element_type();
687  index_exprt index_expr(expr, index, element_type);
688 
690  index_expr.type() == expr.what().type(),
691  "array_of operand type should match array element type");
692 
693  // add constraint
695  lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.what()));
696  add_array_constraint(lazy, false); // added immediately
698  }
699 }
700 
702  const index_sett &index_set,
703  const array_exprt &expr)
704 {
705  // we got x = { v, ... } - add constraint x[i] = v
706  const exprt::operandst &operands = expr.operands();
707 
708  for(const auto &index : index_set)
709  {
710  const typet &element_type = expr.type().element_type();
711  const index_exprt index_expr{expr, index, element_type};
712 
713  if(index.is_constant())
714  {
715  // We have a constant index - just pick the element at that index from the
716  // array constant.
717 
718  const std::size_t i =
719  numeric_cast_v<std::size_t>(to_constant_expr(index));
720  // if the access is out of bounds, we leave it unconstrained
721  if(i >= operands.size())
722  continue;
723 
724  const exprt v = operands[i];
726  index_expr.type() == v.type(),
727  "array operand type should match array element type");
728 
729  // add constraint
731  equal_exprt{index_expr, v}};
732  add_array_constraint(lazy, false); // added immediately
734  }
735  else
736  {
737  // We have a non-constant index into an array constant. We need to build a
738  // case statement testing the index against all possible values. Whenever
739  // neighbouring array elements are the same, we can test the index against
740  // the range rather than individual elements. This should be particularly
741  // helpful when we have arrays of zeros, as is the case for initializers.
742 
743  std::vector<std::pair<std::size_t, std::size_t>> ranges;
744 
745  for(std::size_t i = 0; i < operands.size(); ++i)
746  {
747  if(ranges.empty() || operands[i] != operands[ranges.back().first])
748  ranges.emplace_back(i, i);
749  else
750  ranges.back().second = i;
751  }
752 
753  for(const auto &range : ranges)
754  {
755  exprt index_constraint;
756 
757  if(range.first == range.second)
758  {
759  index_constraint =
760  equal_exprt{index, from_integer(range.first, index.type())};
761  }
762  else
763  {
764  index_constraint = and_exprt{
766  from_integer(range.first, index.type()), ID_le, index},
768  index, ID_le, from_integer(range.second, index.type())}};
769  }
770 
773  implies_exprt{index_constraint,
774  equal_exprt{index_expr, operands[range.first]}}};
775  add_array_constraint(lazy, true); // added lazily
777  }
778  }
779  }
780 }
781 
783  const index_sett &index_set,
784  const array_comprehension_exprt &expr)
785 {
786  // we got x=lambda(i: e)
787  // get all other array index applications
788  // and add constraints x[j]=e[i/j]
789 
790  for(const auto &index : index_set)
791  {
792  index_exprt index_expr{expr, index};
793  exprt comprehension_body = expr.body();
794  replace_expr(expr.arg(), index, comprehension_body);
795 
796  // add constraint
799  equal_exprt(index_expr, comprehension_body));
800 
801  add_array_constraint(lazy, false); // added immediately
803  }
804 }
805 
807  const index_sett &index_set,
808  const if_exprt &expr)
809 {
810  // we got x=(c?a:b)
811  literalt cond_lit=convert(expr.cond());
812 
813  // get other array index applications
814  // and add c => x[i]=a[i]
815  // !c => x[i]=b[i]
816 
817  // first do true case
818 
819  for(const auto &index : index_set)
820  {
821  const typet &element_type = to_array_type(expr.type()).element_type();
822  index_exprt index_expr1(expr, index, element_type);
823  index_exprt index_expr2(expr.true_case(), index, element_type);
824 
825  // add implication
827  or_exprt(literal_exprt(!cond_lit),
828  equal_exprt(index_expr1, index_expr2)));
829  add_array_constraint(lazy, false); // added immediately
831 
832 #if 0 // old code for adding, not significantly faster
833  prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
834 #endif
835  }
836 
837  // now the false case
838  for(const auto &index : index_set)
839  {
840  const typet &element_type = to_array_type(expr.type()).element_type();
841  index_exprt index_expr1(expr, index, element_type);
842  index_exprt index_expr2(expr.false_case(), index, element_type);
843 
844  // add implication
847  or_exprt(literal_exprt(cond_lit),
848  equal_exprt(index_expr1, index_expr2)));
849  add_array_constraint(lazy, false); // added immediately
851 
852 #if 0 // old code for adding, not significantly faster
853  prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
854 #endif
855  }
856 }
857 
859 {
860  switch(type)
861  {
863  return "arrayAckermann";
865  return "arrayWith";
867  return "arrayIf";
869  return "arrayOf";
871  return "arrayTypecast";
873  return "arrayConstant";
875  return "arrayComprehension";
877  return "arrayEquality";
878  default:
879  UNREACHABLE;
880  }
881 }
882 
884 {
885  json_objectt json_result;
886  json_objectt &json_array_theory =
887  json_result["arrayConstraints"].make_object();
888 
889  size_t num_constraints = 0;
890 
891  array_constraint_countt::iterator it = array_constraint_count.begin();
892  while(it != array_constraint_count.end())
893  {
894  std::string contraint_type_string = enum_to_string(it->first);
895  json_array_theory[contraint_type_string] =
896  json_numbert(std::to_string(it->second));
897 
898  num_constraints += it->second;
899  it++;
900  }
901 
902  json_result["numOfConstraints"] =
903  json_numbert(std::to_string(num_constraints));
904  log.status() << ",\n" << json_result;
905 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Theory of Arrays with Extensionality.
Boolean AND.
Definition: std_expr.h:1974
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3182
const exprt & body() const
Definition: std_expr.h:3220
const symbol_exprt & arg() const
Definition: std_expr.h:3206
Array constructor from list of elements.
Definition: std_expr.h:1476
const array_typet & type() const
Definition: std_expr.h:1483
Array constructor from single element.
Definition: std_expr.h:1411
exprt & what()
Definition: std_expr.h:1428
const array_typet & type() const
Definition: std_expr.h:1418
Arrays with given size.
Definition: std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:114
std::unordered_set< irep_idt > array_comprehension_args
Definition: arrays.h:163
index_mapt index_map
Definition: arrays.h:85
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition: arrays.cpp:434
std::set< std::size_t > update_indices
Definition: arrays.h:159
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
Definition: arrays.cpp:676
void add_array_Ackermann_constraints()
Definition: arrays.cpp:323
bool lazy_arrays
Definition: arrays.h:111
void collect_indices()
Definition: arrays.cpp:80
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition: arrays.cpp:619
void collect_arrays(const exprt &a)
Definition: arrays.cpp:127
union_find< exprt, irep_hash > arrays
Definition: arrays.h:78
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:52
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
Definition: arrays.cpp:701
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition: arrays.cpp:26
constraint_typet
Definition: arrays.h:119
std::map< exprt, bool > expr_map
Definition: arrays.h:116
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition: arrays.cpp:806
std::string enum_to_string(constraint_typet)
Definition: arrays.cpp:858
bool get_array_constraints
Definition: arrays.h:113
void add_array_constraints()
Definition: arrays.cpp:273
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
Definition: arrays.cpp:782
virtual bool is_unbounded_array(const typet &type) const =0
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:42
array_equalitiest array_equalities
Definition: arrays.h:75
std::set< exprt > index_sett
Definition: arrays.h:81
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
Definition: arrays.cpp:248
array_constraint_countt array_constraint_count
Definition: arrays.h:131
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition: arrays.cpp:540
bool incremental_cache
Definition: arrays.h:112
void display_array_constraint_count()
Definition: arrays.cpp:883
void update_index_map(bool update_all)
Definition: arrays.cpp:400
messaget log
Definition: arrays.h:57
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
Equality.
Definition: std_expr.h:1225
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
Boolean implication.
Definition: std_expr.h:2037
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
const std::string & id_string() const
Definition: irep.h:399
const irep_idt & id() const
Definition: irep.h:396
json_objectt & make_object()
Definition: json.h:438
const exprt & struct_op() const
Definition: std_expr.h:2697
mstreamt & status() const
Definition: message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Boolean OR.
Definition: std_expr.h:2082
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
TO_BE_DOCUMENTED.
Definition: prop.h:23
void l_set_to_true(literalt a)
Definition: prop.h:50
void lcnf(literalt l0, literalt l1)
Definition: prop.h:56
const irep_idt & get_identifier() const
Definition: std_expr.h:109
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
const exprt & op() const
Definition: std_expr.h:293
size_type number(const T &a)
Definition: union_find.h:235
bool make_union(const T &a, const T &b)
Definition: union_find.h:155
size_t size() const
Definition: union_find.h:268
size_type find_number(const_iterator it) const
Definition: union_find.h:201
bool is_root_number(size_type a) const
Definition: union_find.h:216
Operator to update elements in structs and arrays.
Definition: std_expr.h:2496
exprt & old()
Definition: std_expr.h:2508
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
exprt & old()
Definition: std_expr.h:2322
#define forall_operands(it, expr)
Definition: expr.h:18
static format_containert< T > format(const T &o)
Definition: format.h:37
auto lazy(funt fun) -> lazyt< decltype(fun())>
Delay the computation of fun to the next time the force method is called.
Definition: lazy.h:49
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2561
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1506
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:3249
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1456
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.