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.

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.