From: Gereon Kremer <nafur42@gmail.com>
Date: Fri, 17 Sep 2021 18:03:37 +0000 (+0200)
Subject: Minor cleanup related to EnvObj (#7206)
X-Git-Tag: cvc5-1.0.0~1203
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d4544c5484e85ae75387124c3826531474e15c26;p=cvc5.git

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 9b7678388..ecb62b554 100644
--- 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 221c0a781..fe941a7fb 100644
--- 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.
    */