26 #include <unordered_set>
32 bool _get_array_constraints)
35 log(_message_handler),
36 message_handler(_message_handler)
62 "record_array_equality got equality without matching types",
66 op0.
type().
id() == ID_array,
67 "record_array_equality parameter should be array-typed");
92 if(expr.
id()!=ID_index)
94 if(expr.
id() == ID_array_comprehension)
98 for(
const auto &op : expr.
operands())
117 if(array_op_type.
id()==ID_array)
139 array_type == with_expr.
old().
type(),
140 "collect_arrays got 'with' without matching types",
147 for(std::size_t i = 1; i < with_expr.
operands().size(); i += 2)
153 else if(a.
id()==ID_update)
158 array_type == update_expr.
old().
type(),
159 "collect_arrays got 'update' without matching types",
171 else if(a.
id()==ID_if)
177 "collect_arrays got if without matching types",
182 "collect_arrays got if without matching types",
190 else if(a.
id()==ID_symbol)
193 else if(a.
id()==ID_nondet_symbol)
196 else if(a.
id()==ID_member)
201 struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
202 "unexpected array expression: member with '" + struct_op.id_string() +
205 else if(a.
is_constant() || a.
id() == ID_array || a.
id() == ID_string_constant)
208 else if(a.
id()==ID_array_of)
211 else if(a.
id()==ID_byte_update_little_endian ||
212 a.
id()==ID_byte_update_big_endian)
216 "byte_update should be removed before collect_arrays");
218 else if(a.
id()==ID_typecast)
224 typecast_op.type().id() == ID_array,
225 "unexpected array type cast from " + typecast_op.type().id_string());
230 else if(a.
id()==ID_index)
237 else if(a.
id() == ID_array_comprehension)
244 "unexpected array expression (collect_arrays): '" + a.
id_string() +
"'");
283 std::set<std::size_t> roots_to_process, updated_roots;
287 while(!roots_to_process.empty())
289 for(std::size_t i = 0; i <
arrays.
size(); i++)
306 roots_to_process = std::move(updated_roots);
307 updated_roots.clear();
329 std::cout <<
"arrays.size(): " <<
arrays.
size() <<
'\n';
338 std::cout <<
"index_set.size(): " << index_set.size() <<
'\n';
342 for(index_sett::const_iterator
343 i1=index_set.begin();
346 for(index_sett::const_iterator
352 if(i1->is_constant() && i2->is_constant())
363 const typet &subtype =
368 index_expr2.
index()=*i2;
370 equal_exprt values_equal(index_expr1, index_expr2);
393 INVARIANT(root_number!=i,
"is_root_number incorrect?");
398 root_index_set.insert(index_set.begin(), index_set.end());
426 for(
const auto &index : index_entry.second)
427 std::cout <<
"Index set (" << index_entry.first <<
" = "
430 <<
"): " <<
format(index) <<
'\n';
431 std::cout <<
"-----\n";
441 for(
const auto &index : index_set)
443 const typet &element_type1 =
445 index_exprt index_expr1(array_equality.
f1, index, element_type1);
447 const typet &element_type2 =
449 index_exprt index_expr2(array_equality.
f2, index, element_type2);
452 index_expr1.
type()==index_expr2.
type(),
453 "array elements should all have same type");
456 equal.
f1 = index_expr1;
457 equal.
f2 = index_expr2;
458 equal.
l = array_equality.
l;
459 equal_exprt equality_expr(index_expr1, index_expr2);
473 if(expr.
id()==ID_with)
475 else if(expr.
id()==ID_update)
477 else if(expr.
id()==ID_if)
479 else if(expr.
id()==ID_array_of)
481 else if(expr.
id() == ID_array)
483 else if(expr.
id() == ID_array_comprehension)
489 expr.
id() == ID_symbol || expr.
id() == ID_nondet_symbol ||
491 expr.
id() == ID_string_constant)
495 expr.
id() == ID_member &&
500 else if(expr.
id()==ID_byte_update_little_endian ||
501 expr.
id()==ID_byte_update_big_endian)
503 INVARIANT(
false,
"byte_update should be removed before arrayst");
505 else if(expr.
id()==ID_typecast)
511 for(
const auto &index : index_set)
514 index_exprt index_expr1(expr, index, element_type);
515 index_exprt index_expr2(expr_typecast_op, index, element_type);
518 index_expr1.
type()==index_expr2.
type(),
519 "array elements should all have same type");
528 else if(expr.
id()==ID_index)
535 "unexpected array expression (add_array_constraints): '" +
546 std::unordered_set<exprt, irep_hash> updated_indices;
549 for(std::size_t i = 1; i + 1 < operands.size(); i += 2)
551 const exprt &index = operands[i];
552 const exprt &value = operands[i + 1];
559 "with-expression operand should match array element type",
567 updated_indices.insert(index);
573 for(
auto other_index : index_set)
575 if(updated_indices.find(other_index) == updated_indices.end())
579 disjuncts.reserve(updated_indices.size());
580 for(
const auto &index : updated_indices)
591 index_exprt index_expr1(expr, other_index, element_type);
594 equal_exprt equality_expr(index_expr1, index_expr2);
609 bv.push_back(equality_lit);
610 bv.push_back(guard_lit);
627 const exprt &index=expr.where();
628 const exprt &value=expr.new_value();
635 "update operand should match array element type",
644 for(
auto other_index : index_set)
646 if(other_index!=index)
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);
660 equal_exprt equality_expr(index_expr1, index_expr2);
667 bv.push_back(equality_lit);
668 bv.push_back(guard_lit);
684 for(
const auto &index : index_set)
691 "array_of operand type should match array element type");
708 for(
const auto &index : index_set)
711 const index_exprt index_expr{expr, index, element_type};
713 if(index.is_constant())
718 const std::optional<std::size_t> i =
721 if(!i.has_value() || *i >= operands.size())
724 const exprt v = operands[*i];
726 index_expr.type() == v.
type(),
727 "array operand type should match array element type");
743 std::vector<std::pair<std::size_t, std::size_t>> ranges;
745 for(std::size_t i = 0; i < operands.size(); ++i)
747 if(ranges.empty() || operands[i] != operands[ranges.back().first])
748 ranges.emplace_back(i, i);
750 ranges.back().second = i;
753 for(
const auto &range : ranges)
755 exprt index_constraint;
757 if(range.first == range.second)
768 index, ID_le,
from_integer(range.second, index.type())}};
790 for(
const auto &index : index_set)
819 for(
const auto &index : index_set)
822 index_exprt index_expr1(expr, index, element_type);
838 for(
const auto &index : index_set)
841 index_exprt index_expr1(expr, index, element_type);
863 return "arrayAckermann";
871 return "arrayTypecast";
873 return "arrayConstant";
875 return "arrayComprehension";
877 return "arrayEquality";
889 size_t num_constraints = 0;
895 json_array_theory[contraint_type_string] =
898 num_constraints += it->second;
902 json_result[
"numOfConstraints"] =
Theory of Arrays with Extensionality.
Expression to define a mapping from an argument (index) to elements.
const exprt & body() const
const symbol_exprt & arg() const
Array constructor from list of elements.
const array_typet & type() const
Array constructor from single element.
const array_typet & type() const
const typet & element_type() const
The type of the elements of the array.
std::list< lazy_constraintt > lazy_array_constraints
std::unordered_set< irep_idt > array_comprehension_args
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
std::set< std::size_t > update_indices
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
void add_array_Ackermann_constraints()
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
void collect_arrays(const exprt &a)
union_find< exprt, irep_hash > arrays
literalt record_array_equality(const equal_exprt &expr)
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
std::map< exprt, bool > expr_map
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
std::string enum_to_string(constraint_typet)
bool get_array_constraints
void add_array_constraints()
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
virtual bool is_unbounded_array(const typet &type) const =0
void record_array_index(const index_exprt &expr)
array_equalitiest array_equalities
std::set< exprt > index_sett
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
array_constraint_countt array_constraint_count
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
void display_array_constraint_count()
void update_index_map(bool update_all)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
virtual literalt equality(const exprt &e1, const exprt &e2)
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
The trinary if-then-else operator.
const std::string & id_string() const
const irep_idt & id() const
json_objectt & make_object()
const exprt & struct_op() const
mstreamt & status() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
void l_set_to_true(literalt a)
void lcnf(literalt l0, literalt l1)
const irep_idt & get_identifier() const
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
size_type number(const T &a)
bool make_union(const T &a, const T &b)
size_type find_number(const_iterator it) const
bool is_root_number(size_type a) const
Operator to update elements in structs and arrays.
Operator to update elements in structs and arrays.
auto lazy(funt fun) -> lazyt< decltype(fun())>
Delay the computation of fun to the next time the force method is called.
std::vector< literalt > bvt
literalt const_literal(bool value)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.