cprover
|
#include <equality.h>
Classes | |
struct | typestructt |
Public Member Functions | |
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 | |
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 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 | |
typemapt | typemap |
![]() | |
bool | post_processing_done |
symbolst | symbols |
cachet | cache |
propt & | prop |
![]() | |
const namespacet & | ns |
Additional Inherited Members | |
![]() | |
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 } |
![]() | |
bool | use_cache |
bool | equality_propagation |
bool | freeze_all |
Definition at line 19 of file equality.h.
|
protected |
Definition at line 38 of file equality.h.
|
protected |
Definition at line 36 of file equality.h.
|
protected |
Definition at line 37 of file equality.h.
|
protected |
Definition at line 47 of file equality.h.
|
inline |
Definition at line 22 of file equality.h.
References equality().
|
protectedvirtual |
|
protectedvirtual |
Definition at line 98 of file equality.cpp.
References equalityt::typestructt::elements, bv_utilst::equal(), equalityt::typestructt::equalities, propt::new_variable(), prop_conv_solvert::prop, and propt::set_equal().
Definition at line 17 of file equality.cpp.
References equality2().
Referenced by arrayst::add_array_constraints(), boolbvt::convert_bv_rel(), boolbvt::convert_byte_extract(), boolbvt::convert_byte_update(), boolbvt::convert_extractbit(), boolbvt::convert_index(), equalityt(), and arrayst::record_array_equality().
Definition at line 25 of file equality.cpp.
References const_literal(), equalityt::typestructt::elements, equalityt::typestructt::elements_rev, equalityt::typestructt::equalities, prop_conv_solvert::freeze_all, irept::id(), literalt::is_constant(), propt::new_variable(), prop_conv_solvert::prop, messaget::result(), propt::set_frozen(), exprt::type(), and typemap.
Referenced by equality().
|
inlineoverridevirtual |
Reimplemented from prop_conv_solvert.
Definition at line 28 of file equality.h.
References add_equality_constraints(), prop_conv_solvert::post_process(), and typemap.
Referenced by arrayst::post_process().
|
protected |
Definition at line 49 of file equality.h.
Referenced by add_equality_constraints(), equality2(), and post_process().