cprover
|
#include <aig_prop.h>
Public Member Functions | |
aig_prop_constraintt (aig_plus_constraintst &_dest) | |
bool | has_set_to () const override |
void | lcnf (const bvt &clause) override |
void | l_set_to (literalt a, bool value) override |
![]() | |
aig_prop_baset (aigt &_dest) | |
bool | cnf_handled_well () const override |
literalt | land (literalt a, literalt b) override |
literalt | lor (literalt a, literalt b) override |
literalt | land (const bvt &bv) override |
literalt | lor (const bvt &bv) override |
literalt | lxor (literalt a, literalt b) override |
literalt | lxor (const bvt &bv) override |
literalt | lnand (literalt a, literalt b) override |
literalt | lnor (literalt a, literalt b) override |
literalt | lequal (literalt a, literalt b) override |
literalt | limplies (literalt a, literalt b) override |
literalt | lselect (literalt a, literalt b, literalt c) override |
void | set_equal (literalt a, literalt b) override |
asserts a==b in the propositional formula More... | |
literalt | new_variable () override |
size_t | no_variables () const override |
const std::string | solver_text () override |
tvt | l_get (literalt a) const override |
resultt | prop_solve () override |
![]() | |
propt () | |
virtual | ~propt () |
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 void | set_assumptions (const bvt &_assumptions) |
virtual bool | has_set_assumptions () const |
virtual void | set_variable_name (literalt a, const irep_idt &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 void | set_time_limit_seconds (uint32_t lim) |
Public Attributes | |
aig_plus_constraintst & | dest |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR } |
![]() | |
aigt & | dest |
![]() | |
bvt | lcnf_bv |
Definition at line 67 of file aig_prop.h.
|
inlineexplicit |
Definition at line 70 of file aig_prop.h.
|
inlineoverridevirtual |
Reimplemented from aig_prop_baset.
Definition at line 77 of file aig_prop.h.
|
inlineoverridevirtual |
Reimplemented from aig_prop_baset.
Definition at line 84 of file aig_prop.h.
References aig_plus_constraintst::constraints, and dest.
|
inlineoverridevirtual |
Reimplemented from aig_prop_baset.
Definition at line 79 of file aig_prop.h.
References propt::l_set_to_true(), and aig_prop_baset::lor().
aig_plus_constraintst& aig_prop_constraintt::dest |
Definition at line 76 of file aig_prop.h.
Referenced by l_set_to().