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/base_type.h>
13 #include <util/format_expr.h>
14 #include <util/namespace.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 
25  const namespacet &_ns,
26  propt &_prop):equalityt(_ns, _prop)
27 {
28  lazy_arrays = false; // will be set to true when --refine is used
29  incremental_cache = false; // for incremental solving
30 }
31 
33 {
34  // we are not allowed to put the index directly in the
35  // entry for the root of the equivalence class
36  // because this map is accessed during building the error trace
37  std::size_t number=arrays.number(index.array());
38  index_map[number].insert(index.index());
39  update_indices.insert(number);
40 }
41 
43  const equal_exprt &equality)
44 {
45  const exprt &op0=equality.op0();
46  const exprt &op1=equality.op1();
47 
48  // check types
49  if(!base_type_eq(op0.type(), op1.type(), ns))
50  {
51  prop.error() << equality.pretty() << messaget::eom;
53  false,
54  "record_array_equality got equality without matching types");
55  }
56 
58  ns.follow(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  forall_operands(op, expr) collect_indices(*op);
87  }
88  else
89  {
90  const index_exprt &e = to_index_expr(expr);
91  collect_indices(e.index()); // necessary?
92 
93  const typet &array_op_type=ns.follow(e.array().type());
94 
95  if(array_op_type.id()==ID_array)
96  {
97  const array_typet &array_type=
98  to_array_type(array_op_type);
99 
100  if(is_unbounded_array(array_type))
101  {
103  }
104  }
105  }
106 }
107 
109 {
110  const array_typet &array_type=
111  to_array_type(ns.follow(a.type()));
112 
113  if(a.id()==ID_with)
114  {
115  const with_exprt &with_expr=to_with_expr(a);
116 
117  // check types
118  if(!base_type_eq(array_type, with_expr.old().type(), ns))
119  {
120  prop.error() << a.pretty() << messaget::eom;
121  DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
122  }
123 
124  arrays.make_union(a, with_expr.old());
125  collect_arrays(with_expr.old());
126 
127  // make sure this shows as an application
128  index_exprt index_expr(with_expr.old(), with_expr.where());
129  record_array_index(index_expr);
130  }
131  else if(a.id()==ID_update)
132  {
133  const update_exprt &update_expr=to_update_expr(a);
134 
135  // check types
136  if(!base_type_eq(array_type, update_expr.old().type(), ns))
137  {
138  prop.error() << a.pretty() << messaget::eom;
140  false,
141  "collect_arrays got 'update' without matching types");
142  }
143 
144  arrays.make_union(a, update_expr.old());
145  collect_arrays(update_expr.old());
146 
147 #if 0
148  // make sure this shows as an application
149  index_exprt index_expr(update_expr.old(), update_expr.index());
150  record_array_index(index_expr);
151 #endif
152  }
153  else if(a.id()==ID_if)
154  {
155  const if_exprt &if_expr=to_if_expr(a);
156 
157  // check types
158  if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
159  {
160  prop.error() << a.pretty() << messaget::eom;
161  DATA_INVARIANT(false, "collect_arrays got if without matching types");
162  }
163 
164  // check types
165  if(!base_type_eq(array_type, if_expr.false_case().type(), ns))
166  {
167  prop.error() << a.pretty() << messaget::eom;
168  DATA_INVARIANT(false, "collect_arrays got if without matching types");
169  }
170 
171  arrays.make_union(a, if_expr.true_case());
172  arrays.make_union(a, if_expr.false_case());
173  collect_arrays(if_expr.true_case());
174  collect_arrays(if_expr.false_case());
175  }
176  else if(a.id()==ID_symbol)
177  {
178  }
179  else if(a.id()==ID_nondet_symbol)
180  {
181  }
182  else if(a.id()==ID_member)
183  {
185  to_member_expr(a).struct_op().id()==ID_symbol,
186  ("unexpected array expression: member with `"+
187  a.op0().id_string()+"'").c_str());
188  }
189  else if(a.id()==ID_constant ||
190  a.id()==ID_array ||
191  a.id()==ID_string_constant)
192  {
193  }
194  else if(a.id()==ID_array_of)
195  {
196  }
197  else if(a.id()==ID_byte_update_little_endian ||
198  a.id()==ID_byte_update_big_endian)
199  {
201  false,
202  "byte_update should be removed before collect_arrays");
203  }
204  else if(a.id()==ID_typecast)
205  {
206  // cast between array types?
208  a.operands().size()==1,
209  "typecast must have one operand");
210 
212  a.op0().type().id()==ID_array,
213  ("unexpected array type cast from "+
214  a.op0().type().id_string()).c_str());
215 
216  arrays.make_union(a, a.op0());
217  collect_arrays(a.op0());
218  }
219  else if(a.id()==ID_index)
220  {
221  // nested unbounded arrays
222  arrays.make_union(a, a.op0());
223  collect_arrays(a.op0());
224  }
225  else
226  {
228  false,
229  ("unexpected array expression (collect_arrays): `"+
230  a.id_string()+"'").c_str());
231  }
232 }
233 
235 void arrayst::add_array_constraint(const lazy_constraintt &lazy, bool refine)
236 {
237  if(lazy_arrays && refine)
238  {
239  // lazily add the constraint
241  {
242  if(expr_map.find(lazy.lazy) == expr_map.end())
243  {
244  lazy_array_constraints.push_back(lazy);
245  expr_map[lazy.lazy] = true;
246  }
247  }
248  else
249  {
250  lazy_array_constraints.push_back(lazy);
251  }
252  }
253  else
254  {
255  // add the constraint eagerly
257  }
258 }
259 
261 {
262  collect_indices();
263  // at this point all indices should in the index set
264 
265  // reduce initial index map
266  update_index_map(true);
267 
268  // add constraints for if, with, array_of
269  for(std::size_t i=0; i<arrays.size(); i++)
270  {
271  // take a copy as arrays may get modified by add_array_constraints
272  // in case of nested unbounded arrays
273  exprt a=arrays[i];
274 
276 
277  // we have to update before it gets used in the next add_* call
278  update_index_map(false);
279  }
280 
281  // add constraints for equalities
282  for(const auto &equality : array_equalities)
283  {
286  equality);
287 
288  // update_index_map should not be necessary here
289  }
290 
291  // add the Ackermann constraints
293 }
294 
296 {
297  // this is quadratic!
298 
299 #ifdef DEBUG
300  std::cout << "arrays.size(): " << arrays.size() << '\n';
301 #endif
302 
303  // iterate over arrays
304  for(std::size_t i=0; i<arrays.size(); i++)
305  {
306  const index_sett &index_set=index_map[arrays.find_number(i)];
307 
308 #ifdef DEBUG
309  std::cout << "index_set.size(): " << index_set.size() << '\n';
310 #endif
311 
312  // iterate over indices, 2x!
313  for(index_sett::const_iterator
314  i1=index_set.begin();
315  i1!=index_set.end();
316  i1++)
317  for(index_sett::const_iterator
318  i2=i1;
319  i2!=index_set.end();
320  i2++)
321  if(i1!=i2)
322  {
323  if(i1->is_constant() && i2->is_constant())
324  continue;
325 
326  // index equality
327  equal_exprt indices_equal(*i1, *i2);
328 
329  if(indices_equal.op0().type()!=
330  indices_equal.op1().type())
331  {
332  indices_equal.op1().
333  make_typecast(indices_equal.op0().type());
334  }
335 
336  literalt indices_equal_lit=convert(indices_equal);
337 
338  if(indices_equal_lit!=const_literal(false))
339  {
340  const typet &subtype=ns.follow(arrays[i].type()).subtype();
341  index_exprt index_expr1(arrays[i], *i1, subtype);
342 
343  index_exprt index_expr2=index_expr1;
344  index_expr2.index()=*i2;
345 
346  equal_exprt values_equal(index_expr1, index_expr2);
347 
348  // add constraint
350  implies_exprt(literal_exprt(indices_equal_lit), values_equal));
351  add_array_constraint(lazy, true); // added lazily
352 
353 #if 0 // old code for adding, not significantly faster
354  prop.lcnf(!indices_equal_lit, convert(values_equal));
355 #endif
356  }
357  }
358  }
359 }
360 
362 void arrayst::update_index_map(std::size_t i)
363 {
364  if(arrays.is_root_number(i))
365  return;
366 
367  std::size_t root_number=arrays.find_number(i);
368  INVARIANT(root_number!=i, "is_root_number incorrect?");
369 
370  index_sett &root_index_set=index_map[root_number];
371  index_sett &index_set=index_map[i];
372 
373  root_index_set.insert(index_set.begin(), index_set.end());
374 }
375 
376 void arrayst::update_index_map(bool update_all)
377 {
378  // iterate over non-roots
379  // possible reasons why update is needed:
380  // -- there are new equivalence classes in arrays
381  // -- there are new indices for arrays that are not the root
382  // of an equivalence class
383  // (and we cannot do that in record_array_index())
384  // -- equivalence classes have been merged
385  if(update_all)
386  {
387  for(std::size_t i=0; i<arrays.size(); i++)
388  update_index_map(i);
389  }
390  else
391  {
392  for(const auto &index : update_indices)
393  update_index_map(index);
394 
395  update_indices.clear();
396  }
397 
398 #ifdef DEBUG
399  // print index sets
400  for(const auto &index_entry : index_map)
401  for(const auto &index : index_entry.second)
402  std::cout << "Index set (" << index_entry.first << " = "
403  << arrays.find_number(index_entry.first) << " = "
404  << format(arrays[arrays.find_number(index_entry.first)])
405  << "): " << format(index) << '\n';
406  std::cout << "-----\n";
407 #endif
408 }
409 
411  const index_sett &index_set,
412  const array_equalityt &array_equality)
413 {
414  // add constraints x=y => x[i]=y[i]
415 
416  for(const auto &index : index_set)
417  {
418  const typet &subtype1=ns.follow(array_equality.f1.type()).subtype();
419  index_exprt index_expr1(array_equality.f1, index, subtype1);
420 
421  const typet &subtype2=ns.follow(array_equality.f2.type()).subtype();
422  index_exprt index_expr2(array_equality.f2, index, subtype2);
423 
425  index_expr1.type()==index_expr2.type(),
426  "array elements should all have same type");
427 
428  array_equalityt equal;
429  equal.f1 = index_expr1;
430  equal.f2 = index_expr2;
431  equal.l = array_equality.l;
432  equal_exprt equality_expr(index_expr1, index_expr2);
433 
434  // add constraint
435  // equality constraints are not added lazily
436  // convert must be done to guarantee correct update of the index_set
437  prop.lcnf(!array_equality.l, convert(equality_expr));
438  }
439 }
440 
442  const index_sett &index_set,
443  const exprt &expr)
444 {
445  if(expr.id()==ID_with)
446  return add_array_constraints_with(index_set, to_with_expr(expr));
447  else if(expr.id()==ID_update)
448  return add_array_constraints_update(index_set, to_update_expr(expr));
449  else if(expr.id()==ID_if)
450  return add_array_constraints_if(index_set, to_if_expr(expr));
451  else if(expr.id()==ID_array_of)
452  return add_array_constraints_array_of(index_set, to_array_of_expr(expr));
453  else if(expr.id()==ID_symbol ||
454  expr.id()==ID_nondet_symbol ||
455  expr.id()==ID_constant ||
456  expr.id()=="zero_string" ||
457  expr.id()==ID_array ||
458  expr.id()==ID_string_constant)
459  {
460  }
461  else if(expr.id()==ID_member &&
462  to_member_expr(expr).struct_op().id()==ID_symbol)
463  {
464  }
465  else if(expr.id()==ID_byte_update_little_endian ||
466  expr.id()==ID_byte_update_big_endian)
467  {
468  INVARIANT(false, "byte_update should be removed before arrayst");
469  }
470  else if(expr.id()==ID_typecast)
471  {
472  // we got a=(type[])b
474  expr.operands().size()==1,
475  "typecast should have one operand");
476 
477  // add a[i]=b[i]
478  for(const auto &index : index_set)
479  {
480  const typet &subtype=ns.follow(expr.type()).subtype();
481  index_exprt index_expr1(expr, index, subtype);
482  index_exprt index_expr2(expr.op0(), index, subtype);
483 
485  index_expr1.type()==index_expr2.type(),
486  "array elements should all have same type");
487 
488  // add constraint
490  equal_exprt(index_expr1, index_expr2));
491  add_array_constraint(lazy, false); // added immediately
492  }
493  }
494  else if(expr.id()==ID_index)
495  {
496  }
497  else
498  {
500  false,
501  ("unexpected array expression (add_array_constraints): `"+
502  expr.id_string()+"'").c_str());
503  }
504 }
505 
507  const index_sett &index_set,
508  const with_exprt &expr)
509 {
510  // we got x=(y with [i:=v])
511  // add constraint x[i]=v
512 
513  const exprt &index=expr.where();
514  const exprt &value=expr.new_value();
515 
516  {
517  index_exprt index_expr(expr, index, ns.follow(expr.type()).subtype());
518 
519  if(index_expr.type()!=value.type())
520  {
521  prop.error() << expr.pretty() << messaget::eom;
523  false,
524  "with-expression operand should match array element type");
525  }
526 
527  lazy_constraintt lazy(
528  lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
529  add_array_constraint(lazy, false); // added immediately
530  }
531 
532  // use other array index applications for "else" case
533  // add constraint x[I]=y[I] for I!=i
534 
535  for(auto other_index : index_set)
536  {
537  if(other_index!=index)
538  {
539  // we first build the guard
540 
541  if(other_index.type()!=index.type())
542  other_index.make_typecast(index.type());
543 
544  literalt guard_lit=convert(equal_exprt(index, other_index));
545 
546  if(guard_lit!=const_literal(true))
547  {
548  const typet &subtype=ns.follow(expr.type()).subtype();
549  index_exprt index_expr1(expr, other_index, subtype);
550  index_exprt index_expr2(expr.op0(), other_index, subtype);
551 
552  equal_exprt equality_expr(index_expr1, index_expr2);
553 
554  // add constraint
556  literal_exprt(guard_lit)));
557  add_array_constraint(lazy, false); // added immediately
558 
559 #if 0 // old code for adding, not significantly faster
560  {
561  literalt equality_lit=convert(equality_expr);
562 
563  bvt bv;
564  bv.reserve(2);
565  bv.push_back(equality_lit);
566  bv.push_back(guard_lit);
567  prop.lcnf(bv);
568  }
569 #endif
570  }
571  }
572  }
573 }
574 
576  const index_sett &,
577  const update_exprt &)
578 {
579  // we got x=UPDATE(y, [i], v)
580  // add constaint x[i]=v
581 
582 #if 0
583  const exprt &index=expr.where();
584  const exprt &value=expr.new_value();
585 
586  {
587  index_exprt index_expr(expr, index, ns.follow(expr.type()).subtype());
588 
589  if(index_expr.type()!=value.type())
590  {
591  prop.error() << expr.pretty() << messaget::eom;
593  false,
594  "update operand should match array element type");
595  }
596 
597  set_to_true(equal_exprt(index_expr, value));
598  }
599 
600  // use other array index applications for "else" case
601  // add constraint x[I]=y[I] for I!=i
602 
603  for(auto other_index : index_set)
604  {
605  if(other_index!=index)
606  {
607  // we first build the guard
608 
609  if(other_index.type()!=index.type())
610  other_index.make_typecast(index.type());
611 
612  literalt guard_lit=convert(equal_exprt(index, other_index));
613 
614  if(guard_lit!=const_literal(true))
615  {
616  const typet &subtype=ns.follow(expr.type()).subtype();
617  index_exprt index_expr1(expr, other_index, subtype);
618  index_exprt index_expr2(expr.op0(), other_index, subtype);
619 
620  equal_exprt equality_expr(index_expr1, index_expr2);
621 
622  literalt equality_lit=convert(equality_expr);
623 
624  // add constraint
625  bvt bv;
626  bv.reserve(2);
627  bv.push_back(equality_lit);
628  bv.push_back(guard_lit);
629  prop.lcnf(bv);
630  }
631  }
632  }
633 #endif
634 }
635 
637  const index_sett &index_set,
638  const array_of_exprt &expr)
639 {
640  // we got x=array_of[v]
641  // get other array index applications
642  // and add constraint x[i]=v
643 
644  for(const auto &index : index_set)
645  {
646  const typet &subtype=ns.follow(expr.type()).subtype();
647  index_exprt index_expr(expr, index, subtype);
648 
650  base_type_eq(index_expr.type(), expr.op0().type(), ns),
651  "array_of operand type should match array element type");
652 
653  // add constraint
654  lazy_constraintt lazy(
655  lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.op0()));
656  add_array_constraint(lazy, false); // added immediately
657  }
658 }
659 
661  const index_sett &index_set,
662  const if_exprt &expr)
663 {
664  // we got x=(c?a:b)
665  literalt cond_lit=convert(expr.cond());
666 
667  // get other array index applications
668  // and add c => x[i]=a[i]
669  // !c => x[i]=b[i]
670 
671  // first do true case
672 
673  for(const auto &index : index_set)
674  {
675  const typet subtype=ns.follow(expr.type()).subtype();
676  index_exprt index_expr1(expr, index, subtype);
677  index_exprt index_expr2(expr.true_case(), index, subtype);
678 
679  // add implication
681  or_exprt(literal_exprt(!cond_lit),
682  equal_exprt(index_expr1, index_expr2)));
683  add_array_constraint(lazy, false); // added immediately
684 
685 #if 0 // old code for adding, not significantly faster
686  prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
687 #endif
688  }
689 
690  // now the false case
691  for(const auto &index : index_set)
692  {
693  const typet subtype=ns.follow(expr.type()).subtype();
694  index_exprt index_expr1(expr, index, subtype);
695  index_exprt index_expr2(expr.false_case(), index, subtype);
696 
697  // add implication
698  lazy_constraintt lazy(
700  or_exprt(literal_exprt(cond_lit),
701  equal_exprt(index_expr1, index_expr2)));
702  add_array_constraint(lazy, false); // added immediately
703 
704 #if 0 // old code for adding, not significantly faster
705  prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
706 #endif
707  }
708 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
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:3770
dstringt::c_str
const char * c_str() const
Definition: dstring.h:86
arrayst::array_equalityt::f1
exprt f1
Definition: arrays.h:54
typet::subtype
const typet & subtype() const
Definition: type.h:38
arrayst::record_array_equality
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:42
arith_tools.h
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:485
arrayst::lazy_constraintt
Definition: arrays.h:83
typet
The type of an expression, extends irept.
Definition: type.h:27
update_exprt::old
exprt & old()
Definition: std_expr.h:3729
bvt
std::vector< literalt > bvt
Definition: literal.h:200
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
arrayst::index_map
index_mapt index_map
Definition: arrays.h:71
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
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:3427
arrayst::collect_arrays
void collect_arrays(const exprt &a)
Definition: arrays.cpp:108
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:3552
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:1709
exprt
Base class for all expressions.
Definition: expr.h:54
decision_proceduret::set_to_true
void set_to_true(const exprt &expr)
Definition: decision_procedure.h:40
exprt::op0
exprt & op0()
Definition: expr.h:84
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:49
arrayst::collect_indices
void collect_indices()
Definition: arrays.cpp:74
arrayst::array_equalityt::l
literalt l
Definition: arrays.h:53
messaget::eom
static eomt eom
Definition: message.h:284
arrayst::update_indices
std::set< std::size_t > update_indices
Definition: arrays.h:119
namespace.h
equal_exprt
Equality.
Definition: std_expr.h:1484
arrayst::lazy_typet::ARRAY_IF
@ ARRAY_IF
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
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:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
with_exprt::old
exprt & old()
Definition: std_expr.h:3532
arrayst::add_array_constraints_with
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition: arrays.cpp:506
arrayst::incremental_cache
bool incremental_cache
Definition: arrays.h:96
arrayst::lazy_typet::ARRAY_OF
@ ARRAY_OF
messaget::error
mstreamt & error() const
Definition: message.h:386
or_exprt
Boolean OR.
Definition: std_expr.h:2531
arrayst::add_array_constraints
void add_array_constraints()
Definition: arrays.cpp:260
base_type.h
arrayst::lazy_array_constraints
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:97
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
literal_exprt
Definition: literal_expr.h:17
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1678
std_types.h
arrayst::array_equalities
array_equalitiest array_equalities
Definition: arrays.h:61
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
prop.h
exprt::op1
exprt & op1()
Definition: expr.h:87
const_literal
literalt const_literal(bool value)
Definition: literal.h:187
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:67
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
arrayst::lazy_constraintt::lazy
exprt lazy
Definition: arrays.h:86
arrayst::lazy_typet::ARRAY_WITH
@ ARRAY_WITH
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
arrayst::expr_map
std::map< exprt, bool > expr_map
Definition: arrays.h:99
irept::id
const irep_idt & id() const
Definition: irep.h:259
arrayst::record_array_index
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:32
equalityt
Definition: equality.h:19
arrayst::add_array_Ackermann_constraints
void add_array_Ackermann_constraints()
Definition: arrays.cpp:295
arrayst::array_equalityt::f2
exprt f2
Definition: arrays.h:54
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
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:3569
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3707
arrayst::add_array_constraints_update
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition: arrays.cpp:575
union_find::make_union
bool make_union(const T &a, const T &b)
Definition: union_find.h:154
format_expr.h
arrays.h
propt
TO_BE_DOCUMENTED.
Definition: prop.h:24
arrayst::array_equalityt
Definition: arrays.h:51
array_typet
Arrays with given size.
Definition: std_types.h:1000
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
literalt
Definition: literal.h:24
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
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:636
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
arrayst::update_index_map
void update_index_map(bool update_all)
Definition: arrays.cpp:376
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
exprt::operands
operandst & operands()
Definition: expr.h:78
arrayst::lazy_typet::ARRAY_ACKERMANN
@ ARRAY_ACKERMANN
arrayst::arrays
union_find< exprt > arrays
Definition: arrays.h:64
index_exprt
Array index operator.
Definition: std_expr.h:1595
arrayst::lazy_arrays
bool lazy_arrays
Definition: arrays.h:95
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:235
std_expr.h
with_exprt::where
exprt & where()
Definition: std_expr.h:3542
arrayst::add_array_constraints_equality
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition: arrays.cpp:410
propt::lcnf
void lcnf(literalt l0, literalt l1)
Definition: prop.h:55
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.h:152
arrayst::arrayst
arrayst(const namespacet &_ns, propt &_prop)
Definition: arrays.cpp:24
arrayst::add_array_constraints_if
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition: arrays.cpp:660