cprover
|
#include <qdimacs_cnf.h>
Classes | |
class | quantifiert |
Public Types | |
typedef std::vector< quantifiert > | quantifierst |
![]() | |
typedef std::list< bvt > | clausest |
![]() | |
enum | resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR } |
Public Member Functions | |
qdimacs_cnft () | |
virtual | ~qdimacs_cnft () |
virtual void | write_qdimacs_cnf (std::ostream &out) |
virtual const std::string | solver_text () |
virtual void | add_quantifier (const quantifiert &quantifier) |
void | add_quantifier (const quantifiert::typet type, const literalt l) |
void | add_existential_quantifier (const literalt l) |
void | add_universal_quantifier (const literalt l) |
bool | is_quantified (const literalt l) const |
bool | find_quantifier (const literalt l, quantifiert &q) const |
virtual void | set_quantifier (const quantifiert::typet type, const literalt l) |
void | copy_to (qdimacs_cnft &cnf) const |
bool | operator== (const qdimacs_cnft &other) const |
size_t | hash () const |
![]() | |
dimacs_cnft () | |
virtual | ~dimacs_cnft () |
virtual void | write_dimacs_cnf (std::ostream &out) |
![]() | |
cnf_clause_listt () | |
virtual | ~cnf_clause_listt () |
virtual void | lcnf (const bvt &bv) |
virtual tvt | l_get (literalt literal) const |
virtual resultt | prop_solve () |
virtual size_t | no_clauses () const |
clausest & | get_clauses () |
void | copy_to (cnft &cnf) const |
size_t | hash () const |
![]() | |
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_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 () |
Public Attributes | |
quantifierst | quantifiers |
Protected Member Functions | |
void | write_prefix (std::ostream &out) const |
![]() | |
void | write_problem_line (std::ostream &out) |
void | write_clauses (std::ostream &out) |
![]() | |
bool | process_clause (const bvt &bv, bvt &dest) |
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses More... | |
Additional Inherited Members | |
![]() | |
static size_t | hash_clause (const bvt &bv) |
![]() | |
static bvt | eliminate_duplicates (const bvt &) |
eliminate duplicates from given vector of literals More... | |
![]() | |
static bool | is_all (const bvt &bv, literalt l) |
![]() | |
bool | break_lines |
![]() | |
clausest | clauses |
![]() | |
size_t | _no_variables |
![]() | |
bvt | lcnf_bv |
Definition at line 18 of file qdimacs_cnf.h.
typedef std::vector<quantifiert> qdimacs_cnft::quantifierst |
Definition at line 60 of file qdimacs_cnf.h.
|
inline |
Definition at line 21 of file qdimacs_cnf.h.
|
inlinevirtual |
Definition at line 22 of file qdimacs_cnf.h.
|
inline |
Definition at line 73 of file qdimacs_cnf.h.
References add_quantifier(), and qdimacs_cnft::quantifiert::EXISTENTIAL.
|
inlinevirtual |
Reimplemented in qbf_squolem_coret, and qbf_squolemt.
Definition at line 63 of file qdimacs_cnf.h.
References quantifiers.
Referenced by add_existential_quantifier(), qbf_squolemt::add_quantifier(), qbf_squolem_coret::add_quantifier(), add_quantifier(), add_universal_quantifier(), copy_to(), qbf_bdd_certificatet::new_variable(), and set_quantifier().
|
inline |
Definition at line 68 of file qdimacs_cnf.h.
References add_quantifier().
|
inline |
Definition at line 78 of file qdimacs_cnf.h.
References add_quantifier(), and qdimacs_cnft::quantifiert::UNIVERSAL.
void qdimacs_cnft::copy_to | ( | qdimacs_cnft & | cnf | ) | const |
Definition at line 86 of file qdimacs_cnf.cpp.
References cnft::_no_variables, add_quantifier(), cnf_clause_listt::clauses, cnf_clause_listt::lcnf(), quantifiers, and cnft::set_no_variables().
bool qdimacs_cnft::find_quantifier | ( | const literalt | l, |
quantifiert & | q | ||
) | const |
Definition at line 126 of file qdimacs_cnf.cpp.
References quantifiers, and literalt::var_no().
Referenced by qbf_bdd_certificatet::f_get().
size_t qdimacs_cnft::hash | ( | ) | const |
Definition at line 103 of file qdimacs_cnf.cpp.
References cnf_clause_listt::hash(), quantifiers, and messaget::result().
bool qdimacs_cnft::is_quantified | ( | const literalt | l | ) | const |
Definition at line 115 of file qdimacs_cnf.cpp.
References quantifiers, and literalt::var_no().
Referenced by qbf_bdd_certificatet::new_variable().
bool qdimacs_cnft::operator== | ( | const qdimacs_cnft & | other | ) | const |
Definition at line 64 of file qdimacs_cnf.cpp.
References cnf_clause_listt::clauses, and quantifiers.
|
virtual |
Definition at line 69 of file qdimacs_cnf.cpp.
References add_quantifier(), quantifiers, and literalt::var_no().
Referenced by qbf_squolemt::set_quantifier(), and qbf_squolem_coret::set_quantifier().
|
inlinevirtual |
Reimplemented from dimacs_cnft.
Reimplemented in qbf_bdd_coret, qbf_squolemt, qbf_squolem_coret, qbf_qube_coret, qbf_skizzo_coret, qbf_quantort, qbf_qubet, and qbf_skizzot.
Definition at line 28 of file qdimacs_cnf.h.
|
protected |
Definition at line 21 of file qdimacs_cnf.cpp.
References qdimacs_cnft::quantifiert::EXISTENTIAL, cnft::no_variables(), quantifiers, qdimacs_cnft::quantifiert::type, qdimacs_cnft::quantifiert::UNIVERSAL, and qdimacs_cnft::quantifiert::var_no.
Referenced by write_qdimacs_cnf().
|
virtual |
Reimplemented in qbf_squolem_coret.
Definition at line 14 of file qdimacs_cnf.cpp.
References dimacs_cnft::write_clauses(), write_prefix(), and dimacs_cnft::write_problem_line().
Referenced by qbf_quantort::prop_solve(), qbf_qubet::prop_solve(), qbf_skizzot::prop_solve(), qbf_skizzo_coret::prop_solve(), and qbf_qube_coret::prop_solve().
quantifierst qdimacs_cnft::quantifiers |
Definition at line 61 of file qdimacs_cnf.h.
Referenced by add_quantifier(), qbf_bdd_coret::compress_certificate(), copy_to(), qbf_bdd_certificatet::f_get(), find_quantifier(), hash(), is_quantified(), operator==(), qbf_bdd_coret::prop_solve(), set_quantifier(), qbf_squolem_coret::setup(), and write_prefix().