Remove `TheoryState::options()` (#7148)

This commit removes TheoryState::options() by changing more classes to
EnvObjs.

53 files changed, 151 insertions, 106 deletions

diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 6ab399348..ba2de9fdf 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -23,11 +23,12 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-ArithPreprocess::ArithPreprocess(ArithState& state,
+ArithPreprocess::ArithPreprocess(Env& env,
+                                 ArithState& state,
                                  InferenceManager& im,
                                  ProofNodeManager* pnm,
                                  OperatorElim& oe)
-    : d_im(im), d_opElim(oe), d_reduced(state.getUserContext())
+    : EnvObj(env), d_im(im), d_opElim(oe), d_reduced(userContext())
 {
 }
 TrustNode ArithPreprocess::eliminate(TNode n,
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index a537c33c7..939306a6e 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -19,6 +19,7 @@
 #define CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
 
 #include "context/cdhashmap.h"
+#include "smt/env_obj.h"
 #include "theory/arith/operator_elim.h"
 #include "theory/logic_info.h"
 
@@ -40,10 +41,11 @@ class OperatorElim;
  * extends that utility with the ability to generate lemmas on demand via
  * the provided inference manager.
  */
-class ArithPreprocess
+class ArithPreprocess : protected EnvObj
 {
  public:
-  ArithPreprocess(ArithState& state,
+  ArithPreprocess(Env& env,
+                  ArithState& state,
                   InferenceManager& im,
                   ProofNodeManager* pnm,
                   OperatorElim& oe);
diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp
index ca1a2fa6f..31017dea6 100644
--- a/src/theory/arith/branch_and_bound.cpp
+++ b/src/theory/arith/branch_and_bound.cpp
@@ -28,14 +28,16 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-BranchAndBound::BranchAndBound(ArithState& s,
+BranchAndBound::BranchAndBound(Env& env,
+                               ArithState& s,
                                InferenceManager& im,
                                PreprocessRewriteEq& ppre,
                                ProofNodeManager* pnm)
-    : d_astate(s),
+    : EnvObj(env),
+      d_astate(s),
       d_im(im),
       d_ppre(ppre),
-      d_pfGen(new EagerProofGenerator(pnm, s.getUserContext())),
+      d_pfGen(new EagerProofGenerator(pnm, userContext())),
       d_pnm(pnm)
 {
 }
@@ -45,7 +47,7 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value)
   TrustNode lem = TrustNode::null();
   NodeManager* nm = NodeManager::currentNM();
   Integer floor = value.floor();
-  if (d_astate.options().arith.brabTest)
+  if (options().arith.brabTest)
   {
     Trace("integers") << "branch-round-and-bound enabled" << std::endl;
     Integer ceil = value.ceiling();
diff --git a/src/theory/arith/branch_and_bound.h b/src/theory/arith/branch_and_bound.h
index 4281ba678..52acf6aae 100644
--- a/src/theory/arith/branch_and_bound.h
+++ b/src/theory/arith/branch_and_bound.h
@@ -23,6 +23,7 @@
 #include "expr/node.h"
 #include "proof/proof_node_manager.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/pp_rewrite_eq.h"
@@ -37,10 +38,11 @@ namespace arith {
  * agnostic to the state of solver; instead is simply given (variable, value)
  * pairs in branchIntegerVariable below and constructs the appropriate lemma.
  */
-class BranchAndBound
+class BranchAndBound : protected EnvObj
 {
  public:
-  BranchAndBound(ArithState& s,
+  BranchAndBound(Env& env,
+                 ArithState& s,
                  InferenceManager& im,
                  PreprocessRewriteEq& ppre,
                  ProofNodeManager* pnm);
diff --git a/src/theory/arith/equality_solver.cpp b/src/theory/arith/equality_solver.cpp
index 8b4e1b8dd..8e5cc9a28 100644
--- a/src/theory/arith/equality_solver.cpp
+++ b/src/theory/arith/equality_solver.cpp
@@ -23,12 +23,15 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-EqualitySolver::EqualitySolver(ArithState& astate, InferenceManager& aim)
-    : d_astate(astate),
+EqualitySolver::EqualitySolver(Env& env,
+                               ArithState& astate,
+                               InferenceManager& aim)
+    : EnvObj(env),
+      d_astate(astate),
       d_aim(aim),
       d_notify(*this),
       d_ee(nullptr),
-      d_propLits(astate.getSatContext())
+      d_propLits(context())
 {
 }
 
diff --git a/src/theory/arith/equality_solver.h b/src/theory/arith/equality_solver.h
index bce30e697..8528650f0 100644
--- a/src/theory/arith/equality_solver.h
+++ b/src/theory/arith/equality_solver.h
@@ -21,6 +21,7 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/arith_state.h"
 #include "theory/ee_setup_info.h"
 #include "theory/uf/equality_engine.h"
@@ -39,12 +40,12 @@ class InferenceManager;
  * the literals that it propagates and only explains the literals that
  * originated from this class.
  */
-class EqualitySolver
+class EqualitySolver : protected EnvObj
 {
   using NodeSet = context::CDHashSet<Node>;
 
  public:
-  EqualitySolver(ArithState& astate, InferenceManager& aim);
+  EqualitySolver(Env& env, ArithState& astate, InferenceManager& aim);
   ~EqualitySolver() {}
   //--------------------------------- initialization
   /**
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 5ab606f96..0c6b18893 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -30,7 +30,7 @@ InferenceManager::InferenceManager(Env& env,
                                    ProofNodeManager* pnm)
     : InferenceManagerBuffered(env, ta, astate, pnm, "theory::arith::"),
       // currently must track propagated literals if using the equality solver
-      d_trackPropLits(astate.options().arith.arithEqSolver),
+      d_trackPropLits(options().arith.arithEqSolver),
       d_propLits(context())
 {
 }
@@ -128,7 +128,7 @@ bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 
 bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem)
 {
-  if (d_theoryState.options().arith.nlExtEntailConflicts)
+  if (options().arith.nlExtEntailConflicts)
   {
     Node ch_lemma = lem.d_node.negate();
     ch_lemma = Rewriter::rewrite(ch_lemma);
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index eb5620a82..76d964934 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -34,11 +34,15 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model)
-    : d_im(im),
+IAndSolver::IAndSolver(Env& env,
+                       InferenceManager& im,
+                       ArithState& state,
+                       NlModel& model)
+    : EnvObj(env),
+      d_im(im),
       d_model(model),
       d_astate(state),
-      d_initRefine(state.getUserContext())
+      d_initRefine(userContext())
 {
   NodeManager* nm = NodeManager::currentNM();
   d_false = nm->mkConst(false);
@@ -152,7 +156,7 @@ void IAndSolver::checkFullRefine()
       }
 
       // ************* additional lemma schemas go here
-      if (d_astate.options().smt.iandMode == options::IandMode::SUM)
+      if (options().smt.iandMode == options::IandMode::SUM)
       {
         Node lem = sumBasedLemma(i);  // add lemmas based on sum mode
         Trace("iand-lemma")
@@ -162,7 +166,7 @@ void IAndSolver::checkFullRefine()
         d_im.addPendingLemma(
             lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true);
       }
-      else if (d_astate.options().smt.iandMode == options::IandMode::BITWISE)
+      else if (options().smt.iandMode == options::IandMode::BITWISE)
       {
         Node lem = bitwiseLemma(i);  // check for violated bitwise axioms
         Trace("iand-lemma")
@@ -245,7 +249,7 @@ Node IAndSolver::sumBasedLemma(Node i)
   Node x = i[0];
   Node y = i[1];
   size_t bvsize = i.getOperator().getConst<IntAnd>().d_size;
-  uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity;
+  uint64_t granularity = options().smt.BVAndIntegerGranularity;
   NodeManager* nm = NodeManager::currentNM();
   Node lem = nm->mkNode(
       EQUAL, i, d_iandUtils.createSumNode(x, y, bvsize, granularity));
@@ -259,7 +263,7 @@ Node IAndSolver::bitwiseLemma(Node i)
   Node y = i[1];
 
   unsigned bvsize = i.getOperator().getConst<IntAnd>().d_size;
-  uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity;
+  uint64_t granularity = options().smt.BVAndIntegerGranularity;
 
   Rational absI = d_model.computeAbstractModelValue(i).getConst<Rational>();
   Rational concI = d_model.computeConcreteModelValue(i).getConst<Rational>();
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index 1be469259..0b6a1fac6 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -21,6 +21,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/arith/nl/iand_utils.h"
 
 namespace cvc5 {
@@ -37,12 +38,12 @@ class NlModel;
 /** Integer and solver class
  *
  */
-class IAndSolver
+class IAndSolver : protected EnvObj
 {
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  IAndSolver(InferenceManager& im, ArithState& state, NlModel& model);
+  IAndSolver(Env& env, InferenceManager& im, ArithState& state, NlModel& model);
   ~IAndSolver();
 
   /** init last call
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index db92009f4..742e5ca49 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -58,8 +58,8 @@ NonlinearExtension::NonlinearExtension(Env& env,
       d_tangentPlaneSlv(&d_extState),
       d_cadSlv(d_astate.getEnv(), d_im, d_model),
       d_icpSlv(d_im),
-      d_iandSlv(d_im, state, d_model),
-      d_pow2Slv(d_im, state, d_model)
+      d_iandSlv(env, d_im, state, d_model),
+      d_pow2Slv(env, d_im, state, d_model)
 {
   d_extTheory.addFunctionKind(kind::NONLINEAR_MULT);
   d_extTheory.addFunctionKind(kind::EXPONENTIAL);
diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp
index d708e86e1..597a0df96 100644
--- a/src/theory/arith/nl/pow2_solver.cpp
+++ b/src/theory/arith/nl/pow2_solver.cpp
@@ -33,8 +33,11 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-Pow2Solver::Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model)
-    : d_im(im), d_model(model), d_initRefine(state.getUserContext())
+Pow2Solver::Pow2Solver(Env& env,
+                       InferenceManager& im,
+                       ArithState& state,
+                       NlModel& model)
+    : EnvObj(env), d_im(im), d_model(model), d_initRefine(userContext())
 {
   NodeManager* nm = NodeManager::currentNM();
   d_false = nm->mkConst(false);
diff --git a/src/theory/arith/nl/pow2_solver.h b/src/theory/arith/nl/pow2_solver.h
index 4c6fb8014..b4e12616c 100644
--- a/src/theory/arith/nl/pow2_solver.h
+++ b/src/theory/arith/nl/pow2_solver.h
@@ -20,6 +20,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -35,12 +36,12 @@ class NlModel;
 /** pow2 solver class
  *
  */
-class Pow2Solver
+class Pow2Solver : protected EnvObj
 {
   using NodeSet = context::CDHashSet<Node>;
 
  public:
-  Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model);
+  Pow2Solver(Env& env, InferenceManager& im, ArithState& state, NlModel& model);
   ~Pow2Solver();
 
   /** init last call
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d94f81e9c..9642bf394 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -42,12 +42,12 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
       d_astate(env, valuation),
       d_im(env, *this, d_astate, d_pnm),
       d_ppre(context(), d_pnm),
-      d_bab(d_astate, d_im, d_ppre, d_pnm),
+      d_bab(env, d_astate, d_im, d_ppre, d_pnm),
       d_eqSolver(nullptr),
       d_internal(new TheoryArithPrivate(*this, env, d_bab)),
       d_nonlinearExtension(nullptr),
       d_opElim(d_pnm, logicInfo()),
-      d_arithPreproc(d_astate, d_im, d_pnm, d_opElim),
+      d_arithPreproc(env, d_astate, d_im, d_pnm, d_opElim),
       d_rewriter(d_opElim)
 {
   // currently a cyclic dependency to TheoryArithPrivate
@@ -58,7 +58,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
 
   if (options().arith.arithEqSolver)
   {
-    d_eqSolver.reset(new EqualitySolver(d_astate, d_im));
+    d_eqSolver.reset(new EqualitySolver(env, d_astate, d_im));
   }
 }
 
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index e59dfcc13..4eef9a018 100644
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -33,7 +33,7 @@ InferenceManager::InferenceManager(Env& env,
                                    ProofNodeManager* pnm)
     : TheoryInferenceManager(env, t, state, pnm, "theory::arrays::", false),
       d_lemmaPg(pnm ? new EagerProofGenerator(
-                    pnm, state.getUserContext(), "ArrayLemmaProofGenerator")
+                    pnm, userContext(), "ArrayLemmaProofGenerator")
                     : nullptr)
 {
 }
diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
index 659886e83..7e995eab5 100644
--- a/src/theory/bags/term_registry.cpp
+++ b/src/theory/bags/term_registry.cpp
@@ -26,10 +26,11 @@ namespace cvc5 {
 namespace theory {
 namespace bags {
 
-TermRegistry::TermRegistry(SolverState& state, InferenceManager& im)
-    : d_im(im),
-      d_proxy(state.getUserContext()),
-      d_proxy_to_term(state.getUserContext())
+TermRegistry::TermRegistry(Env& env, SolverState& state, InferenceManager& im)
+    : EnvObj(env),
+      d_im(im),
+      d_proxy(userContext()),
+      d_proxy_to_term(userContext())
 {
 }
 
diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
index 2b0218fdf..f36dda1a9 100644
--- a/src/theory/bags/term_registry.h
+++ b/src/theory/bags/term_registry.h
@@ -22,6 +22,7 @@
 
 #include "context/cdhashmap.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -34,12 +35,12 @@ class SolverState;
  * Term registry, the purpose of this class is to maintain a database of
  * commonly used terms, and mappings from bags to their "proxy variables".
  */
-class TermRegistry
+class TermRegistry : protected EnvObj
 {
   typedef context::CDHashMap<Node, Node> NodeMap;
 
  public:
-  TermRegistry(SolverState& state, InferenceManager& im);
+  TermRegistry(Env& env, SolverState& state, InferenceManager& im);
 
   /**
    * Returns the existing empty bag for type tn
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index c421b9ec2..004766d83 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -35,7 +35,7 @@ TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
       d_notify(*this, d_im),
       d_statistics(),
       d_rewriter(&d_statistics.d_rewrites),
-      d_termReg(d_state, d_im),
+      d_termReg(env, d_state, d_im),
       d_solver(d_state, d_im, d_termReg)
 {
   // use the official theory state and inference manager objects
diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index c9750a505..d158cff08 100644
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -36,12 +36,10 @@ InferenceManager::InferenceManager(Env& env,
                                    ProofNodeManager* pnm)
     : InferenceManagerBuffered(env, t, state, pnm, "theory::datatypes::"),
       d_pnm(pnm),
-      d_ipc(pnm == nullptr ? nullptr
-                           : new InferProofCons(state.getSatContext(), pnm)),
-      d_lemPg(pnm == nullptr
-                  ? nullptr
-                  : new EagerProofGenerator(
-                      pnm, state.getUserContext(), "datatypes::lemPg"))
+      d_ipc(pnm == nullptr ? nullptr : new InferProofCons(context(), pnm)),
+      d_lemPg(pnm == nullptr ? nullptr
+                             : new EagerProofGenerator(
+                                 pnm, userContext(), "datatypes::lemPg"))
 {
   d_false = NodeManager::currentNM()->mkConst(false);
 }
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 8e3c22fb8..ed112e4ea 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1110,7 +1110,7 @@ Node SygusExtension::registerSearchValue(Node a,
             its = d_sampler[a].find(tn);
           }
           // check equivalent
-          its->second.checkEquivalent(bv, bvr, *d_state.options().base.out);
+          its->second.checkEquivalent(bv, bvr, *options().base.out);
         }
       }
 
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index ead42a3cd..dcfa71f8c 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -32,7 +32,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-InstantiationEngine::InstantiationEngine(QuantifiersState& qs,
+InstantiationEngine::InstantiationEngine(Env& env,
+                                         QuantifiersState& qs,
                                          QuantifiersInferenceManager& qim,
                                          QuantifiersRegistry& qr,
                                          TermRegistry& tr)
@@ -46,7 +47,7 @@ InstantiationEngine::InstantiationEngine(QuantifiersState& qs,
 {
   if (options::relevantTriggers())
   {
-    d_quant_rel.reset(new quantifiers::QuantRelevance);
+    d_quant_rel.reset(new quantifiers::QuantRelevance(env));
   }
   if (options::eMatching()) {
     // these are the instantiation strategies for E-matching
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 45e137dd5..50685642d 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -34,7 +34,8 @@ class InstStrategyAutoGenTriggers;
 
 class InstantiationEngine : public QuantifiersModule {
  public:
-  InstantiationEngine(QuantifiersState& qs,
+  InstantiationEngine(Env& env,
+                      QuantifiersState& qs,
                       QuantifiersInferenceManager& qim,
                       QuantifiersRegistry& qr,
                       TermRegistry& tr);
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index f87ec6435..92ec1e452 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -29,8 +29,9 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-EqualityQuery::EqualityQuery(QuantifiersState& qs, FirstOrderModel* m)
-    : d_qstate(qs),
+EqualityQuery::EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m)
+    : QuantifiersUtil(env),
+      d_qstate(qs),
       d_model(m),
       d_eqi_counter(qs.getSatContext()),
       d_reset_count(0)
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index f39ff86e3..200863cd6 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -43,7 +43,7 @@ class QuantifiersState;
 class EqualityQuery : public QuantifiersUtil
 {
  public:
-  EqualityQuery(QuantifiersState& qs, FirstOrderModel* m);
+  EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m);
   virtual ~EqualityQuery();
 
   /** reset */
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index d4bc7dfcb..841177a7f 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -42,13 +42,14 @@ struct ModelBasisArgAttributeId
 };
 using ModelBasisArgAttribute = expr::Attribute<ModelBasisArgAttributeId, uint64_t>;
 
-FirstOrderModel::FirstOrderModel(QuantifiersState& qs,
+FirstOrderModel::FirstOrderModel(Env& env,
+                                 QuantifiersState& qs,
                                  QuantifiersRegistry& qr,
                                  TermRegistry& tr)
     : d_model(nullptr),
       d_qreg(qr),
       d_treg(tr),
-      d_eq_query(qs, this),
+      d_eq_query(env, qs, this),
       d_forall_asserts(qs.getSatContext()),
       d_forallRlvComputed(false)
 {
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 1969fdde7..05bdcbee6 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -39,7 +39,8 @@ class QuantifiersRegistry;
 class FirstOrderModel
 {
  public:
-  FirstOrderModel(QuantifiersState& qs,
+  FirstOrderModel(Env& env,
+                  QuantifiersState& qs,
                   QuantifiersRegistry& qr,
                   TermRegistry& tr);
   virtual ~FirstOrderModel() {}
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
index e17271613..4be13ba5f 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -36,10 +36,11 @@ struct IsStarAttributeId
 };
 using IsStarAttribute = expr::Attribute<IsStarAttributeId, bool>;
 
-FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs,
+FirstOrderModelFmc::FirstOrderModelFmc(Env& env,
+                                       QuantifiersState& qs,
                                        QuantifiersRegistry& qr,
                                        TermRegistry& tr)
-    : FirstOrderModel(qs, qr, tr)
+    : FirstOrderModel(env, qs, qr, tr)
 {
 }
 
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h
index f148a9e19..5a528ede1 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.h
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h
@@ -39,7 +39,8 @@ class FirstOrderModelFmc : public FirstOrderModel
   void processInitializeModelForTerm(Node n) override;
 
  public:
-  FirstOrderModelFmc(QuantifiersState& qs,
+  FirstOrderModelFmc(Env& env,
+                     QuantifiersState& qs,
                      QuantifiersRegistry& qr,
                      TermRegistry& tr);
   ~FirstOrderModelFmc() override;
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index c4f83191b..f8b90f624 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -286,11 +286,13 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
   }
 }
 
-FullModelChecker::FullModelChecker(QuantifiersState& qs,
+FullModelChecker::FullModelChecker(Env& env,
+                                   QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
                                    QuantifiersRegistry& qr,
                                    TermRegistry& tr)
-    : QModelBuilder(qs, qim, qr, tr), d_fm(new FirstOrderModelFmc(qs, qr, tr))
+    : QModelBuilder(env, qs, qim, qr, tr),
+      d_fm(new FirstOrderModelFmc(env, qs, qr, tr))
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index e33d1db6d..f3f8699af 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -155,7 +155,8 @@ protected:
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 
  public:
-  FullModelChecker(QuantifiersState& qs,
+  FullModelChecker(Env& env,
+                   QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    QuantifiersRegistry& qr,
                    TermRegistry& tr);
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index a331409f1..f43b7a6c9 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -30,11 +30,12 @@ using namespace cvc5::context;
 using namespace cvc5::theory;
 using namespace cvc5::theory::quantifiers;
 
-QModelBuilder::QModelBuilder(QuantifiersState& qs,
+QModelBuilder::QModelBuilder(Env& env,
+                             QuantifiersState& qs,
                              QuantifiersInferenceManager& qim,
                              QuantifiersRegistry& qr,
                              TermRegistry& tr)
-    : TheoryEngineModelBuilder(qs.getEnv()),
+    : TheoryEngineModelBuilder(env),
       d_addedLemmas(0),
       d_triedLemmas(0),
       d_qstate(qs),
@@ -48,7 +49,7 @@ QModelBuilder::QModelBuilder(QuantifiersState& qs,
 void QModelBuilder::finishInit()
 {
   // allocate the default model
-  d_modelAloc.reset(new FirstOrderModel(d_qstate, d_qreg, d_treg));
+  d_modelAloc.reset(new FirstOrderModel(d_env, d_qstate, d_qreg, d_treg));
   d_model = d_modelAloc.get();
 }
 
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index a767af47a..f5dc7155b 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -43,7 +43,8 @@ class QModelBuilder : public TheoryEngineModelBuilder
   unsigned d_triedLemmas;
 
  public:
-  QModelBuilder(QuantifiersState& qs,
+  QModelBuilder(Env& env,
+                QuantifiersState& qs,
                 QuantifiersInferenceManager& qim,
                 QuantifiersRegistry& qr,
                 TermRegistry& tr);
diff --git a/src/theory/quantifiers/ho_term_database.cpp b/src/theory/quantifiers/ho_term_database.cpp
index 3b97409cc..a2a8b8145 100644
--- a/src/theory/quantifiers/ho_term_database.cpp
+++ b/src/theory/quantifiers/ho_term_database.cpp
@@ -28,8 +28,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-HoTermDb::HoTermDb(QuantifiersState& qs, QuantifiersRegistry& qr)
-    : TermDb(qs, qr)
+HoTermDb::HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
+    : TermDb(env, qs, qr)
 {
 }
 
@@ -152,7 +152,7 @@ bool HoTermDb::resetInternal(Theory::Effort effort)
 
 bool HoTermDb::finishResetInternal(Theory::Effort effort)
 {
-  if (!d_qstate.options().quantifiers.hoMergeTermDb)
+  if (!options().quantifiers.hoMergeTermDb)
   {
     return true;
   }
diff --git a/src/theory/quantifiers/ho_term_database.h b/src/theory/quantifiers/ho_term_database.h
index 12bf0b49f..885fec8f4 100644
--- a/src/theory/quantifiers/ho_term_database.h
+++ b/src/theory/quantifiers/ho_term_database.h
@@ -34,7 +34,7 @@ namespace quantifiers {
 class HoTermDb : public TermDb
 {
  public:
-  HoTermDb(QuantifiersState& qs, QuantifiersRegistry& qr);
+  HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr);
   ~HoTermDb();
   /** identify */
   std::string identify() const override { return "HoTermDb"; }
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 9010d4fe1..f0af73832 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -42,12 +42,14 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-Instantiate::Instantiate(QuantifiersState& qs,
+Instantiate::Instantiate(Env& env,
+                         QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr,
                          ProofNodeManager* pnm)
-    : d_qstate(qs),
+    : QuantifiersUtil(env),
+      d_qstate(qs),
       d_qim(qim),
       d_qreg(qr),
       d_treg(tr),
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 1f380350f..753213f35 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -104,7 +104,8 @@ class Instantiate : public QuantifiersUtil
       context::CDHashMap<Node, std::shared_ptr<InstLemmaList>>;
 
  public:
-  Instantiate(QuantifiersState& qs,
+  Instantiate(Env& env,
+              QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
               QuantifiersRegistry& qr,
               TermRegistry& tr,
diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp
index 0c1db860f..abb8c9219 100644
--- a/src/theory/quantifiers/quant_relevance.cpp
+++ b/src/theory/quantifiers/quant_relevance.cpp
@@ -23,6 +23,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
+QuantRelevance::QuantRelevance(Env& env) : QuantifiersUtil(env) {}
+
 void QuantRelevance::registerQuantifier(Node f)
 {
   // compute symbols in f
diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h
index c22e560f9..418b859b9 100644
--- a/src/theory/quantifiers/quant_relevance.h
+++ b/src/theory/quantifiers/quant_relevance.h
@@ -40,7 +40,7 @@ class QuantRelevance : public QuantifiersUtil
    * if this is false, then all calls to getRelevance
    * return -1.
    */
-  QuantRelevance() {}
+  QuantRelevance(Env& env);
   ~QuantRelevance() {}
   /** reset */
   bool reset(Theory::Effort e) override { return true; }
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 64a816975..cbe09af2e 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -22,6 +22,8 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace theory {
 
+QuantifiersUtil::QuantifiersUtil(Env& env) : EnvObj(env) {}
+
 QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
   initialize( n, computeEq );
 }
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 7ca17b6ad..a422101f0 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/incomplete_id.h"
 #include "theory/theory.h"
 
@@ -34,9 +35,10 @@ namespace theory {
  * This is a lightweight version of a quantifiers module that does not implement
  * methods for checking satisfiability.
  */
-class QuantifiersUtil {
-public:
-  QuantifiersUtil(){}
+class QuantifiersUtil : protected EnvObj
+{
+ public:
+  QuantifiersUtil(Env& env);
   virtual ~QuantifiersUtil(){}
   /**  Called at the beginning of check-sat call. */
   virtual void presolve() {}
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index 24159d397..b2a08c249 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -30,7 +30,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager(
     TermRegistry& tr,
     ProofNodeManager* pnm)
     : InferenceManagerBuffered(env, t, state, pnm, "theory::quantifiers::"),
-      d_instantiate(new Instantiate(state, *this, qr, tr, pnm)),
+      d_instantiate(new Instantiate(env, state, *this, qr, tr, pnm)),
       d_skolemize(new Skolemize(state, tr, pnm))
 {
 }
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 6cfc48fb9..889b6ac26 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -62,7 +62,7 @@ void QuantifiersModules::initialize(Env& env,
   }
   if (!options::finiteModelFind() || options::fmfInstEngine())
   {
-    d_inst_engine.reset(new InstantiationEngine(qs, qim, qr, tr));
+    d_inst_engine.reset(new InstantiationEngine(env, qs, qim, qr, tr));
     modules.push_back(d_inst_engine.get());
   }
   if (options::cegqi())
@@ -101,7 +101,7 @@ void QuantifiersModules::initialize(Env& env,
   // full saturation : instantiate from relevant domain, then arbitrary terms
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
   {
-    d_rel_dom.reset(new RelevantDomain(qs, qr, tr));
+    d_rel_dom.reset(new RelevantDomain(env, qs, qr, tr));
     d_fs.reset(new InstStrategyEnum(qs, qim, qr, tr, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }
diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp
index 4dc329d8e..6d5e00363 100644
--- a/src/theory/quantifiers/quantifiers_registry.cpp
+++ b/src/theory/quantifiers/quantifiers_registry.cpp
@@ -24,7 +24,8 @@ namespace theory {
 namespace quantifiers {
 
 QuantifiersRegistry::QuantifiersRegistry(Env& env)
-    : d_quantAttr(),
+    : QuantifiersUtil(env),
+      d_quantAttr(),
       d_quantBoundInf(options::fmfTypeCompletionThresh(),
                       options::finiteModelFind()),
       d_quantPreproc(env)
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 7e2c0c909..f4eb95469 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -75,10 +75,11 @@ void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
   }
 }
 
-RelevantDomain::RelevantDomain(QuantifiersState& qs,
+RelevantDomain::RelevantDomain(Env& env,
+                               QuantifiersState& qs,
                                QuantifiersRegistry& qr,
                                TermRegistry& tr)
-    : d_qs(qs), d_qreg(qr), d_treg(tr)
+    : QuantifiersUtil(env), d_qs(qs), d_qreg(qr), d_treg(tr)
 {
   d_is_computed = false;
 }
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 5643a4665..3b44b2263 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -45,7 +45,8 @@ class TermRegistry;
 class RelevantDomain : public QuantifiersUtil
 {
  public:
-  RelevantDomain(QuantifiersState& qs,
+  RelevantDomain(Env& env,
+                 QuantifiersState& qs,
                  QuantifiersRegistry& qr,
                  TermRegistry& tr);
   virtual ~RelevantDomain();
diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
index 1d0ba5bee..e7b3bbaa9 100644
--- a/src/theory/quantifiers/sygus/enum_value_manager.cpp
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -110,7 +110,7 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
             d_samplerRrV->initializeSygus(
                 d_tds, e, options::sygusSamples(), false);
             // use the default output for the output of sygusRewVerify
-            out = d_qstate.options().base.out;
+            out = options().base.out;
           }
           d_secd.reset(new SygusEnumeratorCallbackDefault(
               e, &d_stats, d_eec.get(), d_samplerRrV.get(), out));
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e87857c3b..730482073 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -58,7 +58,7 @@ SynthConjecture::SynthConjecture(Env& env,
       d_treg(tr),
       d_stats(s),
       d_tds(tr.getTermDatabaseSygus()),
-      d_verify(qs.options(), qs.getLogicInfo(), d_tds),
+      d_verify(options(), qs.getLogicInfo(), d_tds),
       d_hasSolution(false),
       d_ceg_si(new CegSingleInv(env, tr, s)),
       d_templInfer(new SygusTemplateInfer),
@@ -515,7 +515,7 @@ bool SynthConjecture::doCheck()
   {
     if (printDebug)
     {
-      const Options& sopts = d_qstate.options();
+      const Options& sopts = options();
       std::ostream& out = *sopts.base.out;
       out << "(sygus-candidate ";
       Assert(d_quant[0].getNumChildren() == candidate_values.size());
@@ -801,8 +801,7 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
   Assert(d_master != nullptr);
   // we have generated a solution, print it
   // get the current output stream
-  const Options& sopts = d_qstate.options();
-  printSynthSolutionInternal(*sopts.base.out);
+  printSynthSolutionInternal(*options().base.out);
   excludeCurrentSolution(enums, values);
 }
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d2f872afb..6aa2a816a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -37,8 +37,9 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-TermDb::TermDb(QuantifiersState& qs, QuantifiersRegistry& qr)
-    : d_qstate(qs),
+TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
+    : QuantifiersUtil(env),
+      d_qstate(qs),
       d_qim(nullptr),
       d_qreg(qr),
       d_termsContext(),
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index a4e95487c..af0b87bd8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -73,8 +73,7 @@ class TermDb : public QuantifiersUtil {
   using NodeDbListMap = context::CDHashMap<Node, std::shared_ptr<DbList>>;
 
  public:
-  TermDb(QuantifiersState& qs,
-         QuantifiersRegistry& qr);
+  TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr);
   virtual ~TermDb();
   /** Finish init, which sets the inference manager */
   void finishInit(QuantifiersInferenceManager* qim);
diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp
index 2d95c8b20..7bac0252d 100644
--- a/src/theory/quantifiers/term_pools.cpp
+++ b/src/theory/quantifiers/term_pools.cpp
@@ -36,7 +36,10 @@ void TermPoolQuantInfo::initialize()
   d_skolemAddToPool.clear();
 }
 
-TermPools::TermPools(QuantifiersState& qs) : d_qs(qs) {}
+TermPools::TermPools(Env& env, QuantifiersState& qs)
+    : QuantifiersUtil(env), d_qs(qs)
+{
+}
 
 bool TermPools::reset(Theory::Effort e)
 {
diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h
index 5a7556ad9..37b16a785 100644
--- a/src/theory/quantifiers/term_pools.h
+++ b/src/theory/quantifiers/term_pools.h
@@ -71,7 +71,7 @@ class TermPoolQuantInfo
 class TermPools : public QuantifiersUtil
 {
  public:
-  TermPools(QuantifiersState& qs);
+  TermPools(Env& env, QuantifiersState& qs);
   ~TermPools() {}
   /** reset, which resets the current values of pools */
   bool reset(Theory::Effort e) override;
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 36dc8865c..7ad782fda 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -35,9 +35,10 @@ TermRegistry::TermRegistry(Env& env,
     : d_presolve(qs.getUserContext(), true),
       d_presolveCache(qs.getUserContext()),
       d_termEnum(new TermEnumeration),
-      d_termPools(new TermPools(qs)),
-      d_termDb(qs.getEnv().getLogicInfo().isHigherOrder() ? new HoTermDb(qs, qr)
-                                                          : new TermDb(qs, qr)),
+      d_termPools(new TermPools(env, qs)),
+      d_termDb(qs.getEnv().getLogicInfo().isHigherOrder()
+                   ? new HoTermDb(env, qs, qr)
+                   : new TermDb(env, qs, qr)),
       d_sygusTdb(nullptr),
       d_qmodel(nullptr)
 {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 40923ad0d..5f914484a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -76,12 +76,12 @@ QuantifiersEngine::QuantifiersEngine(
   {
     Trace("quant-init-debug") << "...make fmc builder." << std::endl;
     d_builder.reset(
-        new quantifiers::fmcheck::FullModelChecker(qs, qim, qr, tr));
+        new quantifiers::fmcheck::FullModelChecker(env, qs, qim, qr, tr));
   }
   else
   {
     Trace("quant-init-debug") << "...make default model builder." << std::endl;
-    d_builder.reset(new quantifiers::QModelBuilder(qs, qim, qr, tr));
+    d_builder.reset(new quantifiers::QModelBuilder(env, qs, qim, qr, tr));
   }
   // set the model object
   d_builder->finishInit();
@@ -113,7 +113,7 @@ void QuantifiersEngine::finishInit(TheoryEngine* te)
   d_model->finishInit(te->getModel());
   d_te = te;
   // Initialize the modules and the utilities here.
-  d_qmodules.reset(new quantifiers::QuantifiersModules);
+  d_qmodules.reset(new quantifiers::QuantifiersModules());
   d_qmodules->initialize(
       d_env, d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules);
   if (d_qmodules->d_rel_dom.get())
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 9162fdeb6..049123b8d 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -48,8 +48,6 @@ class TheoryState : protected EnvObj
   context::UserContext* getUserContext() const;
   /** Get the environment */
   Env& getEnv() const { return d_env; }
-  /** Get the options */
-  const Options& options() const { return getEnv().getOptions(); }
   //-------------------------------------- equality information
   /** Is t registered as a term in the equality engine of this class? */
   virtual bool hasTerm(TNode a) const;