cprover
|
#include <cnf.h>
Public Member Functions | |
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) |
virtual size_t | no_clauses () const =0 |
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 void | lcnf (const bvt &bv)=0 |
virtual bool | has_set_to () const |
virtual bool | cnf_handled_well () const |
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 const std::string | solver_text ()=0 |
virtual resultt | prop_solve ()=0 |
virtual tvt | l_get (literalt a) const =0 |
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 () |
Static Public Member Functions | |
static bvt | eliminate_duplicates (const bvt &) |
eliminate duplicates from given vector of literals More... | |
Protected Member Functions | |
bool | process_clause (const bvt &bv, bvt &dest) |
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses More... | |
Static Protected Member Functions | |
static bool | is_all (const bvt &bv, literalt l) |
Protected Attributes | |
size_t | _no_variables |
![]() | |
bvt | lcnf_bv |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR } |
eliminate duplicates from given vector of literals
Definition at line 400 of file cnf.cpp.
Referenced by land(), lor(), and read_dimacs_cnf().
Tseitin encoding of equality between two literals.
Definition at line 145 of file cnf.cpp.
References gate_xor().
Tseitin encoding of NAND of two literals.
Definition at line 101 of file cnf.cpp.
References propt::lcnf(), neg(), and pos().
Tseitin encoding of NOR of two literals.
Definition at line 123 of file cnf.cpp.
References propt::lcnf(), neg(), and pos().
Tseitin encoding of disjunction of two literals.
Definition at line 48 of file cnf.cpp.
References propt::lcnf(), neg(), and pos().
Referenced by gate_implies(), and lor().
Tseitin encoding of XOR of two literals.
Definition at line 70 of file cnf.cpp.
References propt::lcnf(), neg(), and pos().
Referenced by gate_equal(), and lxor().
Implements propt.
Definition at line 265 of file cnf.cpp.
References gate_and(), literalt::is_false(), literalt::is_true(), and new_variable().
Tseitin encoding of conjunction between multiple literals.
Implements propt.
Definition at line 160 of file cnf.cpp.
References const_literal(), eliminate_duplicates(), is_all(), land(), propt::lcnf(), neg(), new_variable(), and pos().
Implements propt.
Reimplemented in qbf_bdd_coret.
Definition at line 281 of file cnf.cpp.
References gate_or(), literalt::is_false(), literalt::is_true(), and new_variable().
Referenced by limplies(), lnor(), lor(), and lselect().
Tseitin encoding of disjunction between multiple literals.
Implements propt.
Reimplemented in qbf_bdd_coret.
Definition at line 203 of file cnf.cpp.
References const_literal(), eliminate_duplicates(), is_all(), propt::lcnf(), lor(), neg(), new_variable(), and pos().
Implements propt.
Definition at line 346 of file cnf.cpp.
References literalt::is_constant(), land(), propt::lcnf(), lor(), new_variable(), and literalt::sign().
Tseitin encoding of XOR between multiple literals.
Implements propt.
Definition at line 246 of file cnf.cpp.
References const_literal().
Referenced by lequal().
Implements propt.
Definition at line 297 of file cnf.cpp.
References const_literal(), gate_xor(), literalt::is_false(), literalt::is_true(), and new_variable().
|
overridevirtual |
Generate a new variable and return it as a literal.
Implements propt.
Reimplemented in qbf_bdd_coret, and qbf_bdd_certificatet.
Definition at line 387 of file cnf.cpp.
References _no_variables, literalt::set(), and set_no_variables().
Referenced by land(), lor(), lselect(), lxor(), and qbf_bdd_certificatet::new_variable().
|
pure virtual |
Implemented in cnf_solvert, dimacs_cnf_dumpt, qbf_squolem_coret, cnf_clause_listt, and qbf_squolemt.
|
inlineoverridevirtual |
Implements propt.
Definition at line 38 of file cnf.h.
References _no_variables.
Referenced by satcheck_minisat1_baset::add_variables(), cnf_clause_list_assignmentt::copy_assignment_from(), satcheck_zchaff_baset::copy_cnf(), satcheck_booleforce_baset::l_get(), pbs_dimacs_cnft::pbs_solve(), qbf_quantort::prop_solve(), qbf_skizzot::prop_solve(), qbf_qubet::prop_solve(), satcheck_limmatt::prop_solve(), qbf_skizzo_coret::prop_solve(), satcheck_zcoret::prop_solve(), satcheck_lingelingt::prop_solve(), satcheck_precosatt::prop_solve(), qbf_qube_coret::prop_solve(), qbf_squolem_coret::prop_solve(), qbf_squolemt::prop_solve(), pbs_dimacs_cnft::prop_solve(), qbf_bdd_coret::prop_solve(), satcheck_minisat1_coret::prop_solve(), read_dimacs_cnf(), satcheck_smvsatt::satcheck_smvsatt(), qdimacs_cnft::write_prefix(), and dimacs_cnft::write_problem_line().
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition at line 416 of file cnf.cpp.
References _no_variables, and literalt::unused_var_no().
Referenced by satcheck_booleforce_baset::lcnf(), satcheck_picosatt::lcnf(), satcheck_lingelingt::lcnf(), cnf_clause_listt::lcnf(), satcheck_smvsatt::lcnf(), satcheck_precosatt::lcnf(), satcheck_minisat1_baset::lcnf(), qbf_squolemt::lcnf(), qbf_squolem_coret::lcnf(), qbf_bdd_coret::lcnf(), and satcheck_smvsat_interpolatort::lcnf().
|
inlinevirtual |
Reimplemented in qbf_squolem_coret, and qbf_squolemt.
Definition at line 39 of file cnf.h.
References _no_variables.
Referenced by cnf_clause_listt::copy_to(), qdimacs_cnft::copy_to(), new_variable(), read_dimacs_cnf(), qbf_squolemt::set_no_variables(), and qbf_squolem_coret::set_no_variables().
|
protected |
Definition at line 53 of file cnf.h.
Referenced by cnf_clause_listt::copy_to(), qdimacs_cnft::copy_to(), satcheck_picosatt::lcnf(), new_variable(), no_variables(), process_clause(), satcheck_picosatt::prop_solve(), satcheck_minisat1_baset::prop_solve(), satcheck_zchaff_baset::prop_solve(), and set_no_variables().