10 #ifndef CPROVER_SOLVERS_QBF_QBF_QUBE_CORE_H 11 #define CPROVER_SOLVERS_QBF_QBF_QUBE_CORE_H 38 assignmentt::const_iterator fit=
assignment.find(v);
41 return a.
sign()?
tvt(!fit->second) :
tvt(fit->second);
56 INVARIANT(
false,
"qube does not support full certificates.");
60 #endif // CPROVER_SOLVERS_QBF_QBF_QUBE_CORE_H
virtual bool is_in_core(literalt l) const
virtual ~qbf_qube_coret()
virtual tvt l_get(literalt a) const
virtual const std::string solver_text()
virtual const exprt f_get(literalt)
virtual modeltypet m_get(literalt a) const
virtual resultt prop_solve()
Base class for all expressions.
std::map< unsigned, bool > assignmentt