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.");
Base class for all expressions.
virtual const std::string solver_text()
virtual tvt l_get(literalt a) const
std::map< unsigned, bool > assignmentt
virtual modeltypet m_get(literalt a) const
virtual resultt prop_solve()
virtual const exprt f_get(literalt)
virtual ~qbf_qube_coret()
virtual bool is_in_core(literalt l) const
resultt
The result of goto verifying.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.