12 #ifndef CPROVER_SOLVERS_FLATTENING_ARRAYS_H 13 #define CPROVER_SOLVERS_FLATTENING_ARRAYS_H 128 #endif // CPROVER_SOLVERS_FLATTENING_ARRAYS_H
The type of an expression, extends irept.
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
virtual void post_process_arrays()
void collect_arrays(const exprt &a)
union_find< exprt > arrays
void post_process() override
lazy_constraintt(lazy_typet _type, const exprt &_lazy)
void add_array_constraints()
Operator to update elements in structs and arrays.
std::set< exprt > index_sett
The trinary if-then-else operator.
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
arrayst(const namespacet &_ns, propt &_prop)
void update_index_map(bool update_all)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::map< std::size_t, index_sett > index_mapt
Array constructor from single element.
literalt record_array_equality(const equal_exprt &expr)
void post_process() override
std::set< std::size_t > update_indices
array_equalitiest array_equalities
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
void record_array_index(const index_exprt &expr)
Base class for all expressions.
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
std::list< lazy_constraintt > lazy_array_constraints
Operator to update elements in structs and arrays.
virtual bool is_unbounded_array(const typet &type) const =0
std::list< array_equalityt > array_equalitiest
void add_array_Ackermann_constraints()
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
std::map< exprt, bool > expr_map