diff options
Diffstat (limited to 'src/theory/arith')
-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 |
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); |