Go to the documentation of this file.
27 #include <unordered_set>
33 bool _get_array_constraints)
36 log(_message_handler),
37 message_handler(_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");
93 if(expr.
id()!=ID_index)
95 if(expr.
id() == ID_array_comprehension)
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.
id()==ID_constant ||
207 a.
id()==ID_string_constant)
210 else if(a.
id()==ID_array_of)
213 else if(a.
id()==ID_byte_update_little_endian ||
214 a.
id()==ID_byte_update_big_endian)
218 "byte_update should be removed before collect_arrays");
220 else if(a.
id()==ID_typecast)
226 typecast_op.type().id() == ID_array,
227 "unexpected array type cast from " + typecast_op.type().id_string());
232 else if(a.
id()==ID_index)
239 else if(a.
id() == ID_array_comprehension)
246 "unexpected array expression (collect_arrays): '" + a.
id_string() +
"'");
285 std::set<std::size_t> roots_to_process, updated_roots;
289 while(!roots_to_process.empty())
291 for(std::size_t i = 0; i <
arrays.
size(); i++)
308 roots_to_process = std::move(updated_roots);
309 updated_roots.clear();
331 std::cout <<
"arrays.size(): " <<
arrays.
size() <<
'\n';
340 std::cout <<
"index_set.size(): " << index_set.size() <<
'\n';
344 for(index_sett::const_iterator
345 i1=index_set.begin();
348 for(index_sett::const_iterator
354 if(i1->is_constant() && i2->is_constant())
369 index_expr2.
index()=*i2;
371 equal_exprt values_equal(index_expr1, index_expr2);
379 #if 0 // old code for adding, not significantly faster
394 INVARIANT(root_number!=i,
"is_root_number incorrect?");
399 root_index_set.insert(index_set.begin(), index_set.end());
427 for(
const auto &index : index_entry.second)
428 std::cout <<
"Index set (" << index_entry.first <<
" = "
431 <<
"): " <<
format(index) <<
'\n';
432 std::cout <<
"-----\n";
442 for(
const auto &index : index_set)
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)
515 index_exprt index_expr2(expr_typecast_op, index, subtype);
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];
558 "with-expression operand should match array element type",
566 updated_indices.insert(index);
572 for(
auto other_index : index_set)
574 if(updated_indices.find(other_index) == updated_indices.end())
578 disjuncts.reserve(updated_indices.size());
579 for(
const auto &index : updated_indices)
590 index_exprt index_expr1(expr, other_index, subtype);
593 equal_exprt equality_expr(index_expr1, index_expr2);
602 #if 0 // old code for adding, not significantly faster
608 bv.push_back(equality_lit);
609 bv.push_back(guard_lit);
626 const exprt &index=expr.where();
627 const exprt &value=expr.new_value();
634 "update operand should match array element type",
643 for(
auto other_index : index_set)
645 if(other_index!=index)
656 index_exprt index_expr1(expr, other_index, subtype);
657 index_exprt index_expr2(expr.op0(), other_index, subtype);
659 equal_exprt equality_expr(index_expr1, index_expr2);
666 bv.push_back(equality_lit);
667 bv.push_back(guard_lit);
683 for(
const auto &index : index_set)
690 "array_of operand type should match array element type");
707 for(
const auto &index : index_set)
710 const index_exprt index_expr{expr, index, subtype};
712 if(index.is_constant())
717 const std::size_t i =
720 if(i >= operands.size())
723 const exprt v = operands[i];
725 index_expr.type() == v.
type(),
726 "array operand type should match array element type");
742 std::vector<std::pair<std::size_t, std::size_t>> ranges;
744 for(std::size_t i = 0; i < operands.size(); ++i)
746 if(ranges.empty() || operands[i] != operands[ranges.back().first])
747 ranges.emplace_back(i, i);
749 ranges.back().second = i;
752 for(
const auto &range : ranges)
754 exprt index_constraint;
756 if(range.first == range.second)
767 index, ID_le,
from_integer(range.second, index.type())}};
789 for(
const auto &index : index_set)
818 for(
const auto &index : index_set)
831 #if 0 // old code for adding, not significantly faster
837 for(
const auto &index : index_set)
851 #if 0 // old code for adding, not significantly faster
862 return "arrayAckermann";
870 return "arrayTypecast";
872 return "arrayConstant";
874 return "arrayComprehension";
876 return "arrayEquality";
888 size_t num_constraints = 0;
894 json_array_theory[contraint_type_string] =
897 num_constraints += it->second;
901 json_result[
"numOfConstraints"] =
Operator to update elements in structs and arrays.
#define UNREACHABLE
This should be used to mark dead code.
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
mstreamt & status() 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.
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::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::set< std::size_t > update_indices
json_objectt & make_object()
array_constraint_countt array_constraint_count
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
size_type number(const T &a)
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...
size_type find_number(const_iterator it) const
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
bool make_union(const T &a, const T &b)
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.
bool is_root_number(size_type a) const
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 display_array_constraint_count()
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
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, irep_hash > arrays
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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)
bool get_array_constraints
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, bool get_array_constraints=false)
void lcnf(literalt l0, literalt l1)
virtual literalt equality(const exprt &e1, const exprt &e2)
std::string enum_to_string(constraint_typet)
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)