51 std::cout << equality.
pretty() <<
'\n';
52 throw "record_array_equality got equality without matching types";
72 for(std::size_t i=0; i<
arrays.size(); i++)
80 if(expr.
id()!=ID_index)
91 if(array_op_type.id()==ID_array)
116 std::cout << a.
pretty() <<
'\n';
117 throw "collect_arrays got 'with' without matching types";
127 else if(a.
id()==ID_update)
134 std::cout << a.
pretty() <<
'\n';
135 throw "collect_arrays got 'update' without matching types";
147 else if(a.
id()==ID_if)
154 std::cout << a.
pretty() <<
'\n';
155 throw "collect_arrays got if without matching types";
161 std::cout << a.
pretty() <<
'\n';
162 throw "collect_arrays got if without matching types";
170 else if(a.
id()==ID_symbol)
173 else if(a.
id()==ID_nondet_symbol)
176 else if(a.
id()==ID_member)
180 "unexpected array expression: member with `"+a.
op0().
id_string()+
"'";
182 else if(a.
id()==ID_constant ||
184 a.
id()==ID_string_constant)
187 else if(a.
id()==ID_array_of)
190 else if(a.
id()==ID_byte_update_little_endian ||
191 a.
id()==ID_byte_update_big_endian)
195 else if(a.
id()==ID_typecast)
208 else if(a.
id()==ID_index)
215 throw "unexpected array expression (collect_arrays): `"+a.
id_string()+
"'";
253 for(std::size_t i=0; i<
arrays.size(); i++)
284 std::cout <<
"arrays.size(): " <<
arrays.size() <<
'\n';
288 for(std::size_t i=0; i<
arrays.size(); i++)
293 std::cout <<
"index_set.size(): " << index_set.size() <<
'\n';
297 for(index_sett::const_iterator
298 i1=index_set.begin();
301 for(index_sett::const_iterator
302 i2=index_set.begin();
307 if(i1->is_constant() && i2->is_constant())
313 if(indices_equal.
op0().
type()!=
317 make_typecast(indices_equal.
op0().
type());
328 index_expr2.
index()=*i2;
330 equal_exprt values_equal(index_expr1, index_expr2);
337 #if 0 // old code for adding, not significantly faster 352 assert(root_number!=i);
357 root_index_set.insert(index_set.begin(), index_set.end());
371 for(std::size_t i=0; i<
arrays.size(); i++)
379 update_indices.clear();
385 for(
const auto &index : index_entry.second)
386 std::cout <<
"Index set (" << index_entry.first <<
" = " 392 std::cout <<
"-----\n";
402 for(
const auto &index : index_set)
410 assert(index_expr1.
type()==index_expr2.
type());
413 equal.
f1 = index_expr1;
414 equal.f2 = index_expr2;
415 equal.l = array_equality.
l;
416 equal_exprt equality_expr(index_expr1, index_expr2);
429 if(expr.
id()==ID_with)
431 else if(expr.
id()==ID_update)
433 else if(expr.
id()==ID_if)
435 else if(expr.
id()==ID_array_of)
437 else if(expr.
id()==ID_symbol ||
438 expr.
id()==ID_nondet_symbol ||
439 expr.
id()==ID_constant ||
440 expr.
id()==
"zero_string" ||
441 expr.
id()==ID_array ||
442 expr.
id()==ID_string_constant)
445 else if(expr.
id()==ID_member &&
449 else if(expr.
id()==ID_byte_update_little_endian ||
450 expr.
id()==ID_byte_update_big_endian)
454 else if(expr.
id()==ID_typecast)
460 for(
const auto &index : index_set)
466 assert(index_expr1.
type()==index_expr2.type());
474 else if(expr.
id()==ID_index)
479 "unexpected array expression (add_array_constraints): `"+
496 if(index_expr.type()!=value.
type())
498 std::cout << expr.
pretty() <<
'\n';
510 for(
auto other_index : index_set)
512 if(other_index!=index)
516 if(other_index.type()!=index.
type())
517 other_index.make_typecast(index.
type());
524 index_exprt index_expr1(expr, other_index, subtype);
527 equal_exprt equality_expr(index_expr1, index_expr2);
534 #if 0 // old code for adding, not significantly faster 540 bv.push_back(equality_lit);
541 bv.push_back(guard_lit);
558 const exprt &index=expr.where();
564 if(index_expr.type()!=value.
type())
566 std::cout << expr.
pretty() <<
'\n';
576 for(
auto other_index : index_set)
578 if(other_index!=index)
582 if(other_index.type()!=index.
type())
583 other_index.make_typecast(index.
type());
590 index_exprt index_expr1(expr, other_index, subtype);
593 equal_exprt equality_expr(index_expr1, index_expr2);
600 bv.push_back(equality_lit);
601 bv.push_back(guard_lit);
617 for(
const auto &index : index_set)
644 for(
const auto &index : index_set)
656 #if 0 // old code for adding, not significantly faster 662 for(
const auto &index : index_set)
675 #if 0 // old code for adding, not significantly faster
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
The type of an expression.
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
const typet & follow(const typet &src) const
void collect_arrays(const exprt &a)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
union_find< exprt > arrays
virtual literalt convert(const exprt &expr) override
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
size_type find_number(typename numbering< T >::const_iterator it) const
void lcnf(literalt l0, literalt l1)
void add_array_constraints()
Operator to update elements in structs and arrays.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
std::set< exprt > index_sett
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
The trinary if-then-else operator.
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
void l_set_to_true(literalt a)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
arrayst(const namespacet &_ns, propt &_prop)
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
size_type number(const T &a)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Theory of Arrays with Extensionality.
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
void update_index_map(bool update_all)
API to expression classes.
#define forall_operands(it, expr)
array constructor from single element
literalt record_array_equality(const equal_exprt &expr)
std::set< std::size_t > update_indices
array_equalitiest array_equalities
virtual literalt equality(const exprt &e1, const exprt &e2)
literalt const_literal(bool value)
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
void record_array_index(const index_exprt &expr)
Base class for all expressions.
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
const exprt & struct_op() const
std::list< lazy_constraintt > lazy_array_constraints
void set_to_true(const exprt &expr)
Operator to update elements in structs and arrays.
virtual bool is_unbounded_array(const typet &type) const =0
const std::string & id_string() const
bool make_union(const T &a, const T &b)
const typet & subtype() const
void add_array_Ackermann_constraints()
std::vector< literalt > bvt
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
std::map< exprt, bool > expr_map
bool is_root_number(size_type a) const