- Adds a path for Theory to be passed a reference to Options.

- Adds 3 choices of heuristic variable orders to use in ArithPriorityQueue.
- Adds the pivot-rule command line option.

9 files changed, 141 insertions, 9 deletions

diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 14a228e62..23f547344 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -12,9 +12,19 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
 ArithPriorityQueue::ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau):
-  d_partialModel(pm), d_tableau(tableau), d_modeInUse(Collection), d_ZERO_DELTA(0,0)
+  d_pivotRule(MINIMUM),
+  d_partialModel(pm),
+  d_tableau(tableau),
+  d_modeInUse(Collection),
+  d_ZERO_DELTA(0,0)
 {}
 
+void ArithPriorityQueue::setPivotRule(PivotRule rule){
+  Assert(!inDifferenceMode());
+  Debug("arith::setPivotRule") << "setting pivot rule " << rule << endl;
+  d_pivotRule = rule;
+}
+
 ArithVar ArithPriorityQueue::dequeueInconsistentBasicVariable(){
   AlwaysAssert(!inCollectionMode());
 
@@ -23,7 +33,17 @@ ArithVar ArithPriorityQueue::dequeueInconsistentBasicVariable(){
   if(inDifferenceMode()){
     while(!d_diffQueue.empty()){
       ArithVar var = d_diffQueue.front().variable();
-      pop_heap(d_diffQueue.begin(), d_diffQueue.end());
+      switch(d_pivotRule){
+      case MINIMUM:
+        pop_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule);
+        break;
+      case BREAK_TIES:
+        pop_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules);
+        break;
+      case MAXIMUM:
+        pop_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule);
+        break;
+      }
       d_diffQueue.pop_back();
       Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl;
       if(basicAndInconsistent(var)){
@@ -73,7 +93,17 @@ void ArithPriorityQueue::enqueueIfInconsistent(ArithVar basic){
       break;
     case Difference:
       d_diffQueue.push_back(computeDiff(basic));
-      push_heap(d_diffQueue.begin(), d_diffQueue.end());
+      switch(d_pivotRule){
+      case MINIMUM:
+        push_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule);
+        break;
+      case BREAK_TIES:
+        push_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules);
+        break;
+      case MAXIMUM:
+        push_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule);
+        break;
+      }
       break;
     default:
       Unreachable();
@@ -95,7 +125,19 @@ void ArithPriorityQueue::transitionToDifferenceMode() {
       d_diffQueue.push_back(computeDiff(var));
     }
   }
-  make_heap(d_diffQueue.begin(), d_diffQueue.end());
+
+  switch(d_pivotRule){
+  case MINIMUM:
+    make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule);
+    break;
+  case BREAK_TIES:
+    make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules);
+    break;
+  case MAXIMUM:
+    make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule);
+    break;
+  }
+
   d_candidates.clear();
   d_modeInUse = Difference;
 
diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index 2f150b73a..ec0a96aa3 100644
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -41,8 +41,10 @@ namespace arith {
  * The queue begins in Collection mode.
  */
 class ArithPriorityQueue {
-private:
+public:
+  enum PivotRule {MINIMUM, BREAK_TIES, MAXIMUM};
 
+private:
   class VarDRatPair {
   private:
     ArithVar d_variable;
@@ -56,14 +58,38 @@ private:
       return d_variable;
     }
 
-    bool operator<(const VarDRatPair& other){
-      return d_orderBy > other.d_orderBy;
+    static bool minimumRule(const VarDRatPair& a, const VarDRatPair& b){
+      return a.d_orderBy > b.d_orderBy;
+    }
+    static bool maximumRule(const VarDRatPair& a, const VarDRatPair& b){
+      return a.d_orderBy < b.d_orderBy;
+    }
+
+    static bool breakTiesRules(const VarDRatPair& a, const VarDRatPair& b){
+      const Rational& nonInfA = a.d_orderBy.getNoninfinitesimalPart();
+      const Rational& nonInfB = b.d_orderBy.getNoninfinitesimalPart();
+      int cmpNonInf = nonInfA.cmp(nonInfB);
+      if(cmpNonInf == 0){
+        const Rational& infA = a.d_orderBy.getInfinitesimalPart();
+        const Rational& infB = b.d_orderBy.getInfinitesimalPart();
+        int cmpInf = infA.cmp(infB);
+        if(cmpInf == 0){
+          return a.d_variable > b.d_variable;
+        }else{
+          return cmpInf > 0;
+        }
+      }else{
+        return cmpNonInf > 0;
+      }
+
+      return a.d_orderBy > b.d_orderBy;
     }
   };
 
   typedef std::vector<VarDRatPair> DifferenceArray;
   typedef std::vector<ArithVar> ArithVarArray;
 
+  PivotRule d_pivotRule;
 
   /**
    * An unordered array with no heap structure for use during collection mode.
@@ -116,6 +142,9 @@ public:
 
   ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau);
 
+  /** precondition: !inDifferenceMode() */
+  void setPivotRule(PivotRule rule);
+
   ArithVar dequeueInconsistentBasicVariable();
 
   void enqueueIfInconsistent(ArithVar basic);
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 3b86935bd..a32a188b4 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -12,6 +12,8 @@
 #include "theory/arith/partial_model.h"
 #include "theory/output_channel.h"
 
+#include "util/options.h"
+
 #include "util/stats.h"
 
 #include <queue>
@@ -150,6 +152,22 @@ 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);
+    }
+  }
+
   /**
    * 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 e29054c16..dc841170b 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -162,6 +162,9 @@ public:
 
   std::string identify() const { return std::string("TheoryArith"); }
 
+  void notifyOptions(const Options& opt) {
+    d_simplex.notifyOptions(opt);
+  }
 private:
 
   ArithVar determineLeftVariable(TNode assertion, Kind simpleKind);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index b4c3a897b..85ea375f7 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -27,6 +27,7 @@
 #include "context/context.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
+#include "util/options.h"
 
 #include <string>
 #include <iostream>
@@ -95,6 +96,8 @@ protected:
     d_out(&out) {
   }
 
+
+
   /**
    * This is called at shutdown time by the TheoryEngine, just before
    * destruction.  It is important because there are destruction
@@ -376,6 +379,8 @@ public:
    */
   virtual std::string identify() const = 0;
 
+  virtual void notifyOptions(const Options& opt) {}
+
   //
   // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
   //
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 97cb8f471..a577e8f9b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -135,6 +135,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
   d_hasShutDown(false),
   d_incomplete(ctxt, false),
   d_valuation(this),
+  d_opts(opts),
   d_statistics() {
 
   Rewriter::init();
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 6a343717a..7a82a1b05 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -154,6 +154,8 @@ class TheoryEngine {
    */
   Node removeITEs(TNode t);
 
+  const Options& d_opts;
+
 public:
 
   /**
@@ -174,6 +176,8 @@ public:
     TheoryClass* theory = new TheoryClass(d_context, d_theoryOut);
     d_theoryTable[theory->getId()] = theory;
     d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory));
+
+    theory->notifyOptions(d_opts);
   }
 
   SharedTermManager* getSharedTermManager() {
diff --git a/src/util/options.cpp b/src/util/options.cpp
index dcf146010..0c3915d1d 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -120,7 +120,8 @@ enum OptionValue {
   NO_TYPE_CHECKING,
   LAZY_TYPE_CHECKING,
   EAGER_TYPE_CHECKING,
-  INCREMENTAL
+  INCREMENTAL,
+  PIVOT_RULE
 };/* enum OptionValue */
 
 /**
@@ -177,6 +178,7 @@ static struct option cmdlineOptions[] = {
   { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING},
   { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING},
   { "incremental", no_argument, NULL, INCREMENTAL},
+  { "pivot-rule" , required_argument, NULL, PIVOT_RULE  },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -374,6 +376,28 @@ throw(OptionException) {
       incrementalSolving = true;
       break;
 
+    case PIVOT_RULE:
+      if(!strcmp(optarg, "min")) {
+        pivotRule = MINIMUM;
+        break;
+      } else if(!strcmp(optarg, "min-break-ties")) {
+        pivotRule = BREAK_TIES;
+        break;
+      } else if(!strcmp(optarg, "max")) {
+        pivotRule = MAXIMUM;
+        break;
+      } else if(!strcmp(optarg, "help")) {
+        printf("Pivot rules available:\n");
+        printf("min\n");
+        printf("min-break-ties\n");
+        printf("max\n");
+        exit(1);
+      } else {
+        throw OptionException(string("unknown option for --pivot-rule: `") +
+                              optarg + "'.  Try --pivot-rule help.");
+      }
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/util/options.h b/src/util/options.h
index 1eca0d499..2618f8512 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -129,6 +129,10 @@ struct CVC4_PUBLIC Options {
   /** Whether incemental solving (push/pop) */
   bool incrementalSolving;
 
+
+  typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
+  ArithPivotRule pivotRule;
+
   Options() :
     binary_name(),
     statistics(false),
@@ -151,7 +155,9 @@ struct CVC4_PUBLIC Options {
     produceAssignments(false),
     typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
     earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
-    incrementalSolving(false) {
+    incrementalSolving(false),
+    pivotRule(MINIMUM)
+    {
   }
 
   /**