From: Tim King <taking@cs.nyu.edu>
Date: Thu, 24 Feb 2011 20:36:35 +0000 (+0000)
Subject: - Adds an additional mode to ArithPriorityQueue, Collection. Collection is a mode... 
X-Git-Tag: cvc5-1.0.0~8694
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1d64c07f3eb160d297e786b31dac6ed05cd05a1a;p=cvc5.git

- Adds an additional mode to ArithPriorityQueue, Collection. Collection is a mode where the heap structure is not maintained.  There is just a list of variables that may be inconsistent. This is used up until the simplex procedure is invoked.
- Misc. cleanup and renaming in ArithPriorityQueue.
---

diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index f694c9bfd..76db6b580 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -1,6 +1,8 @@
 
 #include "theory/arith/arith_priority_queue.h"
 
+#include <algorithm>
+
 using namespace std;
 
 using namespace CVC4;
@@ -10,17 +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_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;
@@ -28,12 +32,12 @@ ArithVar ArithPriorityQueue::popInconsistentBasicVariable(){
     }
   }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)){
@@ -44,67 +48,108 @@ ArithVar ArithPriorityQueue::popInconsistentBasicVariable(){
   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());
 }
diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index 92e3ffc3a..9cee8b29b 100644
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -11,16 +11,40 @@
 
 
 #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:
@@ -37,10 +61,14 @@ private:
     }
   };
 
-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.
@@ -48,7 +76,7 @@ private:
    * 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.
@@ -60,7 +88,7 @@ private:
    * 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
@@ -71,16 +99,19 @@ private:
   /** 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);
@@ -89,39 +120,129 @@ public:
 
   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();
+    }
+  }
 };
 
 
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 4efa5fa43..ced76c843 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -342,7 +342,7 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
   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){
@@ -410,10 +410,10 @@ Node SimplexDecisionProcedure::selectInitialConflict() {
   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);
@@ -441,6 +441,8 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   d_foundAConflict = false;
   d_pivotsSinceConflict = 0;
 
+  d_queue.transitionToDifferenceMode();
+
   Node possibleConflict = Node::null();
   if(d_queue.size() > 1){
     possibleConflict = selectInitialConflict();
@@ -450,7 +452,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   }
 
   if(!d_queue.empty() && possibleConflict.isNull()){
-    d_queue.useBlandQueue();
+    d_queue.transitionToVariableOrderMode();
     possibleConflict = searchForFeasibleSolution<false>(0);
   }
 
@@ -460,10 +462,11 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   // 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;
 }