Use `EnvObj` methods instead of `Theory` methods (#7144)

This removes the methods `getEnv()`, `options()`, `getSatContext()`, and
`getUserContext()` from the `Theory` class because they are now part of
`EnvObj`. Additionally, this commit converts the inference managers to
`EnvObj` because of there were some calls to retrieve the contexts from
`Theory` in those classes.

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 1563ca418ad718e6acf0b7973e81059f9e976049..5ab606f96456626a490bc8bebe421af5b80ce3d7 100644 (file)
--- 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 eeb9d096f8abd3dfb4750055384cdcc7a67086eb..d327106d733750340cfbb0e766cfc82c3885f155 100644 (file)
--- 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 c28292ad346fd29ad5905e18a6ac0681f3b06c02..f437d5007afb8b79b422cb10ec2140899803d948 100644 (file)
--- 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 6cbbfcdac5e93ffdcdaf166979d9783dbecabb53..f3d6522811a992c8fd4e25cbcdbb253a7de274bc 100644 (file)
--- 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 500b1edcdc4441f90177e458530601733b097b3b..d94f81e9c737ace930c1826c0674a451a54eca2d 100644 (file)
--- 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 347a86c1b297b4828b9df945a6cf09a6a370aad7..4efc4136a13ae0dc396c8c605edb0f5c02b89af0 100644 (file)
--- 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 389262fed14380b95cac3e672a0bd9101d26d955..173579ceff0965f66b14fbf4ffd603a5e4ce570c 100644 (file)
--- 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 2949cf1057e404b6e9b8a80fd401bb225bc46b1c..e59dfcc1349a8617bb43bcfecd77811d609ab711 100644 (file)
--- 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 9b219c9b78fbaa58c08c651970d47d0aa94fb1d2..899df0a6be89ac7da8e2da8a558fc1857fbc117c 100644 (file)
--- 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 48b6573f826eb1853ce72f83a2af189df9a6d81e..c24290b6edcbbe387c4e5813b7a228b2fe6e567c 100644 (file)
--- 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 b53d0e77e39d0e5067cfe7434fb8e2c370bc37cd..c8cff93f88f5a1856e8d2440b444b28ee78c9c38 100644 (file)
--- 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 cc163e6cf859952baa2a63834fb5bb3644e7787a..ee25861be3b4d3f1d34f30055d46ae4e125c60b1 100644 (file)
--- 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 5ce05babacadb8aaca39f0115c60fbde0e55e39c..a9e8d9121fced6f693a23dd48cc96cd5853b7935 100644 (file)
--- 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 f8483064d59030e2fcac5e64e393a36f84c60498..c421b9ec210eaf1efbd42ca19039100cb630d00d 100644 (file)
--- 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 ff718bff38d5d4b7ba1139d62ef314812782a683..cd3b27b6e7180ca59e20eff254764158c6cc9668 100644 (file)
--- 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 d4926a785413a469115088f70b8c0aee99c9d893..7493a54c71692e63af95f73ba966c6967ec58ff2 100644 (file)
--- 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 ccd0e685348e428b64f16b5196cc778e08039ad4..c9750a5050e2ccc604781c53113cb89bb9b4d09c 100644 (file)
--- 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 019efa950b01e10c6b73dcadceaba9cefdb64e81..27e0e90b6d2e260479a4d7ccd1e57f01c6b1b59e 100644 (file)
--- 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 2162c4d14a094f13b1a47fa129d2dcd6a08db232..58d0dbaab99ceda41e72508ea862f9475a7b2612 100644 (file)
--- 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 bd5662cdd81637786876f96939e042817271cedd..ad7c1a656c5a8d2cb573b2f2af1a040c01a5cc01 100644 (file)
--- 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 015da9372be83df7557190ef177fc76f4e81d4a9..5b0dac776c149ee1cf1ea38cea10567464955d75 100644 (file)
--- 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 cc4bd7ba4c8a6f418dde87ec52ab6a1c0f481053..202948d26d85bdd9872230158166b56d943dfc06 100644 (file)
--- 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 67f8f6f8e77d45acf5dccb8bcaa7ab60359b8758..24159d397a761a530814ce5e2b834bbf267d6617 100644 (file)
--- 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 5cb42e33c11a1ebb8a7dccef08d8cee9c50fa23c..20981a795953debc9b117b12551f44d974f5cf0d 100644 (file)
--- 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 67c40eaacbaa9599f99d4d43a08d8874f1bc52cc..dff0ac979262f8d96755363374926cd9cfff377b 100644 (file)
--- 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 b19ba68deff9f462205dd54a4ba2ba2df29577e6..e19e9063498e9ad7667302eca96bb8924351767a 100644 (file)
--- 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 d0dc2183969ff387b7c0d0ef2f96f3593ab5f195..58fcbdae988254928928c6ac73b127f8cc92c7a2 100644 (file)
--- 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 0a7c42e11bab4e8f730786dbf10d1f4410f8d133..a9016ac3d11a1eee2f17090d756a39186db60c3f 100644 (file)
--- 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 8759f705661ce1f2e1d3ea767df600739ece6722..833f4b22d0d1874b1e597e3a1df392aaea6adc98 100644 (file)
--- 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 3817079a31bc47d73c98ea56f37429edde34f70c..8073b4c2acd2f3fc32b310b024f24f53d03ee8d0 100644 (file)
--- 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 3b5ee23905a571d1a37bdbe867029b2bc0a44b20..94ca86e613304707a0fa870c3e03ca0d771945c7 100644 (file)
--- 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 94d99732aa0d74941504f8493d2aee4be701f550..0e971fc54c0b7aa0df4cca6c147d2073831104e7 100644 (file)
--- 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 da44100f99be0f9f71d824f846483919b855a894..49f10d7cbff0109dfec9af7f3f97d9f5177cf519 100644 (file)
--- 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 8b71df31bd2b66bfa6bb30d2cd7ff640818e7e75..3e807c3ac0c835482496748f88642e3197d705e9 100644 (file)
--- 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 0c2624d6401db583a436e3ea29db08314b2f010f..44b3da53ef1b8d0d4c610898d24578d889363d23 100644 (file)
--- 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 371d8f76a37264e5d319b6b25a6a3ef9cc4663d4..a59ee5c5fdf6abf063016b331c1944477c1afd0b 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -458,29 +458,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.
    */
@@ -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 1c47c00c4be7e8a90560614ae4e128d489215112..f83d92158ed8e6b4af427ae891000150c9ff4fc4 100644 (file)
--- 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 cea0e698bdb7c0f473085c32eb1a31d4744b48db..221d25fae64e1b5cc9d8f4639584f7fd023f718e 100644 (file)
--- 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 bdc5304e47888278dfc2ce007ebe1568f94b73ea..07820a41d5a5ef120661ba57fadd3ac7e975ce1b 100644 (file)
--- 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 );