24 #include <unordered_set>
30 bool _get_array_constraints)
33 log(_message_handler),
34 message_handler(_message_handler)
60 "record_array_equality got equality without matching types",
64 op0.
type().
id() == ID_array,
65 "record_array_equality parameter should be array-typed");
90 if(expr.
id()!=ID_index)
92 if(expr.
id() == ID_array_comprehension)
114 if(array_op_type.
id()==ID_array)
136 array_type == with_expr.
old().
type(),
137 "collect_arrays got 'with' without matching types",
144 for(std::size_t i = 1; i < with_expr.
operands().size(); i += 2)
150 else if(a.
id()==ID_update)
155 array_type == update_expr.
old().
type(),
156 "collect_arrays got 'update' without matching types",
168 else if(a.
id()==ID_if)
174 "collect_arrays got if without matching types",
179 "collect_arrays got if without matching types",
187 else if(a.
id()==ID_symbol)
190 else if(a.
id()==ID_nondet_symbol)
193 else if(a.
id()==ID_member)
198 struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
199 "unexpected array expression: member with '" + struct_op.id_string() +
202 else if(a.
id()==ID_constant ||
204 a.
id()==ID_string_constant)
207 else if(a.
id()==ID_array_of)
210 else if(a.
id()==ID_byte_update_little_endian ||
211 a.
id()==ID_byte_update_big_endian)
215 "byte_update should be removed before collect_arrays");
217 else if(a.
id()==ID_typecast)
223 typecast_op.type().id() == ID_array,
224 "unexpected array type cast from " + typecast_op.type().id_string());
229 else if(a.
id()==ID_index)
236 else if(a.
id() == ID_array_comprehension)
243 "unexpected array expression (collect_arrays): '" + a.
id_string() +
"'");
282 std::set<std::size_t> roots_to_process, updated_roots;
286 while(!roots_to_process.empty())
288 for(std::size_t i = 0; i <
arrays.
size(); i++)
305 roots_to_process = std::move(updated_roots);
306 updated_roots.clear();
328 std::cout <<
"arrays.size(): " <<
arrays.
size() <<
'\n';
337 std::cout <<
"index_set.size(): " << index_set.size() <<
'\n';
341 for(index_sett::const_iterator
342 i1=index_set.begin();
345 for(index_sett::const_iterator
351 if(i1->is_constant() && i2->is_constant())
362 const typet &subtype =
367 index_expr2.
index()=*i2;
369 equal_exprt values_equal(index_expr1, index_expr2);
392 INVARIANT(root_number!=i,
"is_root_number incorrect?");
397 root_index_set.insert(index_set.begin(), index_set.end());
425 for(
const auto &index : index_entry.second)
426 std::cout <<
"Index set (" << index_entry.first <<
" = "
429 <<
"): " <<
format(index) <<
'\n';
430 std::cout <<
"-----\n";
440 for(
const auto &index : index_set)
442 const typet &element_type1 =
444 index_exprt index_expr1(array_equality.
f1, index, element_type1);
446 const typet &element_type2 =
448 index_exprt index_expr2(array_equality.
f2, index, element_type2);
451 index_expr1.
type()==index_expr2.
type(),
452 "array elements should all have same type");
455 equal.
f1 = index_expr1;
456 equal.
f2 = index_expr2;
457 equal.
l = array_equality.
l;
458 equal_exprt equality_expr(index_expr1, index_expr2);
472 if(expr.
id()==ID_with)
474 else if(expr.
id()==ID_update)
476 else if(expr.
id()==ID_if)
478 else if(expr.
id()==ID_array_of)
480 else if(expr.
id() == ID_array)
482 else if(expr.
id() == ID_array_comprehension)
487 else if(expr.
id()==ID_symbol ||
488 expr.
id()==ID_nondet_symbol ||
489 expr.
id()==ID_constant ||
490 expr.
id()==
"zero_string" ||
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)
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::size_t i =
721 if(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 &expr)
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.
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.
const typet & subtype() const
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.
#define forall_operands(it, expr)
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)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#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.