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);
Base class for all expressions.
virtual const exprt f_get(literalt l)
virtual void lcnf(const bvt &bv)
virtual void add_quantifier(const quantifiert &quantifier)
virtual resultt prop_solve()
void set_debug_filename(const std::string &str)
const exprt f_get_cnf(WitnessStack *wsp)
virtual ~qbf_squolem_coret()
std::unordered_map< unsigned, exprt > function_cachet
virtual modeltypet m_get(literalt a) const
function_cachet function_cache
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual void write_qdimacs_cnf(std::ostream &out)
virtual bool is_in_core(literalt l) const
const exprt f_get_dnf(WitnessStack *wsp)
virtual const std::string solver_text()
virtual void set_no_variables(size_t no)
virtual size_t no_clauses() const
virtual tvt l_get(literalt a) const
std::vector< literalt > bvt