5 files changed, 289 insertions, 119 deletions

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<VarDRatPair>& trusted){
+  Assert(usingGriggioRule());
+  Assert(empty());
+
+  d_griggioRuleQueue = GriggioPQueue(trusted.begin(), trusted.end());
+  Assert(size() == trusted.size());
+}
+
+
+void ArithPriorityQueue::dumpQueueIntoVector(vector<VarDRatPair>& 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 <queue>
+
+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:
+  /**
+   * 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<VarDRatPair>& trusted);
+
+  void dumpQueueIntoVector(vector<VarDRatPair>& 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 <bool above>
 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<uint32_t>::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<VarDRatPair>  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<VarDRatPair>::iterator i=init.begin(), end=init.end(); i != end; ++i){
+  vector<VarDRatPair>::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<true>(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<false>(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 <bool limitIterations>
+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<useGriggioQueue>();
     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<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;
-
-  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<ArithVar, vector<ArithVar>, std::greater<ArithVar> > 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 <bool limitIterations> 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.