- Misc. cleanup and renaming in ArithPriorityQueue.
#include "theory/arith/arith_priority_queue.h"
+#include <algorithm>
+
using namespace std;
using namespace CVC4;
using namespace CVC4::theory::arith;
ArithPriorityQueue::ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau):
- d_partialModel(pm), d_tableau(tableau), d_usingGriggioRule(true), d_ZERO_DELTA(0,0)
+ d_partialModel(pm), d_tableau(tableau), d_modeInUse(Collection), d_ZERO_DELTA(0,0)
{}
ArithVar ArithPriorityQueue::popInconsistentBasicVariable(){
+ AlwaysAssert(!inCollectionMode());
+
Debug("arith_update") << "popInconsistentBasicVariable()" << endl;
- if(usingGriggioRule()){
- while(!d_griggioRuleQueue.empty()){
- ArithVar var = d_griggioRuleQueue.front().variable();
- pop_heap(d_griggioRuleQueue.begin(), d_griggioRuleQueue.end());
- d_griggioRuleQueue.pop_back();
+ if(inDifferenceMode()){
+ while(!d_diffQueue.empty()){
+ ArithVar var = d_diffQueue.front().variable();
+ pop_heap(d_diffQueue.begin(), d_diffQueue.end());
+ d_diffQueue.pop_back();
Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl;
if(basicAndInconsistent(var)){
return var;
}
}else{
Debug("arith_update") << "possiblyInconsistent.size()"
- << d_possiblyInconsistent.size() << endl;
+ << d_varOrderQueue.size() << endl;
- while(!d_possiblyInconsistent.empty()){
- ArithVar var = d_possiblyInconsistent.front();
- pop_heap(d_
possiblyInconsistent.begin(), d_possiblyInconsistent.end(), std::greater<ArithVar>());
- d_possiblyInconsistent.pop_back();
+ while(!d_varOrderQueue.empty()){
+ ArithVar var = d_varOrderQueue.front();
+ pop_heap(d_
varOrderQueue.begin(), d_varOrderQueue.end(), std::greater<ArithVar>());
+ d_varOrderQueue.pop_back();
Debug("arith_update") << "possiblyInconsistent var" << var << endl;
if(basicAndInconsistent(var)){
return ARITHVAR_SENTINEL;
}
+ArithPriorityQueue::VarDRatPair ArithPriorityQueue::computeDiff(ArithVar basic){
+ Assert(basicAndInconsistent(basic));
+ 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);
+
+ Assert(d_ZERO_DELTA < diff);
+ return VarDRatPair(basic,diff);
+}
+
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);
-
- Assert(d_ZERO_DELTA < diff);
- d_griggioRuleQueue.push_back(VarDRatPair(basic,diff));
- push_heap(d_griggioRuleQueue.begin(), d_griggioRuleQueue.end());
-
- }else{
- d_possiblyInconsistent.push_back(basic);
- push_heap(d_possiblyInconsistent.begin(), d_possiblyInconsistent.end(), std::greater<ArithVar>());
+ switch(d_modeInUse){
+ case Collection:
+ d_candidates.push_back(basic);
+ break;
+ case VariableOrder:
+ d_varOrderQueue.push_back(basic);
+ push_heap(d_varOrderQueue.begin(), d_varOrderQueue.end(), std::greater<ArithVar>());
+ case Difference:
+ d_diffQueue.push_back(computeDiff(basic));
+ push_heap(d_diffQueue.begin(), d_diffQueue.end());
+ break;
+ default:
+ Unreachable();
}
}
}
-ArithPriorityQueue::GriggioPQueue::const_iterator ArithPriorityQueue::queueAsListBegin() const{
- Assert(usingGriggioRule());
- return d_griggioRuleQueue.begin();
-}
-ArithPriorityQueue::GriggioPQueue::const_iterator ArithPriorityQueue::queueAsListEnd() const{
- Assert(usingGriggioRule());
- return d_griggioRuleQueue.end();
-}
+void ArithPriorityQueue::transitionToDifferenceMode() {
+ Assert(inCollectionMode());
+ Assert(d_varOrderQueue.empty());
+ Assert(d_diffQueue.empty());
+ ArithVarArray::const_iterator i = d_candidates.begin(), end = d_candidates.end();
+ for(; i != end; ++i){
+ ArithVar var = *i;
+ if(basicAndInconsistent(var)){
+ d_diffQueue.push_back(computeDiff(var));
+ }
+ }
+ make_heap(d_diffQueue.begin(), d_diffQueue.end());
+ d_candidates.clear();
+ d_modeInUse = Difference;
-void ArithPriorityQueue::useGriggioQueue(){
- Assert(!usingGriggioRule());
- Assert(d_possiblyInconsistent.empty());
- Assert(d_griggioRuleQueue.empty());
- d_usingGriggioRule = true;
+ Assert(inDifferenceMode());
+ Assert(d_varOrderQueue.empty());
+ Assert(d_candidates.empty());
}
-void ArithPriorityQueue::useBlandQueue(){
- Assert(usingGriggioRule());
- Assert(d_possiblyInconsistent.empty());
- for(GriggioPQueue::const_iterator i = d_griggioRuleQueue.begin(), end = d_griggioRuleQueue.end(); i != end; ++i){
+void ArithPriorityQueue::transitionToVariableOrderMode() {
+ Assert(inDifferenceMode());
+ Assert(d_varOrderQueue.empty());
+ Assert(d_candidates.empty());
+
+ DifferenceArray::const_iterator i = d_diffQueue.begin(), end = d_diffQueue.end();
+ for(; i != end; ++i){
ArithVar var = (*i).variable();
if(basicAndInconsistent(var)){
- d_possiblyInconsistent.push_back(var);
+ d_varOrderQueue.push_back(var);
}
}
- d_griggioRuleQueue.clear();
- make_heap(d_possiblyInconsistent.begin(), d_possiblyInconsistent.end(), std::greater<ArithVar>());
- d_usingGriggioRule = false;
+ make_heap(d_varOrderQueue.begin(), d_varOrderQueue.end(), std::greater<ArithVar>());
+ d_diffQueue.clear();
+ d_modeInUse = VariableOrder;
- Assert(d_griggioRuleQueue.empty());
- Assert(!usingGriggioRule());
+ Assert(inVariableOrderMode());
+ Assert(d_diffQueue.empty());
+ Assert(d_candidates.empty());
}
+void ArithPriorityQueue::transitionToCollectionMode() {
+ Assert(inDifferenceMode() || inVariableOrderMode());
+ Assert(d_diffQueue.empty());
+ Assert(d_candidates.empty());
+ Assert(d_varOrderQueue.empty());
+
+ d_modeInUse = Collection;
+}
void ArithPriorityQueue::clear(){
- if(usingGriggioRule() && !d_griggioRuleQueue.empty()){
- d_griggioRuleQueue.clear();
- }else if(!d_possiblyInconsistent.empty()) {
- d_possiblyInconsistent.clear();
+ switch(d_modeInUse){
+ case Collection:
+ d_candidates.clear();
+ break;
+ case VariableOrder:
+ if(!d_varOrderQueue.empty()) {
+ d_varOrderQueue.clear();
+ }
+ break;
+ case Difference:
+ if(!d_diffQueue.empty()){
+ d_diffQueue.clear();
+ }
+ break;
+ default:
+ Unreachable();
}
- Assert(d_possiblyInconsistent.empty());
- Assert(d_griggioRuleQueue.empty());
+ Assert(d_candidates.empty());
+ Assert(d_varOrderQueue.empty());
+ Assert(d_diffQueue.empty());
}
#include <vector>
-#include <algorithm>
namespace CVC4 {
namespace theory {
namespace arith {
+/**
+ * The priority queue has 3 different modes of operation:
+ * - Collection
+ * This passively collects arithmetic variables that may be inconsistent.
+ * This does not maintain any heap structure.
+ * dequeueInconsistentBasicVariable() does not work in this mode!
+ * Entering this mode requires the queue to be empty.
+ *
+ * - Difference Queue
+ * This mode uses the difference between a variables and its bound
+ * to determine which to dequeue first.
+ *
+ * - Variable Order Queue
+ * This mode uses the variable order to determine which ArithVar is deuqued first.
+ *
+ * The transitions between the modes of operation are:
+ * Collection => Difference Queue
+ * Difference Queue => Variable Order Queue
+ * Difference Queue => Collection (queue must be empty!)
+ * Variable Order Queue => Collection (queue must be empty!)
+ *
+ * The queue begins in Collection mode.
+ */
class ArithPriorityQueue {
private:
+
class VarDRatPair {
+ private:
ArithVar d_variable;
DeltaRational d_orderBy;
public:
}
};
-public:
- typedef std::vector<VarDRatPair> GriggioPQueue;
-private:
- typedef std::vector<ArithVar> PQueue;
+ typedef std::vector<VarDRatPair> DifferenceArray;
+ typedef std::vector<ArithVar> ArithVarArray;
+
+
+ /**
+ * An unordered array with no heap structure for use during collection mode.
+ */
+ ArithVarArray d_candidates;
/**
* Priority Queue of the basic variables that may be inconsistent.
* This is a hueristic and makes no guarentees to terminate!
* This heuristic comes from Alberto Griggio's thesis.
*/
- GriggioPQueue d_griggioRuleQueue;
+ DifferenceArray d_diffQueue;
/**
* Priority Queue of the basic variables that may be 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;
+ ArithVarArray d_varOrderQueue;
/**
* Reference to the arithmetic partial model for checking if a variable
/** Reference to the Tableau for checking if a variable is basic. */
const Tableau& d_tableau;
+ enum Mode {Collection, Difference, VariableOrder};
/**
* Controls which priority queue is in use.
* If true, d_griggioRuleQueue is used.
* If false, d_possiblyInconsistent is used.
*/
- bool d_usingGriggioRule;
+ Mode d_modeInUse;
/** Storage of Delta Rational 0 */
DeltaRational d_ZERO_DELTA;
+ VarDRatPair computeDiff(ArithVar basic);
+
public:
ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau);
void enqueueIfInconsistent(ArithVar basic);
- GriggioPQueue::const_iterator queueAsListBegin() const;
- GriggioPQueue::const_iterator queueAsListEnd() const;
-
inline bool basicAndInconsistent(ArithVar var) const{
return d_tableau.isBasic(var)
&& !d_partialModel.assignmentIsConsistent(var) ;
}
- void useGriggioQueue();
+ void transitionToDifferenceMode();
+ void transitionToVariableOrderMode();
+ void transitionToCollectionMode();
- void useBlandQueue();
-
- inline bool usingGriggioRule() const{
- return d_usingGriggioRule;
+ inline bool inDifferenceMode() const{
+ return d_modeInUse == Difference;
+ }
+ inline bool inCollectionMode() const{
+ return d_modeInUse == Collection;
+ }
+ inline bool inVariableOrderMode() const{
+ return d_modeInUse == VariableOrder;
}
inline bool empty() const{
- if(usingGriggioRule()){
- return d_griggioRuleQueue.empty();
- }else{
- return d_possiblyInconsistent.empty();
+ switch(d_modeInUse){
+ case Collection: return d_candidates.empty();
+ case VariableOrder: return d_varOrderQueue.empty();
+ case Difference: return d_diffQueue.empty();
+ default: Unreachable();
}
}
inline size_t size() const {
- if(usingGriggioRule()){
- return d_griggioRuleQueue.size();
- }else{
- return d_possiblyInconsistent.size();
+ switch(d_modeInUse){
+ case Collection: return d_candidates.size();
+ case VariableOrder: return d_varOrderQueue.size();
+ case Difference: return d_diffQueue.size();
+ default: Unreachable();
}
}
+ /** Clears the queue. */
void clear();
+
+
+ class const_iterator {
+ private:
+ Mode d_mode;
+ ArithVarArray::const_iterator d_avIter;
+ DifferenceArray::const_iterator d_diffIter;
+ public:
+ const_iterator(Mode m,
+ ArithVarArray::const_iterator av,
+ DifferenceArray::const_iterator diff):
+ d_mode(m), d_avIter(av), d_diffIter(diff)
+ {}
+ const_iterator(const const_iterator& other):
+ d_mode(other.d_mode), d_avIter(other.d_avIter), d_diffIter(other.d_diffIter)
+ {}
+ bool operator==(const const_iterator& other) const{
+ AlwaysAssert(d_mode == other.d_mode);
+ switch(d_mode){
+ case Collection:
+ case VariableOrder:
+ return d_avIter == other.d_avIter;
+ case Difference:
+ return d_diffIter == other.d_diffIter;
+ default:
+ Unreachable();
+ }
+ }
+ bool operator!=(const const_iterator& other) const{
+ return !(*this == other);
+ }
+ const_iterator& operator++(){
+ switch(d_mode){
+ case Collection:
+ case VariableOrder:
+ ++d_avIter;
+ break;
+ case Difference:
+ ++d_diffIter;
+ break;
+ default:
+ Unreachable();
+ }
+ return *this;
+ }
+
+ ArithVar operator*() const{
+ switch(d_mode){
+ case Collection:
+ case VariableOrder:
+ return *d_avIter;
+ case Difference:
+ return (*d_diffIter).variable();
+ default:
+ Unreachable();
+ }
+ }
+ };
+
+ const_iterator begin() const{
+ switch(d_modeInUse){
+ case Collection:
+ return const_iterator(Collection, d_candidates.begin(), d_diffQueue.end());
+ case VariableOrder:
+ return const_iterator(VariableOrder, d_varOrderQueue.begin(), d_diffQueue.end());
+ case Difference:
+ return const_iterator(Difference, d_varOrderQueue.end(), d_diffQueue.begin());
+ default:
+ Unreachable();
+ }
+ }
+
+ const_iterator end() const{
+ switch(d_modeInUse){
+ case Collection:
+ return const_iterator(Collection, d_candidates.end(), d_diffQueue.end());
+ case VariableOrder:
+ return const_iterator(VariableOrder, d_varOrderQueue.end(), d_diffQueue.end());
+ case Difference:
+ return const_iterator(Difference, d_varOrderQueue.end(), d_diffQueue.end());
+ default:
+ Unreachable();
+ }
+ }
};
ArithVar slack = ARITHVAR_SENTINEL;
uint32_t numRows = std::numeric_limits<uint32_t>::max();
- bool pivotStage = d_queue.usingGriggioRule();
+ bool pivotStage = d_queue.inDifferenceMode();
for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
nbi != end; ++nbi){
TimerStat::CodeTimer codeTimer(d_statistics.d_selectInitialConflictTime);
int conflictChanges = 0;
- ArithPriorityQueue::GriggioPQueue::const_iterator i = d_queue.queueAsListBegin();
- ArithPriorityQueue::GriggioPQueue::const_iterator end = d_queue.queueAsListEnd();
+ ArithPriorityQueue::const_iterator i = d_queue.begin();
+ ArithPriorityQueue::const_iterator end = d_queue.end();
for(; i != end; ++i){
- ArithVar x_i = (*i).variable();
+ ArithVar x_i = *i;
if(d_tableau.isBasic(x_i)){
Node possibleConflict = checkBasicForConflict(x_i);
d_foundAConflict = false;
d_pivotsSinceConflict = 0;
+ d_queue.transitionToDifferenceMode();
+
Node possibleConflict = Node::null();
if(d_queue.size() > 1){
possibleConflict = selectInitialConflict();
}
if(!d_queue.empty() && possibleConflict.isNull()){
- d_queue.useBlandQueue();
+ d_queue.transitionToVariableOrderMode();
possibleConflict = searchForFeasibleSolution<false>(0);
}
// means that the assignment we can always empty these queues.
d_queue.clear();
- if(!d_queue.usingGriggioRule()){
- d_queue.useGriggioQueue();
- }
- Assert(d_queue.usingGriggioRule());
+ Assert(!d_queue.inCollectionMode());
+ d_queue.transitionToCollectionMode();
+
+
+ Assert(d_queue.inCollectionMode());
return possibleConflict;
}
projects / cvc5.git / commitdiff