Eliminate more hard coded uses of user context (#7309)

This is in preparation to make the "lemma context" configurable.

18 files changed, 45 insertions, 54 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index f7d274484..e419f3ae1 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -53,8 +53,6 @@ ArithCongruenceManager::ArithCongruenceManager(
       d_setupLiteral(setup),
       d_avariables(avars),
       d_ee(nullptr),
-      d_satContext(context()),
-      d_userContext(userContext()),
       d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
                                            : nullptr),
       // Construct d_pfGenEe with the SAT context, since its proof include
@@ -84,13 +82,13 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee)
   {
     // use our own copy
     d_allocEe.reset(
-        new eq::EqualityEngine(d_notify, d_satContext, "arithCong::ee", true));
+        new eq::EqualityEngine(d_notify, context(), "arithCong::ee", true));
     d_ee = d_allocEe.get();
     if (d_pnm != nullptr)
     {
       // allocate an internal proof equality engine
       d_allocPfee.reset(
-          new eq::ProofEqEngine(d_satContext, d_userContext, *d_ee, d_pnm));
+          new eq::ProofEqEngine(context(), userContext(), *d_ee, d_pnm));
       d_ee->setProofEqualityEngine(d_allocPfee.get());
     }
   }
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 3050f5821..b847c63ae 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -114,11 +114,6 @@ class ArithCongruenceManager : protected EnvObj
   eq::EqualityEngine* d_ee;
   /** The equality engine we allocated */
   std::unique_ptr<eq::EqualityEngine> d_allocEe;
-  /** The sat context */
-  context::Context* d_satContext;
-  /** The user context */
-  context::UserContext* d_userContext;
-
   /** proof manager */
   ProofNodeManager* d_pnm;
   /** A proof generator for storing proofs of facts that are asserted to the EQ
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 207907fcc..a970abc45 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -47,7 +47,7 @@ NonlinearExtension::NonlinearExtension(Env& env,
       d_hasNlTerms(false),
       d_checkCounter(0),
       d_extTheoryCb(state.getEqualityEngine()),
-      d_extTheory(d_extTheoryCb, context(), userContext(), d_im),
+      d_extTheory(env, d_extTheoryCb, d_im),
       d_model(),
       d_trSlv(d_im, d_model, d_env),
       d_extState(d_im, d_model, d_env),
diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index 627129c3a..9eb6e3cdc 100644
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -81,18 +81,16 @@ bool ExtTheoryCallback::getReduction(int effort,
   return false;
 }
 
-ExtTheory::ExtTheory(ExtTheoryCallback& p,
-                     context::Context* c,
-                     context::UserContext* u,
-                     TheoryInferenceManager& im)
-    : d_parent(p),
+ExtTheory::ExtTheory(Env& env, ExtTheoryCallback& p, TheoryInferenceManager& im)
+    : EnvObj(env),
+      d_parent(p),
       d_im(im),
-      d_ext_func_terms(c),
-      d_extfExtReducedIdMap(c),
-      d_ci_inactive(u),
-      d_has_extf(c),
-      d_lemmas(u),
-      d_pp_lemmas(u)
+      d_ext_func_terms(context()),
+      d_extfExtReducedIdMap(context()),
+      d_ci_inactive(userContext()),
+      d_has_extf(context()),
+      d_lemmas(userContext()),
+      d_pp_lemmas(userContext())
 {
   d_true = NodeManager::currentNM()->mkConst(true);
 }
@@ -260,7 +258,7 @@ bool ExtTheory::doInferencesInternal(int effort,
         bool processed = false;
         if (sterms[i] != terms[i])
         {
-          Node sr = Rewriter::rewrite(sterms[i]);
+          Node sr = rewrite(sterms[i]);
           // ask the theory if this term is reduced, e.g. is it constant or it
           // is a non-extf term.
           ExtReducedId id;
diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h
index 01b191e0a..998dac146 100644
--- a/src/theory/ext_theory.h
+++ b/src/theory/ext_theory.h
@@ -41,6 +41,7 @@
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/theory_inference_manager.h"
 
 namespace cvc5 {
@@ -163,7 +164,7 @@ class ExtTheoryCallback
  * underlying theory for a "derivable substitution", whereby extended functions
  * may be reducable.
  */
-class ExtTheory
+class ExtTheory : protected EnvObj
 {
   using NodeBoolMap = context::CDHashMap<Node, bool>;
   using NodeExtReducedIdMap = context::CDHashMap<Node, ExtReducedId>;
@@ -174,10 +175,7 @@ class ExtTheory
    *
    * If cacheEnabled is false, we do not cache results of getSubstitutedTerm.
    */
-  ExtTheory(ExtTheoryCallback& p,
-            context::Context* c,
-            context::UserContext* u,
-            TheoryInferenceManager& im);
+  ExtTheory(Env& env, ExtTheoryCallback& p, TheoryInferenceManager& im);
   virtual ~ExtTheory() {}
   /** Tells this class to treat terms with Kind k as extended functions */
   void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index d5f06b6e9..da3e506fc 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -54,7 +54,7 @@ void CandidateRewriteFilter::initialize(SygusSampler* ss,
   ssn << "_dyn_rewriter_" << drewrite_counter;
   drewrite_counter++;
   d_drewrite = std::unique_ptr<DynamicRewriter>(
-      new DynamicRewriter(ssn.str(), &d_fake_context));
+      new DynamicRewriter(ssn.str(), &d_fakeContext));
 }
 
 bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h
index 4995dc7c2..527632786 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.h
+++ b/src/theory/quantifiers/candidate_rewrite_filter.h
@@ -104,8 +104,8 @@ class CandidateRewriteFilter
   bool d_use_sygus_type;
 
   //----------------------------congruence filtering
-  /** a (dummy) user context, used for d_drewrite */
-  context::UserContext d_fake_context;
+  /** a (dummy) context, used for d_drewrite */
+  context::Context d_fakeContext;
   /** dynamic rewriter class */
   std::unique_ptr<DynamicRewriter> d_drewrite;
   //----------------------------end congruence filtering
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index 4d69ea732..1fc08b288 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -25,9 +25,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-DynamicRewriter::DynamicRewriter(const std::string& name,
-                                 context::UserContext* u)
-    : d_equalityEngine(u, "DynamicRewriter::" + name, true), d_rewrites(u)
+DynamicRewriter::DynamicRewriter(const std::string& name, context::Context* c)
+    : d_equalityEngine(c, "DynamicRewriter::" + name, true), d_rewrites(c)
 {
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 }
diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
index 3187b7c03..5e1f45b35 100644
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -55,7 +55,7 @@ class DynamicRewriter
   typedef context::CDList<Node> NodeList;
 
  public:
-  DynamicRewriter(const std::string& name, context::UserContext* u);
+  DynamicRewriter(const std::string& name, context::Context* c);
   ~DynamicRewriter() {}
   /** inform this class that the equality a = b holds. */
   void addRewrite(Node a, Node b);
diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp
index e1a342178..a83167591 100644
--- a/src/theory/relevance_manager.cpp
+++ b/src/theory/relevance_manager.cpp
@@ -25,10 +25,9 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace theory {
 
-RelevanceManager::RelevanceManager(context::UserContext* userContext,
-                                   Valuation val)
+RelevanceManager::RelevanceManager(context::Context* lemContext, Valuation val)
     : d_val(val),
-      d_input(userContext),
+      d_input(lemContext),
       d_computed(false),
       d_success(false),
       d_trackRSetExp(false),
@@ -36,7 +35,7 @@ RelevanceManager::RelevanceManager(context::UserContext* userContext,
 {
   if (options::produceDifficulty())
   {
-    d_dman.reset(new DifficultyManager(userContext, val));
+    d_dman.reset(new DifficultyManager(lemContext, val));
     d_trackRSetExp = true;
     // we cannot miniscope AND at the top level, since we need to
     // preserve the exact form of preprocessed assertions so the dependencies
diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h
index f8cd8e1ee..287694445 100644
--- a/src/theory/relevance_manager.h
+++ b/src/theory/relevance_manager.h
@@ -76,7 +76,11 @@ class RelevanceManager
   typedef context::CDList<Node> NodeList;
 
  public:
-  RelevanceManager(context::UserContext* userContext, Valuation val);
+  /**
+   * @param lemContext The context which lemmas live at
+   * @param val The valuation class, for computing what is relevant.
+   */
+  RelevanceManager(context::Context* lemContext, Valuation val);
   /**
    * Notify (preprocessed) assertions. This is called for input formulas or
    * lemmas that need justification that have been fully processed, just before
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index e4f1b6fab..6c0f6ae10 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -37,8 +37,6 @@ SharedTermsDatabase::SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine)
       d_theoryEngine(theoryEngine),
       d_inConflict(env.getContext(), false),
       d_conflictPolarity(),
-      d_satContext(env.getContext()),
-      d_userContext(env.getUserContext()),
       d_equalityEngine(nullptr),
       d_pfee(nullptr)
 {
@@ -55,8 +53,8 @@ void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
     if (d_pfee == nullptr)
     {
       ProofNodeManager* pnm = d_env.getProofNodeManager();
-      d_pfeeAlloc.reset(
-          new eq::ProofEqEngine(d_satContext, d_userContext, *ee, pnm));
+      d_pfeeAlloc.reset(new eq::ProofEqEngine(
+          d_env.getContext(), d_env.getUserContext(), *ee, pnm));
       d_pfee = d_pfeeAlloc.get();
       d_equalityEngine->setProofEqualityEngine(d_pfee);
     }
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 3b21c27a8..2bdb9d574 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -266,10 +266,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
    * This method gets called on backtracks from the context manager.
    */
   void contextNotifyPop() override { backtrack(); }
-  /** The SAT search context. */
-  context::Context* d_satContext;
-  /** The user level assertion context. */
-  context::UserContext* d_userContext;
   /** Equality engine */
   theory::eq::EqualityEngine* d_equalityEngine;
   /** Proof equality engine, if we allocated one */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ac6d9b611..27640341a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -59,7 +59,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
       d_termReg(env, d_state, d_statistics, d_pnm),
       d_extTheoryCb(),
       d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm),
-      d_extTheory(d_extTheoryCb, context(), userContext(), d_im),
+      d_extTheory(env, d_extTheoryCb, d_im),
       d_rewriter(env.getRewriter(), &d_statistics.d_rewrites),
       d_bsolver(env, d_state, d_im),
       d_csolver(env, d_state, d_im, d_termReg, d_bsolver),
diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp
index 073accdae..eaa9a1746 100644
--- a/src/theory/theory_engine_proof_generator.cpp
+++ b/src/theory/theory_engine_proof_generator.cpp
@@ -24,8 +24,8 @@ using namespace cvc5::kind;
 namespace cvc5 {
 
 TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm,
-                                                       context::UserContext* u)
-    : d_pnm(pnm), d_proofs(u)
+                                                       context::Context* c)
+    : d_pnm(pnm), d_proofs(c)
 {
   d_false = NodeManager::currentNM()->mkConst(false);
 }
diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h
index 68f7dea32..1cb99b039 100644
--- a/src/theory/theory_engine_proof_generator.h
+++ b/src/theory/theory_engine_proof_generator.h
@@ -42,7 +42,7 @@ class TheoryEngineProofGenerator : public ProofGenerator
       NodeLazyCDProofMap;
 
  public:
-  TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u);
+  TheoryEngineProofGenerator(ProofNodeManager* pnm, context::Context* c);
   ~TheoryEngineProofGenerator() {}
   /**
    * Make trust explanation. Called when lpf has a proof of lit from free
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index ca8b3f740..b6e445334 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -30,10 +30,10 @@ namespace theory {
 namespace eq {
 
 ProofEqEngine::ProofEqEngine(context::Context* c,
-                             context::UserContext* u,
+                             context::Context* lc,
                              EqualityEngine& ee,
                              ProofNodeManager* pnm)
-    : EagerProofGenerator(pnm, u, "pfee::" + ee.identify()),
+    : EagerProofGenerator(pnm, lc, "pfee::" + ee.identify()),
       d_ee(ee),
       d_factPg(c, pnm),
       d_assumpPg(pnm),
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index baf155dac..9ebdd03e5 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -85,8 +85,14 @@ class ProofEqEngine : public EagerProofGenerator
   typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofMap;
 
  public:
+  /**
+   * @param c The SAT context
+   * @param lc The context lemmas live in
+   * @param ee The equality engine this is layered on
+   * @param pnm The proof node manager for producing proof nodes.
+   */
   ProofEqEngine(context::Context* c,
-                context::UserContext* u,
+                context::Context* lc,
                 EqualityEngine& ee,
                 ProofNodeManager* pnm);
   ~ProofEqEngine() {}