cprover
|
#include <prop_wrapper.h>
Public Member Functions | |
prop_wrappert (propt &_prop) | |
virtual | ~prop_wrappert () |
virtual literalt | constant (bool value) |
virtual literalt | land (literalt a, literalt b) |
virtual literalt | lor (literalt a, literalt b) |
virtual literalt | land (const bvt &bv) |
virtual literalt | lor (const bvt &bv) |
virtual literalt | lxor (literalt a, literalt b) |
virtual literalt | lxor (const bvt &bv) |
virtual literalt | lnand (literalt a, literalt b) |
virtual literalt | lnor (literalt a, literalt b) |
virtual literalt | lequal (literalt a, literalt b) |
virtual literalt | limplies (literalt a, literalt b) |
virtual literalt | lselect (literalt a, literalt b, literalt c) |
virtual void | lcnf (const bvt &bv) |
virtual void | l_set_to (literalt a, bool value) |
virtual literalt | new_variable () |
virtual std::size_t | no_variables () const |
virtual const std::string | solver_text () |
virtual tvt | l_get (literalt a) const |
virtual resultt | prop_solve () |
![]() | |
propt () | |
virtual | ~propt () |
virtual void | set_equal (literalt a, literalt b) |
asserts a==b in the propositional formula More... | |
void | l_set_to_true (literalt a) |
void | l_set_to_false (literalt a) |
void | lcnf (literalt l0, literalt l1) |
void | lcnf (literalt l0, literalt l1, literalt l2) |
void | lcnf (literalt l0, literalt l1, literalt l2, literalt l3) |
virtual bool | has_set_to () const |
virtual bool | cnf_handled_well () const |
virtual void | set_assumptions (const bvt &_assumptions) |
virtual bool | has_set_assumptions () const |
virtual void | set_variable_name (literalt a, const std::string &name) |
bvt | new_variables (std::size_t width) |
generates a bitvector of given width with new variables More... | |
virtual void | set_assignment (literalt a, bool value) |
virtual void | copy_assignment_from (const propt &prop) |
virtual bool | is_in_conflict (literalt l) const |
virtual bool | has_is_in_conflict () const |
virtual void | set_frozen (literalt a) |
![]() | |
virtual | ~prop_assignmentt () |
Protected Attributes | |
propt & | p |
![]() | |
bvt | lcnf_bv |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR } |
Definition at line 15 of file prop_wrapper.h.
|
inlineexplicit |
Definition at line 18 of file prop_wrapper.h.
|
inlinevirtual |
Definition at line 19 of file prop_wrapper.h.
|
inlinevirtual |
Definition at line 21 of file prop_wrapper.h.
References p.
|
inlinevirtual |
Reimplemented from propt.
Definition at line 62 of file prop_wrapper.h.
References propt::l_set_to(), and p.
|
inlinevirtual |
Implements propt.
Definition at line 52 of file prop_wrapper.h.
References propt::limplies(), and p.
|
inlinevirtual |
Implements propt.
Definition at line 66 of file prop_wrapper.h.
References propt::new_variable(), and p.
|
inlinevirtual |
Implements propt.
Definition at line 69 of file prop_wrapper.h.
References propt::no_variables(), and p.
|
inlinevirtual |
Implements propt.
Definition at line 79 of file prop_wrapper.h.
References p, and propt::prop_solve().
|
inlinevirtual |
Implements propt.
Definition at line 73 of file prop_wrapper.h.
References p, and propt::solver_text().
|
protected |
Definition at line 83 of file prop_wrapper.h.
Referenced by constant(), l_get(), l_set_to(), land(), lcnf(), lequal(), limplies(), lnand(), lnor(), lor(), lselect(), lxor(), new_variable(), no_variables(), prop_solve(), and solver_text().