- 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.

3 files changed, 72 insertions, 74 deletions

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<ArithVar>());
+      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<ArithVar>());
     }
   }
 }
 
-
-void ArithPriorityQueue::enqueueTrustedVector(const vector<VarDRatPair>& 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<VarDRatPair>& 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<ArithVar>());
   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 <queue>
+
+#include <vector>
+#include <algorithm>
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
-typedef std::pair<ArithVar, DeltaRational> VarDRatPair;
-
-struct VarDRatPairCompare{
-  inline bool operator()(const VarDRatPair& a, const VarDRatPair& b){
-    return a.second > b.second;
-  }
-};
-
-typedef std::priority_queue<VarDRatPair, std::vector<VarDRatPair>, VarDRatPairCompare> GriggioPQueue;
 
-typedef std::priority_queue<ArithVar, vector<ArithVar>, std::greater<ArithVar> > 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<VarDRatPair> GriggioPQueue;
 private:
+  typedef std::vector<ArithVar> 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<VarDRatPair>& trusted);
-
-  void dumpQueueIntoVector(vector<VarDRatPair>& 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<VarDRatPair>  init;
-  d_queue.dumpQueueIntoVector(init);
-
   int conflictChanges = 0;
-  vector<VarDRatPair>::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<true>(d_numVariables + 1);
   }
 
-  if(possibleConflict.isNull()){
+  if(!d_queue.empty() && possibleConflict.isNull()){
     d_queue.useBlandQueue();
     possibleConflict = searchForFeasibleSolution<false>(0);
   }
@@ -499,16 +490,12 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
 //corresponds to Check() in dM06
 template <bool limitIterations>
 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<useGriggioQueue>();
     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();
 }