Go to the documentation of this file.
24 #include <unordered_set>
30 :
equalityt(_prop, message_handler), ns(_ns)
54 "record_array_equality got equality without matching types",
58 op0.
type().
id() == ID_array,
59 "record_array_equality parameter should be array-typed");
84 if(expr.
id()!=ID_index)
86 if(expr.
id() == ID_array_comprehension)
108 if(array_op_type.
id()==ID_array)
130 array_type == with_expr.
old().
type(),
131 "collect_arrays got 'with' without matching types",
138 for(std::size_t i = 1; i < with_expr.
operands().size(); i += 2)
144 else if(a.
id()==ID_update)
149 array_type == update_expr.
old().
type(),
150 "collect_arrays got 'update' without matching types",
162 else if(a.
id()==ID_if)
168 "collect_arrays got if without matching types",
173 "collect_arrays got if without matching types",
181 else if(a.
id()==ID_symbol)
184 else if(a.
id()==ID_nondet_symbol)
187 else if(a.
id()==ID_member)
192 struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
193 "unexpected array expression: member with '" + struct_op.id_string() +
196 else if(a.
id()==ID_constant ||
198 a.
id()==ID_string_constant)
201 else if(a.
id()==ID_array_of)
204 else if(a.
id()==ID_byte_update_little_endian ||
205 a.
id()==ID_byte_update_big_endian)
209 "byte_update should be removed before collect_arrays");
211 else if(a.
id()==ID_typecast)
217 typecast_op.type().id() == ID_array,
218 "unexpected array type cast from " + typecast_op.type().id_string());
223 else if(a.
id()==ID_index)
230 else if(a.
id() == ID_array_comprehension)
237 "unexpected array expression (collect_arrays): '" + a.
id_string() +
"'");
276 std::set<std::size_t> roots_to_process, updated_roots;
280 while(!roots_to_process.empty())
282 for(std::size_t i = 0; i <
arrays.
size(); i++)
299 roots_to_process = std::move(updated_roots);
300 updated_roots.clear();
322 std::cout <<
"arrays.size(): " <<
arrays.
size() <<
'\n';
331 std::cout <<
"index_set.size(): " << index_set.size() <<
'\n';
335 for(index_sett::const_iterator
336 i1=index_set.begin();
339 for(index_sett::const_iterator
345 if(i1->is_constant() && i2->is_constant())
360 index_expr2.
index()=*i2;
362 equal_exprt values_equal(index_expr1, index_expr2);
369 #if 0 // old code for adding, not significantly faster
384 INVARIANT(root_number!=i,
"is_root_number incorrect?");
389 root_index_set.insert(index_set.begin(), index_set.end());
417 for(
const auto &index : index_entry.second)
418 std::cout <<
"Index set (" << index_entry.first <<
" = "
421 <<
"): " <<
format(index) <<
'\n';
422 std::cout <<
"-----\n";
432 for(
const auto &index : index_set)
441 index_expr1.
type()==index_expr2.
type(),
442 "array elements should all have same type");
445 equal.
f1 = index_expr1;
446 equal.
f2 = index_expr2;
447 equal.
l = array_equality.
l;
448 equal_exprt equality_expr(index_expr1, index_expr2);
461 if(expr.
id()==ID_with)
463 else if(expr.
id()==ID_update)
465 else if(expr.
id()==ID_if)
467 else if(expr.
id()==ID_array_of)
469 else if(expr.
id() == ID_array)
471 else if(expr.
id() == ID_array_comprehension)
476 else if(expr.
id()==ID_symbol ||
477 expr.
id()==ID_nondet_symbol ||
478 expr.
id()==ID_constant ||
479 expr.
id()==
"zero_string" ||
480 expr.
id()==ID_string_constant)
484 expr.
id() == ID_member &&
489 else if(expr.
id()==ID_byte_update_little_endian ||
490 expr.
id()==ID_byte_update_big_endian)
492 INVARIANT(
false,
"byte_update should be removed before arrayst");
494 else if(expr.
id()==ID_typecast)
500 for(
const auto &index : index_set)
504 index_exprt index_expr2(expr_typecast_op, index, subtype);
507 index_expr1.
type()==index_expr2.
type(),
508 "array elements should all have same type");
516 else if(expr.
id()==ID_index)
523 "unexpected array expression (add_array_constraints): '" +
534 std::unordered_set<exprt, irep_hash> updated_indices;
537 for(std::size_t i = 1; i + 1 < operands.size(); i += 2)
539 const exprt &index = operands[i];
540 const exprt &value = operands[i + 1];
546 "with-expression operand should match array element type",
553 updated_indices.insert(index);
559 for(
auto other_index : index_set)
561 if(updated_indices.find(other_index) == updated_indices.end())
565 disjuncts.reserve(updated_indices.size());
566 for(
const auto &index : updated_indices)
577 index_exprt index_expr1(expr, other_index, subtype);
580 equal_exprt equality_expr(index_expr1, index_expr2);
587 #if 0 // old code for adding, not significantly faster
593 bv.push_back(equality_lit);
594 bv.push_back(guard_lit);
611 const exprt &index=expr.where();
612 const exprt &value=expr.new_value();
619 "update operand should match array element type",
628 for(
auto other_index : index_set)
630 if(other_index!=index)
641 index_exprt index_expr1(expr, other_index, subtype);
642 index_exprt index_expr2(expr.op0(), other_index, subtype);
644 equal_exprt equality_expr(index_expr1, index_expr2);
651 bv.push_back(equality_lit);
652 bv.push_back(guard_lit);
668 for(
const auto &index : index_set)
675 "array_of operand type should match array element type");
691 for(
const auto &index : index_set)
694 const index_exprt index_expr{expr, index, subtype};
696 if(index.is_constant())
701 const std::size_t i =
704 if(i >= operands.size())
707 const exprt v = operands[i];
709 index_expr.type() == v.
type(),
710 "array operand type should match array element type");
725 std::vector<std::pair<std::size_t, std::size_t>> ranges;
727 for(std::size_t i = 0; i < operands.size(); ++i)
729 if(ranges.empty() || operands[i] != operands[ranges.back().first])
730 ranges.emplace_back(i, i);
732 ranges.back().second = i;
735 for(
const auto &range : ranges)
737 exprt index_constraint;
739 if(range.first == range.second)
750 index, ID_le,
from_integer(range.second, index.type())}};
771 for(
const auto &index : index_set)
798 for(
const auto &index : index_set)
810 #if 0 // old code for adding, not significantly faster
816 for(
const auto &index : index_set)
829 #if 0 // old code for adding, not significantly faster
Operator to update elements in structs and arrays.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
static exprt conditional_cast(const exprt &expr, const typet &type)
const typet & subtype() const
std::unordered_set< irep_idt > array_comprehension_args
literalt record_array_equality(const equal_exprt &expr)
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
The type of an expression, extends irept.
std::vector< literalt > bvt
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)
For a Boolean expression expr, add the constraint 'expr'.
const array_typet & type() const
const symbol_exprt & arg() const
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.
const array_typet & type() const
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
void add_array_constraints()
std::list< lazy_constraintt > lazy_array_constraints
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define forall_operands(it, expr)
const exprt & struct_op() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
const irep_idt & get_identifier() const
auto lazy(funt fun) -> lazyt< decltype(fun())>
Delay the computation of fun to the next time the force method is called.
Array constructor from single element.
array_equalitiest array_equalities
const std::string & id_string() const
const exprt & body() 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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
std::vector< exprt > operandst
void record_array_index(const index_exprt &expr)
void add_array_Ackermann_constraints()
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
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)
Theory of Arrays with Extensionality.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
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
Expression to define a mapping from an argument (index) to elements.
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
API to expression classes.
Array constructor from list of elements.
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler)
void lcnf(literalt l0, literalt l1)
virtual literalt equality(const exprt &e1, const exprt &e2)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)