- Merged RowVector and ReducedRowVector.

- Renamed NonZeroIterator to const_iterator.
- Both of these changes are in response to the code review.

3 files changed, 161 insertions, 215 deletions

diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
index 0dc483126..6980188a1 100644
--- a/src/theory/arith/row_vector.cpp
+++ b/src/theory/arith/row_vector.cpp
@@ -7,10 +7,10 @@ using namespace CVC4::theory::arith;
 
 using namespace std;
 
-bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) {
+bool ReducedRowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) {
   if(arr.size() >= 2){
-    NonZeroIterator curr = arr.begin();
-    NonZeroIterator end = arr.end();
+    const_iterator curr = arr.begin();
+    const_iterator end = arr.end();
     ArithVar prev = getArithVar(*curr);
     ++curr;
     for(;curr != end; ++curr){
@@ -23,20 +23,26 @@ bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) {
   return true;
 }
 
-RowVector::~RowVector(){
-  NonZeroIterator curr = beginNonZero();
-  NonZeroIterator end = endNonZero();
-  for(;curr != end; ++curr){
+ReducedRowVector::~ReducedRowVector(){
+  //This executes before the super classes destructor RowVector,
+  // which will set this to 0.
+  Assert(d_rowCount[basic()] == 1);
+
+  const_iterator curr = begin();
+  const_iterator endEntries = end();
+  for(;curr != endEntries; ++curr){
     ArithVar v = getArithVar(*curr);
     Assert(d_rowCount[v] >= 1);
+    d_columnMatrix[v].remove(basic());
     --(d_rowCount[v]);
   }
 
   Assert(matchingCounts());
 }
 
-bool RowVector::matchingCounts() const{
-  for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){
+
+bool ReducedRowVector::matchingCounts() const{
+  for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
     ArithVar v = getArithVar(*i);
     if(d_columnMatrix[v].size() != d_rowCount[v]){
       return false;
@@ -45,18 +51,18 @@ bool RowVector::matchingCounts() const{
   return true;
 }
 
-bool RowVector::noZeroCoefficients(const VarCoeffArray& arr){
-  for(NonZeroIterator curr = arr.begin(), end = arr.end();
-      curr != end; ++curr){
+bool ReducedRowVector::noZeroCoefficients(const VarCoeffArray& arr){
+  for(const_iterator curr = arr.begin(), endEntries = arr.end();
+      curr != endEntries; ++curr){
     const Rational& coeff = getCoefficient(*curr);
     if(coeff == 0) return false;
   }
   return true;
 }
 
-void RowVector::zip(const std::vector< ArithVar >& variables,
-                    const std::vector< Rational >& coefficients,
-                    VarCoeffArray& output){
+void ReducedRowVector::zip(const std::vector< ArithVar >& variables,
+                           const std::vector< Rational >& coefficients,
+                           VarCoeffArray& output){
 
   Assert(coefficients.size() == variables.size() );
 
@@ -72,81 +78,56 @@ void RowVector::zip(const std::vector< ArithVar >& variables,
   }
 }
 
-
-RowVector::RowVector(const std::vector< ArithVar >& variables,
-                     const std::vector< Rational >& coefficients,
-                     std::vector<uint32_t>& counts,
-                     std::vector<ArithVarSet>& cm):
-  d_rowCount(counts), d_columnMatrix(cm)
-{
-  zip(variables, coefficients, d_entries);
-
-  std::sort(d_entries.begin(), d_entries.end(), cmp);
-
-  for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){
-    ++d_rowCount[getArithVar(*i)];
-    addArithVar(d_contains, getArithVar(*i));
-  }
-
-  Assert(isSorted(d_entries, true));
-  Assert(noZeroCoefficients(d_entries));
-}
-
-void RowVector::addArithVar(ArithVarContainsSet& contains, ArithVar v){
+void ReducedRowVector::addArithVar(ArithVarContainsSet& contains, ArithVar v){
   if(v >= contains.size()){
     contains.resize(v+1, false);
   }
   contains[v] = true;
 }
 
-void RowVector::removeArithVar(ArithVarContainsSet& contains, ArithVar v){
+void ReducedRowVector::removeArithVar(ArithVarContainsSet& contains, ArithVar v){
   Assert(v < contains.size());
   Assert(contains[v]);
   contains[v] = false;
 }
 
-void RowVector::merge(VarCoeffArray& arr,
-                      ArithVarContainsSet& contains,
-                      const VarCoeffArray& other,
-                      const Rational& c,
-                      std::vector<uint32_t>& counts,
-                      std::vector<ArithVarSet>& columnMatrix,
-                      ArithVar basic){
-  VarCoeffArray copy = arr;
-  arr.clear();
+void ReducedRowVector::merge(const VarCoeffArray& other,
+                             const Rational& c){
+  VarCoeffArray copy = d_entries;
+  d_entries.clear();
 
   iterator curr1 = copy.begin();
   iterator end1 = copy.end();
 
-  NonZeroIterator curr2 = other.begin();
-  NonZeroIterator end2 = other.end();
+  const_iterator curr2 = other.begin();
+  const_iterator end2 = other.end();
 
   while(curr1 != end1 && curr2 != end2){
     if(getArithVar(*curr1) < getArithVar(*curr2)){
-      arr.push_back(*curr1);
+      d_entries.push_back(*curr1);
       ++curr1;
     }else if(getArithVar(*curr1) > getArithVar(*curr2)){
 
-      ++counts[getArithVar(*curr2)];
-      if(basic != ARITHVAR_SENTINEL){
-        columnMatrix[getArithVar(*curr2)].add(basic);
+      ++d_rowCount[getArithVar(*curr2)];
+      if(d_basic != ARITHVAR_SENTINEL){
+        d_columnMatrix[getArithVar(*curr2)].add(d_basic);
       }
 
-      addArithVar(contains, getArithVar(*curr2));
-      arr.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
+      addArithVar(d_contains, getArithVar(*curr2));
+      d_entries.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
       ++curr2;
     }else{
       Rational res = getCoefficient(*curr1) + c * getCoefficient(*curr2);
       if(res != 0){
         //The variable is not new so the count stays the same
 
-        arr.push_back(make_pair(getArithVar(*curr1), res));
+        d_entries.push_back(make_pair(getArithVar(*curr1), res));
       }else{
-        removeArithVar(contains, getArithVar(*curr2));
+        removeArithVar(d_contains, getArithVar(*curr2));
 
-        --counts[getArithVar(*curr2)];
-        if(basic != ARITHVAR_SENTINEL){
-          columnMatrix[getArithVar(*curr2)].remove(basic);
+        --d_rowCount[getArithVar(*curr2)];
+        if(d_basic != ARITHVAR_SENTINEL){
+          d_columnMatrix[getArithVar(*curr2)].remove(d_basic);
         }
       }
       ++curr1;
@@ -154,23 +135,23 @@ void RowVector::merge(VarCoeffArray& arr,
     }
   }
   while(curr1 != end1){
-    arr.push_back(*curr1);
+    d_entries.push_back(*curr1);
     ++curr1;
   }
   while(curr2 != end2){
-    ++counts[getArithVar(*curr2)];
-    if(basic != ARITHVAR_SENTINEL){
-      columnMatrix[getArithVar(*curr2)].add(basic);
+    ++d_rowCount[getArithVar(*curr2)];
+    if(d_basic != ARITHVAR_SENTINEL){
+      d_columnMatrix[getArithVar(*curr2)].add(d_basic);
     }
 
-    addArithVar(contains, getArithVar(*curr2));
+    addArithVar(d_contains, getArithVar(*curr2));
 
-    arr.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
+    d_entries.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
     ++curr2;
   }
 }
 
-void RowVector::multiply(const Rational& c){
+void ReducedRowVector::multiply(const Rational& c){
   Assert(c != 0);
 
   for(iterator i = d_entries.begin(), end = d_entries.end(); i != end; ++i){
@@ -178,14 +159,14 @@ void RowVector::multiply(const Rational& c){
   }
 }
 
-void RowVector::addRowTimesConstant(const Rational& c, const RowVector& other, ArithVar basic){
+void ReducedRowVector::addRowTimesConstant(const Rational& c, const ReducedRowVector& other){
   Assert(c != 0);
 
-  merge(d_entries, d_contains, other.d_entries, c, d_rowCount, d_columnMatrix, basic);
+  merge(other.d_entries, c);
 }
 
-void RowVector::printRow(){
-  for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){
+void ReducedRowVector::printRow(){
+  for(const_iterator i = begin(); i != end(); ++i){
     ArithVar nb = getArithVar(*i);
     Debug("row::print") << "{" << nb << "," << getCoefficient(*i) << "}";
   }
@@ -196,21 +177,23 @@ void RowVector::printRow(){
 ReducedRowVector::ReducedRowVector(ArithVar basic,
                                    const std::vector<ArithVar>& variables,
                                    const std::vector<Rational>& coefficients,
-                                   std::vector<uint32_t>& count,
-                                   std::vector<ArithVarSet>& columnMatrix):
-  RowVector(variables, coefficients, count, columnMatrix), d_basic(basic){
+                                   std::vector<uint32_t>& counts,
+                                   std::vector<ArithVarSet>& cm):
+  d_basic(basic), d_rowCount(counts),  d_columnMatrix(cm)
+{
+  zip(variables, coefficients, d_entries);
+  d_entries.push_back(make_pair(basic, Rational(-1)));
 
+  std::sort(d_entries.begin(), d_entries.end(), cmp);
 
-  for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){
-    //basic is not yet in d_entries
-    Assert(getArithVar(*i) != d_basic);
+  for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
+    ++d_rowCount[getArithVar(*i)];
+    addArithVar(d_contains, getArithVar(*i));
     d_columnMatrix[getArithVar(*i)].add(d_basic);
   }
 
-  VarCoeffArray justBasic;
-  justBasic.push_back(make_pair(basic, Rational(-1)));
-
-  merge(d_entries, d_contains, justBasic, Rational(1), d_rowCount, d_columnMatrix, d_basic);
+  Assert(isSorted(d_entries, true));
+  Assert(noZeroCoefficients(d_entries));
 
   Assert(matchingCounts());
   Assert(wellFormed());
@@ -226,7 +209,7 @@ void ReducedRowVector::substitute(const ReducedRowVector& row_s){
   Rational a_rs = lookup(x_s);
   Assert(a_rs != 0);
 
-  addRowTimesConstant(a_rs, row_s, basic());
+  addRowTimesConstant(a_rs, row_s);
 
 
   Assert(!has(x_s));
@@ -241,7 +224,7 @@ void ReducedRowVector::pivot(ArithVar x_j){
   Rational negInverseA_rs = -(lookup(x_j).inverse());
   multiply(negInverseA_rs);
 
-  for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){
+  for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
     d_columnMatrix[getArithVar(*i)].remove(d_basic);
     d_columnMatrix[getArithVar(*i)].add(x_j);
   }
@@ -264,7 +247,7 @@ Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{
   if(size() > 2){
     NodeBuilder<> sumBuilder(PLUS);
 
-    for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){
+    for(const_iterator i = begin(); i != end(); ++i){
       ArithVar nb = getArithVar(*i);
       if(nb == basic()) continue;
       Node var = (map.find(nb))->second;
@@ -276,7 +259,7 @@ Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{
     sum = sumBuilder;
   }else{
     Assert(size() == 2);
-    NonZeroIterator i = beginNonZero();
+    const_iterator i = begin();
     if(getArithVar(*i) == basic()){
       ++i;
     }
@@ -289,17 +272,3 @@ Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{
   return NodeBuilder<2>(EQUAL) << basicVar << sum;
 }
 
-
-ReducedRowVector::~ReducedRowVector(){
-  //This executes before the super classes destructor RowVector,
-  // which will set this to 0.
-  Assert(d_rowCount[basic()] == 1);
-
-  NonZeroIterator curr = beginNonZero();
-  NonZeroIterator end = endNonZero();
-  for(;curr != end; ++curr){
-    ArithVar v = getArithVar(*curr);
-    Assert(d_rowCount[v] >= 1);
-    d_columnMatrix[v].remove(basic());
-  }
-}
diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index bed33349d..829cecd7e 100644
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -15,58 +15,30 @@ namespace theory {
 namespace arith {
 
 typedef std::pair<ArithVar, Rational> VarCoeffPair;
+
 inline ArithVar getArithVar(const VarCoeffPair& v) { return v.first; }
 inline Rational& getCoefficient(VarCoeffPair& v) { return v.second; }
 inline const Rational& getCoefficient(const VarCoeffPair& v) { return v.second; }
 
 inline bool cmp(const VarCoeffPair& a, const VarCoeffPair& b){
-  return CVC4::theory::arith::getArithVar(a) < CVC4::theory::arith::getArithVar(b);
+  return getArithVar(a) < getArithVar(b);
 }
 
 /**
- * RowVector is a sparse vector representation that represents the
+ * ReducedRowVector is a sparse vector representation that represents the
  * row as a strictly sorted array of "VarCoeffPair"s.
+ * The row has a notion of a basic variable.
+ * This is a variable that must have a coefficient of -1 in the array.
  */
-class RowVector {
+class ReducedRowVector {
 public:
   typedef std::vector<VarCoeffPair> VarCoeffArray;
-  typedef VarCoeffArray::const_iterator NonZeroIterator;
+  typedef VarCoeffArray::const_iterator const_iterator;
 
   typedef std::vector<bool> ArithVarContainsSet;
 
-  /**
-   * Let c be -1 if strictlySorted is true and c be 0 otherwise.
-   * isSorted(arr, strictlySorted) is then equivalent to
-   * If i<j, cmp(getArithVar(d_entries[i]), getArithVar(d_entries[j])) <= c.
-   */
-  static bool isSorted(const VarCoeffArray& arr, bool strictlySorted);
-
-  /**
-   * Zips together an array of variables and coefficients and appends
-   * it to the end of an output vector.
-   */
-  static void zip(const std::vector< ArithVar >& variables,
-                  const std::vector< Rational >& coefficients,
-                  VarCoeffArray& output);
-
-  static void merge(VarCoeffArray& arr,
-                    ArithVarContainsSet& contains,
-                    const VarCoeffArray& other,
-                    const Rational& c,
-                    std::vector<uint32_t>& count,
-                    std::vector<ArithVarSet>& columnMatrix,
-                    ArithVar basic);
-
-protected:
-  /**
-   * Debugging code.
-   * noZeroCoefficients(arr) is equivalent to
-   *  0 != getCoefficient(arr[i]) for all i.
-   */
-  static bool noZeroCoefficients(const VarCoeffArray& arr);
-
-  /** Debugging code.*/
-  bool matchingCounts() const;
+private:
+  typedef VarCoeffArray::iterator iterator;
 
   /**
    * Invariants:
@@ -76,6 +48,13 @@ protected:
   VarCoeffArray d_entries;
 
   /**
+   * The basic variable associated with the row.
+   * Must have a coefficient of -1.
+   */
+  ArithVar d_basic;
+
+
+  /**
    * Invariants:
    * - This set is the same as the set maintained in d_entries.
    */
@@ -84,20 +63,21 @@ protected:
   std::vector<uint32_t>& d_rowCount;
   std::vector<ArithVarSet>& d_columnMatrix;
 
-  NonZeroIterator lower_bound(ArithVar x_j) const{
-    return std::lower_bound(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
-  }
-
-  typedef VarCoeffArray::iterator iterator;
 
 public:
 
-  RowVector(const std::vector< ArithVar >& variables,
-            const std::vector< Rational >& coefficients,
-            std::vector<uint32_t>& counts,
-            std::vector<ArithVarSet>& columnMatrix);
+  ReducedRowVector(ArithVar basic,
+                   const std::vector< ArithVar >& variables,
+                   const std::vector< Rational >& coefficients,
+                   std::vector<uint32_t>& count,
+                   std::vector<ArithVarSet>& columnMatrix);
 
-  ~RowVector();
+  ~ReducedRowVector();
+
+  ArithVar basic() const{
+    Assert(basicIsSet());
+    return d_basic;
+  }
 
   /** Returns the number of nonzero variables in the vector. */
   uint32_t size() const {
@@ -105,8 +85,8 @@ public:
   }
 
   //Iterates over the nonzero entries in the Vector
-  NonZeroIterator beginNonZero() const { return d_entries.begin(); }
-  NonZeroIterator endNonZero() const { return d_entries.end(); }
+  const_iterator begin() const { return d_entries.begin(); }
+  const_iterator end() const { return d_entries.end(); }
 
   /** Returns true if the variable is in the row. */
   bool has(ArithVar x_j) const{
@@ -117,20 +97,13 @@ public:
     }
   }
 
-private:
-  /** Debugging code. */
-  bool hasInEntries(ArithVar x_j) const {
-    return std::binary_search(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
-  }
-public:
-
   /**
    * Returns the coefficient of a variable in the row.
    */
   const Rational& lookup(ArithVar x_j) const{
     Assert(has(x_j));
     Assert(hasInEntries(x_j));
-    NonZeroIterator lb = lower_bound(x_j);
+    const_iterator lb = lower_bound(x_j);
     return getCoefficient(*lb);
   }
 
@@ -143,11 +116,23 @@ public:
    * Updates the current row to be the sum of itself and
    * another vector times c (c != 0).
    */
-  void addRowTimesConstant(const Rational& c, const RowVector& other, ArithVar basic);
+  void addRowTimesConstant(const Rational& c, const ReducedRowVector& other);
 
   void printRow();
 
-protected:
+
+  void pivot(ArithVar x_j);
+
+  void substitute(const ReducedRowVector& other);
+
+  /**
+   * Returns the reduced row as an equality with
+   * the basic variable on the lhs equal to the sum of the non-basics variables.
+   * The mapped from ArithVars to Nodes is specificied by map.
+   */
+  Node asEquality(const ArithVarToNodeMap& map) const;
+
+private:
   /**
    * Adds v to d_contains.
    * This may resize d_contains.
@@ -157,17 +142,39 @@ protected:
   /** Removes v from d_contains. */
   static void removeArithVar(ArithVarContainsSet& contains, ArithVar v);
 
-}; /* class RowVector */
 
-/**
- * A reduced row is similar to a normal row except
- * that it also has a notion of a basic variable.
- * This variable that must have a coefficient of -1 in the array.
- */
-class ReducedRowVector : public RowVector{
-private:
-  ArithVar d_basic;
+  /**
+   * Let c be -1 if strictlySorted is true and c be 0 otherwise.
+   * isSorted(arr, strictlySorted) is then equivalent to
+   * If i<j, cmp(getArithVar(d_entries[i]), getArithVar(d_entries[j])) <= c.
+   */
+  static bool isSorted(const VarCoeffArray& arr, bool strictlySorted);
 
+  /**
+   * Zips together an array of variables and coefficients and appends
+   * it to the end of an output vector.
+   */
+  static void zip(const std::vector< ArithVar >& variables,
+                  const std::vector< Rational >& coefficients,
+                  VarCoeffArray& output);
+
+  void merge(const VarCoeffArray& other, const Rational& c);
+
+  /**
+   * Debugging code.
+   * noZeroCoefficients(arr) is equivalent to
+   *  0 != getCoefficient(arr[i]) for all i.
+   */
+  static bool noZeroCoefficients(const VarCoeffArray& arr);
+
+  /** Debugging code.*/
+  bool matchingCounts() const;
+
+  const_iterator lower_bound(ArithVar x_j) const{
+    return std::lower_bound(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
+  }
+
+  /** Debugging code */
   bool wellFormed() const{
     return
       isSorted(d_entries, true) &&
@@ -177,42 +184,13 @@ private:
       lookup(basic()) == Rational(-1);
   }
 
-public:
-
   bool basicIsSet() const { return d_basic != ARITHVAR_SENTINEL; }
 
-  ReducedRowVector(ArithVar basic,
-                   const std::vector< ArithVar >& variables,
-                   const std::vector< Rational >& coefficients,
-                   std::vector<uint32_t>& count,
-                   std::vector<ArithVarSet>& columnMatrix);
-
-  ~ReducedRowVector();
-
-  ArithVar basic() const{
-    Assert(basicIsSet());
-    return d_basic;
-  }
-
-  /** Return true if x is in the row and is not the basic variable. */
-  bool hasNonBasic(ArithVar x) const {
-    if(x == basic()){
-      return false;
-    }else{
-      return has(x);
-    }
+  /** Debugging code. */
+  bool hasInEntries(ArithVar x_j) const {
+    return std::binary_search(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
   }
 
-  void pivot(ArithVar x_j);
-
-  void substitute(const ReducedRowVector& other);
-
-  /**
-   * Returns the reduced row as an equality with
-   * the basic variable on the lhs equal to the sum of the non-basics variables.
-   * The mapped from ArithVars to Nodes is specificied by map.
-   */
-  Node asEquality(const ArithVarToNodeMap& map) const;
 }; /* class ReducedRowVector */
 
 
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index c8f1ce3e8..02ce310ff 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -253,8 +253,8 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
   if(Debug.isOn("arith::pivotAndUpdate")){
     Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl;
     ReducedRowVector& row_k = d_tableau.lookup(x_i);
-    for(ReducedRowVector::NonZeroIterator varIter = row_k.beginNonZero();
-        varIter != row_k.endNonZero();
+    for(ReducedRowVector::const_iterator varIter = row_k.begin();
+        varIter != row_k.end();
         ++varIter){
 
       ArithVar var = varIter->first;
@@ -332,7 +332,7 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, bool first){
 
   bool pivotStage = !first;
 
-  for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
+  for(ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
       nbi != end; ++nbi){
     ArithVar nonbasic = getArithVar(*nbi);
     if(nonbasic == x_i) continue;
@@ -494,7 +494,7 @@ template <bool limitIterations>
 Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
   Debug("arith") << "updateInconsistentVars" << endl;
 
-  static const uint32_t CHECK_PERIOD = 1000;
+  static const uint32_t CHECK_PERIOD = 100;
 
   while(!limitIterations || remainingIterations > 0){
     if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
@@ -536,12 +536,12 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
       return earlyConflict;
     }
     //Once every CHECK_PERIOD examine the entire queue for conflicts
-    // if(!limitIterations && remainingIterations % CHECK_PERIOD == 0){
-    //   Node earlyConflict = findConflictOnTheQueue(DuringVarOrderSearch);
-    //   if(!earlyConflict.isNull()){
-    //     return earlyConflict;
-    //   }
-    // }
+    if(!limitIterations && remainingIterations % CHECK_PERIOD == 0){
+      Node earlyConflict = findConflictOnTheQueue(DuringVarOrderSearch);
+      if(!earlyConflict.isNull()){
+        return earlyConflict;
+      }
+    }
   }
   AlwaysAssert(limitIterations && remainingIterations == 0);
 
@@ -563,8 +563,7 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
 
   nb << bound;
 
-  typedef ReducedRowVector::NonZeroIterator RowIterator;
-  RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
+  ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
 
   for(; nbi != end; ++nbi){
     ArithVar nonbasic = getArithVar(*nbi);
@@ -604,8 +603,8 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
                  << " " << bound << endl;
   nb << bound;
 
-  typedef ReducedRowVector::NonZeroIterator RowIterator;
-  RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero();
+
+  ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
   for(; nbi != end; ++nbi){
     ArithVar nonbasic = getArithVar(*nbi);
     if(nonbasic == conflictVar) continue;
@@ -642,7 +641,7 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe
   DeltaRational sum = d_constants.d_ZERO_DELTA;
 
   ReducedRowVector& row = d_tableau.lookup(x);
-  for(ReducedRowVector::NonZeroIterator i = row.beginNonZero(), end = row.endNonZero();
+  for(ReducedRowVector::const_iterator i = row.begin(), end = row.end();
       i != end;++i){
     ArithVar nonbasic = getArithVar(*i);
     if(nonbasic == row.basic()) continue;
@@ -669,8 +668,8 @@ void SimplexDecisionProcedure::checkTableau(){
     ReducedRowVector& row_k = d_tableau.lookup(basic);
     DeltaRational sum;
     Debug("paranoid:check_tableau") << "starting row" << basic << endl;
-    for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k.beginNonZero();
-        nonbasicIter != row_k.endNonZero();
+    for(ReducedRowVector::const_iterator nonbasicIter = row_k.begin();
+        nonbasicIter != row_k.end();
         ++nonbasicIter){
       ArithVar nonbasic = nonbasicIter->first;
       if(basic == nonbasic) continue;