This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.
DATATYPES_HEIGHT_ZERO,
// ---------------------------------- end datatypes theory
+ //-------------------------------------- quantifiers theory
+ // skolemization
+ QUANTIFIERS_SKOLEMIZE,
+ // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent
+ QUANTIFIERS_REDUCE_ALPHA_EQ,
+ //-------------------- counterexample-guided instantiation
+ // G2 => G1 where G2 is a counterexample literal for a nested quantifier whose
+ // counterexample literal is G1.
+ QUANTIFIERS_CEGQI_CEX_DEP,
+ // 0 < delta
+ QUANTIFIERS_CEGQI_VTS_LB_DELTA,
+ // delta < c, for positive c
+ QUANTIFIERS_CEGQI_VTS_UB_DELTA,
+ // infinity > c
+ QUANTIFIERS_CEGQI_VTS_LB_INF,
+ //-------------------- sygus solver
+ // preprocessing a sygus conjecture based on quantifier elimination, of the
+ // form Q <=> Q_preprocessed
+ QUANTIFIERS_SYGUS_QE_PREPROC,
+ // G or ~G where G is the active guard for a sygus enumerator
+ QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT,
+ // manual exclusion of a current solution
+ QUANTIFIERS_SYGUS_EXCLUDE_CURRENT,
+ // manual exclusion of a current solution for sygus-stream
+ QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT,
+ // ~Q where Q is a PBE conjecture with conflicting examples
+ QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA,
+ //-------------------------------------- end quantifiers theory
+
// ---------------------------------- sep theory
// ensures that pto is a function: (pto x y) ^ ~(pto z w) ^ x = z => y != w
SEP_PTO_NEG_PROP,
d_cbqi_set_quant_inactive(false),
d_incomplete_check(false),
d_added_cbqi_lemma(qs.getUserContext()),
- d_vtsCache(new VtsTermCache(qe)),
+ d_vtsCache(new VtsTermCache(qim)),
d_bv_invert(nullptr)
{
d_small_const =
Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
Trace("cegqi-lemma")
<< "Counterexample dependency lemma : " << dep_lemma << std::endl;
- d_quantEngine->getOutputChannel().lemma(dep_lemma);
+ d_qim.lemma(dep_lemma, InferenceId::QUANTIFIERS_CEGQI_CEX_DEP);
}
//must register all sub-quantifiers of counterexample lemma, register their lemmas
DecisionStrategy* dlds = nullptr;
if (itds == d_dstrat.end())
{
- d_dstrat[q].reset(
- new DecisionStrategySingleton("CexLiteral",
- ceLit,
- d_qstate.getSatContext(),
- d_quantEngine->getValuation()));
+ d_dstrat[q].reset(new DecisionStrategySingleton("CexLiteral",
+ ceLit,
+ d_qstate.getSatContext(),
+ d_qstate.getValuation()));
dlds = d_dstrat[q].get();
}
else
Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
Node cel = getCounterexampleLiteral(q);
bool value;
- if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
+ if (d_qstate.getValuation().hasSatValue(cel, value))
+ {
Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl;
if( !value ){
- if( d_quantEngine->getValuation().isDecision( cel ) ){
+ if (d_qstate.getValuation().isDecision(cel))
+ {
Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
}else{
Trace("cegqi") << "Inactive : " << q << std::endl;
if( !delta.isNull() ){
Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
- d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
+ d_qim.lemma(delta_lem_ub, InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA);
}
std::vector< Node > inf;
d_vtsCache->getVtsTerms(inf, true, false, false);
for( unsigned i=0; i<inf.size(); i++ ){
Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
- d_quantEngine->getOutputChannel().lemma( inf_lem_lb );
+ d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF);
}
}
}
NodeManager * nm = NodeManager::currentNM();
Node g = nm->mkSkolem("g", nm->booleanType());
// ensure that it is a SAT literal
- Node ceLit = d_quantEngine->getValuation().ensureLiteral(g);
+ Node ceLit = d_qstate.getValuation().ensureLiteral(g);
d_ce_lit[q] = ceLit;
return ceLit;
}
#include "expr/node_algorithm.h"
#include "theory/arith/arith_msum.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
using namespace CVC4::kind;
namespace theory {
namespace quantifiers {
-VtsTermCache::VtsTermCache(QuantifiersEngine* qe) : d_qe(qe)
+VtsTermCache::VtsTermCache(QuantifiersInferenceManager& qim) : d_qim(qim)
{
d_zero = NodeManager::currentNM()->mkConst(Rational(0));
}
nm->realType(),
"free delta for virtual term substitution");
Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero);
- d_qe->getOutputChannel().lemma(delta_lem);
+ d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA);
}
if (d_vts_delta.isNull())
{
namespace CVC4 {
namespace theory {
-class QuantifiersEngine;
-
/** Attribute to mark Skolems as virtual terms */
struct VirtualTermSkolemAttributeId
{
namespace quantifiers {
+class QuantifiersInferenceManager;
+
/** Virtual term substitution term cache
*
* This class stores skolems corresponding to virtual terms (e.g. delta and
class VtsTermCache
{
public:
- VtsTermCache(QuantifiersEngine* qe);
+ VtsTermCache(QuantifiersInferenceManager& qim);
~VtsTermCache() {}
/**
* Get vts delta. The argument isFree indicates if we are getting the
bool containsVtsInfinity(Node n, bool isFree = false);
private:
- /** pointer to the quantifiers engine */
- QuantifiersEngine* d_qe;
+ /** Reference to the quantifiers inference manager */
+ QuantifiersInferenceManager& d_qim;
/** constants */
Node d_zero;
/** The virtual term substitution delta */
HigherOrderTrigger::HigherOrderTrigger(
QuantifiersEngine* qe,
+ quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersInferenceManager& qim,
quantifiers::QuantifiersRegistry& qr,
Node q,
std::vector<Node>& nodes,
std::map<Node, std::vector<Node> >& ho_apps)
- : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
+ : Trigger(qe, qs, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
{
NodeManager* nm = NodeManager::currentNM();
// process the higher-order variable applications
private:
HigherOrderTrigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersInferenceManager& qim,
quantifiers::QuantifiersRegistry& qr,
Node q,
if (d_is_single_trigger[patTerms[0]])
{
tr = Trigger::mkTrigger(d_quantEngine,
+ d_qstate,
d_qim,
d_qreg,
f,
}
// will possibly want to get an old trigger
tr = Trigger::mkTrigger(d_quantEngine,
+ d_qstate,
d_qim,
d_qreg,
f,
{
d_single_trigger_gen[patTerms[index]] = true;
Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
+ d_qstate,
d_qim,
d_qreg,
f,
for (size_t i = 0, usize = ugw.size(); i < usize; i++)
{
Trigger* t = Trigger::mkTrigger(d_quantEngine,
+ d_qstate,
d_qim,
d_qreg,
q,
d_user_gen_wait[q].push_back(nodes);
return;
}
- Trigger* t = Trigger::mkTrigger(
- d_quantEngine, d_qim, d_qreg, q, nodes, true, Trigger::TR_MAKE_NEW);
+ Trigger* t = Trigger::mkTrigger(d_quantEngine,
+ d_qstate,
+ d_qim,
+ d_qreg,
+ q,
+ nodes,
+ true,
+ Trigger::TR_MAKE_NEW);
if (t)
{
d_user_gen[q].push_back(t);
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers_engine.h"
using namespace CVC4::kind;
/** trigger class constructor */
Trigger::Trigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersInferenceManager& qim,
quantifiers::QuantifiersRegistry& qr,
Node q,
std::vector<Node>& nodes)
- : d_quantEngine(qe), d_qim(qim), d_qreg(qr), d_quant(q)
+ : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_quant(q)
{
// We must ensure that the ground subterms of the trigger have been
// preprocessed.
- Valuation& val = qe->getValuation();
+ Valuation& val = d_qstate.getValuation();
for (const Node& n : nodes)
{
Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms);
{
// for each ground term t that does not exist in the equality engine, we
// add a purification lemma of the form (k = t).
- eq::EqualityEngine* ee = d_quantEngine->getState().getEqualityEngine();
+ eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
for (const Node& gt : d_groundTerms)
{
if (!ee->hasTerm(gt))
}
Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersInferenceManager& qim,
quantifiers::QuantifiersRegistry& qr,
Node f,
Trigger* t;
if (!ho_apps.empty())
{
- t = new HigherOrderTrigger(qe, qim, qr, f, trNodes, ho_apps);
+ t = new HigherOrderTrigger(qe, qs, qim, qr, f, trNodes, ho_apps);
}
else
{
- t = new Trigger(qe, qim, qr, f, trNodes);
+ t = new Trigger(qe, qs, qim, qr, f, trNodes);
}
qe->getTriggerDatabase()->addTrigger( trNodes, t );
}
Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersInferenceManager& qim,
quantifiers::QuantifiersRegistry& qr,
Node f,
{
std::vector< Node > nodes;
nodes.push_back( n );
- return mkTrigger(qe, qim, qr, f, nodes, keepAll, trOption, useNVars);
+ return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars);
}
int Trigger::getActiveScore() {
class QuantifiersEngine;
namespace quantifiers {
+class QuantifiersState;
class QuantifiersInferenceManager;
class QuantifiersRegistry;
}
TR_RETURN_NULL //return null if a duplicate is found
};
static Trigger* mkTrigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersInferenceManager& qim,
quantifiers::QuantifiersRegistry& qr,
Node q,
size_t useNVars = 0);
/** single trigger version that calls the above function */
static Trigger* mkTrigger(QuantifiersEngine* qe,
+ quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersInferenceManager& qim,
quantifiers::QuantifiersRegistry& qr,
Node q,
protected:
/** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
Trigger(QuantifiersEngine* ie,
+ quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersInferenceManager& qim,
quantifiers::QuantifiersRegistry& qr,
Node q,
std::vector<Node> d_groundTerms;
/** The quantifiers engine associated with this trigger. */
QuantifiersEngine* d_quantEngine;
+ /** Reference to the quantifiers state */
+ quantifiers::QuantifiersState& d_qstate;
/** Reference to the quantifiers inference manager */
quantifiers::QuantifiersInferenceManager& d_qim;
/** The quantifiers registry */
new IntRangeDecisionHeuristic(r,
d_qstate.getSatContext(),
d_qstate.getUserContext(),
- d_quantEngine->getValuation(),
+ d_qstate.getValuation(),
isProxy));
d_quantEngine->getTheoryEngine()
->getDecisionManager()
nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] );
Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
- d_quantEngine->getOutputChannel().lemma(lem);
+ d_qim.lemma(lem, InferenceId::UNKNOWN);
}
return false;
}else{
Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts)
{
// For resource-limiting (also does a time check).
- d_qe->getOutputChannel().safePoint(ResourceManager::Resource::QuantifierStep);
+ d_qim.safePoint(ResourceManager::Resource::QuantifierStep);
Assert(!d_qstate.isInConflict());
Assert(terms.size() == q[0].getNumChildren());
Assert(d_term_db != nullptr);
namespace theory {
namespace quantifiers {
-Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p)
- : SygusModule(qe, p), d_eval_unfold(nullptr), d_usingSymCons(false)
+Cegis::Cegis(QuantifiersEngine* qe,
+ QuantifiersInferenceManager& qim,
+ SynthConjecture* p)
+ : SygusModule(qe, qim, p), d_eval_unfold(nullptr), d_usingSymCons(false)
{
d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
}
class Cegis : public SygusModule
{
public:
- Cegis(QuantifiersEngine* qe, SynthConjecture* p);
+ Cegis(QuantifiersEngine* qe,
+ QuantifiersInferenceManager& qim,
+ SynthConjecture* p);
~Cegis() override {}
/** initialize */
virtual bool initialize(Node conj,
}
CegisCoreConnective::CegisCoreConnective(QuantifiersEngine* qe,
+ QuantifiersInferenceManager& qim,
SynthConjecture* p)
- : Cegis(qe, p)
+ : Cegis(qe, qim, p)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
class CegisCoreConnective : public Cegis
{
public:
- CegisCoreConnective(QuantifiersEngine* qe, SynthConjecture* p);
+ CegisCoreConnective(QuantifiersEngine* qe,
+ QuantifiersInferenceManager& qim,
+ SynthConjecture* p);
~CegisCoreConnective() {}
/**
* Return whether this module has the possibility to construct solutions. This
CegisUnif::CegisUnif(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
SynthConjecture* p)
- : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, p)
+ : Cegis(qe, qim, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, qim, p)
{
}
<< "CegisUnif::lemma, inter-unif-enumerator "
"symmetry breaking lemma : "
<< slem << "\n";
- d_qe->getOutputChannel().lemma(slem);
+ d_qim.lemma(slem, InferenceId::UNKNOWN);
addedUnifEnumSymBreakLemma = true;
break;
}
{
Trace("cegis-unif-lemma")
<< "CegisUnif::lemma, separation lemma : " << lem << "\n";
- d_qe->getOutputChannel().lemma(lem);
+ d_qim.lemma(lem, InferenceId::UNKNOWN);
}
Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n";
return false;
}
CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
- QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* parent)
- : DecisionStrategyFmf(qs.getSatContext(), qe->getValuation()),
+ QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ SynthConjecture* parent)
+ : DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()),
d_qe(qe),
+ d_qim(qim),
d_parent(parent)
{
d_initialized = false;
// G_uq_i => size(ve) >= log_2( i-1 )
// In other words, if we use i conditions, then we allow terms in our
// solution whose size is at most log_2(i-1).
- d_qe->getOutputChannel().lemma(fair_lemma);
+ d_qim.lemma(fair_lemma, InferenceId::UNKNOWN);
}
}
Trace("cegis-unif-enum-lemma")
<< "CegisUnifEnum::lemma, remove redundant ops of " << e << " : "
<< sym_break_red_ops << "\n";
- d_qe->getOutputChannel().lemma(sym_break_red_ops);
+ d_qim.lemma(sym_break_red_ops, InferenceId::UNKNOWN);
}
// symmetry breaking between enumerators
if (!si.d_enums[index].empty() && index == 0)
Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
Trace("cegis-unif-enum-lemma")
<< "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
- d_qe->getOutputChannel().lemma(sym_break);
+ d_qim.lemma(sym_break, InferenceId::UNKNOWN);
}
// register the enumerator
si.d_enums[index].push_back(e);
Node lem = NodeManager::currentNM()->mkNode(OR, disj);
Trace("cegis-unif-enum-lemma")
<< "CegisUnifEnum::lemma, domain:" << lem << "\n";
- d_qe->getOutputChannel().lemma(lem);
+ d_qim.lemma(lem, InferenceId::UNKNOWN);
}
} // namespace quantifiers
public:
CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
SynthConjecture* parent);
/** Make the n^th literal of this strategy (G_uq_n).
*
private:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
+ /** Reference to the quantifiers inference manager */
+ QuantifiersInferenceManager& d_qim;
/** sygus term database of d_qe */
TermDbSygus* d_tds;
/** reference to the parent conjecture */
class CegisUnif : public Cegis
{
public:
- CegisUnif(QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* p);
+ CegisUnif(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ SynthConjecture* p);
~CegisUnif() override;
/** Retrieves enumerators for constructing solutions
*
namespace theory {
namespace quantifiers {
-SygusModule::SygusModule(QuantifiersEngine* qe, SynthConjecture* p)
- : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), d_parent(p)
+SygusModule::SygusModule(QuantifiersEngine* qe,
+ QuantifiersInferenceManager& qim,
+ SynthConjecture* p)
+ : d_qe(qe), d_qim(qim), d_tds(qe->getTermDatabaseSygus()), d_parent(p)
{
}
class SynthConjecture;
class TermDbSygus;
+class QuantifiersInferenceManager;
/** SygusModule
*
class SygusModule
{
public:
- SygusModule(QuantifiersEngine* qe, SynthConjecture* p);
+ SygusModule(QuantifiersEngine* qe,
+ QuantifiersInferenceManager& qim,
+ SynthConjecture* p);
virtual ~SygusModule() {}
/** initialize
*
protected:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
+ /** Reference to the quantifiers inference manager */
+ QuantifiersInferenceManager& d_qim;
/** sygus term database of d_qe */
- quantifiers::TermDbSygus* d_tds;
+ TermDbSygus* d_tds;
/** reference to the parent conjecture */
SynthConjecture* d_parent;
};
namespace theory {
namespace quantifiers {
-SygusPbe::SygusPbe(QuantifiersEngine* qe, SynthConjecture* p)
- : SygusModule(qe, p)
+SygusPbe::SygusPbe(QuantifiersEngine* qe,
+ QuantifiersInferenceManager& qim,
+ SynthConjecture* p)
+ : SygusModule(qe, qim, p)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
class SygusPbe : public SygusModule
{
public:
- SygusPbe(QuantifiersEngine* qe, SynthConjecture* p);
+ SygusPbe(QuantifiersEngine* qe,
+ QuantifiersInferenceManager& qim,
+ SynthConjecture* p);
~SygusPbe();
/** initialize this class
d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
d_sygus_rconst(new SygusRepairConst(qe)),
d_exampleInfer(new ExampleInfer(d_tds)),
- d_ceg_pbe(new SygusPbe(qe, this)),
- d_ceg_cegis(new Cegis(qe, this)),
- d_ceg_cegisUnif(new CegisUnif(qe, qs, this)),
- d_sygus_ccore(new CegisCoreConnective(qe, this)),
+ d_ceg_pbe(new SygusPbe(qe, qim, this)),
+ d_ceg_cegis(new Cegis(qe, qim, this)),
+ d_ceg_cegisUnif(new CegisUnif(qe, qs, qim, this)),
+ d_sygus_ccore(new CegisCoreConnective(qe, qim, this)),
d_master(nullptr),
d_set_ce_sk_vars(false),
d_repair_index(0),
// initialize the guard
d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
- d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard);
+ d_feasible_guard = d_qstate.getValuation().ensureLiteral(d_feasible_guard);
AlwaysAssert(!d_feasible_guard.isNull());
// pre-simplify the quantified formula based on the process utility
{
// there is a contradictory example pair, the conjecture is infeasible.
Node infLem = d_feasible_guard.negate();
- d_qe->getOutputChannel().lemma(infLem);
+ d_qim.lemma(infLem, InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA);
// we don't need to continue initialization in this case
return;
}
new DecisionStrategySingleton("sygus_feasible",
d_feasible_guard,
d_qstate.getSatContext(),
- d_qe->getValuation()));
+ d_qstate.getValuation()));
d_qe->getDecisionManager()->registerStrategy(
DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
// this must be called, both to ensure that the feasible guard is
// decided on with true polariy, but also to ensure that output channel
// has been used on this call to check.
- d_qe->getOutputChannel().requirePhase(d_feasible_guard, true);
+ d_qim.requirePhase(d_feasible_guard, true);
Node gneg = d_feasible_guard.negate();
for (unsigned i = 0; i < guarded_lemmas.size(); i++)
Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]);
Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem
<< std::endl;
- d_qe->getOutputChannel().lemma(lem);
+ d_qim.lemma(lem, InferenceId::UNKNOWN);
}
Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation()
bool value;
Assert(!d_feasible_guard.isNull());
// non or fully single invocation : look at guard only
- if (d_qe->getValuation().hasSatValue(d_feasible_guard, value))
+ if (d_qstate.getValuation().hasSatValue(d_feasible_guard, value))
{
if (!value)
{
// We should set incomplete, since a "sat" answer should not be
// interpreted as "infeasible", which would make a difference in the rare
// case where e.g. we had a finite grammar and exhausted the grammar.
- d_qe->getOutputChannel().setIncomplete();
+ d_qim.setIncomplete();
return false;
}
// otherwise we are unsat, and we will process the solution below
Node g = d_tds->getActiveGuardForEnumerator(e);
if (!g.isNull())
{
- Node gstatus = d_qe->getValuation().getSatValue(g);
+ Node gstatus = d_qstate.getValuation().getSatValue(g);
if (gstatus.isNull() || !gstatus.getConst<bool>())
{
Trace("sygus-engine-debug")
TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE);
Trace("sygus-active-gen-debug") << std::endl;
}
- d_qe->getOutputChannel().lemma(lem);
+ d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT);
}
else
{
exc_lem = exc_lem.negate();
Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : "
<< exc_lem << std::endl;
- d_qe->getOutputChannel().lemma(exc_lem);
+ d_qim.lemma(exc_lem, InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT);
}
}
Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
<< std::endl;
Trace("sygus-engine-debug") << std::endl;
- Valuation& valuation = d_quantEngine->getValuation();
+ Valuation& valuation = d_qstate.getValuation();
std::vector<SynthConjecture*> activeCheckConj;
for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
{
{
Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
<< std::endl;
- d_quantEngine->getOutputChannel().lemma(lem);
+ d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC);
// we've reduced the original to a preprocessed version, return
return;
}
// make the guard
Node ag = nm->mkSkolem("eG", nm->booleanType());
// must ensure it is a literal immediately here
- ag = d_quantEngine->getValuation().ensureLiteral(ag);
+ ag = d_qstate.getValuation().ensureLiteral(ag);
// must ensure that it is asserted as a literal before we begin solving
Node lem = nm->mkNode(OR, ag, ag.negate());
- d_quantEngine->getOutputChannel().requirePhase(ag, true);
- d_quantEngine->getOutputChannel().lemma(lem);
+ d_qim.requirePhase(ag, true);
+ d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT);
d_enum_to_active_guard[e] = ag;
}
}
Node lit = getCeLiteral(q);
bool value;
- if (d_quantEngine->getValuation().hasSatValue(lit, value))
+ if (d_qstate.getValuation().hasSatValue(lit, value))
{
if (!value)
{
- if (!d_quantEngine->getValuation().isDecision(lit))
+ if (!d_qstate.getValuation().isDecision(lit))
{
model->setQuantifierActive(q, false);
d_active_quant.erase(q);
NodeManager* nm = NodeManager::currentNM();
Node sk = nm->mkSkolem("CeLiteral", nm->booleanType());
- Node lit = d_quantEngine->getValuation().ensureLiteral(sk);
+ Node lit = d_qstate.getValuation().ensureLiteral(sk);
d_ce_lits[q] = lit;
return lit;
}
* counterexample literal is decided on first. It is user-context dependent.
*/
Assert(d_dstrat.find(q) == d_dstrat.end());
- DecisionStrategy* ds =
- new DecisionStrategySingleton("CeLiteral",
- lit,
- d_qstate.getSatContext(),
- d_quantEngine->getValuation());
+ DecisionStrategy* ds = new DecisionStrategySingleton(
+ "CeLiteral", lit, d_qstate.getSatContext(), d_qstate.getValuation());
d_dstrat[q].reset(ds);
d_quantEngine->getDecisionManager()->registerStrategy(
return d_decManager;
}
-OutputChannel& QuantifiersEngine::getOutputChannel()
-{
- return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel();
-}
-Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); }
-
quantifiers::QuantifiersState& QuantifiersEngine::getState()
{
return d_qstate;
{
if( setIncomplete ){
Trace("quant-engine") << "Set incomplete flag." << std::endl;
- getOutputChannel().setIncomplete();
+ d_qim.setIncomplete();
}
//output debug stats
d_instantiate->debugPrintModel();
BoolMap::const_iterator it = d_quants_red.find( q );
if( it==d_quants_red.end() ){
Node lem;
+ InferenceId id = InferenceId::UNKNOWN;
std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
if( itr==d_quants_red_lem.end() ){
if (d_qmodules->d_alpha_equiv)
Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
//add equivalence with another quantified formula
lem = d_qmodules->d_alpha_equiv->reduceQuantifier(q);
+ id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ;
if( !lem.isNull() ){
Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
++(d_statistics.d_red_alpha_equiv);
lem = itr->second;
}
if( !lem.isNull() ){
- getOutputChannel().lemma( lem );
+ d_qim.lemma(lem, id);
}
d_quants_red[q] = !lem.isNull();
return !lem.isNull();
Trace("quantifiers-sk-debug")
<< "Skolemize lemma : " << slem << std::endl;
}
- getOutputChannel().trustedLemma(lem, LemmaProperty::NEEDS_JUSTIFY);
+ d_qim.trustedLemma(lem,
+ InferenceId::QUANTIFIERS_SKOLEMIZE,
+ LemmaProperty::NEEDS_JUSTIFY);
}
return;
}
TheoryEngine* getTheoryEngine() const;
/** Get the decision manager */
DecisionManager* getDecisionManager();
- /** get default output channel for the quantifiers engine */
- OutputChannel& getOutputChannel();
- /** get default valuation for the quantifiers engine */
- Valuation& getValuation();
/** The quantifiers state object */
quantifiers::QuantifiersState& getState();
/** The quantifiers inference manager */
projects / cvc5.git / commitdiff