From: Gereon Kremer <nafur42@gmail.com>
Date: Fri, 17 Sep 2021 18:14:24 +0000 (+0200)
Subject: Replace write access to options by a local variable (#7207)
X-Git-Tag: cvc5-1.0.0~1202
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1f51aa7fe56076c6db970f0ed392ff55a6038a6a;p=cvc5.git

Replace write access to options by a local variable (#7207)

This PR replaces a write to the options object by a local variable in the simplex procedure base class. The write was used to temporarily lower a limit for a single simplex call.
---

diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 543cb9587..16ce2f4c0 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -84,8 +84,7 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
   Result::Sat result = Result::SAT_UNKNOWN;
 
   static const bool verbose = false;
-  exactResult |= options::arithStandardCheckVarOrderPivots() < 0;
-
+  exactResult |= d_varOrderPivotLimit < 0;
 
   uint32_t checkPeriod = options::arithSimplexCheckPeriod();
   if(result == Result::SAT_UNKNOWN){
@@ -127,9 +126,12 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
           result = Result::UNSAT;
         }
       }
-    }else if( options::arithStandardCheckVarOrderPivots() > 0){
+    }
+    else if (d_varOrderPivotLimit > 0)
+    {
       d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
-      if(searchForFeasibleSolution(options::arithStandardCheckVarOrderPivots())){
+      if (searchForFeasibleSolution(d_varOrderPivotLimit))
+      {
         result = Result::UNSAT;
       }
       if (verbose)
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 49c17172f..f706babda 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -113,7 +113,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
 
   Debug("arith::findModel") << "fcFindModel(" << instance <<") start non-trivial" << endl;
 
-  exactResult |= options::arithStandardCheckVarOrderPivots() < 0;
+  exactResult |= d_varOrderPivotLimit < 0;
 
   d_prevWitnessImprovement = HeuristicDegenerate;
   d_witnessImprovementInARow = 0;
@@ -124,7 +124,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
     if(exactResult){
       d_pivotBudget = -1;
     }else{
-      d_pivotBudget = options::arithStandardCheckVarOrderPivots();
+      d_pivotBudget = d_varOrderPivotLimit;
     }
 
     result = dualLike();
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index fe5b26eaa..8e36c1b54 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -128,6 +128,12 @@ protected:
   /** A local copy of -1. */
   const Rational d_negOne;
 
+  /**
+   * Locally cached value of arithStandardCheckVarOrderPivots option. It is
+   * cached here to allow for single runs with a different (lower) limit.
+   */
+  int64_t d_varOrderPivotLimit = -1;
+
   ArithVar constructInfeasiblityFunction(TimerStat& timer);
   ArithVar constructInfeasiblityFunction(TimerStat& timer, ArithVar e);
   ArithVar constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set);
@@ -162,7 +168,11 @@ public:
 
 
   uint32_t getPivots() const { return d_pivots; }
-protected:
+
+  /** Set the variable ordering pivot limit */
+  void setVarOrderPivotLimit(int64_t value) { d_varOrderPivotLimit = value; }
+
+ protected:
 
   /** Reports a conflict to on the output channel. */
   void reportConflict(ArithVar basic);
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index fc2ed8fa9..94f6742e3 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -111,7 +111,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
 
   Debug("soi::findModel") << "fcFindModel(" << instance <<") start non-trivial" << endl;
 
-  exactResult |= options::arithStandardCheckVarOrderPivots() < 0;
+  exactResult |= d_varOrderPivotLimit < 0;
 
   d_prevWitnessImprovement = HeuristicDegenerate;
   d_witnessImprovementInARow = 0;
@@ -122,7 +122,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
     if(exactResult){
       d_pivotBudget = -1;
     }else{
-      d_pivotBudget = options::arithStandardCheckVarOrderPivots();
+      d_pivotBudget = d_varOrderPivotLimit;
     }
 
     result = sumOfInfeasibilities();
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index e43f86743..c0c51f7da 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2899,11 +2899,9 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu
 
   if(d_qflraStatus != Result::UNSAT){
     static const int64_t pass2Limit = 20;
-    int64_t oldCap = options().arith.arithStandardCheckVarOrderPivots;
-    Options::current().arith.arithStandardCheckVarOrderPivots = pass2Limit;
     SimplexDecisionProcedure& simplex = selectSimplex(false);
+    simplex.setVarOrderPivotLimit(pass2Limit);
     d_qflraStatus = simplex.findModel(false);
-    Options::current().arith.arithStandardCheckVarOrderPivots = oldCap;
   }
 
   if(Debug.isOn("arith::importSolution")){