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);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
virtual void set_no_variables(size_t no)
virtual resultt prop_solve()
virtual const std::string solver_text()
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual tvt l_get(literalt a) const
virtual void lcnf(const bvt &bv)
virtual size_t no_clauses() const
virtual void add_quantifier(const quantifiert &quantifier)
std::vector< literalt > bvt
resultt
The result of goto verifying.