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);
72 #endif // CPROVER_SOLVERS_QBF_QBF_BDD_CORE_H virtual bool is_in_core(literalt l) const
virtual void lcnf(const bvt &bv)
virtual resultt prop_solve()
virtual const std::string solver_text()
virtual literalt new_variable(void)
Generate a new variable and return it as a literal.
virtual tvt l_get(literalt a) const
qbf_bdd_certificatet(void)
virtual literalt lor(literalt a, literalt b)
virtual tvt l_get(literalt a) const
virtual modeltypet m_get(literalt a) const
std::vector< BDD * > bdd_variable_mapt
bdd_variable_mapt bdd_variable_map
std::unordered_map< unsigned, exprt > function_cachet
function_cachet function_cache
virtual ~qbf_bdd_certificatet(void)
std::vector< BDD * > model_bddst
Base class for all expressions.
void compress_certificate(void)
virtual const exprt f_get(literalt l)
virtual literalt new_variable()
Generate a new variable and return it as a literal.
std::vector< literalt > bvt