diff options
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r-- | src/theory/arith/simplex.cpp | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 63bb42e7a..e77067d61 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -19,6 +19,7 @@ #include "theory/arith/simplex.h" +#include "theory/arith/options.h" using namespace std; @@ -41,14 +42,14 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, d_pivotsInRound(), d_DELTA_ZERO(0,0) { - switch(Options::ArithHeuristicPivotRule rule = Options::current()->arithHeuristicPivotRule) { - case Options::MINIMUM: + switch(ArithHeuristicPivotRule rule = options::arithHeuristicPivotRule()) { + case MINIMUM: d_queue.setPivotRule(ArithPriorityQueue::MINIMUM); break; - case Options::BREAK_TIES: + case BREAK_TIES: d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES); break; - case Options::MAXIMUM: + case MAXIMUM: d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM); break; default: @@ -262,13 +263,13 @@ Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){ } } static const bool verbose = false; - exactResult |= Options::current()->arithStandardCheckVarOrderPivots < 0; - const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : Options::current()->arithStandardCheckVarOrderPivots; + exactResult |= options::arithStandardCheckVarOrderPivots() < 0; + const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : options::arithStandardCheckVarOrderPivots(); - uint32_t checkPeriod = Options::current()->arithSimplexCheckPeriod; + uint32_t checkPeriod = options::arithSimplexCheckPeriod(); if(result == Result::SAT_UNKNOWN){ - uint32_t numDifferencePivots = Options::current()->arithHeuristicPivots < 0 ? - d_numVariables + 1 : Options::current()->arithHeuristicPivots; + uint32_t numDifferencePivots = options::arithHeuristicPivots() < 0 ? + d_numVariables + 1 : options::arithHeuristicPivots(); // The signed to unsigned conversion is safe. uint32_t pivotsRemaining = numDifferencePivots; while(!d_queue.empty() && @@ -421,7 +422,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera --remainingIterations; - bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= Options::current()->arithPivotThreshold; + bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= options::arithPivotThreshold(); if(!useVarOrderPivot){ d_pivotsInRound.add(x_i); } @@ -429,7 +430,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera Debug("playground") << "pivots in rounds: " << d_pivotsInRound.count(x_i) << " use " << useVarOrderPivot - << " threshold " << Options::current()->arithPivotThreshold + << " threshold " << options::arithPivotThreshold() << endl; PreferenceFunction pf = useVarOrderPivot ? minVarOrder : minBoundAndRowCount; |