diff options
39 files changed, 225 insertions, 200 deletions
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 1563ca418..5ab606f96 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -24,13 +24,14 @@ namespace cvc5 { namespace theory { namespace arith { -InferenceManager::InferenceManager(TheoryArith& ta, +InferenceManager::InferenceManager(Env& env, + TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm) - : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::"), + : InferenceManagerBuffered(env, ta, astate, pnm, "theory::arith::"), // currently must track propagated literals if using the equality solver d_trackPropLits(astate.options().arith.arithEqSolver), - d_propLits(astate.getSatContext()) + d_propLits(context()) { } diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index eeb9d096f..d327106d7 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -46,7 +46,10 @@ class InferenceManager : public InferenceManagerBuffered using NodeSet = context::CDHashSet<Node>; public: - InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm); + InferenceManager(Env& env, + TheoryArith& ta, + ArithState& astate, + ProofNodeManager* pnm); /** * Add a lemma as pending lemma to this inference manager. diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index c28292ad3..f437d5007 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -37,18 +37,17 @@ namespace theory { namespace arith { namespace nl { -NonlinearExtension::NonlinearExtension(TheoryArith& containing, +NonlinearExtension::NonlinearExtension(Env& env, + TheoryArith& containing, ArithState& state) - : d_containing(containing), + : EnvObj(env), + d_containing(containing), d_astate(state), d_im(containing.getInferenceManager()), d_needsLastCall(false), d_checkCounter(0), d_extTheoryCb(state.getEqualityEngine()), - d_extTheory(d_extTheoryCb, - containing.getSatContext(), - containing.getUserContext(), - d_im), + d_extTheory(d_extTheoryCb, context(), userContext(), d_im), d_model(), d_trSlv(d_im, d_model, d_astate.getEnv()), d_extState(d_im, d_model, d_astate.getEnv()), @@ -94,11 +93,6 @@ void NonlinearExtension::processSideEffect(const NlLemma& se) d_trSlv.processSideEffect(se); } -const Options& NonlinearExtension::options() const -{ - return d_containing.options(); -} - void NonlinearExtension::computeRelevantAssertions( const std::vector<Node>& assertions, std::vector<Node>& keep) { diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 6cbbfcdac..f3d652281 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -21,6 +21,7 @@ #include <vector> #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/arith/nl/cad_solver.h" #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/ext/factoring_check.h" @@ -79,12 +80,12 @@ class NlLemma; * for valid arithmetic theory lemmas, based on the current set of assertions, * where d_im is the inference manager of TheoryArith. */ -class NonlinearExtension +class NonlinearExtension : EnvObj { typedef context::CDHashSet<Node> NodeSet; public: - NonlinearExtension(TheoryArith& containing, ArithState& state); + NonlinearExtension(Env& env, TheoryArith& containing, ArithState& state); ~NonlinearExtension(); /** * Does non-context dependent setup for a node connected to a theory. @@ -142,9 +143,6 @@ class NonlinearExtension /** Process side effect se */ void processSideEffect(const NlLemma& se); - /** Obtain options object */ - const Options& options() const; - private: /** Model-based refinement * diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 500b1edcd..d94f81e9c 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -40,8 +40,8 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) d_ppRewriteTimer(smtStatisticsRegistry().registerTimer( "theory::arith::ppRewriteTimer")), d_astate(env, valuation), - d_im(*this, d_astate, d_pnm), - d_ppre(getSatContext(), d_pnm), + d_im(env, *this, d_astate, d_pnm), + d_ppre(context(), d_pnm), d_bab(d_astate, d_im, d_ppre, d_pnm), d_eqSolver(nullptr), d_internal(new TheoryArithPrivate(*this, env, d_bab)), @@ -100,7 +100,8 @@ void TheoryArith::finishInit() // only need to create nonlinear extension if non-linear logic if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()) { - d_nonlinearExtension.reset(new nl::NonlinearExtension(*this, d_astate)); + d_nonlinearExtension.reset( + new nl::NonlinearExtension(d_env, *this, d_astate)); } if (d_eqSolver != nullptr) { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 347a86c1b..4efc4136a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1329,9 +1329,9 @@ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool aux, bool internal){ } d_constraintDatabase.addVariable(varX); - Debug("arith::arithvar") << "@" << getSatContext()->getLevel() - << " " << x << " |-> " << varX - << "(relaiming " << reclaim << ")" << endl; + Debug("arith::arithvar") << "@" << context()->getLevel() << " " << x + << " |-> " << varX << "(relaiming " << reclaim << ")" + << endl; Assert(!d_partialModel.hasUpperBound(varX)); Assert(!d_partialModel.hasLowerBound(varX)); @@ -1412,7 +1412,7 @@ Comparison TheoryArithPrivate::mkIntegerEqualityFromAssignment(ArithVar v){ TrustNode TheoryArithPrivate::dioCutting() { - context::Context::ScopedPush speculativePush(getSatContext()); + context::Context::ScopedPush speculativePush(context()); //DO NOT TOUCH THE OUTPUTSTREAM for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){ @@ -1872,7 +1872,7 @@ void TheoryArithPrivate::outputRestart() { } bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool emmmittedLemmaOrSplit){ - int level = getSatContext()->getLevel(); + int level = context()->getLevel(); Debug("approx") << "attemptSolveInteger " << d_qflraStatus << " " << emmmittedLemmaOrSplit @@ -1900,7 +1900,7 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em if(d_lastContextIntegerAttempted <= 0){ if(hasIntegerModel()){ - d_lastContextIntegerAttempted = getSatContext()->getLevel(); + d_lastContextIntegerAttempted = context()->getLevel(); return false; }else{ return getSolveIntegerResource(); @@ -1940,7 +1940,7 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){ d_replayedLemmas = false; /* use the try block for the purpose of pushing the sat context */ - context::Context::ScopedPush speculativePush(getSatContext()); + context::Context::ScopedPush speculativePush(context()); d_cmEnabled = false; std::vector<ConstraintCPVec> res = replayLogRec(approx, tl.getRootId(), NullConstraint, 1); @@ -2026,8 +2026,9 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const D if(d_partialModel.hasArithVar(norm)){ v = d_partialModel.asArithVar(norm); - Debug("approx::constraint") << "replayGetConstraint found " - << norm << " |-> " << v << " @ " << getSatContext()->getLevel() << endl; + Debug("approx::constraint") + << "replayGetConstraint found " << norm << " |-> " << v << " @ " + << context()->getLevel() << endl; Assert(!branch || d_partialModel.isIntegerInput(v)); }else{ v = requestArithVar(norm, true, true); @@ -2035,8 +2036,9 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const D added = v; - Debug("approx::constraint") << "replayGetConstraint adding " - << norm << " |-> " << v << " @ " << getSatContext()->getLevel() << endl; + Debug("approx::constraint") + << "replayGetConstraint adding " << norm << " |-> " << v << " @ " + << context()->getLevel() << endl; Polynomial poly = Polynomial::parsePolynomial(norm); vector<ArithVar> variables; @@ -2171,7 +2173,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc ConstraintP bcneg = bc->getNegation(); { - context::Context::ScopedPush speculativePush(getSatContext()); + context::Context::ScopedPush speculativePush(context()); replayAssert(bcneg); if(conflictQueueEmpty()){ TimerStat::CodeTimer codeTimer(d_statistics.d_replaySimplexTimer); @@ -2316,7 +2318,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex std::vector<ConstraintCPVec> res; { /* create a block for the purpose of pushing the sat context */ - context::Context::ScopedPush speculativePush(getSatContext()); + context::Context::ScopedPush speculativePush(context()); Assert(!anyConflict()); Assert(conflictQueueEmpty()); set<ConstraintCP> propagated; @@ -2758,7 +2760,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ Assert(options().arith.useApprox); Assert(ApproximateSimplex::enabled()); - int level = getSatContext()->getLevel(); + int level = context()->getLevel(); d_lastContextIntegerAttempted = level; @@ -3652,7 +3654,8 @@ void TheoryArithPrivate::debugPrintModel(std::ostream& out) const{ TrustNode TheoryArithPrivate::explain(TNode n) { - Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl; + Debug("arith::explain") << "explain @" << context()->getLevel() << ": " << n + << endl; ConstraintP c = d_constraintDatabase.lookup(n); TrustNode exp; @@ -3703,7 +3706,8 @@ void TheoryArithPrivate::propagate(Theory::Effort e) { while(d_constraintDatabase.hasMorePropagations()){ ConstraintCP c = d_constraintDatabase.nextPropagation(); - Debug("arith::prop") << "next prop" << getSatContext()->getLevel() << ": " << c << endl; + Debug("arith::prop") << "next prop" << context()->getLevel() << ": " << c + << endl; if(c->negationHasProof()){ Debug("arith::prop") << "negation has proof " << c->getNegation() << endl; @@ -3716,7 +3720,8 @@ void TheoryArithPrivate::propagate(Theory::Effort e) { if(!c->assertedToTheTheory()){ Node literal = c->getLiteral(); - Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl; + Debug("arith::prop") << "propagating @" << context()->getLevel() << " " + << literal << endl; outputPropagate(literal); }else{ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 389262fed..173579cef 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -691,7 +691,6 @@ private: inline bool isLeaf(TNode x) const { return d_containing.isLeaf(x); } inline TheoryId theoryOf(TNode x) const { return d_containing.theoryOf(x); } inline void debugPrintFacts() const { d_containing.debugPrintFacts(); } - inline context::Context* getSatContext() const { return d_containing.getSatContext(); } bool outputTrustedLemma(TrustNode lem, InferenceId id); bool outputLemma(TNode lem, InferenceId id); void outputTrustedConflict(TrustNode conf, InferenceId id); diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index 2949cf105..e59dfcc13 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -27,10 +27,11 @@ namespace cvc5 { namespace theory { namespace arrays { -InferenceManager::InferenceManager(Theory& t, +InferenceManager::InferenceManager(Env& env, + Theory& t, TheoryState& state, ProofNodeManager* pnm) - : TheoryInferenceManager(t, state, pnm, "theory::arrays::", false), + : TheoryInferenceManager(env, t, state, pnm, "theory::arrays::", false), d_lemmaPg(pnm ? new EagerProofGenerator( pnm, state.getUserContext(), "ArrayLemmaProofGenerator") : nullptr) diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h index 9b219c9b7..899df0a6b 100644 --- a/src/theory/arrays/inference_manager.h +++ b/src/theory/arrays/inference_manager.h @@ -33,7 +33,10 @@ namespace arrays { class InferenceManager : public TheoryInferenceManager { public: - InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm); + InferenceManager(Env& env, + Theory& t, + TheoryState& state, + ProofNodeManager* pnm); ~InferenceManager() {} /** diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 48b6573f8..c24290b6e 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -80,36 +80,36 @@ TheoryArrays::TheoryArrays(Env& env, name + "number of setModelVal splits")), d_numSetModelValConflicts(smtStatisticsRegistry().registerInt( name + "number of setModelVal conflicts")), - d_ppEqualityEngine(getUserContext(), name + "pp", true), - d_ppFacts(getUserContext()), + d_ppEqualityEngine(userContext(), name + "pp", true), + d_ppFacts(userContext()), d_rewriter(d_pnm), d_state(env, valuation), - d_im(*this, d_state, d_pnm), - d_literalsToPropagate(getSatContext()), - d_literalsToPropagateIndex(getSatContext(), 0), - d_isPreRegistered(getSatContext()), - d_mayEqualEqualityEngine(getSatContext(), name + "mayEqual", true), + d_im(env, *this, d_state, d_pnm), + d_literalsToPropagate(context()), + d_literalsToPropagateIndex(context(), 0), + d_isPreRegistered(context()), + d_mayEqualEqualityEngine(context(), name + "mayEqual", true), d_notify(*this), - d_infoMap(getSatContext(), name), - d_mergeQueue(getSatContext()), + d_infoMap(context(), name), + d_mergeQueue(context()), d_mergeInProgress(false), - d_RowQueue(getSatContext()), - d_RowAlreadyAdded(getUserContext()), - d_sharedArrays(getSatContext()), - d_sharedOther(getSatContext()), - d_sharedTerms(getSatContext(), false), - d_reads(getSatContext()), - d_constReadsList(getSatContext()), + d_RowQueue(context()), + d_RowAlreadyAdded(userContext()), + d_sharedArrays(context()), + d_sharedOther(context()), + d_sharedTerms(context(), false), + d_reads(context()), + d_constReadsList(context()), d_constReadsContext(new context::Context()), - d_contextPopper(getSatContext(), d_constReadsContext), - d_skolemIndex(getSatContext(), 0), - d_decisionRequests(getSatContext()), - d_permRef(getSatContext()), - d_modelConstraints(getSatContext()), - d_lemmasSaved(getSatContext()), - d_defValues(getSatContext()), + d_contextPopper(context(), d_constReadsContext), + d_skolemIndex(context(), 0), + d_decisionRequests(context()), + d_permRef(context()), + d_modelConstraints(context()), + d_lemmasSaved(context()), + d_defValues(context()), d_readTableContext(new context::Context()), - d_arrayMerges(getSatContext()), + d_arrayMerges(context()), d_inCheckModel(false), d_dstrat(new TheoryArraysDecisionStrategy(this)), d_dstratInit(false) @@ -389,21 +389,22 @@ Theory::PPAssertStatus TheoryArrays::ppAssert( bool TheoryArrays::propagateLit(TNode literal) { - Debug("arrays") << spaces(getSatContext()->getLevel()) + Debug("arrays") << spaces(context()->getLevel()) << "TheoryArrays::propagateLit(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_state.isInConflict()) { - Debug("arrays") << spaces(getSatContext()->getLevel()) + Debug("arrays") << spaces(context()->getLevel()) << "TheoryArrays::propagateLit(" << literal << "): already in conflict" << std::endl; return false; } // Propagate away - if (d_inCheckModel && getSatContext()->getLevel() != d_topLevel) { + if (d_inCheckModel && context()->getLevel() != d_topLevel) + { return true; } bool ok = d_out->propagate(literal); @@ -642,7 +643,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) { return; } - Debug("arrays") << spaces(getSatContext()->getLevel()) + Debug("arrays") << spaces(context()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl; Kind nk = node.getKind(); @@ -694,8 +695,8 @@ void TheoryArrays::preRegisterTermInternal(TNode node) d_infoMap.addIndex(store, node[1]); // Synchronize d_constReadsContext with SAT context - Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel()); - while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) + Assert(d_constReadsContext->getLevel() <= context()->getLevel()); + while (d_constReadsContext->getLevel() < context()->getLevel()) { d_constReadsContext->push(); } @@ -817,8 +818,8 @@ void TheoryArrays::preRegisterTerm(TNode node) void TheoryArrays::explain(TNode literal, Node& explanation) { ++d_numExplain; - Debug("arrays") << spaces(getSatContext()->getLevel()) - << "TheoryArrays::explain(" << literal << ")" << std::endl; + Debug("arrays") << spaces(context()->getLevel()) << "TheoryArrays::explain(" + << literal << ")" << std::endl; std::vector<TNode> assumptions; // Do the work bool polarity = literal.getKind() != kind::NOT; @@ -846,7 +847,7 @@ TrustNode TheoryArrays::explain(TNode literal) void TheoryArrays::notifySharedTerm(TNode t) { - Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) + Debug("arrays::sharing") << spaces(context()->getLevel()) << "TheoryArrays::notifySharedTerm(" << t << ")" << std::endl; if (t.getType().isArray()) { @@ -965,8 +966,9 @@ void TheoryArrays::computeCareGraph() } if (d_sharedTerms) { // Synchronize d_constReadsContext with SAT context - Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel()); - while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) { + Assert(d_constReadsContext->getLevel() <= context()->getLevel()); + while (d_constReadsContext->getLevel() < context()->getLevel()) + { d_constReadsContext->push(); } @@ -1304,7 +1306,8 @@ void TheoryArrays::postCheck(Effort level) << "Arrays::addExtLemma (weak-eq) " << lemma << "\n"; d_out->lemma(lemma, LemmaProperty::SEND_ATOMS); d_readTableContext->pop(); - Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; + Trace("arrays") << spaces(context()->getLevel()) + << "Arrays::check(): done" << endl; return; } } @@ -1326,7 +1329,8 @@ void TheoryArrays::postCheck(Effort level) } } - Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; + Trace("arrays") << spaces(context()->getLevel()) << "Arrays::check(): done" + << endl; } bool TheoryArrays::preNotifyFact( @@ -1466,7 +1470,8 @@ void TheoryArrays::setNonLinear(TNode a) if (options::arraysWeakEquivalence()) return; if (d_infoMap.isNonLinear(a)) return; - Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n"; + Trace("arrays") << spaces(context()->getLevel()) << "Arrays::setNonLinear (" + << a << ")\n"; d_infoMap.setNonLinear(a); ++d_numNonLinear; @@ -1495,7 +1500,9 @@ void TheoryArrays::setNonLinear(TNode a) TNode j = store[1]; TNode c = store[0]; lem = std::make_tuple(store, c, j, i); - Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; + Trace("arrays-lem") << spaces(context()->getLevel()) + << "Arrays::setNonLinear (" << store << ", " << c + << ", " << j << ", " << i << ")\n"; queueRowLemma(lem); } } @@ -1522,7 +1529,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) // so we take its representative to be safe. a = d_equalityEngine->getRepresentative(a); Assert(d_equalityEngine->getRepresentative(b) == a); - Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: (" << a << ", " << b << ")\n"; + Trace("arrays-merge") << spaces(context()->getLevel()) << "Arrays::merge: (" + << a << ", " << b << ")\n"; if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) { bool aNL = d_infoMap.isNonLinear(a); @@ -1642,7 +1650,9 @@ void TheoryArrays::checkStore(TNode a) { TNode j = (*js)[it]; if (i == j) continue; lem = std::make_tuple(a, b, i, j); - Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n"; + Trace("arrays-lem") << spaces(context()->getLevel()) + << "Arrays::checkStore (" << a << ", " << b << ", " + << i << ", " << j << ")\n"; queueRowLemma(lem); } } @@ -1689,7 +1699,9 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) TNode j = store[1]; if (i == j) continue; lem = std::make_tuple(store, store[0], j, i); - Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; + Trace("arrays-lem") << spaces(context()->getLevel()) + << "Arrays::checkRowForIndex (" << store << ", " + << store[0] << ", " << j << ", " << i << ")\n"; queueRowLemma(lem); } @@ -1701,7 +1713,9 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) TNode j = instore[1]; if (i == j) continue; lem = std::make_tuple(instore, instore[0], j, i); - Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; + Trace("arrays-lem") << spaces(context()->getLevel()) + << "Arrays::checkRowForIndex (" << instore << ", " + << instore[0] << ", " << j << ", " << i << ")\n"; queueRowLemma(lem); } } @@ -1749,7 +1763,9 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) TNode j = store[1]; TNode c = store[0]; lem = std::make_tuple(store, c, j, i); - Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; + Trace("arrays-lem") << spaces(context()->getLevel()) + << "Arrays::checkRowLemmas (" << store << ", " << c + << ", " << j << ", " << i << ")\n"; queueRowLemma(lem); } } @@ -1764,7 +1780,9 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) TNode j = store[1]; TNode c = store[0]; lem = std::make_tuple(store, c, j, i); - Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n"; + Trace("arrays-lem") + << spaces(context()->getLevel()) << "Arrays::checkRowLemmas (" + << store << ", " << c << ", " << j << ", " << i << ")\n"; queueRowLemma(lem); } } @@ -1800,7 +1818,9 @@ void TheoryArrays::propagateRowLemma(RowLemmaType lem) if (prop > 0) { if (d_equalityEngine->areDisequal(i, j, true) && (bothExist || prop > 1)) { - Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n"; + Trace("arrays-lem") << spaces(context()->getLevel()) + << "Arrays::queueRowLemma: propagating aj = bj (" + << aj << ", " << bj << ")\n"; Node aj_eq_bj = aj.eqNode(bj); Node reason = (i.isConst() && j.isConst()) ? d_true : i.eqNode(j).notNode(); @@ -1818,7 +1838,9 @@ void TheoryArrays::propagateRowLemma(RowLemmaType lem) } if (bothExist && d_equalityEngine->areDisequal(aj, bj, true)) { - Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n"; + Trace("arrays-lem") << spaces(context()->getLevel()) + << "Arrays::queueRowLemma: propagating i = j (" << i + << ", " << j << ")\n"; Node reason = (aj.isConst() && bj.isConst()) ? d_true : aj.eqNode(bj).notNode(); Node j_eq_i = j.eqNode(i); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index b53d0e77e..c8cff93f8 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -302,7 +302,7 @@ class TheoryArrays : public Theory { bool eqNotifyTriggerPredicate(TNode predicate, bool value) override { Debug("arrays::propagate") - << spaces(d_arrays.getSatContext()->getLevel()) + << spaces(d_arrays.context()->getLevel()) << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; // Just forward to arrays @@ -317,7 +317,10 @@ class TheoryArrays : public Theory { TNode t2, bool value) override { - Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl; + Debug("arrays::propagate") + << spaces(d_arrays.context()->getLevel()) + << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 + << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { // Propagate equality between shared terms return d_arrays.propagateLit(t1.eqNode(t2)); @@ -327,7 +330,9 @@ class TheoryArrays : public Theory { void eqNotifyConstantTermMerge(TNode t1, TNode t2) override { - Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + Debug("arrays::propagate") << spaces(d_arrays.context()->getLevel()) + << "NotifyClass::eqNotifyConstantTermMerge(" + << t1 << ", " << t2 << ")" << std::endl; d_arrays.conflict(t1, t2); } diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp index cc163e6cf..ee25861be 100644 --- a/src/theory/bags/inference_manager.cpp +++ b/src/theory/bags/inference_manager.cpp @@ -24,10 +24,11 @@ namespace cvc5 { namespace theory { namespace bags { -InferenceManager::InferenceManager(Theory& t, +InferenceManager::InferenceManager(Env& env, + Theory& t, SolverState& s, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, s, pnm, "theory::bags::"), d_state(s) + : InferenceManagerBuffered(env, t, s, pnm, "theory::bags::"), d_state(s) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h index 5ce05baba..a9e8d9121 100644 --- a/src/theory/bags/inference_manager.h +++ b/src/theory/bags/inference_manager.h @@ -38,7 +38,7 @@ class InferenceManager : public InferenceManagerBuffered typedef context::CDHashSet<Node> NodeSet; public: - InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm); + InferenceManager(Env& env, Theory& t, SolverState& s, ProofNodeManager* pnm); /** * Do pending method. This processes all pending facts, lemmas and pending diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index f8483064d..c421b9ec2 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -30,7 +30,7 @@ namespace bags { TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_BAGS, env, out, valuation), d_state(env, valuation), - d_im(*this, d_state, d_pnm), + d_im(env, *this, d_state, d_pnm), d_ig(&d_state, &d_im), d_notify(*this, d_im), d_statistics(), diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index ff718bff3..cd3b27b6e 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -29,7 +29,7 @@ TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_BUILTIN, env, out, valuation), d_checker(env), d_state(env, valuation), - d_im(*this, d_state, d_pnm, "theory::builtin::") + d_im(env, *this, d_state, d_pnm, "theory::builtin::") { // indicate we are using the default theory state and inference managers d_theoryState = &d_state; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d4926a785..7493a54c7 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -38,9 +38,9 @@ TheoryBV::TheoryBV(Env& env, d_internal(nullptr), d_rewriter(), d_state(env, valuation), - d_im(*this, d_state, nullptr, "theory::bv::"), + d_im(env, *this, d_state, nullptr, "theory::bv::"), d_notify(d_im), - d_invalidateModelCache(getSatContext(), true), + d_invalidateModelCache(context(), true), d_stats("theory::bv::") { switch (options::bvSolver()) @@ -50,8 +50,8 @@ TheoryBV::TheoryBV(Env& env, break; case options::BVSolver::LAYERED: - d_internal.reset(new BVSolverLayered( - *this, getSatContext(), getUserContext(), d_pnm, name)); + d_internal.reset( + new BVSolverLayered(*this, context(), userContext(), d_pnm, name)); break; default: diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index ccd0e6853..c9750a505 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -30,10 +30,11 @@ namespace cvc5 { namespace theory { namespace datatypes { -InferenceManager::InferenceManager(Theory& t, +InferenceManager::InferenceManager(Env& env, + Theory& t, TheoryState& state, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, state, pnm, "theory::datatypes::"), + : InferenceManagerBuffered(env, t, state, pnm, "theory::datatypes::"), d_pnm(pnm), d_ipc(pnm == nullptr ? nullptr : new InferProofCons(state.getSatContext(), pnm)), diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index 019efa950..27e0e90b6 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -38,7 +38,10 @@ class InferenceManager : public InferenceManagerBuffered friend class DatatypesInference; public: - InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm); + InferenceManager(Env& env, + Theory& t, + TheoryState& state, + ProofNodeManager* pnm); ~InferenceManager(); /** * Add pending inference, which may be processed as either a fact or diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 2162c4d14..58d0dbaab 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -51,16 +51,16 @@ TheoryDatatypes::TheoryDatatypes(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_DATATYPES, env, out, valuation), - d_term_sk(getUserContext()), - d_labels(getSatContext()), - d_selector_apps(getSatContext()), - d_collectTermsCache(getSatContext()), - d_collectTermsCacheU(getUserContext()), - d_functionTerms(getSatContext()), - d_singleton_eq(getUserContext()), + d_term_sk(userContext()), + d_labels(context()), + d_selector_apps(context()), + d_collectTermsCache(context()), + d_collectTermsCacheU(userContext()), + d_functionTerms(context()), + d_singleton_eq(userContext()), d_sygusExtension(nullptr), d_state(env, valuation), - d_im(*this, d_state, d_pnm), + d_im(env, *this, d_state, d_pnm), d_notify(d_im, *this) { @@ -129,7 +129,7 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMak if( eqc_i != d_eqc_info.end() ){ ei = eqc_i->second; }else{ - ei = new EqcInfo( getSatContext() ); + ei = new EqcInfo(context()); d_eqc_info[n] = ei; } if( n.getKind()==APPLY_CONSTRUCTOR ){ diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index bd5662cdd..ad7c1a656 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -63,16 +63,16 @@ Node buildConjunct(const std::vector<TNode> &assumptions) { TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_FP, env, out, valuation), d_notification(*this), - d_registeredTerms(getUserContext()), - d_conv(new FpConverter(getUserContext())), + d_registeredTerms(userContext()), + d_conv(new FpConverter(userContext())), d_expansionRequested(false), - d_realToFloatMap(getUserContext()), - d_floatToRealMap(getUserContext()), - d_abstractionMap(getUserContext()), - d_rewriter(getUserContext()), + d_realToFloatMap(userContext()), + d_floatToRealMap(userContext()), + d_abstractionMap(userContext()), + d_rewriter(userContext()), d_state(env, valuation), - d_im(*this, d_state, d_pnm, "theory::fp::", false), - d_wbFactsCache(getUserContext()) + d_im(env, *this, d_state, d_pnm, "theory::fp::", false), + d_wbFactsCache(userContext()) { // indicate we are using the default theory state and inference manager d_theoryState = &d_state; diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 015da9372..5b0dac776 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -24,12 +24,13 @@ using namespace cvc5::kind; namespace cvc5 { namespace theory { -InferenceManagerBuffered::InferenceManagerBuffered(Theory& t, +InferenceManagerBuffered::InferenceManagerBuffered(Env& env, + Theory& t, TheoryState& state, ProofNodeManager* pnm, const std::string& statsName, bool cacheLemmas) - : TheoryInferenceManager(t, state, pnm, statsName, cacheLemmas), + : TheoryInferenceManager(env, t, state, pnm, statsName, cacheLemmas), d_processingPendingLemmas(false) { } diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index cc4bd7ba4..202948d26 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -32,7 +32,8 @@ namespace theory { class InferenceManagerBuffered : public TheoryInferenceManager { public: - InferenceManagerBuffered(Theory& t, + InferenceManagerBuffered(Env& env, + Theory& t, TheoryState& state, ProofNodeManager* pnm, const std::string& statsName, diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index 67f8f6f8e..24159d397 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -23,12 +23,13 @@ namespace theory { namespace quantifiers { QuantifiersInferenceManager::QuantifiersInferenceManager( + Env& env, Theory& t, QuantifiersState& state, QuantifiersRegistry& qr, TermRegistry& tr, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers::"), + : InferenceManagerBuffered(env, t, state, pnm, "theory::quantifiers::"), d_instantiate(new Instantiate(state, *this, qr, tr, pnm)), d_skolemize(new Skolemize(state, tr, pnm)) { diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h index 5cb42e33c..20981a795 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.h +++ b/src/theory/quantifiers/quantifiers_inference_manager.h @@ -36,7 +36,8 @@ class FirstOrderModel; class QuantifiersInferenceManager : public InferenceManagerBuffered { public: - QuantifiersInferenceManager(Theory& t, + QuantifiersInferenceManager(Env& env, + Theory& t, QuantifiersState& state, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 67c40eaac..dff0ac979 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -37,7 +37,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, d_qstate(env, valuation, logicInfo()), d_qreg(), d_treg(d_qstate, d_qreg), - d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm), + d_qim(env, *this, d_qstate, d_qreg, d_treg, d_pnm), d_qengine(nullptr) { // construct the quantifiers engine diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index b19ba68de..e19e90634 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -44,13 +44,13 @@ namespace sep { TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_SEP, env, out, valuation), - d_lemmas_produced_c(getUserContext()), + d_lemmas_produced_c(userContext()), d_bounds_init(false), d_state(env, valuation), - d_im(*this, d_state, d_pnm, "theory::sep::"), + d_im(env, *this, d_state, d_pnm, "theory::sep::"), d_notify(*this), - d_reduce(getUserContext()), - d_spatial_assertions(getSatContext()) + d_reduce(userContext()), + d_spatial_assertions(context()) { d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); @@ -467,7 +467,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) << std::endl; Node g = sm->mkDummySkolem("G", nm->booleanType()); d_neg_guard_strategy[g].reset(new DecisionStrategySingleton( - "sep_neg_guard", g, getSatContext(), getValuation())); + "sep_neg_guard", g, context(), getValuation())); DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get(); d_im.getDecisionManager()->registerStrategy( DecisionManager::STRAT_SEP_NEG_GUARD, ds); @@ -921,7 +921,7 @@ TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) { std::map< Node, HeapAssertInfo* >::iterator e_i = d_eqc_info.find( n ); if( e_i==d_eqc_info.end() ){ if( doMake ){ - HeapAssertInfo* ei = new HeapAssertInfo( getSatContext() ); + HeapAssertInfo* ei = new HeapAssertInfo(context()); d_eqc_info[n] = ei; return ei; }else{ diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index d0dc21839..58fcbdae9 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -25,10 +25,11 @@ namespace cvc5 { namespace theory { namespace sets { -InferenceManager::InferenceManager(Theory& t, +InferenceManager::InferenceManager(Env& env, + Theory& t, SolverState& s, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, s, pnm, "theory::sets::"), d_state(s) + : InferenceManagerBuffered(env, t, s, pnm, "theory::sets::"), d_state(s) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index 0a7c42e11..a9016ac3d 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -39,7 +39,7 @@ class InferenceManager : public InferenceManagerBuffered typedef context::CDHashSet<Node> NodeSet; public: - InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm); + InferenceManager(Env& env, Theory& t, SolverState& s, ProofNodeManager* pnm); /** * Add facts corresponding to ( exp => fact ) via calls to the assertFact * method of TheorySetsPrivate. diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 8759f7056..833f4b22d 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -31,8 +31,9 @@ TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_SETS, env, out, valuation), d_skCache(), d_state(env, valuation, d_skCache), - d_im(*this, d_state, d_pnm), - d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, d_pnm)), + d_im(env, *this, d_state, d_pnm), + d_internal( + new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_pnm)), d_notify(*d_internal.get(), d_im) { // use the official theory state and inference manager objects diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 3817079a3..8073b4c2a 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -36,13 +36,15 @@ namespace cvc5 { namespace theory { namespace sets { -TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, +TheorySetsPrivate::TheorySetsPrivate(Env& env, + TheorySets& external, SolverState& state, InferenceManager& im, SkolemCache& skc, ProofNodeManager* pnm) - : d_deq(state.getSatContext()), - d_termProcessed(state.getUserContext()), + : EnvObj(env), + d_deq(context()), + d_termProcessed(userContext()), d_fullCheckIncomplete(false), d_fullCheckIncompleteId(IncompleteId::UNKNOWN), d_external(external), @@ -178,7 +180,7 @@ TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo(TNode n, EqcInfo* ei = NULL; if (doMake) { - ei = new EqcInfo(d_external.getSatContext()); + ei = new EqcInfo(context()); d_eqc_info[n] = ei; } return ei; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 3b5ee2390..94ca86e61 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -21,6 +21,7 @@ #include "context/cdhashset.h" #include "context/cdqueue.h" #include "expr/node_trie.h" +#include "smt/env_obj.h" #include "theory/sets/cardinality_extension.h" #include "theory/sets/inference_manager.h" #include "theory/sets/solver_state.h" @@ -37,7 +38,8 @@ namespace sets { /** Internal classes, forward declared here */ class TheorySets; -class TheorySetsPrivate { +class TheorySetsPrivate : protected EnvObj +{ typedef context::CDHashMap<Node, bool> NodeBoolMap; typedef context::CDHashSet<Node> NodeSet; @@ -133,7 +135,8 @@ class TheorySetsPrivate { * Constructs a new instance of TheorySetsPrivate w.r.t. the provided * contexts. */ - TheorySetsPrivate(TheorySets& external, + TheorySetsPrivate(Env& env, + TheorySets& external, SolverState& state, InferenceManager& im, SkolemCache& skc, @@ -234,7 +237,7 @@ class TheorySetsPrivate { /** a map that maps each set to an existential quantifier generated for * operator is_singleton */ std::map<Node, Node> d_isSingletonNodes; -};/* class TheorySetsPrivate */ +}; /* class TheorySetsPrivate */ } // namespace sets } // namespace theory diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 94d99732a..0e971fc54 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -30,19 +30,19 @@ namespace cvc5 { namespace theory { namespace strings { -InferenceManager::InferenceManager(Theory& t, +InferenceManager::InferenceManager(Env& env, + Theory& t, SolverState& s, TermRegistry& tr, ExtTheory& e, SequencesStatistics& statistics, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, s, pnm, "theory::strings::", false), + : InferenceManagerBuffered(env, t, s, pnm, "theory::strings::", false), d_state(s), d_termReg(tr), d_extt(e), d_statistics(statistics), - d_ipc(pnm ? new InferProofCons(d_state.getSatContext(), pnm, d_statistics) - : nullptr) + d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index da44100f9..49f10d7cb 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -77,7 +77,8 @@ class InferenceManager : public InferenceManagerBuffered friend class InferInfo; public: - InferenceManager(Theory& t, + InferenceManager(Env& env, + Theory& t, SolverState& s, TermRegistry& tr, ExtTheory& e, diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8b71df31b..3e807c3ac 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -58,8 +58,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_eagerSolver(d_state), d_termReg(d_state, d_statistics, d_pnm), d_extTheoryCb(), - d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), - d_extTheory(d_extTheoryCb, getSatContext(), getUserContext(), d_im), + d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), + d_extTheory(d_extTheoryCb, context(), userContext(), d_im), d_rewriter(&d_statistics.d_rewrites), d_bsolver(d_state, d_im), d_csolver(d_state, d_im, d_termReg, d_bsolver), @@ -77,8 +77,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_csolver, d_esolver, d_statistics), - d_regexp_elim(options::regExpElimAgg(), d_pnm, getUserContext()), - d_stringsFmf(getSatContext(), getUserContext(), valuation, d_termReg) + d_regexp_elim(options::regExpElimAgg(), d_pnm, userContext()), + d_stringsFmf(context(), userContext(), valuation, d_termReg) { d_termReg.finishInit(&d_im); @@ -370,7 +370,7 @@ bool TheoryStrings::collectModelInfoType( argVal = nfe.d_nf[0][0]; } Assert(!argVal.isNull()) << "No value for " << nfe.d_nf[0][0]; - Node c = Rewriter::rewrite(nm->mkNode(SEQ_UNIT, argVal)); + Node c = rewrite(nm->mkNode(SEQ_UNIT, argVal)); pure_eq_assign[eqc] = c; Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") "; m->getEqualityEngine()->addTerm(c); @@ -914,7 +914,7 @@ void TheoryStrings::checkCodes() Trace("strings-code-debug") << "Get proxy variable for " << c << std::endl; Node cc = nm->mkNode(kind::STRING_TO_CODE, c); - cc = Rewriter::rewrite(cc); + cc = rewrite(cc); Assert(cc.isConst()); Node cp = d_termReg.ensureProxyVariableFor(c); Node vc = nm->mkNode(STRING_TO_CODE, cp); @@ -958,7 +958,7 @@ void TheoryStrings::checkCodes() Node eqn = c1[0].eqNode(c2[0]); // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn); - deq = Rewriter::rewrite(deq); + deq = rewrite(deq); d_im.addPendingPhaseRequirement(deq, false); std::vector<Node> emptyVec; d_im.sendInference(emptyVec, inj_lem, InferenceId::STRINGS_CODE_INJ); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 0c2624d64..44b3da53e 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -132,11 +132,8 @@ void Theory::finishInitStandalone() if (needsEqualityEngine(esi)) { // always associated with the same SAT context as the theory - d_allocEqualityEngine.reset( - new eq::EqualityEngine(*esi.d_notify, - getSatContext(), - esi.d_name, - esi.d_constantsAreTriggers)); + d_allocEqualityEngine.reset(new eq::EqualityEngine( + *esi.d_notify, context(), esi.d_name, esi.d_constantsAreTriggers)); // use it as the official equality engine setEqualityEngine(d_allocEqualityEngine.get()); } diff --git a/src/theory/theory.h b/src/theory/theory.h index 371d8f76a..a59ee5c5f 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -459,29 +459,6 @@ class Theory : protected EnvObj TheoryId getId() const { return d_id; } /** - * Get a reference to the environment. - */ - Env& getEnv() const { return d_env; } - - /** - * Shorthand to access the options object. - */ - const Options& options() const { return getEnv().getOptions(); } - - /** - * Get the SAT context associated to this Theory. - */ - context::Context* getSatContext() const { return d_env.getContext(); } - - /** - * Get the context associated to this Theory. - */ - context::UserContext* getUserContext() const - { - return d_env.getUserContext(); - } - - /** * Get the output channel associated to this theory. */ OutputChannel& getOutputChannel() { return *d_out; } @@ -520,7 +497,7 @@ class Theory : protected EnvObj void assertFact(TNode assertion, bool isPreregistered) { Trace("theory") << "Theory<" << getId() << ">::assertFact[" - << getSatContext()->getLevel() << "](" << assertion << ", " + << context()->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl; d_facts.push_back(Assertion(assertion, isPreregistered)); } diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 1c47c00c4..f83d92158 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -29,12 +29,14 @@ using namespace cvc5::kind; namespace cvc5 { namespace theory { -TheoryInferenceManager::TheoryInferenceManager(Theory& t, +TheoryInferenceManager::TheoryInferenceManager(Env& env, + Theory& t, TheoryState& state, ProofNodeManager* pnm, const std::string& statsName, bool cacheLemmas) - : d_theory(t), + : EnvObj(env), + d_theory(t), d_theoryState(state), d_out(t.getOutputChannel()), d_ee(nullptr), @@ -42,8 +44,8 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t, d_pfee(nullptr), d_pnm(pnm), d_cacheLemmas(cacheLemmas), - d_keep(t.getSatContext()), - d_lemmasSent(t.getUserContext()), + d_keep(context()), + d_lemmasSent(userContext()), d_numConflicts(0), d_numCurrentLemmas(0), d_numCurrentFacts(0), @@ -75,10 +77,8 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) d_pfee = d_ee->getProofEqualityEngine(); if (d_pfee == nullptr) { - d_pfeeAlloc.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(), - d_theoryState.getUserContext(), - *d_ee, - d_pnm)); + d_pfeeAlloc.reset( + new eq::ProofEqEngine(context(), userContext(), *d_ee, d_pnm)); d_pfee = d_pfeeAlloc.get(); d_ee->setProofEqualityEngine(d_pfee); } diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index cea0e698b..221d25fae 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -24,6 +24,7 @@ #include "expr/node.h" #include "proof/proof_rule.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" #include "theory/inference_id.h" #include "theory/output_channel.h" #include "util/statistics_stats.h" @@ -66,7 +67,7 @@ class ProofEqEngine; * setEqualityEngine, and use it for handling variants of assertInternalFact * below that involve proofs. */ -class TheoryInferenceManager +class TheoryInferenceManager : protected EnvObj { typedef context::CDHashSet<Node> NodeSet; @@ -85,7 +86,8 @@ class TheoryInferenceManager * only lemmas that are unique after rewriting are sent to the theory engine * from this inference manager. */ - TheoryInferenceManager(Theory& t, + TheoryInferenceManager(Env& env, + Theory& t, TheoryState& state, ProofNodeManager* pnm, const std::string& statsName, diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index bdc5304e4..07820a41d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -47,11 +47,11 @@ TheoryUF::TheoryUF(Env& env, : Theory(THEORY_UF, env, out, valuation, instanceName), d_thss(nullptr), d_ho(nullptr), - d_functionsTerms(getSatContext()), + d_functionsTerms(context()), d_symb(userContext(), instanceName), d_rewriter(logicInfo().isHigherOrder()), d_state(env, valuation), - d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false), + d_im(env, *this, d_state, d_pnm, "theory::uf::" + instanceName, false), d_notify(d_im, *this) { d_true = NodeManager::currentNM()->mkConst( true ); |