12 #ifndef CPROVER_SOLVERS_SAT_CNF_CLAUSE_LIST_H 13 #define CPROVER_SOLVERS_SAT_CNF_CLAUSE_LIST_H 29 virtual void lcnf(
const bvt &bv);
32 {
return "CNF clause list"; }
50 for(clausest::const_iterator
60 for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
61 result=((result<<2)^it->get())-result;
69 for(clausest::const_iterator it=
clauses.begin(); it!=
clauses.end(); it++)
99 unsigned v=literal.
var_no();
101 if(v==0 || v>=assignment.size())
105 return literal.
sign()?!r:
r;
109 void print_assignment(std::ostream &out)
const;
115 #endif // CPROVER_SOLVERS_SAT_CNF_CLAUSE_LIST_H CNF Generation, via Tseitin.
void lcnf(literalt l0, literalt l1)
assignmentt & get_assignment()
virtual tvt l_get(literalt literal) const
virtual tvt l_get(literalt literal) const
static size_t hash_clause(const bvt &bv)
virtual ~cnf_clause_listt()
std::vector< tvt > assignmentt
std::list< bvt > clausest
virtual const std::string solver_text()
virtual void lcnf(const bvt &bv)
virtual resultt prop_solve()
virtual size_t no_clauses() const
virtual void set_no_variables(size_t no)
virtual void copy_assignment_from(const propt &prop)
void copy_to(cnft &cnf) const
std::vector< literalt > bvt