cprover
|
#include <aig_prop.h>
Public Member Functions | |
aig_prop_baset (aigt &_dest) | |
bool | has_set_to () const override |
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 |
void | lcnf (const bvt &clause) 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... | |
void | l_set_to (literalt a, bool value) override |
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 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 | |
aigt & | dest |
![]() | |
bvt | lcnf_bv |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR } |
Definition at line 20 of file aig_prop.h.
|
inlineexplicit |
Definition at line 23 of file aig_prop.h.
|
inlineoverridevirtual |
|
inlineoverridevirtual |
Reimplemented from propt.
Reimplemented in aig_prop_constraintt.
Definition at line 27 of file aig_prop.h.
Implements propt.
Reimplemented in aig_prop_solvert.
Definition at line 57 of file aig_prop.h.
References tvt::unknown().
Referenced by aig_prop_solvert::solver_text().
|
inlineoverridevirtual |
Reimplemented from propt.
Reimplemented in aig_prop_constraintt.
Definition at line 44 of file aig_prop.h.
Implements propt.
Definition at line 56 of file aig_prop.cpp.
References const_literal(), dest, literalt::is_false(), literalt::is_true(), neg(), and aigt::new_and_node().
Referenced by cnf_handled_well(), land(), lnand(), lor(), lselect(), and lxor().
Implements propt.
Definition at line 22 of file aig_prop.cpp.
References const_literal(), forall_literals, and land().
|
inlineoverridevirtual |
Implements propt.
Reimplemented in aig_prop_constraintt.
Definition at line 34 of file aig_prop.h.
References lequal(), limplies(), lnand(), lnor(), lselect(), lxor(), and set_equal().
Implements propt.
Definition at line 107 of file aig_prop.cpp.
References lxor().
Referenced by lcnf(), and set_equal().
Implements propt.
Definition at line 97 of file aig_prop.cpp.
References land().
Referenced by lcnf().
Implements propt.
Definition at line 102 of file aig_prop.cpp.
References lor().
Referenced by lcnf().
Implements propt.
Definition at line 71 of file aig_prop.cpp.
Referenced by cnf_handled_well(), aig_prop_constraintt::lcnf(), limplies(), lnor(), lselect(), lxor(), and set_equal().
Implements propt.
Definition at line 34 of file aig_prop.cpp.
References const_literal(), forall_literals, land(), and neg().
Implements propt.
Definition at line 117 of file aig_prop.cpp.
References literalt::is_false(), literalt::is_true(), land(), lor(), and neg().
Referenced by lcnf().
Implements propt.
Definition at line 76 of file aig_prop.cpp.
References const_literal(), literalt::is_false(), literalt::is_true(), land(), lor(), and neg().
Implements propt.
Definition at line 46 of file aig_prop.cpp.
References const_literal(), forall_literals, and lxor().
|
inlineoverridevirtual |
|
inlineoverridevirtual |
Implements propt.
Definition at line 51 of file aig_prop.h.
References dest, and aigt::number_of_nodes().
|
inlineoverridevirtual |
Implements propt.
Reimplemented in aig_prop_solvert.
Definition at line 60 of file aig_prop.h.
References propt::P_ERROR.
Referenced by aig_prop_solvert::solver_text().
asserts a==b in the propositional formula
Reimplemented from propt.
Definition at line 132 of file aig_prop.cpp.
References propt::l_set_to_true(), lequal(), lor(), neg(), and pos().
Referenced by lcnf().
|
inlineoverridevirtual |
|
protected |
Definition at line 64 of file aig_prop.h.
Referenced by land(), new_variable(), and no_variables().