From: Tim King Date: Thu, 24 Feb 2011 16:52:15 +0000 (+0000) Subject: - Changes ArithPriorityQueue to use stl::vector<>'s plus stl's heap algorithms instea... X-Git-Tag: cvc5-1.0.0~8695 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d21fc6157aa190944d9e3181de883c080cb6ce3f;p=cvc5.git - Changes ArithPriorityQueue to use stl::vector<>'s plus stl's heap algorithms instead of stl's priority queue (which is really an stl vector plus the stl heap algorithms). This offers more control of the underlying data structure. --- diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index 034a1491e..f694c9bfd 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -10,7 +10,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::arith; ArithPriorityQueue::ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau): - d_partialModel(pm), d_tableau(tableau), d_usingGriggioRule(true) + d_partialModel(pm), d_tableau(tableau), d_usingGriggioRule(true), d_ZERO_DELTA(0,0) {} ArithVar ArithPriorityQueue::popInconsistentBasicVariable(){ @@ -18,8 +18,9 @@ ArithVar ArithPriorityQueue::popInconsistentBasicVariable(){ if(usingGriggioRule()){ while(!d_griggioRuleQueue.empty()){ - ArithVar var = d_griggioRuleQueue.top().first; - d_griggioRuleQueue.pop(); + ArithVar var = d_griggioRuleQueue.front().variable(); + pop_heap(d_griggioRuleQueue.begin(), d_griggioRuleQueue.end()); + d_griggioRuleQueue.pop_back(); Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl; if(basicAndInconsistent(var)){ return var; @@ -30,8 +31,10 @@ ArithVar ArithPriorityQueue::popInconsistentBasicVariable(){ << d_possiblyInconsistent.size() << endl; while(!d_possiblyInconsistent.empty()){ - ArithVar var = d_possiblyInconsistent.top(); - d_possiblyInconsistent.pop(); + ArithVar var = d_possiblyInconsistent.front(); + pop_heap(d_possiblyInconsistent.begin(), d_possiblyInconsistent.end(), std::greater()); + d_possiblyInconsistent.pop_back(); + Debug("arith_update") << "possiblyInconsistent var" << var << endl; if(basicAndInconsistent(var)){ return var; @@ -49,32 +52,25 @@ void ArithPriorityQueue::enqueueIfInconsistent(ArithVar basic){ DeltaRational diff = d_partialModel.belowLowerBound(basic,beta,true) ? d_partialModel.getLowerBound(basic) - beta: beta - d_partialModel.getUpperBound(basic); - d_griggioRuleQueue.push(make_pair(basic,diff)); + + Assert(d_ZERO_DELTA < diff); + d_griggioRuleQueue.push_back(VarDRatPair(basic,diff)); + push_heap(d_griggioRuleQueue.begin(), d_griggioRuleQueue.end()); + }else{ - d_possiblyInconsistent.push(basic); + d_possiblyInconsistent.push_back(basic); + push_heap(d_possiblyInconsistent.begin(), d_possiblyInconsistent.end(), std::greater()); } } } - -void ArithPriorityQueue::enqueueTrustedVector(const vector& trusted){ +ArithPriorityQueue::GriggioPQueue::const_iterator ArithPriorityQueue::queueAsListBegin() const{ Assert(usingGriggioRule()); - Assert(empty()); - - d_griggioRuleQueue = GriggioPQueue(trusted.begin(), trusted.end()); - Assert(size() == trusted.size()); + return d_griggioRuleQueue.begin(); } - - -void ArithPriorityQueue::dumpQueueIntoVector(vector& target){ +ArithPriorityQueue::GriggioPQueue::const_iterator ArithPriorityQueue::queueAsListEnd() const{ Assert(usingGriggioRule()); - while( !d_griggioRuleQueue.empty()){ - ArithVar var = d_griggioRuleQueue.top().first; - if(basicAndInconsistent(var)){ - target.push_back( d_griggioRuleQueue.top()); - } - d_griggioRuleQueue.pop(); - } + return d_griggioRuleQueue.end(); } @@ -87,13 +83,15 @@ void ArithPriorityQueue::useGriggioQueue(){ void ArithPriorityQueue::useBlandQueue(){ Assert(usingGriggioRule()); - while(!d_griggioRuleQueue.empty()){ - ArithVar var = d_griggioRuleQueue.top().first; + Assert(d_possiblyInconsistent.empty()); + for(GriggioPQueue::const_iterator i = d_griggioRuleQueue.begin(), end = d_griggioRuleQueue.end(); i != end; ++i){ + ArithVar var = (*i).variable(); if(basicAndInconsistent(var)){ - d_possiblyInconsistent.push(var); + d_possiblyInconsistent.push_back(var); } - d_griggioRuleQueue.pop(); } + d_griggioRuleQueue.clear(); + make_heap(d_possiblyInconsistent.begin(), d_possiblyInconsistent.end(), std::greater()); d_usingGriggioRule = false; Assert(d_griggioRuleQueue.empty()); @@ -103,9 +101,9 @@ void ArithPriorityQueue::useBlandQueue(){ void ArithPriorityQueue::clear(){ if(usingGriggioRule() && !d_griggioRuleQueue.empty()){ - d_griggioRuleQueue = GriggioPQueue(); + d_griggioRuleQueue.clear(); }else if(!d_possiblyInconsistent.empty()) { - d_possiblyInconsistent = PQueue(); + d_possiblyInconsistent.clear(); } Assert(d_possiblyInconsistent.empty()); Assert(d_griggioRuleQueue.empty()); diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index da5cf78b5..92e3ffc3a 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -9,27 +9,39 @@ #include "theory/arith/tableau.h" #include "theory/arith/partial_model.h" -#include + +#include +#include namespace CVC4 { namespace theory { namespace arith { -typedef std::pair VarDRatPair; - -struct VarDRatPairCompare{ - inline bool operator()(const VarDRatPair& a, const VarDRatPair& b){ - return a.second > b.second; - } -}; - -typedef std::priority_queue, VarDRatPairCompare> GriggioPQueue; -typedef std::priority_queue, std::greater > PQueue; +class ArithPriorityQueue { +private: + class VarDRatPair { + ArithVar d_variable; + DeltaRational d_orderBy; + public: + VarDRatPair(ArithVar var, const DeltaRational& dr): + d_variable(var), d_orderBy(dr) + { } + + ArithVar variable() const { + return d_variable; + } + bool operator<(const VarDRatPair& other){ + return d_orderBy > other.d_orderBy; + } + }; -class ArithPriorityQueue { +public: + typedef std::vector GriggioPQueue; private: + typedef std::vector PQueue; + /** * Priority Queue of the basic variables that may be inconsistent. * Variables are ordered according to which violates its bound the most. @@ -66,16 +78,19 @@ private: */ bool d_usingGriggioRule; + /** Storage of Delta Rational 0 */ + DeltaRational d_ZERO_DELTA; + public: + ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau); ArithVar popInconsistentBasicVariable(); void enqueueIfInconsistent(ArithVar basic); - void enqueueTrustedVector(const vector& trusted); - - void dumpQueueIntoVector(vector& target); + GriggioPQueue::const_iterator queueAsListBegin() const; + GriggioPQueue::const_iterator queueAsListEnd() const; inline bool basicAndInconsistent(ArithVar var) const{ return d_tableau.isBasic(var) diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 2785222e3..4efa5fa43 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -84,7 +84,6 @@ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_ } }else{ d_queue.enqueueIfInconsistent(x_i); - //checkBasicVariable(x_i); } return false; @@ -285,15 +284,10 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR ArithVarSet::iterator basicIter = d_tableau.beginColumn(x_j); ArithVarSet::iterator endIter = d_tableau.endColumn(x_j); for(; basicIter != endIter; ++basicIter){ - - //ArithVarSet::iterator basicIter = d_tableau.begin(), end = d_tableau.end(); - //for(; basicIter != end; ++basicIter){ ArithVar x_k = *basicIter; ReducedRowVector& row_k = d_tableau.lookup(x_k); Assert(row_k.has(x_j)); - - //if(x_k != x_i && row_k.has(x_j)){ if(x_k != x_i ){ const Rational& a_kj = row_k.lookup(x_j); DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); @@ -415,28 +409,25 @@ Node SimplexDecisionProcedure::selectInitialConflict() { TimerStat::CodeTimer codeTimer(d_statistics.d_selectInitialConflictTime); - vector init; - d_queue.dumpQueueIntoVector(init); - int conflictChanges = 0; - vector::iterator i=init.begin(), end=init.end(); + ArithPriorityQueue::GriggioPQueue::const_iterator i = d_queue.queueAsListBegin(); + ArithPriorityQueue::GriggioPQueue::const_iterator end = d_queue.queueAsListEnd(); for(; i != end; ++i){ - ArithVar x_i = (*i).first; + ArithVar x_i = (*i).variable(); - Node possibleConflict = checkBasicForConflict(x_i); - if(!possibleConflict.isNull()){ - Node better = betterConflict(bestConflict, possibleConflict); + if(d_tableau.isBasic(x_i)){ + Node possibleConflict = checkBasicForConflict(x_i); + if(!possibleConflict.isNull()){ + Node better = betterConflict(bestConflict, possibleConflict); - if(better != bestConflict){ - ++conflictChanges; + if(better != bestConflict){ + ++conflictChanges; + } + bestConflict = better; + ++(d_statistics.d_statEarlyConflicts); } - bestConflict = better; - ++(d_statistics.d_statEarlyConflicts); } } - if(bestConflict.isNull()){ - d_queue.enqueueTrustedVector(init); - } if(conflictChanges > 1) ++(d_statistics.d_statEarlyConflictImprovements); return bestConflict; @@ -458,7 +449,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ possibleConflict = searchForFeasibleSolution(d_numVariables + 1); } - if(possibleConflict.isNull()){ + if(!d_queue.empty() && possibleConflict.isNull()){ d_queue.useBlandQueue(); possibleConflict = searchForFeasibleSolution(0); } @@ -499,16 +490,12 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ //corresponds to Check() in dM06 template Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){ - Debug("arith") << "updateInconsistentVars" << endl; - //uint32_t iteratationNum = 0; - while(!limitIterations || remainingIterations > 0){ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } ArithVar x_i = d_queue.popInconsistentBasicVariable(); - //selectSmallestInconsistentVar(); Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl; if(x_i == ARITHVAR_SENTINEL){ Debug("arith_update") << "No inconsistent variables" << endl; @@ -545,11 +532,9 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera return earlyConflict; } } - if(remainingIterations == 0 && limitIterations){ - return Node::null(); - } + AlwaysAssert(limitIterations && remainingIterations == 0); - Unreachable(); + return Node::null(); }