diff options
Diffstat (limited to 'src/theory/arith/simplex.h')
-rw-r--r-- | src/theory/arith/simplex.h | 34 |
1 files changed, 15 insertions, 19 deletions
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 91f0bccfc..b1ebe2972 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -48,7 +48,21 @@ public: d_numVariables(0), d_delayedLemmas(), d_ZERO(0) - {} + { + switch(Options::ArithPivotRule rule = Options::current()->pivotRule) { + case Options::MINIMUM: + d_queue.setPivotRule(ArithPriorityQueue::MINIMUM); + break; + case Options::BREAK_TIES: + d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES); + break; + case Options::MAXIMUM: + d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM); + break; + default: + Unhandled(rule); + } + } /** * Assert*(n, orig) takes an bound n that is implied by orig. @@ -179,24 +193,6 @@ private: Node generateConflictBelow(ArithVar conflictVar); public: - void notifyOptions(const Options& opt){ - switch(opt.pivotRule){ - case Options::MINIMUM: - d_queue.setPivotRule(ArithPriorityQueue::MINIMUM); - break; - case Options::BREAK_TIES: - d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES); - break; - case Options::MAXIMUM: - d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM); - break; - default: - Unhandled(opt.pivotRule); - } - } - - -public: /** * Checks to make sure the assignment is consistent with the tableau. * This code is for debugging. |