cprover
|
#include <prop_conv_store.h>
Classes | |
class | constraintst |
struct | constraintt |
Public Member Functions | |
prop_conv_storet (const namespacet &_ns) | |
const constraintst & | get_constraints () const |
virtual void | set_to (const exprt &expr, bool value) |
virtual literalt | convert (const exprt &expr) |
![]() | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
literalt | operator() (const exprt &expr) |
virtual tvt | l_get (literalt a) const =0 |
virtual void | set_frozen (literalt a) |
virtual void | set_frozen (const bvt &) |
virtual void | set_assumptions (const bvt &_assumptions) |
virtual bool | has_set_assumptions () const |
virtual void | set_all_frozen () |
virtual bool | is_in_conflict (literalt l) const |
determine whether a variable is in the final conflict More... | |
virtual bool | has_is_in_conflict () const |
![]() | |
decision_proceduret (const namespacet &_ns) | |
virtual exprt | get (const exprt &expr) const =0 |
virtual void | print_assignment (std::ostream &out) const =0 |
void | set_to_true (const exprt &expr) |
void | set_to_false (const exprt &expr) |
virtual resultt | dec_solve ()=0 |
resultt | operator() () |
virtual bool | in_core (const exprt &expr) |
virtual std::string | decision_procedure_text () const =0 |
Protected Attributes | |
constraintst | constraints |
![]() | |
const namespacet & | ns |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
Definition at line 15 of file prop_conv_store.h.
|
inlineexplicit |
Definition at line 18 of file prop_conv_store.h.
Implements prop_convt.
Definition at line 21 of file prop_conv_store.cpp.
References prop_conv_storet::constraintst::add_constraint(), constraints, prop_conv_storet::constraintt::CONVERT, prop_conv_storet::constraintt::expr, prop_conv_storet::constraintt::literal, and prop_conv_storet::constraintt::type.
Referenced by get_constraints().
|
inline |
Definition at line 55 of file prop_conv_store.h.
References constraints, convert(), prop_conv_storet::constraintt::expr, set_to(), and prop_conv_storet::constraintt::value.
|
virtual |
Implements decision_proceduret.
Definition at line 13 of file prop_conv_store.cpp.
References prop_conv_storet::constraintst::add_constraint(), constraints, prop_conv_storet::constraintt::expr, prop_conv_storet::constraintt::SET_TO, prop_conv_storet::constraintt::type, and prop_conv_storet::constraintt::value.
Referenced by get_constraints().
|
protected |
Definition at line 65 of file prop_conv_store.h.
Referenced by convert(), get_constraints(), and set_to().