27#include <unordered_set>
33 bool _get_array_constraints)
36 log(_message_handler),
63 "record_array_equality got equality without matching types",
67 op0.
type().
id() == ID_array,
68 "record_array_equality parameter should be array-typed");
76 arrays.make_union(op0, op1);
85 for(std::size_t i=0; i<
arrays.size(); i++)
93 if(expr.
id()!=ID_index)
95 if(expr.
id() == ID_array_comprehension)
99 for(
const auto &op : expr.
operands())
118 if(array_op_type.
id()==ID_array)
140 array_type == with_expr.
old().
type(),
141 "collect_arrays got 'with' without matching types",
151 else if(a.
id()==ID_update)
156 array_type == update_expr.
old().
type(),
157 "collect_arrays got 'update' without matching types",
169 else if(a.
id()==ID_if)
175 "collect_arrays got if without matching types",
180 "collect_arrays got if without matching types",
188 else if(a.
id()==ID_symbol)
191 else if(a.
id()==ID_nondet_symbol)
194 else if(a.
id()==ID_member)
199 struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
200 "unexpected array expression: member with '" + struct_op.id_string() +
203 else if(a.
is_constant() || a.
id() == ID_array || a.
id() == ID_string_constant)
206 else if(a.
id()==ID_array_of)
209 else if(a.
id()==ID_byte_update_little_endian ||
210 a.
id()==ID_byte_update_big_endian)
214 "byte_update should be removed before collect_arrays");
216 else if(a.
id()==ID_typecast)
222 typecast_op.type().id() == ID_array,
223 "unexpected array type cast from " + typecast_op.type().id_string());
225 arrays.make_union(a, typecast_op);
228 else if(a.
id()==ID_index)
232 arrays.make_union(a, array_op);
235 else if(a.
id() == ID_array_comprehension)
240 arrays.make_union(a, let_expr->where());
247 "unexpected array expression (collect_arrays): '" + a.
id_string() +
"'");
286 std::set<std::size_t> roots_to_process, updated_roots;
287 for(std::size_t i=0; i<
arrays.size(); i++)
288 roots_to_process.insert(
arrays.find_number(i));
290 while(!roots_to_process.empty())
292 for(std::size_t i = 0; i <
arrays.size(); i++)
294 if(roots_to_process.count(
arrays.find_number(i)) == 0)
305 updated_roots.insert(
arrays.find_number(u));
309 roots_to_process = std::move(updated_roots);
310 updated_roots.clear();
332 std::cout <<
"arrays.size(): " <<
arrays.size() <<
'\n';
336 for(std::size_t i=0; i<
arrays.size(); i++)
341 std::cout <<
"index_set.size(): " << index_set.size() <<
'\n';
345 for(index_sett::const_iterator
346 i1=index_set.begin();
349 for(index_sett::const_iterator
355 if(i1->is_constant() && i2->is_constant())
366 const typet &subtype =
371 index_expr2.
index()=*i2;
373 equal_exprt values_equal(index_expr1, index_expr2);
382 prop.lcnf(!indices_equal_lit,
convert(values_equal));
392 if(
arrays.is_root_number(i))
395 std::size_t root_number=
arrays.find_number(i);
396 INVARIANT(root_number!=i,
"is_root_number incorrect?");
401 root_index_set.insert(index_set.begin(), index_set.end());
415 for(std::size_t i=0; i<
arrays.size(); i++)
429 for(
const auto &index : index_entry.second)
430 std::cout <<
"Index set (" << index_entry.first <<
" = "
431 <<
arrays.find_number(index_entry.first) <<
" = "
433 <<
"): " <<
format(index) <<
'\n';
434 std::cout <<
"-----\n";
444 for(
const auto &index : index_set)
446 const typet &element_type1 =
448 index_exprt index_expr1(array_equality.
f1, index, element_type1);
450 const typet &element_type2 =
452 index_exprt index_expr2(array_equality.
f2, index, element_type2);
455 index_expr1.
type()==index_expr2.
type(),
456 "array elements should all have same type");
459 equal.
f1 = index_expr1;
460 equal.
f2 = index_expr2;
461 equal.
l = array_equality.
l;
462 equal_exprt equality_expr(index_expr1, index_expr2);
476 if(expr.
id()==ID_with)
478 else if(expr.
id()==ID_update)
480 else if(expr.
id()==ID_if)
482 else if(expr.
id()==ID_array_of)
484 else if(expr.
id() == ID_array)
486 else if(expr.
id() == ID_array_comprehension)
492 expr.
id() == ID_symbol || expr.
id() == ID_nondet_symbol ||
494 expr.
id() == ID_string_constant)
498 expr.
id() == ID_member &&
503 else if(expr.
id()==ID_byte_update_little_endian ||
504 expr.
id()==ID_byte_update_big_endian)
506 INVARIANT(
false,
"byte_update should be removed before arrayst");
508 else if(expr.
id()==ID_typecast)
514 for(
const auto &index : index_set)
517 index_exprt index_expr1(expr, index, element_type);
518 index_exprt index_expr2(expr_typecast_op, index, element_type);
521 index_expr1.
type()==index_expr2.
type(),
522 "array elements should all have same type");
531 else if(expr.
id()==ID_index)
539 exprt where = let_expr->where();
541 for(
const auto &binding :
542 make_range(let_expr->variables()).zip(let_expr->values()))
544 replace_symbol.
insert(binding.first, binding.second);
546 replace_symbol(where);
548 for(
const auto &index : index_set)
565 "unexpected array expression (add_array_constraints): '" +
576 std::unordered_set<exprt, irep_hash> updated_indices;
583 "with-expression operand should match array element type",
591 updated_indices.insert(expr.
where());
596 for(
auto other_index : index_set)
598 if(updated_indices.find(other_index) == updated_indices.end())
602 disjuncts.reserve(updated_indices.size());
603 for(
const auto &index : updated_indices)
614 index_exprt index_expr1(expr, other_index, element_type);
617 equal_exprt equality_expr(index_expr1, index_expr2);
632 bv.push_back(equality_lit);
633 bv.push_back(guard_lit);
650 const exprt &index=expr.where();
651 const exprt &value=expr.new_value();
658 "update operand should match array element type",
667 for(
auto other_index : index_set)
669 if(other_index!=index)
679 const typet &subtype=expr.type().subtype();
680 index_exprt index_expr1(expr, other_index, subtype);
681 index_exprt index_expr2(expr.op0(), other_index, subtype);
683 equal_exprt equality_expr(index_expr1, index_expr2);
690 bv.push_back(equality_lit);
691 bv.push_back(guard_lit);
707 for(
const auto &index : index_set)
714 "array_of operand type should match array element type");
731 for(
const auto &index : index_set)
734 const index_exprt index_expr{expr, index, element_type};
736 if(index.is_constant())
741 const std::optional<std::size_t> i =
744 if(!i.has_value() || *i >= operands.size())
747 const exprt v = operands[*i];
750 "array operand type should match array element type");
766 std::vector<std::pair<std::size_t, std::size_t>> ranges;
768 for(std::size_t i = 0; i < operands.size(); ++i)
770 if(ranges.empty() || operands[i] != operands[ranges.back().first])
771 ranges.emplace_back(i, i);
773 ranges.back().second = i;
776 for(
const auto &range : ranges)
778 exprt index_constraint;
780 if(range.first == range.second)
791 index, ID_le,
from_integer(range.second, index.type())}};
813 for(
const auto &index : index_set)
842 for(
const auto &index : index_set)
845 index_exprt index_expr1(expr, index, element_type);
861 for(
const auto &index : index_set)
864 index_exprt index_expr1(expr, index, element_type);
886 return "arrayAckermann";
894 return "arrayTypecast";
896 return "arrayConstant";
898 return "arrayComprehension";
900 return "arrayEquality";
914 size_t num_constraints = 0;
920 json_array_theory[contraint_type_string] =
923 num_constraints += it->second;
927 json_result[
"numOfConstraints"] =
929 log.status() <<
",\n" << json_result;
Theory of Arrays with Extensionality.
Expression to define a mapping from an argument (index) to elements.
const symbol_exprt & arg() const
const exprt & body() 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)
message_handlert & message_handler
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'.
equalityt(propt &_prop, message_handlert &message_handler)
virtual literalt equality(const exprt &e1, const exprt &e2)
Base class for all expressions.
std::vector< exprt > operandst
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
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
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.
Replace a symbol expression by a given expression.
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Operator to update elements in structs and arrays.
Operator to update elements in structs and arrays.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
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)
ranget< iteratort > make_range(iteratort begin, iteratort end)
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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#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 array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_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 with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.