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 543cb9587f2e70f269b327d0e18b2a5d11041f74..16ce2f4c0ac15376a9805d4814ac05b7e8105b06 100644 (file)
--- 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 49c17172f3b6b929b5fe26e81676bc221f217621..f706babda20a13047ac44e9f35c82f896f940c03 100644 (file)
--- 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 fe5b26eaa65853e33d2d1e4dc489b174c8a8177c..8e36c1b549d4ceee8f37302ebbf32a2bf785ad87 100644 (file)
--- 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 fc2ed8fa9cbdcd5687fc807c0fbb49568d6f28d0..94f6742e32f99e8984ff2f8ccfbbd4e86afd3d81 100644 (file)
--- 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 e43f86743dfa4525698cff7f0ee5644fbb0a8154..c0c51f7da00bb67bd738621cf1181c8e0ba5b51c 100644 (file)
--- 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")){