From 159cb7ee8b6f28f3784a3f24b371760c2ab77f86 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 1 Apr 2011 00:56:42 +0000
Subject: 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.
---
 src/theory/arith/arith_priority_queue.cpp | 18 ++++++++++++++++
 src/theory/arith/arith_priority_queue.h   |  1 +
 src/theory/arith/arith_rewriter.cpp       |  2 +-
 src/theory/arith/simplex.h                | 34 ++++++++++++++-----------------
 src/theory/arith/theory_arith.h           |  3 ---
 5 files changed, 35 insertions(+), 23 deletions(-)

(limited to 'src/theory/arith')

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.
@@ -178,24 +192,6 @@ private:
   Node generateConflictAbove(ArithVar conflictVar);
   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.
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;
-- 
cgit v1.2.3