10#ifndef CPROVER_SOLVERS_QBF_QBF_QUBE_CORE_H
11#define CPROVER_SOLVERS_QBF_QBF_QUBE_CORE_H
36 unsigned v=
a.var_no();
56 INVARIANT(
false,
"qube does not support full certificates.");
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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'.