CBMC
|
#include <satcheck_picosat.h>
Protected Member Functions | |
resultt | do_prop_solve (const bvt &assumptions) override |
![]() | |
void | gate_and (literalt a, literalt b, literalt o) |
Tseitin encoding of conjunction of two literals. | |
void | gate_or (literalt a, literalt b, literalt o) |
Tseitin encoding of disjunction of two literals. | |
void | gate_xor (literalt a, literalt b, literalt o) |
Tseitin encoding of XOR of two literals. | |
void | gate_nand (literalt a, literalt b, literalt o) |
Tseitin encoding of NAND of two literals. | |
void | gate_nor (literalt a, literalt b, literalt o) |
Tseitin encoding of NOR of two literals. | |
void | gate_equal (literalt a, literalt b, literalt o) |
Tseitin encoding of equality between two literals. | |
void | gate_implies (literalt a, literalt b, literalt o) |
Tseitin encoding of implication between two literals. | |
bool | process_clause (const bvt &bv, bvt &dest) const |
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses | |
Private Attributes | |
PicoSAT * | picosat |
Additional Inherited Members | |
![]() | |
enum class | resultt { P_SATISFIABLE , P_UNSATISFIABLE , P_ERROR } |
![]() | |
enum class | statust { INIT , SAT , UNSAT , ERROR } |
![]() | |
static bvt | eliminate_duplicates (const bvt &) |
eliminate duplicates from given vector of literals | |
static bool | is_all (const bvt &bv, literalt l) |
![]() | |
statust | status |
size_t | clause_counter |
![]() | |
size_t | _no_variables |
![]() | |
bvt | lcnf_bv |
messaget | log |
std::size_t | number_of_solver_calls = 0 |
Definition at line 18 of file satcheck_picosat.h.
satcheck_picosatt::satcheck_picosatt | ( | ) |
Definition at line 111 of file satcheck_picosat.cpp.
satcheck_picosatt::~satcheck_picosatt | ( | ) |
Definition at line 116 of file satcheck_picosat.cpp.
|
overrideprotectedvirtual |
Implements propt.
Definition at line 68 of file satcheck_picosat.cpp.
|
inlineoverridevirtual |
Reimplemented from propt.
Definition at line 31 of file satcheck_picosat.h.
|
inlineoverridevirtual |
Reimplemented from propt.
Definition at line 35 of file satcheck_picosat.h.
Returns true if an assumption is in the final conflict.
Note that only literals that are assumptions (see set_assumptions) may be queried.
Implements propt.
Definition at line 121 of file satcheck_picosat.cpp.
Implements propt.
Definition at line 25 of file satcheck_picosat.cpp.
Implements propt.
Definition at line 51 of file satcheck_picosat.cpp.
Implements propt.
Definition at line 106 of file satcheck_picosat.cpp.
|
overridevirtual |
Implements propt.
Definition at line 46 of file satcheck_picosat.cpp.
|
private |
Definition at line 44 of file satcheck_picosat.h.