cprover
|
#include <satcheck_picosat.h>
Public Member Functions | |
satcheck_picosatt () | |
~satcheck_picosatt () | |
virtual const std::string | solver_text () |
virtual resultt | prop_solve () |
virtual tvt | l_get (literalt a) const |
virtual void | lcnf (const bvt &bv) |
virtual void | set_assignment (literalt a, bool value) |
virtual bool | is_in_conflict (literalt a) const |
Returns true if an assumption is in the final conflict. More... | |
virtual void | set_assumptions (const bvt &_assumptions) |
virtual bool | has_set_assumptions () const |
virtual bool | has_is_in_conflict () const |
![]() | |
cnf_solvert () | |
virtual size_t | no_clauses () const override |
![]() | |
cnft () | |
virtual | ~cnft () |
virtual literalt | land (literalt a, literalt b) override |
virtual literalt | lor (literalt a, literalt b) override |
virtual literalt | land (const bvt &bv) override |
Tseitin encoding of conjunction between multiple literals. More... | |
virtual literalt | lor (const bvt &bv) override |
Tseitin encoding of disjunction between multiple literals. More... | |
virtual literalt | lxor (const bvt &bv) override |
Tseitin encoding of XOR between multiple literals. More... | |
virtual literalt | lxor (literalt a, literalt b) override |
virtual literalt | lnand (literalt a, literalt b) override |
virtual literalt | lnor (literalt a, literalt b) override |
virtual literalt | lequal (literalt a, literalt b) override |
virtual literalt | limplies (literalt a, literalt b) override |
virtual literalt | lselect (literalt a, literalt b, literalt c) override |
virtual literalt | new_variable () override |
Generate a new variable and return it as a literal. More... | |
virtual size_t | no_variables () const override |
virtual void | set_no_variables (size_t no) |
void | gate_and (literalt a, literalt b, literalt o) |
Tseitin encoding of conjunction of two literals. More... | |
void | gate_or (literalt a, literalt b, literalt o) |
Tseitin encoding of disjunction of two literals. More... | |
void | gate_xor (literalt a, literalt b, literalt o) |
Tseitin encoding of XOR of two literals. More... | |
void | gate_nand (literalt a, literalt b, literalt o) |
Tseitin encoding of NAND of two literals. More... | |
void | gate_nor (literalt a, literalt b, literalt o) |
Tseitin encoding of NOR of two literals. More... | |
void | gate_equal (literalt a, literalt b, literalt o) |
Tseitin encoding of equality between two literals. More... | |
void | gate_implies (literalt a, literalt b, literalt o) |
Tseitin encoding of implication between two literals. More... | |
![]() | |
propt () | |
virtual | ~propt () |
virtual void | set_equal (literalt a, literalt b) |
asserts a==b in the propositional formula More... | |
virtual void | l_set_to (literalt a, bool value) |
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_variable_name (literalt, const irep_idt &) |
bvt | new_variables (std::size_t width) |
generates a bitvector of given width with new variables More... | |
virtual void | set_frozen (literalt) |
virtual void | set_time_limit_seconds (uint32_t) |
Protected Attributes | |
bvt | assumptions |
![]() | |
statust | status |
size_t | clause_counter |
![]() | |
size_t | _no_variables |
![]() | |
bvt | lcnf_bv |
Private Attributes | |
PicoSAT * | picosat |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR } |
![]() | |
static bvt | eliminate_duplicates (const bvt &) |
eliminate duplicates from given vector of literals More... | |
![]() | |
enum | statust { statust::INIT, statust::SAT, statust::UNSAT, statust::ERROR } |
![]() | |
bool | process_clause (const bvt &bv, bvt &dest) |
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses More... | |
![]() | |
static bool | is_all (const bvt &bv, literalt l) |
Definition at line 18 of file satcheck_picosat.h.
satcheck_picosatt::satcheck_picosatt | ( | ) |
Definition at line 107 of file satcheck_picosat.cpp.
References picosat.
satcheck_picosatt::~satcheck_picosatt | ( | ) |
Definition at line 112 of file satcheck_picosat.cpp.
References picosat.
|
inlinevirtual |
Reimplemented from propt.
Definition at line 34 of file satcheck_picosat.h.
|
inlinevirtual |
Reimplemented from propt.
Definition at line 33 of file satcheck_picosat.h.
|
virtual |
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 117 of file satcheck_picosat.cpp.
References literalt::dimacs(), literalt::is_constant(), and picosat.
Implements propt.
Definition at line 24 of file satcheck_picosat.cpp.
References literalt::dimacs(), literalt::is_constant(), picosat, messaget::result(), literalt::sign(), tvt::TV_UNKNOWN, and literalt::var_no().
|
virtual |
Implements propt.
Definition at line 50 of file satcheck_picosat.cpp.
References cnft::_no_variables, cnf_solvert::clause_counter, forall_literals, picosat, and cnft::process_clause().
|
virtual |
Implements propt.
Definition at line 67 of file satcheck_picosat.cpp.
References cnft::_no_variables, assumptions, messaget::eom(), forall_literals, picosat, messaget::status(), and to_string().
|
virtual |
Implements propt.
Definition at line 102 of file satcheck_picosat.cpp.
|
virtual |
Reimplemented from propt.
Definition at line 124 of file satcheck_picosat.cpp.
References assumptions, and forall_literals.
|
virtual |
Implements propt.
Definition at line 45 of file satcheck_picosat.cpp.
|
protected |
Definition at line 37 of file satcheck_picosat.h.
Referenced by prop_solve(), and set_assumptions().
|
private |
Definition at line 40 of file satcheck_picosat.h.
Referenced by is_in_conflict(), l_get(), lcnf(), prop_solve(), satcheck_picosatt(), and ~satcheck_picosatt().