cprover
|
#include <arrays.h>
Classes | |
struct | array_equalityt |
struct | lazy_constraintt |
Public Types | |
typedef equalityt | SUB |
![]() | |
typedef std::map< irep_idt, literalt > | symbolst |
typedef std::unordered_map< exprt, literalt, irep_hash > | cachet |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
Public Member Functions | |
arrayst (const namespacet &_ns, propt &_prop) | |
void | post_process () override |
literalt | record_array_equality (const equal_exprt &expr) |
void | record_array_index (const index_exprt &expr) |
![]() | |
equalityt (const namespacet &_ns, propt &_prop) | |
virtual literalt | equality (const exprt &e1, const exprt &e2) |
void | post_process () override |
![]() | |
prop_conv_solvert (const namespacet &_ns, propt &_prop) | |
virtual | ~prop_conv_solvert () |
virtual void | set_to (const exprt &expr, bool value) override |
virtual decision_proceduret::resultt | dec_solve () override |
virtual void | print_assignment (std::ostream &out) const override |
virtual std::string | decision_procedure_text () const override |
virtual exprt | get (const exprt &expr) const override |
virtual tvt | l_get (literalt a) const override |
virtual void | set_frozen (literalt a) override |
virtual void | set_assumptions (const bvt &_assumptions) override |
virtual bool | has_set_assumptions () const override |
virtual void | set_all_frozen () override |
virtual literalt | convert (const exprt &expr) override |
virtual bool | is_in_conflict (literalt l) const override |
determine whether a variable is in the final conflict More... | |
virtual bool | has_is_in_conflict () const override |
virtual bool | literal (const exprt &expr, literalt &literal) const |
virtual void | clear_cache () |
const cachet & | get_cache () const |
const symbolst & | get_symbols () const |
![]() | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
literalt | operator() (const exprt &expr) |
virtual void | set_frozen (const bvt &) |
![]() | |
decision_proceduret (const namespacet &_ns) | |
void | set_to_true (const exprt &expr) |
void | set_to_false (const exprt &expr) |
resultt | operator() () |
virtual bool | in_core (const exprt &expr) |
Protected Types | |
enum | lazy_typet { lazy_typet::ARRAY_ACKERMANN, lazy_typet::ARRAY_WITH, lazy_typet::ARRAY_IF, lazy_typet::ARRAY_OF, lazy_typet::ARRAY_TYPECAST } |
typedef std::list< array_equalityt > | array_equalitiest |
typedef std::set< exprt > | index_sett |
typedef std::map< std::size_t, index_sett > | index_mapt |
![]() | |
typedef std::unordered_map< const exprt, unsigned, irep_hash > | elementst |
typedef std::map< std::pair< unsigned, unsigned >, literalt > | equalitiest |
typedef std::map< unsigned, exprt > | elements_revt |
typedef std::unordered_map< const typet, typestructt, irep_hash > | typemapt |
Protected Member Functions | |
virtual void | post_process_arrays () |
void | add_array_constraint (const lazy_constraintt &lazy, bool refine=true) |
adds array constraints (refine=true...lazily for the refinement loop) More... | |
void | add_array_constraints () |
void | add_array_Ackermann_constraints () |
void | add_array_constraints_equality (const index_sett &index_set, const array_equalityt &array_equality) |
void | add_array_constraints (const index_sett &index_set, const exprt &expr) |
void | add_array_constraints_if (const index_sett &index_set, const if_exprt &exprt) |
void | add_array_constraints_with (const index_sett &index_set, const with_exprt &expr) |
void | add_array_constraints_update (const index_sett &index_set, const update_exprt &expr) |
void | add_array_constraints_array_of (const index_sett &index_set, const array_of_exprt &exprt) |
void | update_index_map (bool update_all) |
void | update_index_map (std::size_t i) |
merge the indices into the root More... | |
void | collect_arrays (const exprt &a) |
void | collect_indices () |
void | collect_indices (const exprt &a) |
virtual bool | is_unbounded_array (const typet &type) const =0 |
![]() | |
virtual literalt | equality2 (const exprt &e1, const exprt &e2) |
virtual void | add_equality_constraints () |
virtual void | add_equality_constraints (const typestructt &typestruct) |
![]() | |
virtual bool | get_bool (const exprt &expr, tvt &value) const |
get a boolean value from counter example if not valid More... | |
virtual literalt | convert_rest (const exprt &expr) |
virtual literalt | convert_bool (const exprt &expr) |
virtual bool | set_equality_to_true (const equal_exprt &expr) |
virtual literalt | get_literal (const irep_idt &symbol) |
virtual void | ignoring (const exprt &expr) |
Protected Attributes | |
array_equalitiest | array_equalities |
union_find< exprt > | arrays |
index_mapt | index_map |
bool | lazy_arrays |
bool | incremental_cache |
std::list< lazy_constraintt > | lazy_array_constraints |
std::map< exprt, bool > | expr_map |
std::set< std::size_t > | update_indices |
![]() | |
typemapt | typemap |
![]() | |
bool | post_processing_done |
symbolst | symbols |
cachet | cache |
propt & | prop |
![]() | |
const namespacet & | ns |
Additional Inherited Members | |
![]() | |
bool | use_cache |
bool | equality_propagation |
bool | freeze_all |
|
protected |
|
protected |
|
protected |
typedef equalityt arrayst::SUB |
|
strongprotected |
arrayst::arrayst | ( | const namespacet & | _ns, |
propt & | _prop | ||
) |
Definition at line 24 of file arrays.cpp.
References incremental_cache, and lazy_arrays.
|
protected |
Definition at line 279 of file arrays.cpp.
References add_array_constraint(), ARRAY_ACKERMANN, arrays, const_literal(), prop_conv_solvert::convert(), union_find< T >::find_number(), namespace_baset::follow(), index_exprt::index(), index_map, propt::lcnf(), decision_proceduret::ns, exprt::op0(), exprt::op1(), prop_conv_solvert::prop, typet::subtype(), and exprt::type().
Referenced by add_array_constraints().
|
protected |
adds array constraints (refine=true...lazily for the refinement loop)
Definition at line 219 of file arrays.cpp.
References prop_conv_solvert::convert(), expr_map, incremental_cache, propt::l_set_to_true(), arrayst::lazy_constraintt::lazy, lazy_array_constraints, lazy_arrays, and prop_conv_solvert::prop.
Referenced by add_array_Ackermann_constraints(), add_array_constraints(), add_array_constraints_array_of(), add_array_constraints_if(), and add_array_constraints_with().
|
protected |
Definition at line 244 of file arrays.cpp.
References add_array_Ackermann_constraints(), add_array_constraints_equality(), array_equalities, arrays, collect_indices(), equalityt::equality(), union_find< T >::find_number(), index_map, and update_index_map().
Referenced by post_process_arrays(), and bv_refinementt::post_process_arrays().
|
protected |
Definition at line 425 of file arrays.cpp.
References add_array_constraint(), add_array_constraints_array_of(), add_array_constraints_if(), add_array_constraints_update(), add_array_constraints_with(), ARRAY_TYPECAST, namespace_baset::follow(), irept::id(), irept::id_string(), decision_proceduret::ns, exprt::op0(), exprt::operands(), member_exprt::struct_op(), to_array_of_expr(), to_if_expr(), to_member_expr(), to_update_expr(), to_with_expr(), and exprt::type().
|
protected |
Definition at line 609 of file arrays.cpp.
References add_array_constraint(), ARRAY_OF, base_type_eq(), namespace_baset::follow(), decision_proceduret::ns, exprt::op0(), and exprt::type().
Referenced by add_array_constraints().
|
protected |
Definition at line 396 of file arrays.cpp.
References prop_conv_solvert::convert(), arrayst::array_equalityt::f1, arrayst::array_equalityt::f2, namespace_baset::follow(), arrayst::array_equalityt::l, propt::lcnf(), decision_proceduret::ns, prop_conv_solvert::prop, and exprt::type().
Referenced by add_array_constraints().
|
protected |
Definition at line 631 of file arrays.cpp.
References add_array_constraint(), ARRAY_IF, if_exprt::cond(), prop_conv_solvert::convert(), if_exprt::false_case(), namespace_baset::follow(), propt::lcnf(), decision_proceduret::ns, prop_conv_solvert::prop, if_exprt::true_case(), and exprt::type().
Referenced by add_array_constraints().
|
protected |
Definition at line 550 of file arrays.cpp.
References const_literal(), prop_conv_solvert::convert(), namespace_baset::follow(), propt::lcnf(), update_exprt::new_value(), decision_proceduret::ns, exprt::op0(), irept::pretty(), prop_conv_solvert::prop, decision_proceduret::set_to_true(), and exprt::type().
Referenced by add_array_constraints().
|
protected |
Definition at line 483 of file arrays.cpp.
References add_array_constraint(), ARRAY_WITH, const_literal(), prop_conv_solvert::convert(), namespace_baset::follow(), propt::lcnf(), with_exprt::new_value(), decision_proceduret::ns, exprt::op0(), irept::pretty(), prop_conv_solvert::prop, exprt::type(), and with_exprt::where().
Referenced by add_array_constraints().
|
protected |
Definition at line 104 of file arrays.cpp.
References arrays, base_type_eq(), if_exprt::false_case(), namespace_baset::follow(), irept::id(), irept::id_string(), union_find< T >::make_union(), decision_proceduret::ns, with_exprt::old(), update_exprt::old(), exprt::op0(), exprt::operands(), irept::pretty(), record_array_index(), member_exprt::struct_op(), to_array_type(), to_if_expr(), to_member_expr(), to_update_expr(), to_with_expr(), if_exprt::true_case(), exprt::type(), and with_exprt::where().
Referenced by record_array_equality().
|
protected |
Definition at line 70 of file arrays.cpp.
References arrays.
Referenced by add_array_constraints(), collect_indices(), and bv_refinementt::post_process_arrays().
|
protected |
Definition at line 78 of file arrays.cpp.
References index_exprt::array(), collect_indices(), namespace_baset::follow(), forall_operands, irept::id(), index_exprt::index(), is_unbounded_array(), decision_proceduret::ns, record_array_index(), to_array_type(), to_index_expr(), and exprt::type().
|
protectedpure virtual |
Implemented in boolbvt.
Referenced by collect_indices().
|
inlineoverridevirtual |
Reimplemented from prop_conv_solvert.
Reimplemented in boolbvt, and bv_pointerst.
Definition at line 33 of file arrays.h.
References equalityt::post_process(), and post_process_arrays().
Referenced by boolbvt::post_process().
|
inlineprotectedvirtual |
Reimplemented in bv_refinementt.
Definition at line 46 of file arrays.h.
References add_array_constraints().
Referenced by post_process().
literalt arrayst::record_array_equality | ( | const equal_exprt & | expr | ) |
Definition at line 42 of file arrays.cpp.
References array_equalities, arrays, base_type_eq(), collect_arrays(), equalityt::equality(), namespace_baset::follow(), union_find< T >::make_union(), decision_proceduret::ns, exprt::op0(), exprt::op1(), irept::pretty(), and exprt::type().
Referenced by boolbvt::convert_equality().
void arrayst::record_array_index | ( | const index_exprt & | expr | ) |
Definition at line 32 of file arrays.cpp.
References index_exprt::array(), arrays, index_exprt::index(), index_map, union_find< T >::number(), and update_indices.
Referenced by collect_arrays(), collect_indices(), and boolbvt::convert_index().
|
protected |
Definition at line 360 of file arrays.cpp.
References arrays, union_find< T >::find_number(), from_expr(), index_map, decision_proceduret::ns, and update_indices.
Referenced by add_array_constraints(), and bv_refinementt::post_process_arrays().
|
protected |
merge the indices into the root
Definition at line 346 of file arrays.cpp.
References arrays, union_find< T >::find_number(), index_map, and union_find< T >::is_root_number().
|
protected |
Definition at line 61 of file arrays.h.
Referenced by add_array_constraints(), and record_array_equality().
|
protected |
Definition at line 64 of file arrays.h.
Referenced by add_array_Ackermann_constraints(), add_array_constraints(), boolbvt::bv_get_unbounded_array(), collect_arrays(), collect_indices(), record_array_equality(), record_array_index(), and update_index_map().
|
protected |
Definition at line 99 of file arrays.h.
Referenced by add_array_constraint().
|
protected |
Definition at line 96 of file arrays.h.
Referenced by add_array_constraint(), and arrayst().
|
protected |
Definition at line 71 of file arrays.h.
Referenced by add_array_Ackermann_constraints(), add_array_constraints(), boolbvt::bv_get_unbounded_array(), record_array_index(), and update_index_map().
|
protected |
Definition at line 97 of file arrays.h.
Referenced by add_array_constraint(), bv_refinementt::arrays_overapproximated(), and bv_refinementt::freeze_lazy_constraints().
|
protected |
Definition at line 95 of file arrays.h.
Referenced by add_array_constraint(), arrayst(), bv_refinementt::freeze_lazy_constraints(), and bv_refinementt::post_process_arrays().
|
protected |
Definition at line 119 of file arrays.h.
Referenced by record_array_index(), and update_index_map().