cprover
|
TO_BE_DOCUMENTED. More...
#include <prop_conv.h>
Public Types | |
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 | |
prop_conv_solvert (const namespacet &_ns, propt &_prop) | |
virtual | ~prop_conv_solvert ()=default |
void | set_to (const exprt &expr, bool value) override |
decision_proceduret::resultt | dec_solve () override |
void | print_assignment (std::ostream &out) const override |
std::string | decision_procedure_text () const override |
exprt | get (const exprt &expr) const override |
virtual tvt | l_get (literalt a) const override |
void | set_frozen (literalt a) override |
void | set_assumptions (const bvt &_assumptions) override |
bool | has_set_assumptions () const override |
void | set_all_frozen () override |
literalt | convert (const exprt &expr) override |
bool | is_in_conflict (literalt l) const override |
determine whether a variable is in the final conflict More... | |
bool | has_is_in_conflict () const override |
bool | literal (const symbol_exprt &expr, literalt &literal) const |
virtual void | clear_cache () |
const cachet & | get_cache () const |
const symbolst & | get_symbols () const |
void | set_time_limit_seconds (uint32_t lim) override |
virtual void | set_frozen (literalt a) |
virtual void | set_frozen (const bvt &) |
![]() | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
literalt | operator() (const exprt &expr) |
virtual void | set_frozen (const bvt &) |
![]() | |
decision_proceduret (const namespacet &_ns) | |
virtual | ~decision_proceduret () |
void | set_to_true (const exprt &expr) |
void | set_to_false (const exprt &expr) |
resultt | operator() () |
Public Attributes | |
bool | use_cache = true |
bool | equality_propagation = true |
bool | freeze_all = false |
Protected Member Functions | |
virtual void | post_process () |
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 | |
bool | post_processing_done = false |
symbolst | symbols |
cachet | cache |
propt & | prop |
![]() | |
const namespacet & | ns |
Additional Inherited Members |
TO_BE_DOCUMENTED.
Definition at line 70 of file prop_conv.h.
typedef std::unordered_map<exprt, literalt, irep_hash> prop_conv_solvert::cachet |
Definition at line 118 of file prop_conv.h.
typedef std::map<irep_idt, literalt> prop_conv_solvert::symbolst |
Definition at line 117 of file prop_conv.h.
|
inline |
Definition at line 73 of file prop_conv.h.
|
virtualdefault |
|
inlinevirtual |
Reimplemented in boolbvt.
Definition at line 115 of file prop_conv.h.
Implements prop_convt.
Definition at line 157 of file prop_conv.cpp.
Definition at line 190 of file prop_conv.cpp.
Reimplemented in boolbvt, and bv_pointerst.
Definition at line 330 of file prop_conv.cpp.
|
overridevirtual |
Implements decision_proceduret.
Reimplemented in string_refinementt, and bv_refinementt.
Definition at line 465 of file prop_conv.cpp.
|
inlineoverridevirtual |
Implements decision_proceduret.
Reimplemented in string_refinementt, and bv_refinementt.
Definition at line 83 of file prop_conv.h.
Implements decision_proceduret.
Reimplemented in string_refinementt.
Definition at line 485 of file prop_conv.cpp.
get a boolean value from counter example if not valid
Definition at line 69 of file prop_conv.cpp.
|
inline |
Definition at line 120 of file prop_conv.h.
Definition at line 51 of file prop_conv.cpp.
|
inline |
Definition at line 121 of file prop_conv.h.
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Definition at line 105 of file prop_conv.h.
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Definition at line 96 of file prop_conv.h.
|
protectedvirtual |
Definition at line 454 of file prop_conv.cpp.
|
inlineoverridevirtual |
determine whether a variable is in the final conflict
Reimplemented from prop_convt.
Definition at line 103 of file prop_conv.h.
Implements prop_convt.
Definition at line 89 of file prop_conv.h.
bool prop_conv_solvert::literal | ( | const symbol_exprt & | expr, |
literalt & | literal | ||
) | const |
Definition at line 36 of file prop_conv.cpp.
|
protectedvirtual |
Reimplemented in boolbvt, arrayst, equalityt, and bv_pointerst.
Definition at line 461 of file prop_conv.cpp.
|
overridevirtual |
Implements decision_proceduret.
Definition at line 509 of file prop_conv.cpp.
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Definition at line 98 of file prop_conv.h.
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Reimplemented in bv_refinementt.
Definition at line 94 of file prop_conv.h.
|
protectedvirtual |
Definition at line 337 of file prop_conv.cpp.
void prop_convt::set_frozen |
Definition at line 24 of file prop_conv.cpp.
void prop_convt::set_frozen |
Definition at line 29 of file prop_conv.cpp.
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Definition at line 90 of file prop_conv.h.
|
inlineoverridevirtual |
Reimplemented from prop_convt.
Definition at line 123 of file prop_conv.h.
|
overridevirtual |
Implements decision_proceduret.
Reimplemented in string_refinementt.
Definition at line 364 of file prop_conv.cpp.
|
protected |
Definition at line 147 of file prop_conv.h.
bool prop_conv_solvert::equality_propagation = true |
Definition at line 112 of file prop_conv.h.
bool prop_conv_solvert::freeze_all = false |
Definition at line 113 of file prop_conv.h.
|
protected |
Definition at line 131 of file prop_conv.h.
|
protected |
Definition at line 152 of file prop_conv.h.
|
protected |
Definition at line 142 of file prop_conv.h.
bool prop_conv_solvert::use_cache = true |
Definition at line 111 of file prop_conv.h.