10#ifndef CPROVER_SOLVERS_QBF_QBF_BDD_CORE_H
11#define CPROVER_SOLVERS_QBF_QBF_BDD_CORE_H
57 virtual void lcnf(
const bvt &bv);
Base class for all expressions.
std::vector< BDD * > model_bddst
virtual const exprt f_get(literalt l)
std::unordered_map< unsigned, exprt > function_cachet
virtual ~qbf_bdd_certificatet(void)
qbf_bdd_certificatet(void)
virtual literalt new_variable(void)
Generate a new variable and return it as a literal.
virtual tvt l_get(literalt a) const
function_cachet function_cache
virtual modeltypet m_get(literalt a) const
virtual tvt l_get(literalt a) const
virtual literalt new_variable()
Generate a new variable and return it as a literal.
virtual const std::string solver_text()
virtual void lcnf(const bvt &bv)
virtual bool is_in_core(literalt l) const
virtual literalt lor(literalt a, literalt b)
bdd_variable_mapt bdd_variable_map
virtual resultt prop_solve()
std::vector< BDD * > bdd_variable_mapt
void compress_certificate(void)
std::vector< literalt > bvt
resultt
The result of goto verifying.