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 | |
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')
-rw-r--r-- | src/theory/arith/arith_priority_queue.cpp | 50 | ||||
-rw-r--r-- | src/theory/arith/arith_priority_queue.h | 35 | ||||
-rw-r--r-- | src/theory/arith/simplex.h | 18 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 3 | ||||
-rw-r--r-- | src/theory/theory.h | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 4 |
7 files changed, 109 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); 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() { |