12 #ifndef CPROVER_SOLVERS_QBF_QBF_SQUOLEM_H 13 #define CPROVER_SOLVERS_QBF_QBF_SQUOLEM_H 15 #include <quannon/squolem2/squolem2.h> 33 virtual void lcnf(
const bvt &bv);
37 virtual size_t no_clauses()
const {
return squolem.clauses(); }
40 #endif // CPROVER_SOLVERS_QBF_QBF_SQUOLEM_H virtual void lcnf(const bvt &bv)
virtual void set_no_variables(size_t no)
virtual const std::string solver_text()
virtual size_t no_clauses() const
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
virtual void add_quantifier(const quantifiert &quantifier)
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
std::vector< literalt > bvt