Remove context getters from `TheoryState` (#7174)

This removes TheoryState::getSatContext() and
TheoryState::getUserContext().

20 files changed, 67 insertions, 67 deletions

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 8334cc248..1ccfd8ede 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -56,7 +56,7 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env,
       d_irew(new InstRewriterCegqi(this)),
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
-      d_added_cbqi_lemma(qs.getUserContext()),
+      d_added_cbqi_lemma(userContext()),
       d_vtsCache(new VtsTermCache(qim)),
       d_bv_invert(nullptr),
       d_small_const_multiplier(
@@ -168,10 +168,8 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
     DecisionStrategy* dlds = nullptr;
     if (itds == d_dstrat.end())
     {
-      d_dstrat[q].reset(new DecisionStrategySingleton("CexLiteral",
-                                                      ceLit,
-                                                      d_qstate.getSatContext(),
-                                                      d_qstate.getValuation()));
+      d_dstrat[q].reset(new DecisionStrategySingleton(
+          d_env, "CexLiteral", ceLit, d_qstate.getValuation()));
       dlds = d_dstrat[q].get();
     }
     else
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index f9625d7ac..da8727c12 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -167,7 +167,7 @@ ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bo
   if( eqc_i!=d_eqc_info.end() ){
     return eqc_i->second;
   }else if( doMake ){
-    EqcInfo* ei = new EqcInfo(d_qstate.getSatContext());
+    EqcInfo* ei = new EqcInfo(context());
     d_eqc_info[n] = ei;
     return ei;
   }else{
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 92ec1e452..30d223b2a 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -33,7 +33,7 @@ EqualityQuery::EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m)
     : QuantifiersUtil(env),
       d_qstate(qs),
       d_model(m),
-      d_eqi_counter(qs.getSatContext()),
+      d_eqi_counter(context()),
       d_reset_count(0)
 {
 }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 841177a7f..cfd903646 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -46,11 +46,12 @@ FirstOrderModel::FirstOrderModel(Env& env,
                                  QuantifiersState& qs,
                                  QuantifiersRegistry& qr,
                                  TermRegistry& tr)
-    : d_model(nullptr),
+    : EnvObj(env),
+      d_model(nullptr),
       d_qreg(qr),
       d_treg(tr),
       d_eq_query(env, qs, this),
-      d_forall_asserts(qs.getSatContext()),
+      d_forall_asserts(context()),
       d_forallRlvComputed(false)
 {
 }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 05bdcbee6..526bbe10b 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -19,6 +19,7 @@
 #define CVC5__FIRST_ORDER_MODEL_H
 
 #include "context/cdlist.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_model.h"
@@ -36,7 +37,7 @@ class TermRegistry;
 class QuantifiersRegistry;
 
 // TODO (#1301) : document and refactor this class
-class FirstOrderModel
+class FirstOrderModel : protected EnvObj
 {
  public:
   FirstOrderModel(Env& env,
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index b04391db3..4a3e13dd0 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -37,12 +37,10 @@ using namespace cvc5::theory::quantifiers;
 using namespace cvc5::kind;
 
 BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
-    Node r,
-    context::Context* c,
-    context::Context* u,
-    Valuation valuation,
-    bool isProxy)
-    : DecisionStrategyFmf(c, valuation), d_range(r), d_ranges_proxied(u)
+    Env& env, Node r, Valuation valuation, bool isProxy)
+    : DecisionStrategyFmf(env, valuation),
+      d_range(r),
+      d_ranges_proxied(userContext())
 {
   if( options::fmfBoundLazy() ){
     SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
@@ -514,12 +512,8 @@ void BoundedIntegers::checkOwnership(Node f)
           {
             Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;
             d_ranges.push_back( r );
-            d_rms[r].reset(
-                new IntRangeDecisionHeuristic(r,
-                                              d_qstate.getSatContext(),
-                                              d_qstate.getUserContext(),
-                                              d_qstate.getValuation(),
-                                              isProxy));
+            d_rms[r].reset(new IntRangeDecisionHeuristic(
+                d_env, r, d_qstate.getValuation(), isProxy));
             dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
                                  d_rms[r].get());
           }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 8c468c1de..2c3a86fc7 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -100,9 +100,8 @@ private:
  class IntRangeDecisionHeuristic : public DecisionStrategyFmf
  {
   public:
-   IntRangeDecisionHeuristic(Node r,
-                             context::Context* c,
-                             context::Context* u,
+   IntRangeDecisionHeuristic(Env& env,
+                             Node r,
                              Valuation valuation,
                              bool isProxy);
    /** make the n^th literal of this strategy */
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index ba9ea9152..a4107564e 100644
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -189,16 +189,18 @@ CDInstMatchTrie::~CDInstMatchTrie()
   d_data.clear();
 }
 
-bool CDInstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
+bool CDInstMatchTrie::existsInstMatch(context::Context* context,
+                                      quantifiers::QuantifiersState& qs,
                                       Node q,
                                       const std::vector<Node>& m,
                                       bool modEq,
                                       unsigned index)
 {
-  return !addInstMatch(qs, q, m, modEq, index, true);
+  return !addInstMatch(context, qs, q, m, modEq, index, true);
 }
 
-bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
+bool CDInstMatchTrie::addInstMatch(context::Context* context,
+                                   quantifiers::QuantifiersState& qs,
                                    Node f,
                                    const std::vector<Node>& m,
                                    bool modEq,
@@ -226,7 +228,8 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
   std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
   if (it != d_data.end())
   {
-    bool ret = it->second->addInstMatch(qs, f, m, modEq, index + 1, onlyExist);
+    bool ret =
+        it->second->addInstMatch(context, qs, f, m, modEq, index + 1, onlyExist);
     if (!onlyExist || !ret)
     {
       return reset || ret;
@@ -246,7 +249,8 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
           std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
           if (itc != d_data.end())
           {
-            if (itc->second->addInstMatch(qs, f, m, modEq, index + 1, true))
+            if (itc->second->addInstMatch(
+                    context, qs, f, m, modEq, index + 1, true))
             {
               return false;
             }
@@ -259,10 +263,10 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
 
   if (!onlyExist)
   {
-    CDInstMatchTrie* imt = new CDInstMatchTrie(qs.getUserContext());
+    CDInstMatchTrie* imt = new CDInstMatchTrie(context);
     Assert(d_data.find(n) == d_data.end());
     d_data[n] = imt;
-    imt->addInstMatch(qs, f, m, modEq, index + 1, false);
+    imt->addInstMatch(context, qs, f, m, modEq, index + 1, false);
   }
   return true;
 }
diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index 83bd8d3b1..5ddc299af 100644
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -23,6 +23,7 @@
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -131,7 +132,8 @@ class CDInstMatchTrie
    * equalities in the equality engine of qs.
    * It additionally takes a context c, for which the entry is valid in.
    */
-  bool existsInstMatch(QuantifiersState& qs,
+  bool existsInstMatch(context::Context* context,
+                       QuantifiersState& qs,
                        Node q,
                        const std::vector<Node>& m,
                        bool modEq = false,
@@ -145,7 +147,8 @@ class CDInstMatchTrie
    * equalities in the equality engine of qs.
    * It additionally takes a context c, for which the entry is valid in.
    */
-  bool addInstMatch(QuantifiersState& qs,
+  bool addInstMatch(context::Context* context,
+                    QuantifiersState& qs,
                     Node q,
                     const std::vector<Node>& m,
                     bool modEq = false,
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index f0af73832..2a3974d49 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -54,11 +54,10 @@ Instantiate::Instantiate(Env& env,
       d_qreg(qr),
       d_treg(tr),
       d_pnm(pnm),
-      d_insts(qs.getUserContext()),
-      d_c_inst_match_trie_dom(qs.getUserContext()),
-      d_pfInst(
-          pnm ? new CDProof(pnm, qs.getUserContext(), "Instantiate::pfInst")
-              : nullptr)
+      d_insts(userContext()),
+      d_c_inst_match_trie_dom(userContext()),
+      d_pfInst(pnm ? new CDProof(pnm, userContext(), "Instantiate::pfInst")
+                   : nullptr)
 {
 }
 
@@ -507,7 +506,7 @@ bool Instantiate::existsInstantiation(Node q,
     std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
     if (it != d_c_inst_match_trie.end())
     {
-      return it->second->existsInstMatch(d_qstate, q, terms, modEq);
+      return it->second->existsInstMatch(userContext(), d_qstate, q, terms, modEq);
     }
   }
   else
@@ -594,10 +593,10 @@ bool Instantiate::recordInstantiationInternal(Node q, std::vector<Node>& terms)
     const auto res = d_c_inst_match_trie.insert({q, nullptr});
     if (res.second)
     {
-      res.first->second = new CDInstMatchTrie(d_qstate.getUserContext());
+      res.first->second = new CDInstMatchTrie(userContext());
     }
     d_c_inst_match_trie_dom.insert(q);
-    return res.first->second->addInstMatch(d_qstate, q, terms);
+    return res.first->second->addInstMatch(userContext(), d_qstate, q, terms);
   }
   Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
   return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms);
@@ -750,7 +749,7 @@ InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q)
     return it->second.get();
   }
   std::shared_ptr<InstLemmaList> ill =
-      std::make_shared<InstLemmaList>(d_qstate.getUserContext());
+      std::make_shared<InstLemmaList>(userContext());
   d_insts.insert(q, ill);
   return ill.get();
 }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 983eee9ae..1de60422f 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1859,7 +1859,7 @@ QuantConflictFind::QuantConflictFind(Env& env,
                                      QuantifiersRegistry& qr,
                                      TermRegistry& tr)
     : QuantifiersModule(env, qs, qim, qr, tr),
-      d_conflict(qs.getSatContext(), false),
+      d_conflict(context(), false),
       d_true(NodeManager::currentNM()->mkConst<bool>(true)),
       d_false(NodeManager::currentNM()->mkConst<bool>(false)),
       d_effort(EFFORT_INVALID)
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 905424107..db07d07d0 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -33,8 +33,7 @@ QuantDSplit::QuantDSplit(Env& env,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr)
-    : QuantifiersModule(env, qs, qim, qr, tr),
-      d_added_split(qs.getUserContext())
+    : QuantifiersModule(env, qs, qim, qr, tr), d_added_split(userContext())
 {
 }
 
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index b2a08c249..20987b02e 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -31,7 +31,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager(
     ProofNodeManager* pnm)
     : InferenceManagerBuffered(env, t, state, pnm, "theory::quantifiers::"),
       d_instantiate(new Instantiate(env, state, *this, qr, tr, pnm)),
-      d_skolemize(new Skolemize(state, tr, pnm))
+      d_skolemize(new Skolemize(env, state, tr, pnm))
 {
 }
 
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 23b66b1de..bb0fa3899 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -35,16 +35,18 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-Skolemize::Skolemize(QuantifiersState& qs,
+Skolemize::Skolemize(Env& env,
+                     QuantifiersState& qs,
                      TermRegistry& tr,
                      ProofNodeManager* pnm)
-    : d_qstate(qs),
+    : EnvObj(env),
+      d_qstate(qs),
       d_treg(tr),
-      d_skolemized(qs.getUserContext()),
+      d_skolemized(userContext()),
       d_pnm(pnm),
-      d_epg(pnm == nullptr ? nullptr
-                           : new EagerProofGenerator(
-                                 pnm, qs.getUserContext(), "Skolemize::epg"))
+      d_epg(pnm == nullptr
+                ? nullptr
+                : new EagerProofGenerator(pnm, userContext(), "Skolemize::epg"))
 {
 }
 
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index fbb79f5d2..294ad0084 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -26,6 +26,7 @@
 #include "expr/type_node.h"
 #include "proof/eager_proof_generator.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -63,12 +64,15 @@ class TermRegistry;
  * default and can be enabled by option:
  *   --quant-ind
  */
-class Skolemize
+class Skolemize : protected EnvObj
 {
   typedef context::CDHashMap<Node, Node> NodeNodeMap;
 
  public:
-  Skolemize(QuantifiersState& qs, TermRegistry& tr, ProofNodeManager* pnm);
+  Skolemize(Env& env,
+            QuantifiersState& qs,
+            TermRegistry& tr,
+            ProofNodeManager* pnm);
   ~Skolemize() {}
   /** skolemize quantified formula q
    * If the return value ret of this function is non-null, then ret is a trust
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 871a85fbd..6b260bb81 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -409,7 +409,7 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
     QuantifiersInferenceManager& qim,
     TermDbSygus* tds,
     SynthConjecture* parent)
-    : DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()),
+    : DecisionStrategyFmf(env, qs.getValuation()),
       d_qim(qim),
       d_tds(tds),
       d_parent(parent)
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index da021227a..22ba879d7 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -241,11 +241,8 @@ void SynthConjecture::assign(Node q)
   }
 
   // register the strategy
-  d_feasible_strategy.reset(
-      new DecisionStrategySingleton("sygus_feasible",
-                                    d_feasible_guard,
-                                    d_qstate.getSatContext(),
-                                    d_qstate.getValuation()));
+  d_feasible_strategy.reset(new DecisionStrategySingleton(
+      d_env, "sygus_feasible", d_feasible_guard, d_qstate.getValuation()));
   d_qim.getDecisionManager()->registerStrategy(
       DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
   // this must be called, both to ensure that the feasible guard is
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 4da273cd9..64bc578a5 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -529,7 +529,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
    */
   Assert(d_dstrat.find(q) == d_dstrat.end());
   DecisionStrategy* ds = new DecisionStrategySingleton(
-      "CeLiteral", lit, d_qstate.getSatContext(), d_qstate.getValuation());
+      d_env, "CeLiteral", lit, d_qstate.getValuation());
 
   d_dstrat[q].reset(ds);
   d_qim.getDecisionManager()->registerStrategy(
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 6aa2a816a..7126d3567 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -43,13 +43,12 @@ TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
       d_qim(nullptr),
       d_qreg(qr),
       d_termsContext(),
-      d_termsContextUse(options::termDbCd() ? qs.getSatContext()
-                                            : &d_termsContext),
+      d_termsContextUse(options::termDbCd() ? context() : &d_termsContext),
       d_processed(d_termsContextUse),
       d_typeMap(d_termsContextUse),
       d_ops(d_termsContextUse),
       d_opMap(d_termsContextUse),
-      d_inactive_map(qs.getSatContext())
+      d_inactive_map(context())
 {
   d_consistent_ee = true;
   d_true = NodeManager::currentNM()->mkConst(true);
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 98618f3f7..ab999ad9b 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -33,8 +33,8 @@ TermRegistry::TermRegistry(Env& env,
                            QuantifiersState& qs,
                            QuantifiersRegistry& qr)
     : EnvObj(env),
-      d_presolve(qs.getUserContext(), true),
-      d_presolveCache(qs.getUserContext()),
+      d_presolve(userContext(), true),
+      d_presolveCache(userContext()),
       d_termEnum(new TermEnumeration),
       d_termPools(new TermPools(env, qs)),
       d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr)