- 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.

4 files changed, 99 insertions, 7 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);