Minor cleanup related to EnvObj (#7206)

This PR does a bit of cleanup in the nonlinear arithmetic code related to the usage of EnvObj.

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index 9b76783882c55d0faad32ea66c282f83730dff3b..ecb62b55488daedd50a53c9e68b87542a5219475 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -47,7 +47,7 @@ CDCAC::CDCAC(Env& env, const std::vector<poly::Variable>& ordering)
   if (d_env.isTheoryProofProducing())
   {
     d_proof.reset(
-        new CADProofGenerator(d_env.getContext(), d_env.getProofNodeManager()));
+        new CADProofGenerator(context(), d_env.getProofNodeManager()));
   }
 }
 
@@ -76,7 +76,7 @@ void CDCAC::computeVariableOrdering()
 
 void CDCAC::retrieveInitialAssignment(NlModel& model, const Node& ran_variable)
 {
-  if (!d_env.getOptions().arith.nlCadUseInitial) return;
+  if (!options().arith.nlCadUseInitial) return;
   d_initialAssignment.clear();
   Trace("cdcac") << "Retrieving initial assignment:" << std::endl;
   for (const auto& var : d_variableOrdering)
@@ -102,7 +102,7 @@ std::vector<CACInterval> CDCAC::getUnsatIntervals(std::size_t cur_variable)
 {
   std::vector<CACInterval> res;
   LazardEvaluation le;
-  if (d_env.getOptions().arith.nlCadLifting
+  if (options().arith.nlCadLifting
       == options::NlCadLiftingMode::LAZARD)
   {
     for (size_t vid = 0; vid < cur_variable; ++vid)
@@ -127,7 +127,7 @@ 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 (d_env.getOptions().arith.nlCadLifting
+    if (options().arith.nlCadLifting
         == options::NlCadLiftingMode::LAZARD)
     {
       intervals = le.infeasibleRegions(p, sc);
@@ -172,7 +172,7 @@ bool CDCAC::sampleOutsideWithInitial(const std::vector<CACInterval>& infeasible,
                                      poly::Value& sample,
                                      std::size_t cur_variable)
 {
-  if (d_env.getOptions().arith.nlCadUseInitial
+  if (options().arith.nlCadUseInitial
       && cur_variable < d_initialAssignment.size())
   {
     const poly::Value& suggested = d_initialAssignment[cur_variable];
@@ -306,7 +306,7 @@ PolyVector CDCAC::requiredCoefficients(const poly::Polynomial& p)
                    << requiredCoefficientsOriginal(p, d_assignment)
                    << std::endl;
   }
-  switch (d_env.getOptions().arith.nlCadProjection)
+  switch (options().arith.nlCadProjection)
   {
     case options::NlCadProjectionMode::MCCALLUM:
       return requiredCoefficientsOriginal(p, d_assignment);

diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 221c0a781532ddeea51291264352e09e720047c1..fe941a7fb49c520fd92645dd90d1762c901aeb34 100644 (file)
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -89,8 +89,6 @@ class TheoryArithPrivate : protected EnvObj
 
   TheoryArith& d_containing;
 
-  const Options& options() const { return d_env.getOptions(); }
-
   /**
    * Whether we encountered non-linear arithmetic at any time during solving.
    */