diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-01 00:56:42 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-01 00:56:42 +0000 |
commit | 159cb7ee8b6f28f3784a3f24b371760c2ab77f86 (patch) | |
tree | d510bfa3e4977b5c532d9ab82b6cd5d9581365a3 /src/theory/arith/simplex.h | |
parent | ceca24424da629db2e133f7864b0bac03ad44829 (diff) |
This commit is a merge from the "betterstats" branch, which:
* Makes Options an "omnipresent thread-local global" (like the notion
of the "current NodeManager" was already). Options::current() accesses
this structure.
* Removes Options from constructors and data structures everywhere
(this cleans up a lot of things).
* No longer uses StatisticsRegistry statically. An instance of the
registry is created and linked to a NodeManager.
* StatisticsRegistry::current() is similar to Options::current(), but
the pointer is stowed in the NodeManager (rather than stored)
* The static functions of StatisticsRegistry have been left, for backward
compatibility; they now use the "current" statistics registry.
* SmtEngine::getStatisticsRegistry() is a public accessor for the
registry; this is needed by main() to reach in and get the registry,
for flushing statistics at the end.
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. |