12 #ifndef CPROVER_SOLVERS_QBF_QBF_SQUOLEM_CORE_H 13 #define CPROVER_SOLVERS_QBF_QBF_SQUOLEM_CORE_H 15 #include <quannon/squolem2/squolem2.h> 37 virtual void lcnf(
const bvt &bv);
61 #endif // CPROVER_SOLVERS_QBF_QBF_SQUOLEM_CORE_H virtual const std::string solver_text()
virtual void add_quantifier(const quantifiert &quantifier)
virtual modeltypet m_get(literalt a) const
virtual ~qbf_squolem_coret()
const exprt f_get_dnf(WitnessStack *wsp)
virtual size_t no_clauses() const
virtual void set_no_variables(size_t no)
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual void write_qdimacs_cnf(std::ostream &out)
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
Base class for all expressions.
virtual const exprt f_get(literalt l)
void set_debug_filename(const std::string &str)
function_cachet function_cache
virtual void lcnf(const bvt &bv)
const exprt f_get_cnf(WitnessStack *wsp)
std::unordered_map< unsigned, exprt > function_cachet
std::vector< literalt > bvt
virtual bool is_in_core(literalt l) const