EnvObj: Add options(), context(), userContext(). (#7137)

This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.

28 files changed, 150 insertions, 172 deletions

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index eb6410291..7f3d778fd 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -299,9 +299,9 @@ void usortsToBitVectors(const LogicInfo& d_logic,
 
 Ackermann::Ackermann(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "ackermann"),
-      d_funcToSkolem(preprocContext->getUserContext()),
-      d_usVarsToBVVars(preprocContext->getUserContext()),
-      d_logic(preprocContext->getLogicInfo())
+      d_funcToSkolem(userContext()),
+      d_usVarsToBVVars(userContext()),
+      d_logic(logicInfo())
 {
 }
 
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index ad2707035..65c9bb012 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -928,11 +928,11 @@ Node BVToInt::reconstructNode(Node originalNode,
 
 BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "bv-to-int"),
-      d_binarizeCache(preprocContext->getUserContext()),
-      d_eliminationCache(preprocContext->getUserContext()),
-      d_rebuildCache(preprocContext->getUserContext()),
-      d_bvToIntCache(preprocContext->getUserContext()),
-      d_rangeAssertions(preprocContext->getUserContext())
+      d_binarizeCache(userContext()),
+      d_eliminationCache(userContext()),
+      d_rebuildCache(userContext()),
+      d_bvToIntCache(userContext()),
+      d_rangeAssertions(userContext())
 {
   d_nm = NodeManager::currentNM();
   d_zero = d_nm->mkConst<Rational>(0);
diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp
index 888d5e43a..6040b3669 100644
--- a/src/preprocessing/passes/foreign_theory_rewrite.cpp
+++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp
@@ -28,9 +28,10 @@ namespace preprocessing {
 namespace passes {
 
 using namespace cvc5::theory;
-ForeignTheoryRewrite::ForeignTheoryRewrite(PreprocessingPassContext* preprocContext)
+ForeignTheoryRewrite::ForeignTheoryRewrite(
+    PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "foreign-theory-rewrite"),
-      d_cache(preprocContext->getUserContext()){};
+      d_cache(userContext()){};
 
 Node ForeignTheoryRewrite::simplify(Node n)
 {
diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index 44dafefcb..2405702b0 100644
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -39,8 +39,7 @@ FunDefFmf::FunDefFmf(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "fun-def-fmf"),
       d_fmfRecFunctionsDefined(nullptr)
 {
-  d_fmfRecFunctionsDefined =
-      new (true) NodeList(preprocContext->getUserContext());
+  d_fmfRecFunctionsDefined = new (true) NodeList(userContext());
 }
 
 FunDefFmf::~FunDefFmf() { d_fmfRecFunctionsDefined->deleteSelf(); }
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 54e2b657e..434256d28 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -144,16 +144,17 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
   }
 
   // Do theory specific preprocessing passes
-  if (d_env.getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH)
+  if (logicInfo().isTheoryEnabled(theory::THEORY_ARITH)
       && !options::incrementalSolving())
   {
     if (!simpDidALotOfWork)
     {
       util::ContainsTermITEVisitor& contains =
           *(d_iteUtilities.getContainsVisitor());
-      arith::ArithIteUtils aiteu(contains,
-                                 d_preprocContext->getUserContext(),
-                                 d_preprocContext->getTopLevelSubstitutions().get());
+      arith::ArithIteUtils aiteu(
+          contains,
+          userContext(),
+          d_preprocContext->getTopLevelSubstitutions().get());
       bool anyItes = false;
       for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
       {
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 5610b0117..8f390a402 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -53,16 +53,12 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "non-clausal-simp"),
       d_pnm(preprocContext->getProofNodeManager()),
       d_llpg(d_pnm ? new smt::PreprocessProofGenerator(
-                         d_pnm,
-                         preprocContext->getUserContext(),
-                         "NonClausalSimp::llpg")
+                 d_pnm, userContext(), "NonClausalSimp::llpg")
                    : nullptr),
-      d_llra(d_pnm ? new LazyCDProof(d_pnm,
-                                     nullptr,
-                                     preprocContext->getUserContext(),
-                                     "NonClausalSimp::llra")
+      d_llra(d_pnm ? new LazyCDProof(
+                 d_pnm, nullptr, userContext(), "NonClausalSimp::llra")
                    : nullptr),
-      d_tsubsList(preprocContext->getUserContext())
+      d_tsubsList(userContext())
 {
 }
 
@@ -91,7 +87,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   Trace("non-clausal-simplify") << "asserting to propagator" << std::endl;
   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
-    Assert(Rewriter::rewrite((*assertionsToPreprocess)[i])
+    Assert(rewrite((*assertionsToPreprocess)[i])
            == (*assertionsToPreprocess)[i]);
     // Don't reprocess substitutions
     if (assertionsToPreprocess->isSubstsIndex(i))
@@ -122,7 +118,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       << "Iterate through " << propagator->getLearnedLiterals().size()
       << " learned literals." << std::endl;
   // No conflict, go through the literals and solve them
-  context::Context* u = d_preprocContext->getUserContext();
+  context::Context* u = userContext();
   TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions();
   CVC5_UNUSED SubstitutionMap& top_level_substs = ttls.get();
   // constant propagations
@@ -152,7 +148,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   {
     // Simplify the literal we learned wrt previous substitutions
     Node learnedLiteral = learned_literals[i].getNode();
-    Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
+    Assert(rewrite(learnedLiteral) == learnedLiteral);
     Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral);
     // process the learned literal with substitutions and const propagations
     learnedLiteral = processLearnedLit(
@@ -198,7 +194,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
         // The literal should rewrite to true
         Trace("non-clausal-simplify")
             << "solved " << learnedLiteral << std::endl;
-        Assert(Rewriter::rewrite(nss.apply(learnedLiteral)).isConst());
+        Assert(rewrite(nss.apply(learnedLiteral)).isConst());
         // else fall through
         break;
       }
@@ -282,7 +278,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos)
   {
     Assert((*pos).second.isConst());
-    Assert(Rewriter::rewrite((*pos).first) == (*pos).first);
+    Assert(rewrite((*pos).first) == (*pos).first);
     Assert(cps.apply((*pos).second) == (*pos).second);
   }
 #endif /* CVC5_ASSERTIONS */
@@ -304,7 +300,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
           << "assertionNew = " << assertionNew.getNode() << std::endl;
       assertionsToPreprocess->replaceTrusted(i, assertionNew);
       assertion = assertionNew.getNode();
-      Assert(Rewriter::rewrite(assertion) == assertion);
+      Assert(rewrite(assertion) == assertion);
     }
     for (;;)
     {
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index c60e636bd..ca61c9197 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -35,9 +35,9 @@ using namespace cvc5::theory::arith;
 PseudoBooleanProcessor::PseudoBooleanProcessor(
     PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "pseudo-boolean-processor"),
-      d_pbBounds(preprocContext->getUserContext()),
-      d_subCache(preprocContext->getUserContext()),
-      d_pbs(preprocContext->getUserContext(), 0)
+      d_pbBounds(userContext()),
+      d_subCache(userContext()),
+      d_pbs(userContext(), 0)
 {
 }
 
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index a60b4a097..3cfc29ed6 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -34,8 +34,7 @@ namespace preprocessing {
 namespace passes {
 
 RealToInt::RealToInt(PreprocessingPassContext* preprocContext)
-    : PreprocessingPass(preprocContext, "real-to-int"),
-      d_cache(preprocContext->getUserContext())
+    : PreprocessingPass(preprocContext, "real-to-int"), d_cache(userContext())
 {
 }
 
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index c0cddda5e..d105c436a 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -295,9 +295,7 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions,
 
   // make a separate smt call
   std::unique_ptr<SmtEngine> rrSygus;
-  theory::initializeSubsolver(rrSygus,
-                              d_preprocContext->getOptions(),
-                              d_preprocContext->getLogicInfo());
+  theory::initializeSubsolver(rrSygus, options(), logicInfo());
   rrSygus->assertFormula(body);
   Trace("sygus-infer") << "*** Check sat..." << std::endl;
   Result r = rrSygus->checkSat();
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index f13de5e74..c8ddfc2fa 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -42,8 +42,8 @@ UnconstrainedSimplifier::UnconstrainedSimplifier(
     : PreprocessingPass(preprocContext, "unconstrained-simplifier"),
       d_numUnconstrainedElim(smtStatisticsRegistry().registerInt(
           "preprocessor::number of unconstrained elims")),
-      d_context(preprocContext->getDecisionContext()),
-      d_substitutions(preprocContext->getDecisionContext())
+      d_context(context()),
+      d_substitutions(context())
 {
 }
 
@@ -591,7 +591,7 @@ void UnconstrainedSimplifier::processUnconstrained()
         // Uninterpreted function - if domain is infinite, no quantifiers are
         // used, and any child is unconstrained, result is unconstrained
         case kind::APPLY_UF:
-          if (d_preprocContext->getLogicInfo().isQuantified()
+          if (logicInfo().isQuantified()
               || !current.getType().getCardinality().isInfinite())
           {
             break;
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index ac0301cc0..a0894351d 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -31,20 +31,11 @@ PreprocessingPassContext::PreprocessingPassContext(
     : EnvObj(env),
       d_smt(smt),
       d_circuitPropagator(circuitPropagator),
-      d_llm(env.getTopLevelSubstitutions(),
-            env.getUserContext(),
-            env.getProofNodeManager()),
-      d_symsInAssertions(env.getUserContext())
+      d_llm(
+          env.getTopLevelSubstitutions(), userContext(), getProofNodeManager()),
+      d_symsInAssertions(userContext())
 {
 }
-const Options& PreprocessingPassContext::getOptions() const
-{
-  return d_env.getOptions();
-}
-const LogicInfo& PreprocessingPassContext::getLogicInfo() const
-{
-  return d_env.getLogicInfo();
-}
 
 theory::TrustSubstitutionMap&
 PreprocessingPassContext::getTopLevelSubstitutions() const
@@ -60,14 +51,7 @@ prop::PropEngine* PreprocessingPassContext::getPropEngine() const
 {
   return d_smt->getPropEngine();
 }
-context::Context* PreprocessingPassContext::getUserContext() const
-{
-  return d_env.getUserContext();
-}
-context::Context* PreprocessingPassContext::getDecisionContext() const
-{
-  return d_env.getContext();
-}
+
 void PreprocessingPassContext::spendResource(Resource r)
 {
   d_env.getResourceManager()->spendResource(r);
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 29b2fda7f..79b89dda8 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -59,10 +59,6 @@ class PreprocessingPassContext : protected EnvObj
   TheoryEngine* getTheoryEngine() const;
   /** Get the associated Propengine. */
   prop::PropEngine* getPropEngine() const;
-  /** Get the current user context. */
-  context::Context* getUserContext() const;
-  /** Get the current decision context. */
-  context::Context* getDecisionContext() const;
 
   /** Get the associated circuit propagator. */
   theory::booleans::CircuitPropagator* getCircuitPropagator() const
@@ -82,11 +78,6 @@ class PreprocessingPassContext : protected EnvObj
   /** Spend resource in the resource manager of the associated Env. */
   void spendResource(Resource r);
 
-  /** Get the options of the environment */
-  const Options& getOptions() const;
-  /** Get the current logic info of the environment */
-  const LogicInfo& getLogicInfo() const;
-
   /** Get a reference to the top-level substitution map */
   theory::TrustSubstitutionMap& getTopLevelSubstitutions() const;
 
diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp
index 04a5050db..acc3ab038 100644
--- a/src/smt/env_obj.cpp
+++ b/src/smt/env_obj.cpp
@@ -26,6 +26,15 @@ EnvObj::EnvObj(Env& env) : d_env(env) {}
 
 Node EnvObj::rewrite(TNode node) { return d_env.getRewriter()->rewrite(node); }
 
-const LogicInfo& EnvObj::getLogicInfo() const { return d_env.getLogicInfo(); }
+const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); }
+
+const Options& EnvObj::options() const { return d_env.getOptions(); }
+
+context::Context* EnvObj::context() const { return d_env.getContext(); }
+
+context::UserContext* EnvObj::userContext() const
+{
+  return d_env.getUserContext();
+}
 
 }  // namespace cvc5
diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h
index ffd5a3915..d1c882b96 100644
--- a/src/smt/env_obj.h
+++ b/src/smt/env_obj.h
@@ -30,6 +30,11 @@ class LogicInfo;
 class NodeManager;
 class Options;
 
+namespace context {
+class Context;
+class UserContext;
+}  // namespace context
+
 class EnvObj
 {
  protected:
@@ -46,7 +51,16 @@ class EnvObj
   Node rewrite(TNode node);
 
   /** Get the current logic information. */
-  const LogicInfo& getLogicInfo() const;
+  const LogicInfo& logicInfo() const;
+
+  /** Get the options object (const version only) via Env. */
+  const Options& options() const;
+
+  /** Get a pointer to the Context via Env. */
+  context::Context* context() const;
+
+  /** Get a pointer to the UserContext via Env. */
+  context::UserContext* userContext() const;
 
   /** The associated environment. */
   Env& d_env;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ccdf5a90a..500b1edcd 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -46,7 +46,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
       d_eqSolver(nullptr),
       d_internal(new TheoryArithPrivate(*this, env, d_bab)),
       d_nonlinearExtension(nullptr),
-      d_opElim(d_pnm, getLogicInfo()),
+      d_opElim(d_pnm, logicInfo()),
       d_arithPreproc(d_astate, d_im, d_pnm, d_opElim),
       d_rewriter(d_opElim)
 {
@@ -87,8 +87,8 @@ bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi)
 }
 void TheoryArith::finishInit()
 {
-  if (getLogicInfo().isTheoryEnabled(THEORY_ARITH)
-      && getLogicInfo().areTranscendentalsUsed())
+  const LogicInfo& logic = logicInfo();
+  if (logic.isTheoryEnabled(THEORY_ARITH) && logic.areTranscendentalsUsed())
   {
     // witness is used to eliminate square root
     d_valuation.setUnevaluatedKind(kind::WITNESS);
@@ -98,8 +98,7 @@ void TheoryArith::finishInit()
     d_valuation.setUnevaluatedKind(kind::PI);
   }
   // only need to create nonlinear extension if non-linear logic
-  const LogicInfo& logicInfo = getLogicInfo();
-  if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
+  if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())
   {
     d_nonlinearExtension.reset(new nl::NonlinearExtension(*this, d_astate));
   }
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 070300b3b..347a86c1b 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -96,9 +96,9 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
                                            : nullptr),
       d_checker(),
-      d_pfGen(new EagerProofGenerator(d_pnm, d_env.getUserContext())),
-      d_constraintDatabase(d_env.getContext(),
-                           d_env.getUserContext(),
+      d_pfGen(new EagerProofGenerator(d_pnm, userContext())),
+      d_constraintDatabase(context(),
+                           userContext(),
                            d_partialModel,
                            d_congruenceManager,
                            RaiseConflict(*this),
@@ -107,15 +107,15 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_qflraStatus(Result::SAT_UNKNOWN),
       d_unknownsInARow(0),
       d_hasDoneWorkSinceCut(false),
-      d_learner(d_env.getUserContext()),
-      d_assertionsThatDoNotMatchTheirLiterals(d_env.getContext()),
+      d_learner(userContext()),
+      d_assertionsThatDoNotMatchTheirLiterals(context()),
       d_nextIntegerCheckVar(0),
-      d_constantIntegerVariables(d_env.getContext()),
-      d_diseqQueue(d_env.getContext(), false),
+      d_constantIntegerVariables(context()),
+      d_diseqQueue(context(), false),
       d_currentPropagationList(),
-      d_learnedBounds(d_env.getContext()),
-      d_preregisteredNodes(d_env.getContext()),
-      d_partialModel(d_env.getContext(), DeltaComputeCallback(*this)),
+      d_learnedBounds(context()),
+      d_preregisteredNodes(context()),
+      d_partialModel(context(), DeltaComputeCallback(*this)),
       d_errorSet(
           d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)),
       d_tableau(),
@@ -123,23 +123,22 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
               d_tableau,
               d_rowTracking,
               BasicVarModelUpdateCallBack(*this)),
-      d_diosolver(d_env.getContext()),
+      d_diosolver(context()),
       d_restartsCounter(0),
       d_tableauSizeHasBeenModified(false),
       d_tableauResetDensity(1.6),
       d_tableauResetPeriod(10),
-      d_conflicts(d_env.getContext()),
-      d_blackBoxConflict(d_env.getContext(), Node::null()),
-      d_blackBoxConflictPf(d_env.getContext(),
-                           std::shared_ptr<ProofNode>(nullptr)),
-      d_congruenceManager(d_env.getContext(),
-                          d_env.getUserContext(),
+      d_conflicts(context()),
+      d_blackBoxConflict(context(), Node::null()),
+      d_blackBoxConflictPf(context(), std::shared_ptr<ProofNode>(nullptr)),
+      d_congruenceManager(context(),
+                          userContext(),
                           d_constraintDatabase,
                           SetupLiteralCallBack(*this),
                           d_partialModel,
                           RaiseEqualityEngineConflict(*this),
                           d_pnm),
-      d_cmEnabled(d_env.getContext(), options().arith.arithCongMan),
+      d_cmEnabled(context(), options().arith.arithCongMan),
 
       d_dualSimplex(
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
@@ -151,22 +150,22 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
       d_pass1SDP(NULL),
       d_otherSDP(NULL),
-      d_lastContextIntegerAttempted(d_env.getContext(), -1),
+      d_lastContextIntegerAttempted(context(), -1),
 
       d_DELTA_ZERO(0),
-      d_approxCuts(d_env.getContext()),
+      d_approxCuts(context()),
       d_fullCheckCounter(0),
-      d_cutCount(d_env.getContext(), 0),
-      d_cutInContext(d_env.getContext()),
-      d_likelyIntegerInfeasible(d_env.getContext(), false),
-      d_guessedCoeffSet(d_env.getContext(), false),
+      d_cutCount(context(), 0),
+      d_cutInContext(context()),
+      d_likelyIntegerInfeasible(context(), false),
+      d_guessedCoeffSet(context(), false),
       d_guessedCoeffs(),
       d_treeLog(NULL),
       d_replayVariables(),
       d_replayConstraints(),
       d_lhsTmp(),
       d_approxStats(NULL),
-      d_attemptSolveIntTurnedOff(d_env.getUserContext(), 0),
+      d_attemptSolveIntTurnedOff(userContext(), 0),
       d_dioSolveResources(0),
       d_solveIntMaybeHelp(0u),
       d_solveIntAttempts(0u),
@@ -1153,7 +1152,8 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){
   if(!vl.singleton()){
     // vl is the product of at least 2 variables
     // vl : (* v1 v2 ...)
-    if(getLogicInfo().isLinear()){
+    if (logicInfo().isLinear())
+    {
       throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic.");
     }
     d_foundNl = true;
@@ -1305,7 +1305,8 @@ void TheoryArithPrivate::releaseArithVar(ArithVar v){
 ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool aux, bool internal){
   //TODO : The VarList trick is good enough?
   Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS || internal);
-  if(getLogicInfo().isLinear() && Variable::isDivMember(x)){
+  if (logicInfo().isLinear() && Variable::isDivMember(x))
+  {
     stringstream ss;
     ss << "A non-linear fact (involving div/mod/divisibility) was asserted to "
           "arithmetic in a linear logic: "
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 2b746cba1..dd06d4afd 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -46,9 +46,8 @@ ModelManager::~ModelManager() {}
 void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
 {
   // construct the model
-  const LogicInfo& logicInfo = d_env.getLogicInfo();
   // Initialize the model and model builder.
-  if (logicInfo.isQuantified())
+  if (logicInfo().isQuantified())
   {
     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
     Assert(qe != nullptr);
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 2b6719b27..bcd826799 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -189,7 +189,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
 
   // check whether it is not in the current logic, e.g. non-linear arithmetic.
   // if so, undo replacements until it is in the current logic.
-  const LogicInfo& logic = getLogicInfo();
+  const LogicInfo& logic = logicInfo();
   if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
   {
     fo_body = fitToLogic(sygusBody,
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 2ad475f01..67c40eaac 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -34,7 +34,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env,
                                      OutputChannel& out,
                                      Valuation valuation)
     : Theory(THEORY_QUANTIFIERS, env, out, valuation),
-      d_qstate(env, valuation, getLogicInfo()),
+      d_qstate(env, valuation, logicInfo()),
       d_qreg(),
       d_treg(d_qstate, d_qreg),
       d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm),
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index ba1680c6b..b19ba68de 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1208,7 +1208,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
     bool tn_is_monotonic = true;
     if( tn.isSort() ){
       //TODO: use monotonicity inference
-      tn_is_monotonic = !getLogicInfo().isQuantified();
+      tn_is_monotonic = !logicInfo().isQuantified();
     }else{
       tn_is_monotonic = tn.getCardinality().isInfinite();
     }
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 23ac08749..8759f7056 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -146,7 +146,7 @@ TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
   if (nk == COMPREHENSION)
   {
     // set comprehension is an implicit quantifier, require it in the logic
-    if (!getLogicInfo().isQuantified())
+    if (!logicInfo().isQuantified())
     {
       std::stringstream ss;
       ss << "Set comprehensions require quantifiers in the background logic.";
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index db2db9937..b0f2a2472 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -881,7 +881,7 @@ bool SortInference::isMonotonic( TypeNode tn ) {
 
 bool SortInference::isHandledApplyUf(Kind k) const
 {
-  return k == APPLY_UF && !d_env.getLogicInfo().isHigherOrder();
+  return k == APPLY_UF && !logicInfo().isHigherOrder();
 }
 
 }  // namespace theory
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index f6513933f..0c2624d64 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -338,7 +338,7 @@ bool Theory::isLegalElimination(TNode x, TNode val)
   {
     return false;
   }
-  if (!options::produceModels() && !getLogicInfo().isQuantified())
+  if (!options::produceModels() && !logicInfo().isQuantified())
   {
     // Don't care about the model and logic is not quantified, we can eliminate.
     return true;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 72f3d78ac..13e41978c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -158,7 +158,7 @@ void TheoryEngine::finishInit()
   if (options::relevanceFilter())
   {
     d_relManager.reset(
-        new RelevanceManager(d_env.getUserContext(), theory::Valuation(this)));
+        new RelevanceManager(userContext(), theory::Valuation(this)));
   }
 
   // initialize the quantifiers engine
@@ -208,14 +208,11 @@ void TheoryEngine::finishInit()
 
 ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
 
-context::Context* TheoryEngine::getSatContext() const
-{
-  return d_env.getContext();
-}
+context::Context* TheoryEngine::getSatContext() const { return context(); }
 
 context::UserContext* TheoryEngine::getUserContext() const
 {
-  return d_env.getUserContext();
+  return userContext();
 }
 
 TheoryEngine::TheoryEngine(Env& env)
@@ -224,36 +221,34 @@ TheoryEngine::TheoryEngine(Env& env)
       d_logicInfo(env.getLogicInfo()),
       d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
                                            : nullptr),
-      d_lazyProof(d_pnm != nullptr
-                      ? new LazyCDProof(d_pnm,
-                                        nullptr,
-                                        d_env.getUserContext(),
-                                        "TheoryEngine::LazyCDProof")
-                      : nullptr),
-      d_tepg(new TheoryEngineProofGenerator(d_pnm, d_env.getUserContext())),
+      d_lazyProof(
+          d_pnm != nullptr ? new LazyCDProof(
+              d_pnm, nullptr, userContext(), "TheoryEngine::LazyCDProof")
+                           : nullptr),
+      d_tepg(new TheoryEngineProofGenerator(d_pnm, userContext())),
       d_tc(nullptr),
       d_sharedSolver(nullptr),
       d_quantEngine(nullptr),
-      d_decManager(new DecisionManager(d_env.getUserContext())),
+      d_decManager(new DecisionManager(userContext())),
       d_relManager(nullptr),
-      d_inConflict(d_env.getContext(), false),
+      d_inConflict(context(), false),
       d_inSatMode(false),
       d_hasShutDown(false),
-      d_incomplete(d_env.getContext(), false),
-      d_incompleteTheory(d_env.getContext(), THEORY_BUILTIN),
-      d_incompleteId(d_env.getContext(), IncompleteId::UNKNOWN),
-      d_propagationMap(d_env.getContext()),
-      d_propagationMapTimestamp(d_env.getContext(), 0),
-      d_propagatedLiterals(d_env.getContext()),
-      d_propagatedLiteralsIndex(d_env.getContext(), 0),
-      d_atomRequests(d_env.getContext()),
+      d_incomplete(context(), false),
+      d_incompleteTheory(context(), THEORY_BUILTIN),
+      d_incompleteId(context(), IncompleteId::UNKNOWN),
+      d_propagationMap(context()),
+      d_propagationMapTimestamp(context(), 0),
+      d_propagatedLiterals(context()),
+      d_propagatedLiteralsIndex(context(), 0),
+      d_atomRequests(context()),
       d_combineTheoriesTime(smtStatisticsRegistry().registerTimer(
           "TheoryEngine::combineTheoriesTime")),
       d_true(),
       d_false(),
       d_interrupted(false),
       d_inPreregister(false),
-      d_factsAsserted(d_env.getContext(), false)
+      d_factsAsserted(context(), false)
 {
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
       ++ theoryId)
@@ -1063,7 +1058,7 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
   Debug("theory::propagate")
       << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
 
-  Trace("dtview::prop") << std::string(d_env.getContext()->getLevel(), ' ')
+  Trace("dtview::prop") << std::string(context()->getLevel(), ' ')
                         << ":THEORY-PROP: " << literal << endl;
 
   // spendResource();
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 4cc25a887..0c14f329a 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -40,7 +40,7 @@ TheoryModel::TheoryModel(Env& env, std::string name, bool enableFuncModels)
       d_enableFuncModels(enableFuncModels)
 {
   // must use function models when ufHo is enabled
-  Assert(d_enableFuncModels || !d_env.getLogicInfo().isHigherOrder());
+  Assert(d_enableFuncModels || !logicInfo().isHigherOrder());
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 }
@@ -53,7 +53,7 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee)
   d_equalityEngine = ee;
   // The kinds we are treating as function application in congruence
   d_equalityEngine->addFunctionKind(
-      kind::APPLY_UF, false, d_env.getLogicInfo().isHigherOrder());
+      kind::APPLY_UF, false, logicInfo().isHigherOrder());
   d_equalityEngine->addFunctionKind(kind::HO_APPLY);
   d_equalityEngine->addFunctionKind(kind::SELECT);
   // d_equalityEngine->addFunctionKind(kind::STORE);
@@ -294,8 +294,7 @@ Node TheoryModel::getModelValue(TNode n) const
   // return the representative of the term in the equality engine, if it exists
   TypeNode t = ret.getType();
   bool eeHasTerm;
-  if (!d_env.getLogicInfo().isHigherOrder()
-      && (t.isFunction() || t.isPredicate()))
+  if (!logicInfo().isHigherOrder() && (t.isFunction() || t.isPredicate()))
   {
     // functions are in the equality engine, but *not* as first-class members
     // when higher-order is disabled. In this case, we cannot query
@@ -694,7 +693,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) {
   Trace("model-builder") << "  Assigning function (" << f << ") to (" << f_def << ")" << endl;
   Assert(d_uf_models.find(f) == d_uf_models.end());
 
-  if (d_env.getLogicInfo().isHigherOrder())
+  if (logicInfo().isHigherOrder())
   {
     //we must rewrite the function value since the definition needs to be a constant value
     f_def = Rewriter::rewrite( f_def );
@@ -708,7 +707,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) {
     d_uf_models[f] = f_def;
   }
 
-  if (d_env.getLogicInfo().isHigherOrder() && d_equalityEngine->hasTerm(f))
+  if (logicInfo().isHigherOrder() && d_equalityEngine->hasTerm(f))
   {
     Trace("model-builder-debug") << "  ...function is first-class member of equality engine" << std::endl;
     // assign to representative if higher-order
@@ -743,7 +742,7 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() {
     Assert(d_env.getTopLevelSubstitutions().apply(n) == n);
     if( !hasAssignedFunctionDefinition( n ) ){
       Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl;
-      if (d_env.getLogicInfo().isHigherOrder())
+      if (logicInfo().isHigherOrder())
       {
         // if in higher-order mode, assign function definitions modulo equality
         Node r = getRepresentative( n );
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 23a76d273..bbe1588d6 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -130,7 +130,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n)
   {
     // selectors are always assignable (where we guarantee that they are not
     // evaluatable here)
-    if (!d_env.getLogicInfo().isHigherOrder())
+    if (!logicInfo().isHigherOrder())
     {
       Assert(!n.getType().isFunction());
       return true;
@@ -152,7 +152,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n)
   else
   {
     // non-function variables, and fully applied functions
-    if (!d_env.getLogicInfo().isHigherOrder())
+    if (!logicInfo().isHigherOrder())
     {
       // no functions exist, all functions are fully applied
       Assert(n.getKind() != kind::HO_APPLY);
@@ -1229,7 +1229,7 @@ bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m)
 
 void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
 {
-  Assert(!d_env.getLogicInfo().isHigherOrder());
+  Assert(!logicInfo().isHigherOrder());
   uf::UfModelTree ufmt(f);
   Node default_v;
   for (size_t i = 0; i < m->d_uf_terms[f].size(); i++)
@@ -1274,7 +1274,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
 
 void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
 {
-  Assert(d_env.getLogicInfo().isHigherOrder());
+  Assert(logicInfo().isHigherOrder());
   TypeNode type = f.getType();
   std::vector<TypeNode> argTypes = type.getArgTypes();
   std::vector<Node> args;
@@ -1398,7 +1398,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
   Trace("model-builder") << "Assigning function values..." << std::endl;
   std::vector<Node> funcs_to_assign = m->getFunctionsToAssign();
 
-  if (d_env.getLogicInfo().isHigherOrder())
+  if (logicInfo().isHigherOrder())
   {
     // sort based on type size if higher-order
     Trace("model-builder") << "Sort functions by type..." << std::endl;
@@ -1425,7 +1425,7 @@ void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
     Trace("model-builder") << "  Function #" << k << " is " << f << std::endl;
     // std::map< Node, std::vector< Node > >::iterator itht =
     // m->d_ho_uf_terms.find( f );
-    if (!d_env.getLogicInfo().isHigherOrder())
+    if (!logicInfo().isHigherOrder())
     {
       Trace("model-builder") << "  Assign function value for " << f
                              << " based on APPLY_UF" << std::endl;
diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index e3655e3ab..ec7955125 100644
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -21,23 +21,17 @@ namespace cvc5 {
 namespace theory {
 
 TheoryState::TheoryState(Env& env, Valuation val)
-    : EnvObj(env),
-      d_valuation(val),
-      d_ee(nullptr),
-      d_conflict(d_env.getContext(), false)
+    : EnvObj(env), d_valuation(val), d_ee(nullptr), d_conflict(context(), false)
 {
 }
 
 void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
 
-context::Context* TheoryState::getSatContext() const
-{
-  return d_env.getContext();
-}
+context::Context* TheoryState::getSatContext() const { return context(); }
 
 context::UserContext* TheoryState::getUserContext() const
 {
-  return d_env.getUserContext();
+  return userContext();
 }
 
 bool TheoryState::hasTerm(TNode a) const
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9c506f2ac..bdc5304e4 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -48,8 +48,8 @@ TheoryUF::TheoryUF(Env& env,
       d_thss(nullptr),
       d_ho(nullptr),
       d_functionsTerms(getSatContext()),
-      d_symb(getUserContext(), instanceName),
-      d_rewriter(env.getLogicInfo().isHigherOrder()),
+      d_symb(userContext(), instanceName),
+      d_rewriter(logicInfo().isHigherOrder()),
       d_state(env, valuation),
       d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false),
       d_notify(d_im, *this)
@@ -95,9 +95,9 @@ void TheoryUF::finishInit() {
     d_thss.reset(new CardinalityExtension(d_state, d_im, this));
   }
   // The kinds we are treating as function application in congruence
-  d_equalityEngine->addFunctionKind(
-      kind::APPLY_UF, false, getLogicInfo().isHigherOrder());
-  if (getLogicInfo().isHigherOrder())
+  bool isHo = logicInfo().isHigherOrder();
+  d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, isHo);
+  if (isHo)
   {
     d_equalityEngine->addFunctionKind(kind::HO_APPLY);
     d_ho.reset(new HoExtension(d_state, d_im));
@@ -148,7 +148,7 @@ void TheoryUF::postCheck(Effort level)
   // check with the higher-order extension at full effort
   if (!d_state.isInConflict() && fullEffort(level))
   {
-    if (getLogicInfo().isHigherOrder())
+    if (logicInfo().isHigherOrder())
     {
       d_ho->check();
     }
@@ -171,7 +171,7 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
   {
     case kind::EQUAL:
     {
-      if (getLogicInfo().isHigherOrder() && options::ufHoExt())
+      if (logicInfo().isHigherOrder() && options::ufHoExt())
       {
         if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction())
         {
@@ -186,7 +186,7 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
     {
       if (d_thss == nullptr)
       {
-        if (!getLogicInfo().hasCardinalityConstraints())
+        if (!logicInfo().hasCardinalityConstraints())
         {
           std::stringstream ss;
           ss << "Cardinality constraint " << atom
@@ -214,7 +214,7 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
   Kind k = node.getKind();
   if (k == kind::HO_APPLY)
   {
-    if (!getLogicInfo().isHigherOrder())
+    if (!logicInfo().isHigherOrder())
     {
       std::stringstream ss;
       ss << "Partial function applications are only supported with "
@@ -234,7 +234,7 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
     // check for higher-order
     // logic exception if higher-order is not enabled
     if (isHigherOrderType(node.getOperator().getType())
-        && !getLogicInfo().isHigherOrder())
+        && !logicInfo().isHigherOrder())
     {
       std::stringstream ss;
       ss << "UF received an application whose operator has higher-order type "
@@ -256,8 +256,7 @@ void TheoryUF::preRegisterTerm(TNode node)
   }
 
   // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order
-  Assert(node.getKind() != kind::HO_APPLY
-         || getLogicInfo().isHigherOrder());
+  Assert(node.getKind() != kind::HO_APPLY || logicInfo().isHigherOrder());
 
   Kind k = node.getKind();
   switch (k)
@@ -318,7 +317,7 @@ TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); }
 
 bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 {
-  if (getLogicInfo().isHigherOrder())
+  if (logicInfo().isHigherOrder())
   {
     // must add extensionality disequalities for all pairs of (non-disequal)
     // function equivalence classes.