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

1 files changed, 18 insertions, 0 deletions

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.