From a101b2e309dd2818a85c954e45af586e530e289a Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 21 Feb 2011 19:15:33 +0000 Subject: [PATCH] - Adds the ArithPriorityQueue class. The ArithPriorityQueue class provides an abstraction to the previous priority queues representing the 2 different pivoting rules. --- src/theory/arith/Makefile.am | 2 + src/theory/arith/arith_priority_queue.cpp | 112 +++++++++++++++++ src/theory/arith/arith_priority_queue.h | 117 ++++++++++++++++++ src/theory/arith/simplex.cpp | 141 ++++++++-------------- src/theory/arith/simplex.h | 36 +----- 5 files changed, 289 insertions(+), 119 deletions(-) create mode 100644 src/theory/arith/arith_priority_queue.cpp create mode 100644 src/theory/arith/arith_priority_queue.h diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 002c080f7..48be16f90 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -21,6 +21,8 @@ libarith_la_SOURCES = \ arithvar_set.h \ tableau.h \ tableau.cpp \ + arith_priority_queue.h \ + arith_priority_queue.cpp \ simplex.h \ simplex.cpp \ row_vector.h \ diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp new file mode 100644 index 000000000..034a1491e --- /dev/null +++ b/src/theory/arith/arith_priority_queue.cpp @@ -0,0 +1,112 @@ + +#include "theory/arith/arith_priority_queue.h" + +using namespace std; + +using namespace CVC4; +using namespace CVC4::kind; + +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) +{} + +ArithVar ArithPriorityQueue::popInconsistentBasicVariable(){ + Debug("arith_update") << "popInconsistentBasicVariable()" << endl; + + if(usingGriggioRule()){ + while(!d_griggioRuleQueue.empty()){ + ArithVar var = d_griggioRuleQueue.top().first; + d_griggioRuleQueue.pop(); + Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl; + if(basicAndInconsistent(var)){ + return var; + } + } + }else{ + Debug("arith_update") << "possiblyInconsistent.size()" + << d_possiblyInconsistent.size() << endl; + + while(!d_possiblyInconsistent.empty()){ + ArithVar var = d_possiblyInconsistent.top(); + d_possiblyInconsistent.pop(); + Debug("arith_update") << "possiblyInconsistent var" << var << endl; + if(basicAndInconsistent(var)){ + return var; + } + } + } + return ARITHVAR_SENTINEL; +} + +void ArithPriorityQueue::enqueueIfInconsistent(ArithVar basic){ + Assert(d_tableau.isBasic(basic)); + if(basicAndInconsistent(basic)){ + if( usingGriggioRule() ){ + const DeltaRational& beta = d_partialModel.getAssignment(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)); + }else{ + d_possiblyInconsistent.push(basic); + } + } +} + + +void ArithPriorityQueue::enqueueTrustedVector(const vector& trusted){ + Assert(usingGriggioRule()); + Assert(empty()); + + d_griggioRuleQueue = GriggioPQueue(trusted.begin(), trusted.end()); + Assert(size() == trusted.size()); +} + + +void ArithPriorityQueue::dumpQueueIntoVector(vector& target){ + Assert(usingGriggioRule()); + while( !d_griggioRuleQueue.empty()){ + ArithVar var = d_griggioRuleQueue.top().first; + if(basicAndInconsistent(var)){ + target.push_back( d_griggioRuleQueue.top()); + } + d_griggioRuleQueue.pop(); + } +} + + +void ArithPriorityQueue::useGriggioQueue(){ + Assert(!usingGriggioRule()); + Assert(d_possiblyInconsistent.empty()); + Assert(d_griggioRuleQueue.empty()); + d_usingGriggioRule = true; +} + +void ArithPriorityQueue::useBlandQueue(){ + Assert(usingGriggioRule()); + while(!d_griggioRuleQueue.empty()){ + ArithVar var = d_griggioRuleQueue.top().first; + if(basicAndInconsistent(var)){ + d_possiblyInconsistent.push(var); + } + d_griggioRuleQueue.pop(); + } + d_usingGriggioRule = false; + + Assert(d_griggioRuleQueue.empty()); + Assert(!usingGriggioRule()); +} + + +void ArithPriorityQueue::clear(){ + if(usingGriggioRule() && !d_griggioRuleQueue.empty()){ + d_griggioRuleQueue = GriggioPQueue(); + }else if(!d_possiblyInconsistent.empty()) { + d_possiblyInconsistent = PQueue(); + } + 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 new file mode 100644 index 000000000..da5cf78b5 --- /dev/null +++ b/src/theory/arith/arith_priority_queue.h @@ -0,0 +1,117 @@ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H +#define __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H + +#include "theory/arith/arith_utilities.h" +#include "theory/arith/delta_rational.h" +#include "theory/arith/tableau.h" +#include "theory/arith/partial_model.h" + +#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: + /** + * Priority Queue of the basic variables that may be inconsistent. + * Variables are ordered according to which violates its bound the most. + * This is a hueristic and makes no guarentees to terminate! + * This heuristic comes from Alberto Griggio's thesis. + */ + GriggioPQueue d_griggioRuleQueue; + + /** + * Priority Queue of the basic variables that may be inconsistent. + * + * This is required to contain at least 1 instance of every inconsistent + * basic variable. This is only required to be a superset though so its + * contents must be checked to still be basic and inconsistent. + * + * This is also required to agree with the row on variable order for termination. + * Effectively this means that this must be a min-heap. + */ + PQueue d_possiblyInconsistent; + + /** + * Reference to the arithmetic partial model for checking if a variable + * is consistent with its upper and lower bounds. + */ + ArithPartialModel& d_partialModel; + + /** Reference to the Tableau for checking if a variable is basic. */ + const Tableau& d_tableau; + + /** + * Controls which priority queue is in use. + * If true, d_griggioRuleQueue is used. + * If false, d_possiblyInconsistent is used. + */ + bool d_usingGriggioRule; + +public: + ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau); + + ArithVar popInconsistentBasicVariable(); + + void enqueueIfInconsistent(ArithVar basic); + + void enqueueTrustedVector(const vector& trusted); + + void dumpQueueIntoVector(vector& target); + + inline bool basicAndInconsistent(ArithVar var) const{ + return d_tableau.isBasic(var) + && !d_partialModel.assignmentIsConsistent(var) ; + } + + void useGriggioQueue(); + + void useBlandQueue(); + + inline bool usingGriggioRule() const{ + return d_usingGriggioRule; + } + + inline bool empty() const{ + if(usingGriggioRule()){ + return d_griggioRuleQueue.empty(); + }else{ + return d_possiblyInconsistent.empty(); + } + } + + inline size_t size() const { + if(usingGriggioRule()){ + return d_griggioRuleQueue.size(); + }else{ + return d_possiblyInconsistent.size(); + } + } + + void clear(); +}; + + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH_PRIORITY_QUEUE_H */ diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index d8d39c24f..d837d7ac0 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -9,8 +9,6 @@ using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::arith; -const static uint64_t ACTIVITY_THRESHOLD = 100; - SimplexDecisionProcedure::Statistics::Statistics(): d_statPivots("theory::arith::pivots",0), d_statUpdates("theory::arith::updates",0), @@ -85,7 +83,8 @@ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_ update(x_i, c_i); } }else{ - checkBasicVariable(x_i); + d_queue.enqueueIfInconsistent(x_i); + //checkBasicVariable(x_i); } return false; @@ -116,7 +115,7 @@ bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_ update(x_i, c_i); } }else{ - checkBasicVariable(x_i); + d_queue.enqueueIfInconsistent(x_i); } d_partialModel.printModel(x_i); return false; @@ -162,7 +161,8 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& update(x_i, c_i); } }else{ - checkBasicVariable(x_i); + d_queue.enqueueIfInconsistent(x_i); + //checkBasicVariable(x_i); } return false; @@ -190,7 +190,8 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ DeltaRational nAssignment = assignment+(diff * a_ji); d_partialModel.setAssignment(x_j, nAssignment); - checkBasicVariable(x_j); + d_queue.enqueueIfInconsistent(x_j); + //checkBasicVariable(x_j); } } @@ -259,7 +260,7 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); d_partialModel.setAssignment(x_k, nextAssignment); - checkBasicVariable(x_k); + d_queue.enqueueIfInconsistent(x_k); } } @@ -279,7 +280,7 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR d_tableau.pivot(x_i, x_j); - checkBasicVariable(x_j); + d_queue.enqueueIfInconsistent(x_j); // Debug found conflict if( !d_foundAConflict ){ @@ -301,37 +302,6 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR } } -ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){ - Debug("arith_update") << "selectSmallestInconsistentVar()" << endl; - Debug("arith_update") << "possiblyInconsistent.size()" - << d_possiblyInconsistent.size() << endl; - - if(d_pivotStage){ - while(!d_griggioRuleQueue.empty()){ - ArithVar var = d_griggioRuleQueue.top().first; - Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl; - if(d_tableau.isBasic(var)){ - if(!d_partialModel.assignmentIsConsistent(var)){ - return var; - } - } - d_griggioRuleQueue.pop(); - } - }else{ - while(!d_possiblyInconsistent.empty()){ - ArithVar var = d_possiblyInconsistent.top(); - Debug("arith_update") << "possiblyInconsistent var" << var << endl; - if(d_tableau.isBasic(var)){ - if(!d_partialModel.assignmentIsConsistent(var)){ - return var; - } - } - d_possiblyInconsistent.pop(); - } - } - return ARITHVAR_SENTINEL; -} - template ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ ReducedRowVector& row_i = d_tableau.lookup(x_i); @@ -339,6 +309,8 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ ArithVar slack = ARITHVAR_SENTINEL; uint32_t numRows = std::numeric_limits::max(); + bool pivotStage = d_queue.usingGriggioRule(); + for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); @@ -348,7 +320,7 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ int cmp = a_ij.cmp(d_constants.d_ZERO); if(above){ // beta(x_i) > u_i if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ - if(d_pivotStage){ + if(pivotStage){ if(d_tableau.getRowCount(nonbasic) < numRows){ slack = nonbasic; numRows = d_tableau.getRowCount(nonbasic); @@ -357,7 +329,7 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ slack = nonbasic; break; } }else if( cmp > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ - if(d_pivotStage){ + if(pivotStage){ if(d_tableau.getRowCount(nonbasic) < numRows){ slack = nonbasic; numRows = d_tableau.getRowCount(nonbasic); @@ -368,7 +340,7 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ } }else{ //beta(x_i) < l_i if(cmp > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ - if(d_pivotStage){ + if(pivotStage){ if(d_tableau.getRowCount(nonbasic) < numRows){ slack = nonbasic; numRows = d_tableau.getRowCount(nonbasic); @@ -377,7 +349,7 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ slack = nonbasic; break; } }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ - if(d_pivotStage){ + if(pivotStage){ if(d_tableau.getRowCount(nonbasic) < numRows){ slack = nonbasic; numRows = d_tableau.getRowCount(nonbasic); @@ -405,22 +377,12 @@ Node SimplexDecisionProcedure::selectInitialConflict() { TimerStat::CodeTimer codeTimer(d_statistics.d_selectInitialConflictTime); vector init; - - while( !d_griggioRuleQueue.empty()){ - ArithVar var = d_griggioRuleQueue.top().first; - if(d_tableau.isBasic(var)){ - if(!d_partialModel.assignmentIsConsistent(var)){ - init.push_back( d_griggioRuleQueue.top()); - } - } - d_griggioRuleQueue.pop(); - } + d_queue.dumpQueueIntoVector(init); int conflictChanges = 0; - - for(vector::iterator i=init.begin(), end=init.end(); i != end; ++i){ + vector::iterator i=init.begin(), end=init.end(); + for(; i != end; ++i){ ArithVar x_i = (*i).first; - d_griggioRuleQueue.push(*i); Node possibleConflict = checkBasicForConflict(x_i); if(!possibleConflict.isNull()){ @@ -433,34 +395,45 @@ Node SimplexDecisionProcedure::selectInitialConflict() { ++(d_statistics.d_statEarlyConflicts); } } + if(bestConflict.isNull()){ + d_queue.enqueueTrustedVector(init); + } + if(conflictChanges > 1) ++(d_statistics.d_statEarlyConflictImprovements); return bestConflict; } Node SimplexDecisionProcedure::updateInconsistentVars(){ - if(d_griggioRuleQueue.empty()) return Node::null(); + if(d_queue.empty()){ + return Node::null(); + } d_foundAConflict = false; d_pivotsSinceConflict = 0; Node possibleConflict = Node::null(); - if(d_griggioRuleQueue.size() > 1){ + if(d_queue.size() > 1){ possibleConflict = selectInitialConflict(); } if(possibleConflict.isNull()){ - possibleConflict = privateUpdateInconsistentVars(); + possibleConflict = searchForFeasibleSolution(d_numVariables + 1); } - Assert(!possibleConflict.isNull() || d_griggioRuleQueue.empty()); - Assert(!possibleConflict.isNull() || d_possiblyInconsistent.empty()); - d_pivotStage = true; - - while(!d_griggioRuleQueue.empty()){ - d_griggioRuleQueue.pop(); + if(possibleConflict.isNull()){ + d_queue.useBlandQueue(); + possibleConflict = searchForFeasibleSolution(0); } - while(!d_possiblyInconsistent.empty()){ - d_possiblyInconsistent.pop(); + + Assert(!possibleConflict.isNull() || d_queue.empty()); + + // Curiously the invariant that we always do a full check + // means that the assignment we can always empty these queues. + d_queue.clear(); + + if(!d_queue.usingGriggioRule()){ + d_queue.useGriggioQueue(); } + Assert(d_queue.usingGriggioRule()); return possibleConflict; } @@ -485,44 +458,45 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ } //corresponds to Check() in dM06 -Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ - Assert(d_pivotStage || d_griggioRuleQueue.empty()); +template +Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){ Debug("arith") << "updateInconsistentVars" << endl; - uint32_t iteratationNum = 0; + //uint32_t iteratationNum = 0; - while(!d_pivotStage || iteratationNum <= d_numVariables){ + while(!limitIterations || remainingIterations > 0){ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } - ArithVar x_i = selectSmallestInconsistentVar(); + 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; return Node::null(); //sat } - ++iteratationNum; + --remainingIterations; DeltaRational beta_i = d_partialModel.getAssignment(x_i); ArithVar x_j = ARITHVAR_SENTINEL; if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ - DeltaRational l_i = d_partialModel.getLowerBound(x_i); x_j = selectSlackBelow(x_i); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictBelow(x_i); //unsat } + DeltaRational l_i = d_partialModel.getLowerBound(x_i); pivotAndUpdate(x_i, x_j, l_i); }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){ - DeltaRational u_i = d_partialModel.getUpperBound(x_i); x_j = selectSlackAbove(x_i); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictAbove(x_i); //unsat } + DeltaRational u_i = d_partialModel.getUpperBound(x_i); pivotAndUpdate(x_i, x_j, u_i); } Assert(x_j != ARITHVAR_SENTINEL); @@ -532,18 +506,8 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ return earlyConflict; } } - - if(d_pivotStage && iteratationNum >= d_numVariables){ - while(!d_griggioRuleQueue.empty()){ - ArithVar var = d_griggioRuleQueue.top().first; - if(d_tableau.isBasic(var)){ - d_possiblyInconsistent.push(var); - } - d_griggioRuleQueue.pop(); - } - - d_pivotStage = false; - return privateUpdateInconsistentVars(); + if(remainingIterations == 0 && limitIterations){ + return Node::null(); } Unreachable(); @@ -655,7 +619,7 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe return sum; } - +/* void SimplexDecisionProcedure::checkBasicVariable(ArithVar basic){ Assert(d_tableau.isBasic(basic)); if(!d_partialModel.assignmentIsConsistent(basic)){ @@ -670,6 +634,7 @@ void SimplexDecisionProcedure::checkBasicVariable(ArithVar basic){ } } } +*/ /** * This check is quite expensive. diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index c5c4da661..9fed7dc0b 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -5,6 +5,7 @@ #define __CVC4__THEORY__ARITH__SIMPLEX_H #include "theory/arith/arith_utilities.h" +#include "theory/arith/arith_priority_queue.h" #include "theory/arith/arithvar_set.h" #include "theory/arith/delta_rational.h" #include "theory/arith/tableau.h" @@ -21,30 +22,7 @@ namespace arith { class SimplexDecisionProcedure { private: - 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; - - GriggioPQueue d_griggioRuleQueue; - - /** - * Priority Queue of the basic variables that may be inconsistent. - * - * This is required to contain at least 1 instance of every inconsistent - * basic variable. This is only required to be a superset though so its - * contents must be checked to still be basic and inconsistent. - * - * This is also required to agree with the row on variable order for termination. - * Effectively this means that this must be a min-heap. - */ - typedef std::priority_queue, std::greater > PQueue; - - PQueue d_possiblyInconsistent; /** Stores system wide constants to avoid unnessecary reconstruction. */ const ArithConstants& d_constants; @@ -58,23 +36,21 @@ private: OutputChannel* d_out; Tableau& d_tableau; + ArithPriorityQueue d_queue; ArithVar d_numVariables; - bool d_pivotStage; - public: SimplexDecisionProcedure(const ArithConstants& constants, ArithPartialModel& pm, OutputChannel* out, Tableau& tableau) : - d_possiblyInconsistent(), d_constants(constants), d_partialModel(pm), d_out(out), d_tableau(tableau), - d_numVariables(0), - d_pivotStage(true) + d_queue(pm, tableau), + d_numVariables(0) {} void increaseMax() {d_numVariables++;} @@ -130,7 +106,7 @@ public: */ Node updateInconsistentVars(); private: - Node privateUpdateInconsistentVars(); + template Node searchForFeasibleSolution(uint32_t maxIterations); Node selectInitialConflict(); @@ -182,8 +158,6 @@ public: DeltaRational computeRowValue(ArithVar x, bool useSafe); private: - /** Check to make sure all of the basic variables are within their bounds. */ - void checkBasicVariable(ArithVar basic); /** * Checks a basic variable, b, to see if it is in conflict. -- 2.30.2