CBMC
|
#include <satcheck_minisat.h>
Protected Member Functions | |
resultt | do_prop_solve (const bvt &assumptions) override |
void | add_variables () |
![]() | |
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 | |
Protected Attributes | |
class Solver * | solver |
bool | empty_clause_added |
![]() | |
statust | status |
size_t | clause_counter |
![]() | |
size_t | _no_variables |
![]() | |
bvt | lcnf_bv |
messaget | log |
std::size_t | number_of_solver_calls = 0 |
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) |
Definition at line 18 of file satcheck_minisat.h.
|
inline |
Definition at line 21 of file satcheck_minisat.h.
|
virtual |
Definition at line 245 of file satcheck_minisat.cpp.
|
protected |
Definition at line 116 of file satcheck_minisat.cpp.
|
overrideprotectedvirtual |
Implements propt.
Reimplemented in satcheck_minisat1_coret.
Definition at line 153 of file satcheck_minisat.cpp.
|
inlineoverridevirtual |
Reimplemented from propt.
Definition at line 35 of file satcheck_minisat.h.
|
inlineoverridevirtual |
Reimplemented from propt.
Definition at line 39 of file satcheck_minisat.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 204 of file satcheck_minisat.cpp.
Implements propt.
Definition at line 84 of file satcheck_minisat.cpp.
Implements propt.
Definition at line 122 of file satcheck_minisat.cpp.
Implements propt.
Definition at line 195 of file satcheck_minisat.cpp.
|
overridevirtual |
Implements propt.
Reimplemented in satcheck_minisat1_prooft, and satcheck_minisat1_coret.
Definition at line 111 of file satcheck_minisat.cpp.
|
protected |
Definition at line 52 of file satcheck_minisat.h.
Definition at line 50 of file satcheck_minisat.h.