diff options
author | Tim King <taking@cs.nyu.edu> | 2011-02-27 19:59:52 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-02-27 19:59:52 +0000 |
commit | ec834d513b8d390682a08f2ea2d159c3e35a4a2d (patch) | |
tree | 7b0953b87d04a2c76b8282d2469caddb2eaafbb2 /src/theory/arith/simplex.h | |
parent | 57fe149cf7915d721912e1d1866c31346f66e2f8 (diff) |
- 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.
Diffstat (limited to 'src/theory/arith/simplex.h')
-rw-r--r-- | src/theory/arith/simplex.h | 18 |
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. |