Use Env class in nonlinear extension (#7039)

This PR refactors the nonlinear extension(s) to access options only via the environment class.

diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp
index 22859977b695f90d90397420f7e29a52e71ef968..ca1a2fa6fd0d1df10ef55da190683df11ed92b8b 100644 (file)
--- a/src/theory/arith/branch_and_bound.cpp
+++ b/src/theory/arith/branch_and_bound.cpp
@@ -45,7 +45,7 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value)
   TrustNode lem = TrustNode::null();
   NodeManager* nm = NodeManager::currentNM();
   Integer floor = value.floor();
-  if (options::brabTest())
+  if (d_astate.options().arith.brabTest)
   {
     Trace("integers") << "branch-round-and-bound enabled" << std::endl;
     Integer ceil = value.ceiling();

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 9cb23290874288155c4a5220364a1a16d002607a..1563ca418ad718e6acf0b7973e81059f9e976049 100644 (file)
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -29,7 +29,7 @@ InferenceManager::InferenceManager(TheoryArith& ta,
                                    ProofNodeManager* pnm)
     : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::"),
       // currently must track propagated literals if using the equality solver
-      d_trackPropLits(options::arithEqSolver()),
+      d_trackPropLits(astate.options().arith.arithEqSolver),
       d_propLits(astate.getSatContext())
 {
 }
@@ -127,7 +127,7 @@ bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 
 bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem)
 {
-  if (options::nlExtEntailConflicts())
+  if (d_theoryState.options().arith.nlExtEntailConflicts)
   {
     Node ch_lemma = lem.d_node.negate();
     ch_lemma = Rewriter::rewrite(ch_lemma);

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index 57010d1a1b3c8bffc684c64599e861bb4e40d60b..9b37a135f649e92d21e6c5e1e3325bd0e3cfc54a 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -41,14 +41,13 @@ namespace arith {
 namespace nl {
 namespace cad {
 
-CDCAC::CDCAC(context::Context* ctx,
-             ProofNodeManager* pnm,
-             const std::vector<poly::Variable>& ordering)
-    : d_variableOrdering(ordering)
+CDCAC::CDCAC(Env& env, const std::vector<poly::Variable>& ordering)
+    : d_env(env), d_variableOrdering(ordering)
 {
-  if (pnm != nullptr)
+  if (d_env.isTheoryProofProducing())
   {
-    d_proof.reset(new CADProofGenerator(ctx, pnm));
+    d_proof.reset(
+        new CADProofGenerator(d_env.getContext(), d_env.getProofNodeManager()));
   }
 }
 
@@ -77,7 +76,7 @@ void CDCAC::computeVariableOrdering()
 
 void CDCAC::retrieveInitialAssignment(NlModel& model, const Node& ran_variable)
 {
-  if (!options::nlCadUseInitial()) return;
+  if (!d_env.getOptions().arith.nlCadUseInitial) return;
   d_initialAssignment.clear();
   Trace("cdcac") << "Retrieving initial assignment:" << std::endl;
   for (const auto& var : d_variableOrdering)
@@ -103,7 +102,8 @@ std::vector<CACInterval> CDCAC::getUnsatIntervals(std::size_t cur_variable)
 {
   std::vector<CACInterval> res;
   LazardEvaluation le;
-  if (options::nlCadLifting() == options::NlCadLiftingMode::LAZARD)
+  if (d_env.getOptions().arith.nlCadLifting
+      == options::NlCadLiftingMode::LAZARD)
   {
     for (size_t vid = 0; vid < cur_variable; ++vid)
     {
@@ -127,7 +127,8 @@ std::vector<CACInterval> CDCAC::getUnsatIntervals(std::size_t cur_variable)
     Trace("cdcac") << "Infeasible intervals for " << p << " " << sc
                    << " 0 over " << d_assignment << std::endl;
     std::vector<poly::Interval> intervals;
-    if (options::nlCadLifting() == options::NlCadLiftingMode::LAZARD)
+    if (d_env.getOptions().arith.nlCadLifting
+        == options::NlCadLiftingMode::LAZARD)
     {
       intervals = le.infeasibleRegions(p, sc);
       if (Trace.isOn("cdcac"))
@@ -171,7 +172,8 @@ bool CDCAC::sampleOutsideWithInitial(const std::vector<CACInterval>& infeasible,
                                      poly::Value& sample,
                                      std::size_t cur_variable)
 {
-  if (options::nlCadUseInitial() && cur_variable < d_initialAssignment.size())
+  if (d_env.getOptions().arith.nlCadUseInitial
+      && cur_variable < d_initialAssignment.size())
   {
     const poly::Value& suggested = d_initialAssignment[cur_variable];
     for (const auto& i : infeasible)
@@ -305,7 +307,7 @@ PolyVector CDCAC::requiredCoefficients(const poly::Polynomial& p)
                    << requiredCoefficientsOriginal(p, d_assignment)
                    << std::endl;
   }
-  switch (options::nlCadProjection())
+  switch (d_env.getOptions().arith.nlCadProjection)
   {
     case options::NlCadProjectionMode::MCCALLUM:
       return requiredCoefficientsOriginal(p, d_assignment);

diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index a7552895396f1d35ebb863d0d3f0afbae7ac055c..b504998d87f00aee291dc44c0f5fb07c90b20213 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -25,6 +25,7 @@
 
 #include <vector>
 
+#include "smt/env.h"
 #include "theory/arith/nl/cad/cdcac_utils.h"
 #include "theory/arith/nl/cad/constraints.h"
 #include "theory/arith/nl/cad/proof_generator.h"
@@ -47,9 +48,7 @@ class CDCAC
 {
  public:
   /** Initialize this method with the given variable ordering. */
-  CDCAC(context::Context* ctx,
-        ProofNodeManager* pnm,
-        const std::vector<poly::Variable>& ordering = {});
+  CDCAC(Env& env, const std::vector<poly::Variable>& ordering = {});
 
   /** Reset this instance. */
   void reset();
@@ -185,6 +184,9 @@ class CDCAC
    */
   void pruneRedundantIntervals(std::vector<CACInterval>& intervals);
 
+  /** A reference to the environment */
+  Env& d_env;
+
   /**
    * The current assignment. When the method terminates with SAT, it contains a
    * model for the input constraints.

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 5d30d5db49d7ccae52a31c94089ac9996736bb75..ebaeb9d61aa7b98a2aa6710a07739b6f25eddc88 100644 (file)
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -27,13 +27,10 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-CadSolver::CadSolver(InferenceManager& im,
-                     NlModel& model,
-                     context::Context* ctx,
-                     ProofNodeManager* pnm)
+CadSolver::CadSolver(Env& env, InferenceManager& im, NlModel& model)
     :
 #ifdef CVC5_POLY_IMP
-      d_CAC(ctx, pnm),
+      d_CAC(env),
 #endif
       d_foundSatisfiability(false),
       d_im(im),
@@ -44,9 +41,9 @@ CadSolver::CadSolver(InferenceManager& im,
   d_ranVariable = sm->mkDummySkolem(
       "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME);
 #ifdef CVC5_POLY_IMP
-  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
-  if (pc != nullptr)
+  if (env.isTheoryProofProducing())
   {
+    ProofChecker* pc = env.getProofNodeManager()->getChecker();
     // add checkers
     d_proofChecker.registerTo(pc);
   }

diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index b9becec44725384bdcdba2e8b849ea7ca62e09fe..94bcb2907b97b0c721f392b3e022ef20d6549e18 100644 (file)
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -43,10 +43,7 @@ class NlModel;
 class CadSolver
 {
  public:
-  CadSolver(InferenceManager& im,
-            NlModel& model,
-            context::Context* ctx,
-            ProofNodeManager* pnm);
+  CadSolver(Env& env, InferenceManager& im, NlModel& model);
   ~CadSolver();
 
   /**

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 8200ff08eaaf24425778a3610932977eafbfba3c..eb5620a82fc0106a9055141a1fbdf72fc3feeac4 100644 (file)
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -37,6 +37,7 @@ namespace nl {
 IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model)
     : d_im(im),
       d_model(model),
+      d_astate(state),
       d_initRefine(state.getUserContext())
 {
   NodeManager* nm = NodeManager::currentNM();
@@ -151,7 +152,7 @@ void IAndSolver::checkFullRefine()
       }
 
       // ************* additional lemma schemas go here
-      if (options::iandMode() == options::IandMode::SUM)
+      if (d_astate.options().smt.iandMode == options::IandMode::SUM)
       {
         Node lem = sumBasedLemma(i);  // add lemmas based on sum mode
         Trace("iand-lemma")
@@ -161,7 +162,7 @@ void IAndSolver::checkFullRefine()
         d_im.addPendingLemma(
             lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true);
       }
-      else if (options::iandMode() == options::IandMode::BITWISE)
+      else if (d_astate.options().smt.iandMode == options::IandMode::BITWISE)
       {
         Node lem = bitwiseLemma(i);  // check for violated bitwise axioms
         Trace("iand-lemma")
@@ -244,7 +245,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 = options::BVAndIntegerGranularity();
+  uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity;
   NodeManager* nm = NodeManager::currentNM();
   Node lem = nm->mkNode(
       EQUAL, i, d_iandUtils.createSumNode(x, y, bvsize, granularity));
@@ -258,7 +259,7 @@ Node IAndSolver::bitwiseLemma(Node i)
   Node y = i[1];
 
   unsigned bvsize = i.getOperator().getConst<IntAnd>().d_size;
-  uint64_t granularity = options::BVAndIntegerGranularity();
+  uint64_t granularity = d_astate.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 c80edbeb312a9118a094c3193d875c375e978450..1be469259921a0b15ed015121a0411dad207881f 100644 (file)
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -85,6 +85,8 @@ class IAndSolver
   InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
+  /** Reference to the arithmetic state */
+  ArithState& d_astate;
   /** commonly used terms */
   Node d_false;
   Node d_true;

diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index ed4a5318f291f8b5254aa0e85b5dd149135b103e..ca75a1a064dd0cbd1892ec60780e578ae3f76814 100644 (file)
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -32,7 +32,7 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-NlModel::NlModel(context::Context* c) : d_used_approx(false)
+NlModel::NlModel() : d_used_approx(false)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -1263,7 +1263,8 @@ void NlModel::printModelValue(const char* c, Node n, unsigned prec) const
 void NlModel::getModelValueRepair(
     std::map<Node, Node>& arithModel,
     std::map<Node, std::pair<Node, Node>>& approximations,
-    std::map<Node, Node>& witnesses)
+    std::map<Node, Node>& witnesses,
+    bool witnessToValue)
 {
   Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl;
   // If we extended the model with entries x -> 0 for unconstrained values,
@@ -1289,7 +1290,7 @@ void NlModel::getModelValueRepair(
       pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v));
       Trace("nl-model") << v << " approximated as " << pred << std::endl;
       Node witness;
-      if (options::modelWitnessValue())
+      if (witnessToValue)
       {
         // witness is the midpoint
         witness = nm->mkNode(

diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index acf5ee7f5405319d72c02124299140285d69801f..526a9393497a6ffa6d8f30367fb879a3ae5b2ffa 100644 (file)
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -52,7 +52,7 @@ class NlModel
   friend class NonlinearExtension;
 
  public:
-  NlModel(context::Context* c);
+  NlModel();
   ~NlModel();
   /**
    * This method is called once at the beginning of a last call effort check,
@@ -194,7 +194,8 @@ class NlModel
   void getModelValueRepair(
       std::map<Node, Node>& arithModel,
       std::map<Node, std::pair<Node, Node>>& approximations,
-      std::map<Node, Node>& witnesses);
+      std::map<Node, Node>& witnesses,
+      bool witnessToValue);
 
  private:
   /** The current model */

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index df531fca79440cea8b12f9ea27c0ada6cdb36d65..c0ea3195ada0616faa0774f13338ba7e3e814625 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/nl/nonlinear_extension.h"
 
 #include "options/arith_options.h"
+#include "options/smt_options.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/bound_inference.h"
 #include "theory/arith/inference_manager.h"
@@ -48,7 +49,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                   containing.getSatContext(),
                   containing.getUserContext(),
                   d_im),
-      d_model(containing.getSatContext()),
+      d_model(),
       d_trSlv(d_im, d_model, d_astate.getEnv()),
       d_extState(d_im, d_model, d_astate.getEnv()),
       d_factoringSlv(&d_extState),
@@ -56,10 +57,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_monomialSlv(&d_extState),
       d_splitZeroSlv(&d_extState),
       d_tangentPlaneSlv(&d_extState),
-      d_cadSlv(d_im,
-               d_model,
-               state.getUserContext(),
-               d_astate.getEnv().getProofNodeManager()),
+      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)
@@ -121,11 +119,11 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
 {
   Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl;
   bool useRelevance = false;
-  if (options::nlRlvMode() == options::NlRlvMode::INTERLEAVE)
+  if (options().arith.nlRlvMode == options::NlRlvMode::INTERLEAVE)
   {
     useRelevance = (d_checkCounter % 2);
   }
-  else if (options::nlRlvMode() == options::NlRlvMode::ALWAYS)
+  else if (options().arith.nlRlvMode == options::NlRlvMode::ALWAYS)
   {
     useRelevance = true;
   }
@@ -228,7 +226,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions)
   // relevance here, since we may have discarded literals that are relevant
   // that are entailed based on the techniques in getAssertions.
   std::vector<Node> passertions = assertions;
-  if (options::nlExt() == options::NlExtMode::FULL)
+  if (options().arith.nlExt == options::NlExtMode::FULL)
   {
     // preprocess the assertions with the trancendental solver
     if (!d_trSlv.preprocessAssertionsCheckModel(passertions))
@@ -236,7 +234,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions)
       return false;
     }
   }
-  if (options::nlCad())
+  if (options().arith.nlCad)
   {
     d_cadSlv.constructModelIfAvailable(passertions);
   }
@@ -260,7 +258,7 @@ void NonlinearExtension::check(Theory::Effort e)
   if (e == Theory::EFFORT_FULL)
   {
     d_needsLastCall = true;
-    if (options::nlExtRewrites())
+    if (options().arith.nlExtRewrites)
     {
       std::vector<Node> nred;
       if (!d_extTheory.doInferences(0, nred))
@@ -484,8 +482,8 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termS
       }
 
       // we are incomplete
-      if (options::nlExt() == options::NlExtMode::FULL
-          && options::nlExtIncPrecision() && d_model.usedApproximate())
+      if (options().arith.nlExt == options::NlExtMode::FULL
+          && options().arith.nlExtIncPrecision && d_model.usedApproximate())
       {
         d_trSlv.incrementTaylorDegree();
         needsRecheck = true;
@@ -529,7 +527,10 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel,
     d_approximations.clear();
     d_witnesses.clear();
     // modify the model values
-    d_model.getModelValueRepair(arithModel, d_approximations, d_witnesses);
+    d_model.getModelValueRepair(arithModel,
+                                d_approximations,
+                                d_witnesses,
+                                options().smt.modelWitnessValue);
   }
 }
 
@@ -554,7 +555,7 @@ void NonlinearExtension::runStrategy(Theory::Effort effort,
   }
   if (!d_strategy.isStrategyInit())
   {
-    d_strategy.initializeStrategy();
+    d_strategy.initializeStrategy(options());
   }
 
   auto steps = d_strategy.getStrategy();

diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp
index f20cf42216028e23f91151560a21f19256eac358..b33e45129a3d7b0e2e80cbdd94b927d9abfd0a3d 100644 (file)
--- a/src/theory/arith/nl/strategy.cpp
+++ b/src/theory/arith/nl/strategy.cpp
@@ -105,22 +105,22 @@ bool StepGenerator::hasNext() const { return d_next < d_steps.size(); }
 InferStep StepGenerator::next() { return d_steps[d_next++]; }
 
 bool Strategy::isStrategyInit() const { return !d_interleaving.empty(); }
-void Strategy::initializeStrategy()
+void Strategy::initializeStrategy(const Options& options)
 {
   StepSequence one;
-  if (options::nlICP())
+  if (options.arith.nlICP)
   {
     one << InferStep::ICP << InferStep::BREAK;
   }
-  if (options::nlExt() == options::NlExtMode::FULL
-      || options::nlExt() == options::NlExtMode::LIGHT)
+  if (options.arith.nlExt == options::NlExtMode::FULL
+      || options.arith.nlExt == options::NlExtMode::LIGHT)
   {
     one << InferStep::NL_INIT << InferStep::BREAK;
   }
-  if (options::nlExt() == options::NlExtMode::FULL)
+  if (options.arith.nlExt == options::NlExtMode::FULL)
   {
     one << InferStep::TRANS_INIT << InferStep::BREAK;
-    if (options::nlExtSplitZero())
+    if (options.arith.nlExtSplitZero)
     {
       one << InferStep::NL_SPLIT_ZERO << InferStep::BREAK;
     }
@@ -130,39 +130,39 @@ void Strategy::initializeStrategy()
   one << InferStep::IAND_INITIAL << InferStep::BREAK;
   one << InferStep::POW2_INIT;
   one << InferStep::POW2_INITIAL << InferStep::BREAK;
-  if (options::nlExt() == options::NlExtMode::FULL
-      || options::nlExt() == options::NlExtMode::LIGHT)
+  if (options.arith.nlExt == options::NlExtMode::FULL
+      || options.arith.nlExt == options::NlExtMode::LIGHT)
   {
     one << InferStep::NL_MONOMIAL_SIGN << InferStep::BREAK;
     one << InferStep::NL_MONOMIAL_MAGNITUDE0 << InferStep::BREAK;
   }
-  if (options::nlExt() == options::NlExtMode::FULL)
+  if (options.arith.nlExt == options::NlExtMode::FULL)
   {
     one << InferStep::TRANS_MONOTONIC << InferStep::BREAK;
     one << InferStep::NL_MONOMIAL_MAGNITUDE1 << InferStep::BREAK;
     one << InferStep::NL_MONOMIAL_MAGNITUDE2 << InferStep::BREAK;
     one << InferStep::NL_MONOMIAL_INFER_BOUNDS;
-    if (options::nlExtTangentPlanes()
-        && options::nlExtTangentPlanesInterleave())
+    if (options.arith.nlExtTangentPlanes
+        && options.arith.nlExtTangentPlanesInterleave)
     {
       one << InferStep::NL_TANGENT_PLANES;
     }
     one << InferStep::BREAK;
     one << InferStep::FLUSH_WAITING_LEMMAS << InferStep::BREAK;
-    if (options::nlExtFactor())
+    if (options.arith.nlExtFactor)
     {
       one << InferStep::NL_FACTORING << InferStep::BREAK;
     }
-    if (options::nlExtResBound())
+    if (options.arith.nlExtResBound)
     {
       one << InferStep::NL_MONOMIAL_INFER_BOUNDS << InferStep::BREAK;
     }
-    if (options::nlExtTangentPlanes()
-        && !options::nlExtTangentPlanesInterleave())
+    if (options.arith.nlExtTangentPlanes
+        && !options.arith.nlExtTangentPlanesInterleave)
     {
       one << InferStep::NL_TANGENT_PLANES_WAITING;
     }
-    if (options::nlExtTfTangentPlanes())
+    if (options.arith.nlExtTfTangentPlanes)
     {
       one << InferStep::TRANS_TANGENT_PLANES;
     }
@@ -170,11 +170,11 @@ void Strategy::initializeStrategy()
   }
   one << InferStep::IAND_FULL << InferStep::BREAK;
   one << InferStep::POW2_FULL << InferStep::BREAK;
-  if (options::nlCad())
+  if (options.arith.nlCad)
   {
     one << InferStep::CAD_INIT;
   }
-  if (options::nlCad())
+  if (options.arith.nlCad)
   {
     one << InferStep::CAD_FULL << InferStep::BREAK;
   }

diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h
index e2fc6c1c65703f4c91ba2997917540a5ffa2ac7c..d5010885139d0d01fc75e124d5ea1258398c8fac 100644 (file)
--- a/src/theory/arith/nl/strategy.h
+++ b/src/theory/arith/nl/strategy.h
@@ -19,6 +19,8 @@
 #include <iosfwd>
 #include <vector>
 
+#include "options/options.h"
+
 namespace cvc5 {
 namespace theory {
 namespace arith {
@@ -170,7 +172,7 @@ class Strategy
   /** Is this strategy initialized? */
   bool isStrategyInit() const;
   /** Initialize this strategy */
-  void initializeStrategy();
+  void initializeStrategy(const Options& options);
   /** Retrieve the strategy for the given effort e */
   StepGenerator getStrategy();
 

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index aabf017a8494dbd0130797f7133f7cea4faed4de..cb3f21da03d4d1e82a47d863af4683f3ffcbd935 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -56,7 +56,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
   d_theoryState = &d_astate;
   d_inferManager = &d_im;
 
-  if (options::arithEqSolver())
+  if (options().arith.arithEqSolver)
   {
     d_eqSolver.reset(new EqualitySolver(d_astate, d_im));
   }

diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp
index d7580a9cd65e28b93730f6abb2186d4333de9ead..4c9b104c73c13092fccc24dc846ba8d943e10d40 100644 (file)
--- a/test/unit/theory/theory_arith_cad_white.cpp
+++ b/test/unit/theory/theory_arith_cad_white.cpp
@@ -224,7 +224,9 @@ TEST_F(TestTheoryWhiteArithCAD, lazard_eval)
 
 TEST_F(TestTheoryWhiteArithCAD, test_cdcac_1)
 {
-  cad::CDCAC cac(nullptr, nullptr, {});
+  Options opts;
+  Env env(NodeManager::currentNM(), &opts);
+  cad::CDCAC cac(env, {});
   poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x"));
   poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y"));
 
@@ -244,7 +246,9 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_1)
 
 TEST_F(TestTheoryWhiteArithCAD, test_cdcac_2)
 {
-  cad::CDCAC cac(nullptr, nullptr, {});
+  Options opts;
+  Env env(NodeManager::currentNM(), &opts);
+  cad::CDCAC cac(env, {});
   poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x"));
   poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y"));
 
@@ -273,7 +277,9 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_2)
 
 TEST_F(TestTheoryWhiteArithCAD, test_cdcac_3)
 {
-  cad::CDCAC cac(nullptr, nullptr, {});
+  Options opts;
+  Env env(NodeManager::currentNM(), &opts);
+  cad::CDCAC cac(env, {});
   poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x"));
   poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y"));
   poly::Variable z = cac.getConstraints().varMapper()(make_real_variable("z"));
@@ -294,7 +300,9 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_3)
 
 TEST_F(TestTheoryWhiteArithCAD, test_cdcac_4)
 {
-  cad::CDCAC cac(nullptr, nullptr, {});
+  Options opts;
+  Env env(NodeManager::currentNM(), &opts);
+  cad::CDCAC cac(env, {});
   poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x"));
   poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y"));
   poly::Variable z = cac.getConstraints().varMapper()(make_real_variable("z"));
@@ -317,7 +325,9 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_4)
 
 void test_delta(const std::vector<Node>& a)
 {
-  cad::CDCAC cac(nullptr, nullptr, {});
+  Options opts;
+  Env env(NodeManager::currentNM(), &opts);
+  cad::CDCAC cac(env, {});
   cac.reset();
   for (const Node& n : a)
   {