Go to the documentation of this file.
54 "record_array_equality got equality without matching types");
59 "record_array_equality parameter should be array-typed");
84 if(expr.
id()!=ID_index)
95 if(array_op_type.
id()==ID_array)
121 DATA_INVARIANT(
false,
"collect_arrays got 'with' without matching types");
131 else if(a.
id()==ID_update)
141 "collect_arrays got 'update' without matching types");
153 else if(a.
id()==ID_if)
161 DATA_INVARIANT(
false,
"collect_arrays got if without matching types");
168 DATA_INVARIANT(
false,
"collect_arrays got if without matching types");
176 else if(a.
id()==ID_symbol)
179 else if(a.
id()==ID_nondet_symbol)
182 else if(a.
id()==ID_member)
186 (
"unexpected array expression: member with `"+
189 else if(a.
id()==ID_constant ||
191 a.
id()==ID_string_constant)
194 else if(a.
id()==ID_array_of)
197 else if(a.
id()==ID_byte_update_little_endian ||
198 a.
id()==ID_byte_update_big_endian)
202 "byte_update should be removed before collect_arrays");
204 else if(a.
id()==ID_typecast)
209 "typecast must have one operand");
213 (
"unexpected array type cast from "+
219 else if(a.
id()==ID_index)
229 (
"unexpected array expression (collect_arrays): `"+
300 std::cout <<
"arrays.size(): " <<
arrays.
size() <<
'\n';
309 std::cout <<
"index_set.size(): " << index_set.size() <<
'\n';
313 for(index_sett::const_iterator
314 i1=index_set.begin();
317 for(index_sett::const_iterator
323 if(i1->is_constant() && i2->is_constant())
329 if(indices_equal.
op0().
type()!=
333 make_typecast(indices_equal.
op0().
type());
344 index_expr2.
index()=*i2;
346 equal_exprt values_equal(index_expr1, index_expr2);
353 #if 0 // old code for adding, not significantly faster
368 INVARIANT(root_number!=i,
"is_root_number incorrect?");
373 root_index_set.insert(index_set.begin(), index_set.end());
401 for(
const auto &index : index_entry.second)
402 std::cout <<
"Index set (" << index_entry.first <<
" = "
405 <<
"): " <<
format(index) <<
'\n';
406 std::cout <<
"-----\n";
416 for(
const auto &index : index_set)
425 index_expr1.
type()==index_expr2.
type(),
426 "array elements should all have same type");
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);
445 if(expr.
id()==ID_with)
447 else if(expr.
id()==ID_update)
449 else if(expr.
id()==ID_if)
451 else if(expr.
id()==ID_array_of)
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)
461 else if(expr.
id()==ID_member &&
465 else if(expr.
id()==ID_byte_update_little_endian ||
466 expr.
id()==ID_byte_update_big_endian)
468 INVARIANT(
false,
"byte_update should be removed before arrayst");
470 else if(expr.
id()==ID_typecast)
475 "typecast should have one operand");
478 for(
const auto &index : index_set)
485 index_expr1.
type()==index_expr2.
type(),
486 "array elements should all have same type");
494 else if(expr.
id()==ID_index)
501 (
"unexpected array expression (add_array_constraints): `"+
524 "with-expression operand should match array element type");
535 for(
auto other_index : index_set)
537 if(other_index!=index)
541 if(other_index.type()!=index.
type())
542 other_index.make_typecast(index.
type());
549 index_exprt index_expr1(expr, other_index, subtype);
552 equal_exprt equality_expr(index_expr1, index_expr2);
559 #if 0 // old code for adding, not significantly faster
565 bv.push_back(equality_lit);
566 bv.push_back(guard_lit);
583 const exprt &index=expr.where();
584 const exprt &value=expr.new_value();
594 "update operand should match array element type");
603 for(
auto other_index : index_set)
605 if(other_index!=index)
609 if(other_index.type()!=index.
type())
610 other_index.make_typecast(index.
type());
617 index_exprt index_expr1(expr, other_index, subtype);
618 index_exprt index_expr2(expr.op0(), other_index, subtype);
620 equal_exprt equality_expr(index_expr1, index_expr2);
627 bv.push_back(equality_lit);
628 bv.push_back(guard_lit);
644 for(
const auto &index : index_set)
651 "array_of operand type should match array element type");
673 for(
const auto &index : index_set)
685 #if 0 // old code for adding, not significantly faster
691 for(
const auto &index : index_set)
704 #if 0 // old code for adding, not significantly faster
Operator to update elements in structs and arrays.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const char * c_str() const
const typet & subtype() const
literalt record_array_equality(const equal_exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
The type of an expression, extends irept.
std::vector< literalt > bvt
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
size_type find_number(typename numbering< T >::const_iterator it) const
bool is_root_number(size_type a) const
The trinary if-then-else operator.
void collect_arrays(const exprt &a)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Base class for all expressions.
void set_to_true(const exprt &expr)
void l_set_to_true(literalt a)
std::set< std::size_t > update_indices
size_type number(const T &a)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
void add_array_constraints()
std::list< lazy_constraintt > lazy_array_constraints
#define forall_operands(it, expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Array constructor from single element.
array_equalitiest array_equalities
const std::string & id_string() const
literalt const_literal(bool value)
virtual bool is_unbounded_array(const typet &type) const =0
std::set< exprt > index_sett
std::map< exprt, bool > expr_map
const irep_idt & id() const
void record_array_index(const index_exprt &expr)
void add_array_Ackermann_constraints()
literalt convert(const exprt &expr) override
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Operator to update elements in structs and arrays.
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
bool make_union(const T &a, const T &b)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
void update_index_map(bool update_all)
union_find< exprt > arrays
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
void lcnf(literalt l0, literalt l1)
virtual literalt equality(const exprt &e1, const exprt &e2)
arrayst(const namespacet &_ns, propt &_prop)
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)