Start using Options via Env in arithmetic (#7032)

This PR refactors part of the arithmetic theory to use the options via the Env object.

13 files changed, 204 insertions, 169 deletions

diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index 7db6c266f..b196f9990 100644
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -30,20 +30,18 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-ExtState::ExtState(InferenceManager& im,
-                   NlModel& model,
-                   ProofNodeManager* pnm,
-                   context::UserContext* c)
-    : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c)
+ExtState::ExtState(InferenceManager& im, NlModel& model, Env& env)
+    : d_im(im), d_model(model), d_env(env)
 {
   d_false = NodeManager::currentNM()->mkConst(false);
   d_true = NodeManager::currentNM()->mkConst(true);
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
-  if (d_pnm != nullptr)
+  if (d_env.isTheoryProofProducing())
   {
-    d_proof.reset(new CDProofSet<CDProof>(d_pnm, d_ctx, "nl-ext"));
+    d_proof.reset(new CDProofSet<CDProof>(
+        d_env.getProofNodeManager(), d_env.getUserContext(), "nl-ext"));
   }
 }
 
@@ -105,7 +103,7 @@ bool ExtState::isProofEnabled() const { return d_proof.get() != nullptr; }
 CDProof* ExtState::getProof()
 {
   Assert(isProofEnabled());
-  return d_proof->allocateProof(d_ctx);
+  return d_proof->allocateProof(d_env.getUserContext());
 }
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index 7c2cc1b9b..ac00f6f87 100644
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -20,6 +20,7 @@
 
 #include "expr/node.h"
 #include "proof/proof_set.h"
+#include "smt/env.h"
 #include "theory/arith/nl/ext/monomial.h"
 
 namespace cvc5 {
@@ -37,10 +38,7 @@ class NlModel;
 
 struct ExtState
 {
-  ExtState(InferenceManager& im,
-           NlModel& model,
-           ProofNodeManager* pnm,
-           context::UserContext* c);
+  ExtState(InferenceManager& im, NlModel& model, Env& env);
 
   void init(const std::vector<Node>& xts);
 
@@ -63,13 +61,8 @@ struct ExtState
   InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
-  /**
-   * Pointer to the current proof node manager. nullptr, if proofs are
-   * disabled.
-   */
-  ProofNodeManager* d_pnm;
-  /** The user context. */
-  context::UserContext* d_ctx;
+  /** Reference to the environment */
+  Env& d_env;
   /**
    * A CDProofSet that hands out CDProof objects for lemmas.
    */
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 0deb2c99d..31bc4c662 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -207,7 +207,7 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
       }
       // compute if bound is not satisfied, and store what is required
       // for a possible refinement
-      if (options::nlExtTangentPlanes())
+      if (d_data->d_env.getOptions().arith.nlExtTangentPlanes)
       {
         if (is_false_lit)
         {
diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index 6d9faa356..dcd6398b5 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -29,7 +29,7 @@ namespace arith {
 namespace nl {
 
 SplitZeroCheck::SplitZeroCheck(ExtState* data)
-    : d_data(data), d_zero_split(d_data->d_ctx)
+    : d_data(data), d_zero_split(d_data->d_env.getUserContext())
 {
 }
 
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 785127db5..df531fca7 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -37,27 +37,29 @@ namespace arith {
 namespace nl {
 
 NonlinearExtension::NonlinearExtension(TheoryArith& containing,
-                                       ArithState& state,
-                                       eq::EqualityEngine* ee,
-                                       ProofNodeManager* pnm)
+                                       ArithState& state)
     : d_containing(containing),
+      d_astate(state),
       d_im(containing.getInferenceManager()),
       d_needsLastCall(false),
       d_checkCounter(0),
-      d_extTheoryCb(ee),
+      d_extTheoryCb(state.getEqualityEngine()),
       d_extTheory(d_extTheoryCb,
                   containing.getSatContext(),
                   containing.getUserContext(),
                   d_im),
       d_model(containing.getSatContext()),
-      d_trSlv(d_im, d_model, pnm, containing.getUserContext()),
-      d_extState(d_im, d_model, pnm, containing.getUserContext()),
+      d_trSlv(d_im, d_model, d_astate.getEnv()),
+      d_extState(d_im, d_model, d_astate.getEnv()),
       d_factoringSlv(&d_extState),
       d_monomialBoundsSlv(&d_extState),
       d_monomialSlv(&d_extState),
       d_splitZeroSlv(&d_extState),
       d_tangentPlaneSlv(&d_extState),
-      d_cadSlv(d_im, d_model, state.getUserContext(), pnm),
+      d_cadSlv(d_im,
+               d_model,
+               state.getUserContext(),
+               d_astate.getEnv().getProofNodeManager()),
       d_icpSlv(d_im),
       d_iandSlv(d_im, state, d_model),
       d_pow2Slv(d_im, state, d_model)
@@ -73,9 +75,9 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
 
-  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
-  if (pc != nullptr)
+  if (d_astate.getEnv().isTheoryProofProducing())
   {
+    ProofChecker* pc = d_astate.getEnv().getProofNodeManager()->getChecker();
     d_proofChecker.registerTo(pc);
   }
 }
@@ -94,6 +96,11 @@ void NonlinearExtension::processSideEffect(const NlLemma& se)
   d_trSlv.processSideEffect(se);
 }
 
+const Options& NonlinearExtension::options() const
+{
+  return d_containing.options();
+}
+
 void NonlinearExtension::computeRelevantAssertions(
     const std::vector<Node>& assertions, std::vector<Node>& keep)
 {
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index aae19df6e..6cbbfcdac 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -84,10 +84,7 @@ class NonlinearExtension
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  NonlinearExtension(TheoryArith& containing,
-                     ArithState& state,
-                     eq::EqualityEngine* ee,
-                     ProofNodeManager* pnm);
+  NonlinearExtension(TheoryArith& containing, ArithState& state);
   ~NonlinearExtension();
   /**
    * Does non-context dependent setup for a node connected to a theory.
@@ -145,6 +142,9 @@ class NonlinearExtension
   /** Process side effect se */
   void processSideEffect(const NlLemma& se);
 
+  /** Obtain options object */
+  const Options& options() const;
+
  private:
   /** Model-based refinement
    *
@@ -223,6 +223,8 @@ class NonlinearExtension
   Node d_true;
   // The theory of arithmetic containing this extension.
   TheoryArith& d_containing;
+  /** A reference to the arithmetic state object */
+  ArithState& d_astate;
   InferenceManager& d_im;
   /** The statistics class */
   NlStats d_stats;
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 0d5e5ad04..c7bb14b3f 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -39,11 +39,10 @@ namespace transcendental {
 
 TranscendentalSolver::TranscendentalSolver(InferenceManager& im,
                                            NlModel& m,
-                                           ProofNodeManager* pnm,
-                                           context::UserContext* c)
-    : d_tstate(im, m, pnm, c), d_expSlv(&d_tstate), d_sineSlv(&d_tstate)
+                                           Env& env)
+    : d_tstate(im, m, env), d_expSlv(&d_tstate), d_sineSlv(&d_tstate)
 {
-  d_taylor_degree = options::nlExtTfTaylorDegree();
+  d_taylor_degree = d_tstate.d_env.getOptions().arith.nlExtTfTaylorDegree;
 }
 
 TranscendentalSolver::~TranscendentalSolver() {}
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h
index 54bad2c1d..b63ebf29d 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.h
@@ -50,10 +50,7 @@ namespace transcendental {
 class TranscendentalSolver
 {
  public:
-  TranscendentalSolver(InferenceManager& im,
-                       NlModel& m,
-                       ProofNodeManager* pnm,
-                       context::UserContext* c);
+  TranscendentalSolver(InferenceManager& im, NlModel& m, Env& env);
   ~TranscendentalSolver();
 
   /** init last call
@@ -187,7 +184,7 @@ class TranscendentalSolver
    * initially to options::nlExtTfTaylorDegree() and may be incremented
    * if the option options::nlExtTfIncPrecision() is enabled.
    */
-  unsigned d_taylor_degree;
+  uint64_t d_taylor_degree;
 
   /** Common state for transcendental solver */
   transcendental::TranscendentalState d_tstate;
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index db20713f1..19a334729 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -30,20 +30,20 @@ namespace transcendental {
 
 TranscendentalState::TranscendentalState(InferenceManager& im,
                                          NlModel& model,
-                                         ProofNodeManager* pnm,
-                                         context::UserContext* c)
-    : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c)
+                                         Env& env)
+    : d_im(im), d_model(model), d_env(env)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
-  if (d_pnm != nullptr)
+  if (d_env.isTheoryProofProducing())
   {
-    d_proof.reset(new CDProofSet<CDProof>(d_pnm, d_ctx, "nl-trans"));
+    d_proof.reset(new CDProofSet<CDProof>(
+        d_env.getProofNodeManager(), d_env.getUserContext(), "nl-trans"));
     d_proofChecker.reset(new TranscendentalProofRuleChecker());
-    d_proofChecker->registerTo(pnm->getChecker());
+    d_proofChecker->registerTo(d_env.getProofNodeManager()->getChecker());
   }
 }
 
@@ -55,7 +55,7 @@ bool TranscendentalState::isProofEnabled() const
 CDProof* TranscendentalState::getProof()
 {
   Assert(isProofEnabled());
-  return d_proof->allocateProof(d_ctx);
+  return d_proof->allocateProof(d_env.getUserContext());
 }
 
 void TranscendentalState::init(const std::vector<Node>& xts,
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 56cbec79a..65215c83c 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -18,6 +18,7 @@
 
 #include "expr/node.h"
 #include "proof/proof_set.h"
+#include "smt/env.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/transcendental/proof_checker.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
@@ -61,10 +62,7 @@ inline std::ostream& operator<<(std::ostream& os, Convexity c) {
  */
 struct TranscendentalState
 {
-  TranscendentalState(InferenceManager& im,
-                      NlModel& model,
-                      ProofNodeManager* pnm,
-                      context::UserContext* c);
+  TranscendentalState(InferenceManager& im, NlModel& model, Env& env);
 
   /**
    * Checks whether proofs are enabled.
@@ -170,16 +168,11 @@ struct TranscendentalState
   InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
+  /** Reference to the environment */
+  Env& d_env;
   /** Utility to compute taylor approximations */
   TaylorGenerator d_taylor;
   /**
-   * Pointer to the current proof node manager. nullptr, if proofs are
-   * disabled.
-   */
-  ProofNodeManager* d_pnm;
-  /** The user context. */
-  context::UserContext* d_ctx;
-  /**
    * A CDProofSet that hands out CDProof objects for lemmas.
    */
   std::unique_ptr<CDProofSet<CDProof>> d_proof;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 37069d8b8..aabf017a8 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -44,8 +44,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
       d_ppre(getSatContext(), d_pnm),
       d_bab(d_astate, d_im, d_ppre, d_pnm),
       d_eqSolver(nullptr),
-      d_internal(new TheoryArithPrivate(
-          *this, getSatContext(), getUserContext(), d_bab, d_pnm)),
+      d_internal(new TheoryArithPrivate(*this, env, d_bab)),
       d_nonlinearExtension(nullptr),
       d_opElim(d_pnm, getLogicInfo()),
       d_arithPreproc(d_astate, d_im, d_pnm, d_opElim),
@@ -102,8 +101,7 @@ void TheoryArith::finishInit()
   const LogicInfo& logicInfo = getLogicInfo();
   if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
   {
-    d_nonlinearExtension.reset(
-        new nl::NonlinearExtension(*this, d_astate, d_equalityEngine, d_pnm));
+    d_nonlinearExtension.reset(new nl::NonlinearExtension(*this, d_astate));
   }
   if (d_eqSolver != nullptr)
   {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 3102dc7b8..ea2887c44 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -86,19 +86,19 @@ static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum)
 static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap);
 
 TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
-                                       context::Context* c,
-                                       context::UserContext* u,
-                                       BranchAndBound& bab,
-                                       ProofNodeManager* pnm)
+                                       Env& env,
+                                       BranchAndBound& bab)
     : d_containing(containing),
+      d_env(env),
       d_foundNl(false),
       d_rowTracking(),
       d_bab(bab),
-      d_pnm(pnm),
+      d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
+                                           : nullptr),
       d_checker(),
-      d_pfGen(new EagerProofGenerator(d_pnm, u)),
-      d_constraintDatabase(c,
-                           u,
+      d_pfGen(new EagerProofGenerator(d_pnm, d_env.getUserContext())),
+      d_constraintDatabase(d_env.getContext(),
+                           d_env.getUserContext(),
                            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(u),
-      d_assertionsThatDoNotMatchTheirLiterals(c),
+      d_learner(d_env.getUserContext()),
+      d_assertionsThatDoNotMatchTheirLiterals(d_env.getContext()),
       d_nextIntegerCheckVar(0),
-      d_constantIntegerVariables(c),
-      d_diseqQueue(c, false),
+      d_constantIntegerVariables(d_env.getContext()),
+      d_diseqQueue(d_env.getContext(), false),
       d_currentPropagationList(),
-      d_learnedBounds(c),
-      d_preregisteredNodes(u),
-      d_partialModel(c, DeltaComputeCallback(*this)),
+      d_learnedBounds(d_env.getContext()),
+      d_preregisteredNodes(d_env.getUserContext()),
+      d_partialModel(d_env.getContext(), DeltaComputeCallback(*this)),
       d_errorSet(
           d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)),
       d_tableau(),
@@ -123,22 +123,23 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
               d_tableau,
               d_rowTracking,
               BasicVarModelUpdateCallBack(*this)),
-      d_diosolver(c),
+      d_diosolver(d_env.getContext()),
       d_restartsCounter(0),
       d_tableauSizeHasBeenModified(false),
       d_tableauResetDensity(1.6),
       d_tableauResetPeriod(10),
-      d_conflicts(c),
-      d_blackBoxConflict(c, Node::null()),
-      d_blackBoxConflictPf(c, std::shared_ptr<ProofNode>(nullptr)),
-      d_congruenceManager(c,
-                          u,
+      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_constraintDatabase,
                           SetupLiteralCallBack(*this),
                           d_partialModel,
                           RaiseEqualityEngineConflict(*this),
                           d_pnm),
-      d_cmEnabled(c, options::arithCongMan()),
+      d_cmEnabled(d_env.getContext(), options().arith.arithCongMan),
 
       d_dualSimplex(
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
@@ -150,22 +151,22 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
       d_pass1SDP(NULL),
       d_otherSDP(NULL),
-      d_lastContextIntegerAttempted(c, -1),
+      d_lastContextIntegerAttempted(d_env.getContext(), -1),
 
       d_DELTA_ZERO(0),
-      d_approxCuts(c),
+      d_approxCuts(d_env.getContext()),
       d_fullCheckCounter(0),
-      d_cutCount(c, 0),
-      d_cutInContext(c),
-      d_likelyIntegerInfeasible(c, false),
-      d_guessedCoeffSet(c, false),
+      d_cutCount(d_env.getContext(), 0),
+      d_cutInContext(d_env.getContext()),
+      d_likelyIntegerInfeasible(d_env.getContext(), false),
+      d_guessedCoeffSet(d_env.getContext(), false),
       d_guessedCoeffs(),
       d_treeLog(NULL),
       d_replayVariables(),
       d_replayConstraints(),
       d_lhsTmp(),
       d_approxStats(NULL),
-      d_attemptSolveIntTurnedOff(u, 0),
+      d_attemptSolveIntTurnedOff(d_env.getUserContext(), 0),
       d_dioSolveResources(0),
       d_solveIntMaybeHelp(0u),
       d_solveIntAttempts(0u),
@@ -509,13 +510,13 @@ bool TheoryArithPrivate::getDioCuttingResource(){
   if(d_dioSolveResources > 0){
     d_dioSolveResources--;
     if(d_dioSolveResources == 0){
-      d_dioSolveResources = -options::rrTurns();
+      d_dioSolveResources = -options().arith.rrTurns;
     }
     return true;
   }else{
     d_dioSolveResources++;
     if(d_dioSolveResources >= 0){
-      d_dioSolveResources = options::dioSolverTurns();
+      d_dioSolveResources = options().arith.dioSolverTurns;
     }
     return false;
   }
@@ -1047,7 +1048,7 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(
       // Add the substitution if not recursive
       Assert(elim == Rewriter::rewrite(elim));
 
-      if (right.size() > options::ppAssertMaxSubSize())
+      if (right.size() > options().arith.ppAssertMaxSubSize)
       {
         Debug("simplify")
             << "TheoryArithPrivate::solve(): did not substitute due to the "
@@ -1882,7 +1883,10 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em
 
   if(d_qflraStatus == Result::UNSAT){ return false; }
   if(emmmittedLemmaOrSplit){ return false; }
-  if(!options::useApprox()){ return false; }
+  if (!options().arith.useApprox)
+  {
+    return false;
+  }
   if(!ApproximateSimplex::enabled()){ return false; }
 
   if(Theory::fullEffort(effortLevel)){
@@ -1902,8 +1906,10 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em
     }
   }
 
-
-  if(!options::trySolveIntStandardEffort()){ return false; }
+  if (!options().arith.trySolveIntStandardEffort)
+  {
+    return false;
+  }
 
   if (d_lastContextIntegerAttempted <= (level >> 2))
   {
@@ -2352,7 +2358,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
 
         if(ci->reconstructed() && ci->proven()){
           const DenseMap<Rational>& row = ci->getReconstruction().lhs;
-          reject = !complexityBelow(row, options::replayRejectCutSize());
+          reject = !complexityBelow(row, options().arith.replayRejectCutSize);
         }
       }
       if(conflictQueueEmpty()){
@@ -2400,8 +2406,9 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
 
     /* check if the system is feasible under with the cuts */
     if(conflictQueueEmpty()){
-      Assert(options::replayEarlyCloseDepths() >= 1);
-      if(!nl.isBranch() || depth % options::replayEarlyCloseDepths() == 0 ){
+      Assert(options().arith.replayEarlyCloseDepths >= 1);
+      if (!nl.isBranch() || depth % options().arith.replayEarlyCloseDepths == 0)
+      {
         TimerStat::CodeTimer codeTimer(d_statistics.d_replaySimplexTimer);
         //test for linear feasibility
         d_partialModel.stopQueueingBoundCounts();
@@ -2515,8 +2522,8 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
     resolveOutPropagated(res, propagated);
     Debug("approx::replayLogRec") << "replayLogRec() ending" << std::endl;
 
-
-    if(options::replayFailureLemma()){
+    if (options().arith.replayFailureLemma)
+    {
       // must be done inside the sat context to get things
       // propagated at this level
       if(res.empty() && nid == getTreeLog().getRootId()){
@@ -2659,7 +2666,8 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
       Assert(cut->proven());
 
       const DenseMap<Rational>& row =  cut->getReconstruction().lhs;
-      if(!complexityBelow(row, options::lemmaRejectCutSize())){
+      if (!complexityBelow(row, options().arith.lemmaRejectCutSize))
+      {
         ++(d_statistics.d_cutsRejectedDuringLemmas);
         continue;
       }
@@ -2746,7 +2754,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
   }
 
   // if integers are attempted,
-  Assert(options::useApprox());
+  Assert(options().arith.useApprox);
   Assert(ApproximateSimplex::enabled());
 
   int level = getSatContext()->getLevel();
@@ -2769,8 +2777,9 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
       approx->setOptCoeffs(d_guessedCoeffs);
     }
     static const int32_t depthForLikelyInfeasible = 10;
-    int maxDepthPass1 = d_likelyIntegerInfeasible ?
-      depthForLikelyInfeasible : options::maxApproxDepth();
+    int maxDepthPass1 = d_likelyIntegerInfeasible
+                            ? depthForLikelyInfeasible
+                            : options().arith.maxApproxDepth;
     approx->setBranchingDepth(maxDepthPass1);
     approx->setBranchOnVariableLimit(100);
     LinResult relaxRes = approx->solveRelaxation();
@@ -2833,7 +2842,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
           }
         }
         if(!(anyConflict() || !d_approxCuts.empty())){
-          turnOffApproxFor(options::replayNumericFailurePenalty());
+          turnOffApproxFor(options().arith.replayNumericFailurePenalty);
         }
         break;
       case BranchesExhausted:
@@ -2873,11 +2882,16 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
 SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){
   if(pass1){
     if(d_pass1SDP == NULL){
-      if(options::useFC()){
+      if (options().arith.useFC)
+      {
         d_pass1SDP = (SimplexDecisionProcedure*)(&d_fcSimplex);
-      }else if(options::useSOI()){
+      }
+      else if (options().arith.useSOI)
+      {
         d_pass1SDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
-      }else{
+      }
+      else
+      {
         d_pass1SDP = (SimplexDecisionProcedure*)(&d_dualSimplex);
       }
     }
@@ -2885,13 +2899,18 @@ SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){
     return *d_pass1SDP;
   }else{
      if(d_otherSDP == NULL){
-      if(options::useFC()){
-        d_otherSDP  = (SimplexDecisionProcedure*)(&d_fcSimplex);
-      }else if(options::useSOI()){
-        d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
-      }else{
-        d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
-      }
+       if (options().arith.useFC)
+       {
+         d_otherSDP = (SimplexDecisionProcedure*)(&d_fcSimplex);
+       }
+       else if (options().arith.useSOI)
+       {
+         d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
+       }
+       else
+       {
+         d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
+       }
     }
     Assert(d_otherSDP != NULL);
     return *d_otherSDP;
@@ -2912,8 +2931,8 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu
   }
 
   if(d_qflraStatus != Result::UNSAT){
-    static const int32_t pass2Limit = 20;
-    int16_t oldCap = options::arithStandardCheckVarOrderPivots();
+    static const int64_t pass2Limit = 20;
+    int64_t oldCap = options().arith.arithStandardCheckVarOrderPivots;
     Options::current().arith.arithStandardCheckVarOrderPivots = pass2Limit;
     SimplexDecisionProcedure& simplex = selectSimplex(false);
     d_qflraStatus = simplex.findModel(false);
@@ -2964,20 +2983,19 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
   d_partialModel.processBoundsQueue(utcb);
   d_linEq.startTrackingBoundCounts();
 
-  bool noPivotLimit = Theory::fullEffort(effortLevel) ||
-    !options::restrictedPivots();
+  bool noPivotLimit =
+      Theory::fullEffort(effortLevel) || !options().arith.restrictedPivots;
 
   SimplexDecisionProcedure& simplex = selectSimplex(true);
 
-  bool useApprox = options::useApprox() && ApproximateSimplex::enabled() && getSolveIntegerResource();
+  bool useApprox = options().arith.useApprox && ApproximateSimplex::enabled()
+                   && getSolveIntegerResource();
 
   Debug("TheoryArithPrivate::solveRealRelaxation")
-    << "solveRealRelaxation() approx"
-    << " " <<  options::useApprox()
-    << " " << ApproximateSimplex::enabled()
-    << " " << useApprox
-    << " " << safeToCallApprox()
-    << endl;
+      << "solveRealRelaxation() approx"
+      << " " << options().arith.useApprox << " "
+      << ApproximateSimplex::enabled() << " " << useApprox << " "
+      << safeToCallApprox() << endl;
 
   bool noPivotLimitPass1 = noPivotLimit && !useApprox;
   d_qflraStatus = simplex.findModel(noPivotLimitPass1);
@@ -3136,7 +3154,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
 
   if(anyConflict()){
     d_qflraStatus = Result::UNSAT;
-    if (options::revertArithModels() && d_previousStatus == Result::SAT)
+    if (options().arith.revertArithModels && d_previousStatus == Result::SAT)
     {
       ++d_statistics.d_revertsOnConflicts;
       Debug("arith::bt") << "clearing here "
@@ -3211,10 +3229,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
     if(Debug.isOn("arith::consistency")){
       Assert(entireStateIsConsistent("sat comit"));
     }
-    if(useSimplex && options::collectPivots()){
-      if(options::useFC()){
+    if (useSimplex && options().arith.collectPivots)
+    {
+      if (options().arith.useFC)
+      {
         d_statistics.d_satPivots << d_fcSimplex.getPivots();
-      }else{
+      }
+      else
+      {
         d_statistics.d_satPivots << d_dualSimplex.getPivots();
       }
     }
@@ -3229,10 +3251,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
     d_partialModel.commitAssignmentChanges();
     d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow);
 
-    if(useSimplex && options::collectPivots()){
-      if(options::useFC()){
+    if (useSimplex && options().arith.collectPivots)
+    {
+      if (options().arith.useFC)
+      {
         d_statistics.d_unknownPivots << d_fcSimplex.getPivots();
-      }else{
+      }
+      else
+      {
         d_statistics.d_unknownPivots << d_dualSimplex.getPivots();
       }
     }
@@ -3255,10 +3281,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
     emmittedConflictOrSplit = true;
     Debug("arith::conflict") << "simplex conflict" << endl;
 
-    if(useSimplex && options::collectPivots()){
-      if(options::useFC()){
+    if (useSimplex && options().arith.collectPivots)
+    {
+      if (options().arith.useFC)
+      {
         d_statistics.d_unsatPivots << d_fcSimplex.getPivots();
-      }else{
+      }
+      else
+      {
         d_statistics.d_unsatPivots << d_dualSimplex.getPivots();
       }
     }
@@ -3268,8 +3298,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
   }
   d_statistics.d_avgUnknownsInARow << d_unknownsInARow;
 
-  size_t nPivots =
-      options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots();
+  size_t nPivots = options().arith.useFC ? d_fcSimplex.getPivots()
+                                         : d_dualSimplex.getPivots();
   for (std::size_t i = 0; i < nPivots; ++i)
   {
     d_containing.d_out->spendResource(
@@ -3298,9 +3328,9 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
 
   // This should be fine if sat or unknown
   if (!emmittedConflictOrSplit
-      && (options::arithPropagationMode()
+      && (options().arith.arithPropagationMode
               == options::ArithPropagationMode::UNATE_PROP
-          || options::arithPropagationMode()
+          || options().arith.arithPropagationMode
                  == options::ArithPropagationMode::BOTH_PROP))
   {
     TimerStat::CodeTimer codeTimer0(d_statistics.d_newPropTime);
@@ -3383,7 +3413,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
 
   if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel) && !hasIntegerModel()){
     Node possibleConflict = Node::null();
-    if(!emmittedConflictOrSplit && options::arithDioSolver()){
+    if (!emmittedConflictOrSplit && options().arith.arithDioSolver)
+    {
       possibleConflict = callDioSolver();
       if(possibleConflict != Node::null()){
         revertOutOfConflict();
@@ -3395,7 +3426,9 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
       }
     }
 
-    if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && options::arithDioSolver()){
+    if (!emmittedConflictOrSplit && d_hasDoneWorkSinceCut
+        && options().arith.arithDioSolver)
+    {
       if(getDioCuttingResource()){
         TrustNode possibleLemma = dioCutting();
         if(!possibleLemma.isNull()){
@@ -3425,7 +3458,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
       }
     }
 
-    if(options::maxCutsInContext() <= d_cutCount){
+    if (options().arith.maxCutsInContext <= d_cutCount)
+    {
       if(d_diosolver.hasMoreDecompositionLemmas()){
         while(d_diosolver.hasMoreDecompositionLemmas()){
           Node decompositionLemma = d_diosolver.nextDecompositionLemma();
@@ -3497,7 +3531,8 @@ std::vector<ArithVar> TheoryArithPrivate::cutAllBounded() const{
   vector<ArithVar> lemmas;
   ArithVar max = d_partialModel.getNumberOfVariables();
 
-  if(options::doCutAllBounded() && max > 0){
+  if (options().arith.doCutAllBounded && max > 0)
+  {
     for(ArithVar iter = 0; iter != max; ++iter){
     //Do not include slack variables
       const DeltaRational& d = d_partialModel.getAssignment(iter);
@@ -3645,15 +3680,18 @@ TrustNode TheoryArithPrivate::explain(TNode n)
 void TheoryArithPrivate::propagate(Theory::Effort e) {
   // This uses model values for safety. Disable for now.
   if (d_qflraStatus == Result::SAT
-      && (options::arithPropagationMode()
+      && (options().arith.arithPropagationMode
               == options::ArithPropagationMode::BOUND_INFERENCE_PROP
-          || options::arithPropagationMode()
+          || options().arith.arithPropagationMode
                  == options::ArithPropagationMode::BOTH_PROP)
       && hasAnyUpdates())
   {
-    if(options::newProp()){
+    if (options().arith.newProp)
+    {
       propagateCandidatesNew();
-    }else{
+    }
+    else
+    {
       propagateCandidates();
     }
   }
@@ -4022,8 +4060,10 @@ void TheoryArithPrivate::presolve(){
   }
 
   vector<TrustNode> lemmas;
-  if(!options::incrementalSolving()) {
-    switch(options::arithUnateLemmaMode()){
+  if (!options().base.incrementalSolving)
+  {
+    switch (options().arith.arithUnateLemmaMode)
+    {
       case options::ArithUnateLemmaMode::NO: break;
       case options::ArithUnateLemmaMode::INEQUALITY:
         d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
@@ -4035,7 +4075,7 @@ void TheoryArithPrivate::presolve(){
         d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
         d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
         break;
-      default: Unhandled() << options::arithUnateLemmaMode();
+      default: Unhandled() << options().arith.arithUnateLemmaMode;
     }
   }
 
@@ -4183,10 +4223,14 @@ void TheoryArithPrivate::propagateCandidates(){
   DenseSet::const_iterator end = d_updatedBounds.end();
   for(; i != end; ++i){
     ArithVar var = *i;
-    if(d_tableau.isBasic(var) &&
-       d_tableau.basicRowLength(var) <= options::arithPropagateMaxLength()){
+    if (d_tableau.isBasic(var)
+        && d_tableau.basicRowLength(var)
+               <= options().arith.arithPropagateMaxLength)
+    {
       d_candidateBasics.softAdd(var);
-    }else{
+    }
+    else
+    {
       Tableau::ColIterator basicIter = d_tableau.colIterator(var);
       for(; !basicIter.atEnd(); ++basicIter){
         const Tableau::Entry& entry = *basicIter;
@@ -4194,7 +4238,9 @@ void TheoryArithPrivate::propagateCandidates(){
         ArithVar rowVar = d_tableau.rowIndexToBasic(ridx);
         Assert(entry.getColVar() == var);
         Assert(d_tableau.isBasic(rowVar));
-        if(d_tableau.getRowLength(ridx) <= options::arithPropagateMaxLength()){
+        if (d_tableau.getRowLength(ridx)
+            <= options().arith.arithPropagateMaxLength)
+        {
           d_candidateBasics.softAdd(rowVar);
         }
       }
@@ -4428,7 +4474,8 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
     //   * coeffs[0] is for implied
     //   * coeffs[i+1] is for explain[i]
     d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs);
-    if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
+    if (d_tableau.getRowLength(ridx) <= options().arith.arithPropAsLemmaLength)
+    {
       if (Debug.isOn("arith::prop::pf")) {
         for (const auto & constraint : explain) {
           Assert(constraint->hasProof());
@@ -4493,7 +4540,9 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
       {
         outputLemma(clause, InferenceId::ARITH_ROW_IMPL);
       }
-    }else{
+    }
+    else
+    {
       Assert(!implied->negationHasProof());
       implied->impliedByFarkas(explain, coeffs, false);
       implied->tryToPropagate();
@@ -4521,9 +4570,9 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
   Debug("arith::prop")
     << "propagateCandidateRow " << instance << " attempt " << rowLength << " " <<  hasCount << endl;
 
-  if (rowLength >= options::arithPropagateMaxLength()
+  if (rowLength >= options().arith.arithPropagateMaxLength
       && Random::getRandom().pickWithProb(
-             1.0 - double(options::arithPropagateMaxLength()) / rowLength))
+          1.0 - double(options().arith.arithPropagateMaxLength) / rowLength))
   {
     return false;
   }
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 4afe121b9..0cdc031e1 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -88,6 +88,9 @@ private:
   static const uint32_t RESET_START = 2;
 
   TheoryArith& d_containing;
+  Env& d_env;
+
+  const Options& options() const { return d_env.getOptions(); }
 
   /**
    * Whether we encountered non-linear arithmetic at any time during solving.
@@ -423,11 +426,7 @@ private:
   DeltaRational getDeltaValue(TNode term) const
       /* throw(DeltaRationalException, ModelException) */;
  public:
-  TheoryArithPrivate(TheoryArith& containing,
-                     context::Context* c,
-                     context::UserContext* u,
-                     BranchAndBound& bab,
-                     ProofNodeManager* pnm);
+  TheoryArithPrivate(TheoryArith& containing, Env& env, BranchAndBound& bab);
   ~TheoryArithPrivate();
 
   //--------------------------------- initialization