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.

8 files changed, 39 insertions, 38 deletions

diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 3bd5dc91d..4905f4dc5 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -255,3 +255,21 @@ void ArithPriorityQueue::clear(){
   Assert(d_varOrderQueue.empty());
   Assert(d_diffQueue.empty());
 }
+
+std::ostream& CVC4::theory::arith::operator<<(std::ostream& out, ArithPriorityQueue::PivotRule rule) {
+  switch(rule) {
+  case ArithPriorityQueue::MINIMUM:
+    out << "MINIMUM";
+    break;
+  case ArithPriorityQueue::BREAK_TIES:
+    out << "BREAK_TIES";
+    break;
+  case ArithPriorityQueue::MAXIMUM:
+    out << "MAXIMUM";
+    break;
+  default:
+    out << "PivotRule!UNKNOWN";
+  }
+
+  return out;
+}
diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index 4c83d648f..f912d7753 100644
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -294,6 +294,7 @@ private:
   Statistics d_statistics;
 };
 
+std::ostream& operator<<(std::ostream& out, ArithPriorityQueue::PivotRule rule);
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index cecbefdee..09cfabdc8 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -261,7 +261,7 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
   }else if(reduction.getKind() == kind::LT){
     Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
     reduction = currNM->mkNode(kind::NOT, geq);
-  }else if( Options::rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
+  }else if( Options::current()->rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
     Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
     Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]);
     reduction = currNM->mkNode(kind::AND, geq, leq);
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.
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index a90e37bdc..85f554849 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -171,9 +171,6 @@ public:
 
   std::string identify() const { return std::string("TheoryArith"); }
 
-  void notifyOptions(const Options& opt) {
-    d_simplex.notifyOptions(opt);
-  }
 private:
   /** The constant zero. */
   DeltaRational d_DELTA_ZERO;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 72341869d..b5122d3c5 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -405,11 +405,6 @@ public:
    */
   virtual std::string identify() const = 0;
 
-  /**
-   * Notify the theory of the current set of options.
-   */
-  virtual void notifyOptions(const Options& opt) { }
-
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, Theory::Effort level);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2411956f5..d1040e6fc 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -68,7 +68,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
     d_engine->getSharedTermManager()->addEq(fact);
   }
 
-  if(d_engine->d_theoryRegistration && !fact.getAttribute(RegisteredAttr())) {
+  if(Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr())) {
     list<TNode> toReg;
     toReg.push_back(fact);
 
@@ -126,17 +126,15 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
         d_engine->theoryOf(n)->registerTerm(n);
       }
     }
-  }/* d_engine->d_theoryRegistration && !fact.getAttribute(RegisteredAttr()) */
+  }/* Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr()) */
 }
 
-TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
+TheoryEngine::TheoryEngine(context::Context* ctxt) :
   d_propEngine(NULL),
   d_context(ctxt),
   d_theoryOut(this, ctxt),
-  d_theoryRegistration(opts.theoryRegistration),
   d_hasShutDown(false),
   d_incomplete(ctxt, false),
-  d_opts(opts),
   d_statistics() {
 
   Rewriter::init();
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index b773a84ee..be2e6e271 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -155,14 +155,12 @@ class TheoryEngine {
    */
   Node removeITEs(TNode t);
 
-  const Options& d_opts;
-
 public:
 
   /**
    * Construct a theory engine.
    */
-  TheoryEngine(context::Context* ctxt, const Options& opts);
+  TheoryEngine(context::Context* ctxt);
 
   /**
    * Destroy a theory engine.
@@ -177,8 +175,6 @@ public:
     TheoryClass* theory = new TheoryClass(d_context, d_theoryOut, theory::Valuation(this));
     d_theoryTable[theory->getId()] = theory;
     d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory));
-
-    theory->notifyOptions(d_opts);
   }
 
   SharedTermManager* getSharedTermManager() {