Remove `TheoryState::getEnv()` (#7163)

38 files changed, 129 insertions, 88 deletions

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 742e5ca49..b8170df45 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -49,14 +49,14 @@ NonlinearExtension::NonlinearExtension(Env& env,
       d_extTheoryCb(state.getEqualityEngine()),
       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()),
+      d_trSlv(d_im, d_model, d_env),
+      d_extState(d_im, d_model, d_env),
       d_factoringSlv(&d_extState),
       d_monomialBoundsSlv(&d_extState),
       d_monomialSlv(&d_extState),
       d_splitZeroSlv(&d_extState),
       d_tangentPlaneSlv(&d_extState),
-      d_cadSlv(d_astate.getEnv(), d_im, d_model),
+      d_cadSlv(d_env, d_im, d_model),
       d_icpSlv(d_im),
       d_iandSlv(env, d_im, state, d_model),
       d_pow2Slv(env, d_im, state, d_model)
@@ -72,9 +72,9 @@ NonlinearExtension::NonlinearExtension(Env& env,
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
 
-  if (d_astate.getEnv().isTheoryProofProducing())
+  if (d_env.isTheoryProofProducing())
   {
-    ProofChecker* pc = d_astate.getEnv().getProofNodeManager()->getChecker();
+    ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
     d_proofChecker.registerTo(pc);
   }
 }
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 81366fabd..8334cc248 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -47,11 +47,12 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
   return d_parent->rewriteInstantiation(q, terms, inst, doVts);
 }
 
-InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs,
+InstStrategyCegqi::InstStrategyCegqi(Env& env,
+                                     QuantifiersState& qs,
                                      QuantifiersInferenceManager& qim,
                                      QuantifiersRegistry& qr,
                                      TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr),
+    : QuantifiersModule(env, qs, qim, qr, tr),
       d_irew(new InstRewriterCegqi(this)),
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
@@ -70,7 +71,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs,
   }
   if (options::cegqiNestedQE())
   {
-    d_nestedQe.reset(new NestedQe(qs.getEnv()));
+    d_nestedQe.reset(new NestedQe(d_env));
   }
 }
 
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index 882f69b85..a568b0b4d 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
 #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
 
+#include "smt/env_obj.h"
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/bv_inverter.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
@@ -69,7 +70,8 @@ class InstStrategyCegqi : public QuantifiersModule
   typedef context::CDHashMap<Node, int> NodeIntMap;
 
  public:
-  InstStrategyCegqi(QuantifiersState& qs,
+  InstStrategyCegqi(Env& env,
+                    QuantifiersState& qs,
                     QuantifiersInferenceManager& qim,
                     QuantifiersRegistry& qr,
                     TermRegistry& tr);
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 17eaad5c6..f9625d7ac 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -86,15 +86,15 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >&
   }
 }
 
-ConjectureGenerator::ConjectureGenerator(QuantifiersState& qs,
+ConjectureGenerator::ConjectureGenerator(Env& env,
+                                         QuantifiersState& qs,
                                          QuantifiersInferenceManager& qim,
                                          QuantifiersRegistry& qr,
                                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr),
+    : QuantifiersModule(env, qs, qim, qr, tr),
       d_notify(*this),
-      d_uequalityEngine(
-          d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false),
-      d_ee_conjectures(qs.getSatContext()),
+      d_uequalityEngine(d_notify, context(), "ConjectureGenerator::ee", false),
+      d_ee_conjectures(context()),
       d_conj_count(0),
       d_subs_confirmCount(0),
       d_subs_unkCount(0),
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index ef60792a6..bc5f3fb13 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -21,6 +21,7 @@
 #include "context/cdhashmap.h"
 #include "expr/node_trie.h"
 #include "expr/term_canonize.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/quant_module.h"
 #include "theory/type_enumerator.h"
 
@@ -437,7 +438,8 @@ private:  //information about ground equivalence classes
   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
 
  public:
-  ConjectureGenerator(QuantifiersState& qs,
+  ConjectureGenerator(Env& env,
+                      QuantifiersState& qs,
                       QuantifiersInferenceManager& qim,
                       QuantifiersRegistry& qr,
                       TermRegistry& tr);
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index dcfa71f8c..62c5c2440 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -37,7 +37,7 @@ InstantiationEngine::InstantiationEngine(Env& env,
                                          QuantifiersInferenceManager& qim,
                                          QuantifiersRegistry& qr,
                                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr),
+    : QuantifiersModule(env, qs, qim, qr, tr),
       d_instStrategies(),
       d_isup(),
       d_i_ag(),
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 3fd478c31..b04391db3 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -88,11 +88,12 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
   return lem;
 }
 
-BoundedIntegers::BoundedIntegers(QuantifiersState& qs,
+BoundedIntegers::BoundedIntegers(Env& env,
+                                 QuantifiersState& qs,
                                  QuantifiersInferenceManager& qim,
                                  QuantifiersRegistry& qr,
                                  TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr)
+    : QuantifiersModule(env, qs, qim, qr, tr)
 {
 }
 
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index d37e71b72..8c468c1de 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -18,13 +18,13 @@
 #ifndef CVC5__BOUNDED_INTEGERS_H
 #define CVC5__BOUNDED_INTEGERS_H
 
-#include "theory/quantifiers/quant_module.h"
-
 #include "context/cdhashmap.h"
 #include "context/context.h"
 #include "expr/attribute.h"
+#include "smt/env_obj.h"
 #include "theory/decision_strategy.h"
 #include "theory/quantifiers/quant_bound_inference.h"
+#include "theory/quantifiers/quant_module.h"
 
 namespace cvc5 {
 namespace theory {
@@ -164,7 +164,8 @@ private:
   std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
 
  public:
-  BoundedIntegers(QuantifiersState& qs,
+  BoundedIntegers(Env& env,
+                  QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
                   QuantifiersRegistry& qr,
                   TermRegistry& tr);
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index e58f66d0b..256899580 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -31,12 +31,13 @@ namespace theory {
 namespace quantifiers {
 
 //Model Engine constructor
-ModelEngine::ModelEngine(QuantifiersState& qs,
+ModelEngine::ModelEngine(Env& env,
+                         QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr,
                          QModelBuilder* builder)
-    : QuantifiersModule(qs, qim, qr, tr),
+    : QuantifiersModule(env, qs, qim, qr, tr),
       d_incomplete_check(true),
       d_addedLemmas(0),
       d_triedLemmas(0),
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index f818a6362..b5ab86f20 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
 #define CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
 
+#include "smt/env_obj.h"
 #include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/quantifiers/quant_module.h"
 #include "theory/theory_model.h"
@@ -42,7 +43,8 @@ private:
   int d_triedLemmas;
   int d_totalLemmas;
 public:
- ModelEngine(QuantifiersState& qs,
+ ModelEngine(Env& env,
+             QuantifiersState& qs,
              QuantifiersInferenceManager& qim,
              QuantifiersRegistry& qr,
              TermRegistry& tr,
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index aeff27433..6769d8bc2 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -29,12 +29,13 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-InstStrategyEnum::InstStrategyEnum(QuantifiersState& qs,
+InstStrategyEnum::InstStrategyEnum(Env& env,
+                                   QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
                                    QuantifiersRegistry& qr,
                                    TermRegistry& tr,
                                    RelevantDomain* rd)
-    : QuantifiersModule(qs, qim, qr, tr), d_rd(rd), d_fullSaturateLimit(-1)
+    : QuantifiersModule(env, qs, qim, qr, tr), d_rd(rd), d_fullSaturateLimit(-1)
 {
 }
 void InstStrategyEnum::presolve()
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index a298e3a8a..66315c070 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H
 #define CVC5__INST_STRATEGY_ENUMERATIVE_H
 
+#include "smt/env_obj.h"
 #include "theory/quantifiers/quant_module.h"
 
 namespace cvc5 {
@@ -62,7 +63,8 @@ class RelevantDomain;
 class InstStrategyEnum : public QuantifiersModule
 {
  public:
-  InstStrategyEnum(QuantifiersState& qs,
+  InstStrategyEnum(Env& env,
+                   QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    QuantifiersRegistry& qr,
                    TermRegistry& tr,
diff --git a/src/theory/quantifiers/inst_strategy_pool.cpp b/src/theory/quantifiers/inst_strategy_pool.cpp
index 0e32c246e..cadda033b 100644
--- a/src/theory/quantifiers/inst_strategy_pool.cpp
+++ b/src/theory/quantifiers/inst_strategy_pool.cpp
@@ -30,11 +30,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-InstStrategyPool::InstStrategyPool(QuantifiersState& qs,
+InstStrategyPool::InstStrategyPool(Env& env,
+                                   QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
                                    QuantifiersRegistry& qr,
                                    TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr)
+    : QuantifiersModule(env, qs, qim, qr, tr)
 {
 }
 
diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h
index acdc0010b..1f79717af 100644
--- a/src/theory/quantifiers/inst_strategy_pool.h
+++ b/src/theory/quantifiers/inst_strategy_pool.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
 #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
 
+#include "smt/env_obj.h"
 #include "theory/quantifiers/quant_module.h"
 
 namespace cvc5 {
@@ -38,7 +39,8 @@ namespace quantifiers {
 class InstStrategyPool : public QuantifiersModule
 {
  public:
-  InstStrategyPool(QuantifiersState& qs,
+  InstStrategyPool(Env& env,
+                   QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    QuantifiersRegistry& qr,
                    TermRegistry& tr);
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 8c4d68631..983eee9ae 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1853,11 +1853,12 @@ bool MatchGen::isHandled( TNode n ) {
   return true;
 }
 
-QuantConflictFind::QuantConflictFind(QuantifiersState& qs,
+QuantConflictFind::QuantConflictFind(Env& env,
+                                     QuantifiersState& qs,
                                      QuantifiersInferenceManager& qim,
                                      QuantifiersRegistry& qr,
                                      TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr),
+    : QuantifiersModule(env, qs, qim, qr, tr),
       d_conflict(qs.getSatContext(), false),
       d_true(NodeManager::currentNM()->mkConst<bool>(true)),
       d_false(NodeManager::currentNM()->mkConst<bool>(false)),
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index de521cd07..927a74ff2 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -238,7 +238,8 @@ private:  //for equivalence classes
   bool areMatchDisequal( TNode n1, TNode n2 );
 
  public:
-  QuantConflictFind(QuantifiersState& qs,
+  QuantConflictFind(Env& env,
+                    QuantifiersState& qs,
                     QuantifiersInferenceManager& qim,
                     QuantifiersRegistry& qr,
                     TermRegistry& tr);
diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp
index d5488f0c9..8fb37c548 100644
--- a/src/theory/quantifiers/quant_module.cpp
+++ b/src/theory/quantifiers/quant_module.cpp
@@ -21,11 +21,12 @@ namespace cvc5 {
 namespace theory {
 
 QuantifiersModule::QuantifiersModule(
+    Env& env,
     quantifiers::QuantifiersState& qs,
     quantifiers::QuantifiersInferenceManager& qim,
     quantifiers::QuantifiersRegistry& qr,
     quantifiers::TermRegistry& tr)
-    : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
+    : EnvObj(env), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
 {
 }
 
diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h
index 7358aa555..639f9c2b4 100644
--- a/src/theory/quantifiers/quant_module.h
+++ b/src/theory/quantifiers/quant_module.h
@@ -60,7 +60,8 @@ class QuantifiersModule : protected EnvObj
   };
 
  public:
-  QuantifiersModule(quantifiers::QuantifiersState& qs,
+  QuantifiersModule(Env& env,
+                    quantifiers::QuantifiersState& qs,
                     quantifiers::QuantifiersInferenceManager& qim,
                     quantifiers::QuantifiersRegistry& qr,
                     quantifiers::TermRegistry& tr);
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 941b94d23..905424107 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -28,11 +28,13 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-QuantDSplit::QuantDSplit(QuantifiersState& qs,
+QuantDSplit::QuantDSplit(Env& env,
+                         QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr), d_added_split(qs.getUserContext())
+    : QuantifiersModule(env, qs, qim, qr, tr),
+      d_added_split(qs.getUserContext())
 {
 }
 
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 18aeec773..84cc6fea7 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -19,6 +19,7 @@
 #define CVC5__THEORY__QUANT_SPLIT_H
 
 #include "context/cdo.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/quant_module.h"
 
 namespace cvc5 {
@@ -50,7 +51,8 @@ class QuantDSplit : public QuantifiersModule {
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  QuantDSplit(QuantifiersState& qs,
+  QuantDSplit(Env& env,
+              QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
               QuantifiersRegistry& qr,
               TermRegistry& tr);
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 889b6ac26..563951189 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -52,12 +52,12 @@ void QuantifiersModules::initialize(Env& env,
   // add quantifiers modules
   if (options::quantConflictFind())
   {
-    d_qcf.reset(new QuantConflictFind(qs, qim, qr, tr));
+    d_qcf.reset(new QuantConflictFind(env, qs, qim, qr, tr));
     modules.push_back(d_qcf.get());
   }
   if (options::conjectureGen())
   {
-    d_sg_gen.reset(new ConjectureGenerator(qs, qim, qr, tr));
+    d_sg_gen.reset(new ConjectureGenerator(env, qs, qim, qr, tr));
     modules.push_back(d_sg_gen.get());
   }
   if (!options::finiteModelFind() || options::fmfInstEngine())
@@ -67,7 +67,7 @@ void QuantifiersModules::initialize(Env& env,
   }
   if (options::cegqi())
   {
-    d_i_cbqi.reset(new InstStrategyCegqi(qs, qim, qr, tr));
+    d_i_cbqi.reset(new InstStrategyCegqi(env, qs, qim, qr, tr));
     modules.push_back(d_i_cbqi.get());
     qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
   }
@@ -80,18 +80,18 @@ void QuantifiersModules::initialize(Env& env,
   // fmfBound, or if strings are enabled.
   if (options::fmfBound() || options::stringExp())
   {
-    d_bint.reset(new BoundedIntegers(qs, qim, qr, tr));
+    d_bint.reset(new BoundedIntegers(env, qs, qim, qr, tr));
     modules.push_back(d_bint.get());
   }
 
   if (options::finiteModelFind() || options::fmfBound() || options::stringExp())
   {
-    d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, builder));
+    d_model_engine.reset(new ModelEngine(env, qs, qim, qr, tr, builder));
     modules.push_back(d_model_engine.get());
   }
   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
   {
-    d_qsplit.reset(new QuantDSplit(qs, qim, qr, tr));
+    d_qsplit.reset(new QuantDSplit(env, qs, qim, qr, tr));
     modules.push_back(d_qsplit.get());
   }
   if (options::quantAlphaEquiv())
@@ -102,17 +102,17 @@ void QuantifiersModules::initialize(Env& env,
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
   {
     d_rel_dom.reset(new RelevantDomain(env, qs, qr, tr));
-    d_fs.reset(new InstStrategyEnum(qs, qim, qr, tr, d_rel_dom.get()));
+    d_fs.reset(new InstStrategyEnum(env, qs, qim, qr, tr, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }
   if (options::poolInst())
   {
-    d_ipool.reset(new InstStrategyPool(qs, qim, qr, tr));
+    d_ipool.reset(new InstStrategyPool(env, qs, qim, qr, tr));
     modules.push_back(d_ipool.get());
   }
   if (options::sygusInst())
   {
-    d_sygus_inst.reset(new SygusInst(qs, qim, qr, tr));
+    d_sygus_inst.reset(new SygusInst(env, qs, qim, qr, tr));
     modules.push_back(d_sygus_inst.get());
   }
 }
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 708bffe80..f5774c761 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -32,11 +32,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-Cegis::Cegis(QuantifiersState& qs,
+Cegis::Cegis(Env& env,
+             QuantifiersState& qs,
              QuantifiersInferenceManager& qim,
              TermDbSygus* tds,
              SynthConjecture* p)
-    : SygusModule(qs, qim, tds, p),
+    : SygusModule(env, qs, qim, tds, p),
       d_eval_unfold(tds->getEvalUnfold()),
       d_usingSymCons(false)
 {
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index d6678a305..d72805950 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -19,6 +19,8 @@
 #define CVC5__THEORY__QUANTIFIERS__CEGIS_H
 
 #include <map>
+
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/sygus_module.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
@@ -42,7 +44,8 @@ namespace quantifiers {
 class Cegis : public SygusModule
 {
  public:
-  Cegis(QuantifiersState& qs,
+  Cegis(Env& env,
+        QuantifiersState& qs,
         QuantifiersInferenceManager& qim,
         TermDbSygus* tds,
         SynthConjecture* p);
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 9a9d8f02d..a42323227 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -68,11 +68,12 @@ bool VariadicTrie::hasSubset(const std::vector<Node>& is) const
   return false;
 }
 
-CegisCoreConnective::CegisCoreConnective(QuantifiersState& qs,
+CegisCoreConnective::CegisCoreConnective(Env& env,
+                                         QuantifiersState& qs,
                                          QuantifiersInferenceManager& qim,
                                          TermDbSygus* tds,
                                          SynthConjecture* p)
-    : Cegis(qs, qim, tds, p)
+    : Cegis(env, qs, qim, tds, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -629,9 +630,7 @@ bool CegisCoreConnective::getUnsatCore(
 Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
 {
   Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
-  Env& env = d_qstate.getEnv();
-  Result r =
-      checkWithSubsolver(n, d_vars, mvs, env.getOptions(), env.getLogicInfo());
+  Result r = checkWithSubsolver(n, d_vars, mvs, options(), logicInfo());
   Trace("sygus-ccore-debug") << "...got " << r << std::endl;
   return r;
 }
@@ -739,7 +738,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
     addSuccess = false;
     // try a new core
     std::unique_ptr<SmtEngine> checkSol;
-    initializeSubsolver(checkSol, d_qstate.getEnv());
+    initializeSubsolver(checkSol, d_env);
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
     rasserts.push_back(d_sc);
@@ -779,7 +778,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
           // In terms of Variant #2, this is the check "if S ^ U is unsat"
           Trace("sygus-ccore") << "----- Check side condition" << std::endl;
           std::unique_ptr<SmtEngine> checkSc;
-          initializeSubsolver(checkSc, d_qstate.getEnv());
+          initializeSubsolver(checkSc, d_env);
           std::vector<Node> scasserts;
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
           scasserts.push_back(d_sc);
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index e9a73e9bb..80ba6f26e 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -22,6 +22,7 @@
 
 #include "expr/node.h"
 #include "expr/node_trie.h"
+#include "smt/env_obj.h"
 #include "theory/evaluator.h"
 #include "theory/quantifiers/sygus/cegis.h"
 #include "util/result.h"
@@ -160,7 +161,8 @@ class VariadicTrie
 class CegisCoreConnective : public Cegis
 {
  public:
-  CegisCoreConnective(QuantifiersState& qs,
+  CegisCoreConnective(Env& env,
+                      QuantifiersState& qs,
                       QuantifiersInferenceManager& qim,
                       TermDbSygus* tds,
                       SynthConjecture* p);
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 797aecdab..871a85fbd 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -30,13 +30,14 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-CegisUnif::CegisUnif(QuantifiersState& qs,
+CegisUnif::CegisUnif(Env& env,
+                     QuantifiersState& qs,
                      QuantifiersInferenceManager& qim,
                      TermDbSygus* tds,
                      SynthConjecture* p)
-    : Cegis(qs, qim, tds, p),
-      d_sygus_unif(qs.getEnv(), p),
-      d_u_enum_manager(qs, qim, tds, p)
+    : Cegis(env, qs, qim, tds, p),
+      d_sygus_unif(env, p),
+      d_u_enum_manager(env, qs, qim, tds, p)
 {
 }
 
@@ -403,6 +404,7 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars, Node lem)
 }
 
 CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
+    Env& env,
     QuantifiersState& qs,
     QuantifiersInferenceManager& qim,
     TermDbSygus* tds,
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 0cddff9c1..da47aabbe 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -20,6 +20,7 @@
 #include <map>
 #include <vector>
 
+#include "smt/env_obj.h"
 #include "theory/decision_strategy.h"
 #include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
@@ -49,7 +50,8 @@ namespace quantifiers {
 class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 {
  public:
-  CegisUnifEnumDecisionStrategy(QuantifiersState& qs,
+  CegisUnifEnumDecisionStrategy(Env& env,
+                                QuantifiersState& qs,
                                 QuantifiersInferenceManager& qim,
                                 TermDbSygus* tds,
                                 SynthConjecture* parent);
@@ -207,7 +209,8 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 class CegisUnif : public Cegis
 {
  public:
-  CegisUnif(QuantifiersState& qs,
+  CegisUnif(Env& env,
+            QuantifiersState& qs,
             QuantifiersInferenceManager& qim,
             TermDbSygus* tds,
             SynthConjecture* p);
diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index 8272c6418..1840f0eb1 100644
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -21,11 +21,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusModule::SygusModule(QuantifiersState& qs,
+SygusModule::SygusModule(Env& env,
+                         QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          TermDbSygus* tds,
                          SynthConjecture* p)
-    : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p)
+    : EnvObj(env), d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p)
 {
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 8070fe009..8ee1fc9b4 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -53,7 +53,8 @@ class QuantifiersInferenceManager;
 class SygusModule : protected EnvObj
 {
  public:
-  SygusModule(QuantifiersState& qs,
+  SygusModule(Env& env,
+              QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
               TermDbSygus* tds,
               SynthConjecture* p);
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 52bca1586..453ac5c18 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -30,11 +30,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusPbe::SygusPbe(QuantifiersState& qs,
+SygusPbe::SygusPbe(Env& env,
+                   QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    TermDbSygus* tds,
                    SynthConjecture* p)
-    : SygusModule(qs, qim, tds, p)
+    : SygusModule(env, qs, qim, tds, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 867764617..e55479e18 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -18,6 +18,7 @@
 #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H
 #define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H
 
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/sygus_module.h"
 
 namespace cvc5 {
@@ -86,7 +87,8 @@ class SynthConjecture;
 class SygusPbe : public SygusModule
 {
  public:
-  SygusPbe(QuantifiersState& qs,
+  SygusPbe(Env& env,
+           QuantifiersState& qs,
            QuantifiersInferenceManager& qim,
            TermDbSygus* tds,
            SynthConjecture* p);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 730482073..da021227a 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -66,10 +66,10 @@ SynthConjecture::SynthConjecture(Env& env,
       d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
       d_sygus_rconst(new SygusRepairConst(env, d_tds)),
       d_exampleInfer(new ExampleInfer(d_tds)),
-      d_ceg_pbe(new SygusPbe(qs, qim, d_tds, this)),
-      d_ceg_cegis(new Cegis(qs, qim, d_tds, this)),
-      d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)),
-      d_sygus_ccore(new CegisCoreConnective(qs, qim, d_tds, this)),
+      d_ceg_pbe(new SygusPbe(env, qs, qim, d_tds, this)),
+      d_ceg_cegis(new Cegis(env, qs, qim, d_tds, this)),
+      d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)),
+      d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)),
       d_master(nullptr),
       d_set_ce_sk_vars(false),
       d_repair_index(0),
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 64227793d..454442351 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -31,7 +31,7 @@ SynthEngine::SynthEngine(Env& env,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp(qs.getEnv())
+    : QuantifiersModule(env, qs, qim, qr, tr), d_conj(nullptr), d_sqp(env)
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
       new SynthConjecture(env, qs, qim, qr, tr, d_statistics)));
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 21852f25a..4da273cd9 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -182,14 +182,15 @@ void addSpecialValues(const TypeNode& tn,
 
 }  // namespace
 
-SygusInst::SygusInst(QuantifiersState& qs,
+SygusInst::SygusInst(Env& env,
+                     QuantifiersState& qs,
                      QuantifiersInferenceManager& qim,
                      QuantifiersRegistry& qr,
                      TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr),
-      d_ce_lemma_added(qs.getUserContext()),
-      d_global_terms(qs.getUserContext()),
-      d_notified_assertions(qs.getUserContext())
+    : QuantifiersModule(env, qs, qim, qr, tr),
+      d_ce_lemma_added(userContext()),
+      d_global_terms(userContext()),
+      d_notified_assertions(userContext())
 {
 }
 
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 80c7e809f..060ab7226 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -22,6 +22,7 @@
 #include <unordered_set>
 
 #include "context/cdhashset.h"
+#include "smt/env_obj.h"
 #include "theory/decision_strategy.h"
 #include "theory/quantifiers/quant_module.h"
 
@@ -64,7 +65,8 @@ namespace quantifiers {
 class SygusInst : public QuantifiersModule
 {
  public:
-  SygusInst(QuantifiersState& qs,
+  SygusInst(Env& env,
+            QuantifiersState& qs,
             QuantifiersInferenceManager& qim,
             QuantifiersRegistry& qr,
             TermRegistry& tr);
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 7ad782fda..98618f3f7 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -32,13 +32,13 @@ namespace quantifiers {
 TermRegistry::TermRegistry(Env& env,
                            QuantifiersState& qs,
                            QuantifiersRegistry& qr)
-    : d_presolve(qs.getUserContext(), true),
+    : EnvObj(env),
+      d_presolve(qs.getUserContext(), true),
       d_presolveCache(qs.getUserContext()),
       d_termEnum(new TermEnumeration),
       d_termPools(new TermPools(env, qs)),
-      d_termDb(qs.getEnv().getLogicInfo().isHigherOrder()
-                   ? new HoTermDb(env, qs, qr)
-                   : new TermDb(env, qs, qr)),
+      d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr)
+                                           : new TermDb(env, qs, qr)),
       d_sygusTdb(nullptr),
       d_qmodel(nullptr)
 {
diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index e0ce73286..175d450df 100644
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -22,6 +22,7 @@
 #include <unordered_set>
 
 #include "context/cdhashset.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
@@ -37,7 +38,7 @@ class FirstOrderModel;
  * Term Registry, which manages notifying modules within quantifiers about
  * (ground) terms that exist in the current context.
  */
-class TermRegistry
+class TermRegistry : protected EnvObj
 {
   using NodeSet = context::CDHashSet<Node>;
 
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 049123b8d..574aa9355 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -46,8 +46,6 @@ class TheoryState : protected EnvObj
   context::Context* getSatContext() const;
   /** Get the user context */
   context::UserContext* getUserContext() const;
-  /** Get the environment */
-  Env& getEnv() const { return d_env; }
   //-------------------------------------- equality information
   /** Is t registered as a term in the equality engine of this class? */
   virtual bool hasTerm(TNode a) const;