The Row implementation has no been replaced by RowVector and ReducedRowVector. A RowVector is an array of ArithVar and Rational pairs. (This replaces a map based implementation in Row.) ReducedRowVector is a RowVector with a notion of having a basic variable. The Tableau is now a collection of ReduceRowVector's. A major difference between ReducedRowVectors and Rows is that the iterator now includes the basic variable and its coefficient (always -1). Before only nonbasic members were accessible by the iterator.

7 files changed, 374 insertions, 194 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 21ec99390..907c8820f 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -21,6 +21,8 @@ libarith_la_SOURCES = \
 	arithvar_dense_set.h \
 	tableau.h \
 	tableau.cpp \
+	row_vector.h \
+	row_vector.cpp \
 	arith_propagator.h \
 	arith_propagator.cpp \
 	theory_arith.h \
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 0a962283c..1c9b2685d 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -740,6 +740,11 @@ public:
 
   static Comparison parseNormalForm(TNode n);
 
+  inline static bool isNormalAtom(TNode n){
+    Comparison parse = Comparison::parseNormalForm(n);
+    return parse.isNormalForm();
+  }
+
 };/* class Comparison */
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
new file mode 100644
index 000000000..6835fc435
--- /dev/null
+++ b/src/theory/arith/row_vector.cpp
@@ -0,0 +1,131 @@
+
+#include "theory/arith/row_vector.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith ;
+
+void RowVector::zip(const vector< ArithVar >& variables,
+                    const vector< Rational >& coefficients,
+                    VarCoeffArray& output){
+
+  Assert(coefficients.size() == variables.size() );
+
+  vector<Rational>::const_iterator coeffIter = coefficients.begin();
+  vector<Rational>::const_iterator coeffEnd = coefficients.end();
+  vector<ArithVar>::const_iterator varIter = variables.begin();
+
+  for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){
+    const Rational& coeff = *coeffIter;
+    ArithVar var_i = *varIter;
+
+    output.push_back(make_pair(var_i, coeff));
+  }
+}
+
+RowVector::RowVector(const vector< ArithVar >& variables,
+                     const vector< Rational >& coefficients){
+  zip(variables, coefficients, d_entries);
+
+  std::sort(d_entries.begin(), d_entries.end(), cmp);
+
+  Assert(isSorted(d_entries, true));
+  Assert(noZeroCoefficients(d_entries));
+}
+
+void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c){
+  VarCoeffArray copy = arr;
+  arr.clear();
+
+  iterator curr1 = copy.begin();
+  iterator end1 = copy.end();
+
+  NonZeroIterator curr2 = other.begin();
+  NonZeroIterator end2 = other.end();
+
+  while(curr1 != end1 && curr2 != end2){
+    if(getArithVar(*curr1) < getArithVar(*curr2)){
+      arr.push_back(*curr1);
+      ++curr1;
+    }else if(getArithVar(*curr1) > getArithVar(*curr2)){
+      arr.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
+      ++curr2;
+    }else{
+      Rational res = getCoefficient(*curr1) + c * getCoefficient(*curr2);
+      if(res != 0){
+        arr.push_back(make_pair(getArithVar(*curr1), res));
+      }
+      ++curr1;
+      ++curr2;
+    }
+  }
+  while(curr1 != end1){
+    arr.push_back(*curr1);
+    ++curr1;
+  }
+  while(curr2 != end2){
+    arr.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
+    ++curr2;
+  }
+}
+
+void RowVector::multiply(const Rational& c){
+  Assert(c != 0);
+
+  for(iterator i = d_entries.begin(), end = d_entries.end(); i != end; ++i){
+    getCoefficient(*i) *= c;
+  }
+}
+
+void RowVector::addRowTimesConstant(const Rational& c, const RowVector& other){
+  Assert(c != 0);
+
+  merge(d_entries, other.d_entries, c);
+}
+
+void RowVector::printRow(){
+  for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){
+    ArithVar nb = getArithVar(*i);
+    Debug("tableau") << "{" << nb << "," << getCoefficient(*i) << "}";
+  }
+  Debug("tableau") << std::endl;
+}
+
+ReducedRowVector::ReducedRowVector(ArithVar basic,
+                                   const vector<ArithVar>& variables,
+                                   const vector<Rational>& coefficients):
+  RowVector(variables, coefficients), d_basic(basic){
+
+
+  VarCoeffArray justBasic;
+  justBasic.push_back(make_pair(basic, Rational(-1)));
+
+  merge(d_entries,justBasic, Rational(1));
+
+  Assert(wellFormed());
+}
+
+void ReducedRowVector::substitute(const ReducedRowVector& row_s){
+  ArithVar x_s = row_s.basic();
+
+  Assert(has(x_s));
+  Assert(x_s != basic());
+
+  Rational a_rs = lookup(x_s);
+  Assert(a_rs != 0);
+
+  addRowTimesConstant(a_rs, row_s);
+
+  Assert(!has(x_s));
+  Assert(wellFormed());
+}
+
+void ReducedRowVector::pivot(ArithVar x_j){
+  Assert(has(x_j));
+  Assert(basic() != x_j);
+  Rational negInverseA_rs = -(lookup(x_j).inverse());
+  multiply(negInverseA_rs);
+  d_basic = x_j;
+
+  Assert(wellFormed());
+}
diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
new file mode 100644
index 000000000..2c88721ea
--- /dev/null
+++ b/src/theory/arith/row_vector.h
@@ -0,0 +1,176 @@
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ROW_VECTOR_H
+#define __CVC4__THEORY__ARITH__ROW_VECTOR_H
+
+#include "theory/arith/arith_utilities.h"
+#include "util/rational.h"
+#include <vector>
+
+namespace CVC4 {
+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);
+}
+
+/**
+ * RowVector is a sparse vector representation that represents the
+ * row as a strictly sorted array of "VarCoeffPair"s.
+ */
+class RowVector {
+public:
+  typedef std::vector<VarCoeffPair> VarCoeffArray;
+  typedef VarCoeffArray::const_iterator NonZeroIterator;
+
+  /**
+   * 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) {
+    if(arr.size() >= 2){
+      NonZeroIterator curr = arr.begin();
+      NonZeroIterator end = arr.end();
+      ArithVar prev = getArithVar(*curr);
+      ++curr;
+      for(;curr != end; ++curr){
+        ArithVar v = getArithVar(*curr);
+        if(strictlySorted && prev > v) return false;
+        if(!strictlySorted && prev >= v) return false;
+        prev = v;
+      }
+    }
+    return true;
+  }
+
+  /**
+   * noZeroCoefficients(arr) is equivalent to
+   *  0 != getCoefficient(arr[i]) for all i.
+   */
+  static bool noZeroCoefficients(const VarCoeffArray& arr){
+    for(NonZeroIterator curr = arr.begin(), end = arr.end();
+        curr != end; ++curr){
+      const Rational& coeff = getCoefficient(*curr);
+      if(coeff == 0) return false;
+    }
+    return true;
+  }
+
+  /**
+   * 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, const VarCoeffArray& other, const Rational& c);
+
+
+protected:
+  /**
+   * Invariants:
+   * - isSorted(d_entries, true)
+   * - noZeroCoefficients(d_entries)
+   */
+  VarCoeffArray d_entries;
+
+  NonZeroIterator lower_bound(ArithVar x_j) const{
+    return std::lower_bound(d_entries.begin(), d_entries.end(), make_pair(x_j,0), cmp);
+  }
+
+  typedef VarCoeffArray::iterator iterator;
+
+public:
+
+  RowVector() : d_entries() {}
+
+  RowVector(const std::vector< ArithVar >& variables,
+            const std::vector< Rational >& coefficients);
+
+
+  //Iterates over the nonzero entries in the Vector
+  NonZeroIterator beginNonZero() const { return d_entries.begin(); }
+  NonZeroIterator endNonZero() const { return d_entries.end(); }
+
+  /** Returns true if the variable is in the row. */
+  bool has(ArithVar x_j) const{
+    NonZeroIterator lb = lower_bound(x_j);
+    return getArithVar(*lb) == x_j;
+  }
+
+  /**
+   * Returns the coefficient of a variable in the row.
+   */
+  const Rational& lookup(ArithVar x_j) const{
+    Assert(has(x_j));
+    NonZeroIterator lb = lower_bound(x_j);
+    return getCoefficient(*lb);
+  }
+
+  /** Multiplies the coefficients of the RowVector by c (where c != 0). */
+  void multiply(const Rational& c);
+
+  /**
+   * \sum(this->entries) += c * (\sum(other.d_entries) )
+   *
+   * 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);
+
+  void printRow();
+}; /* 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;
+
+  bool wellFormed() const{
+    return
+      isSorted(d_entries, true) &&
+      noZeroCoefficients(d_entries) &&
+      basicIsSet() &&
+      has(basic()) &&
+      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);
+
+
+  ArithVar basic() const{
+    Assert(basicIsSet());
+    return d_basic;
+  }
+
+  void pivot(ArithVar x_j);
+
+  void substitute(const ReducedRowVector& other);
+}; /* class ReducedRowVector */
+
+
+}/* namespace CVC4::theory::arith */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 2490ed51b..c22c21a46 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -24,85 +24,6 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
-Row::Row(ArithVar basic,
-         const std::vector< Rational >& coefficients,
-         const std::vector< ArithVar >& variables):
-  d_x_i(basic),
-  d_coeffs(){
-
-  Assert(coefficients.size() == variables.size() );
-
-  std::vector<Rational>::const_iterator coeffIter = coefficients.begin();
-  std::vector<Rational>::const_iterator coeffEnd = coefficients.end();
-  std::vector<ArithVar>::const_iterator varIter = variables.begin();
-
-  for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){
-    const Rational& coeff = *coeffIter;
-    ArithVar var_i = *varIter;
-
-    Assert(var_i != d_x_i);
-    Assert(!has(var_i));
-    Assert(coeff != Rational(0,1));
-
-    d_coeffs[var_i] = coeff;
-    Assert(d_coeffs[var_i] != Rational(0,1));
-  }
-}
-void Row::substitute(Row& row_s){
-  ArithVar x_s = row_s.basicVar();
-
-  Assert(has(x_s));
-  Assert(x_s != d_x_i);
-
-  Rational zero(0,1);
-
-  Rational a_rs = lookup(x_s);
-  Assert(a_rs != zero);
-  d_coeffs.erase(x_s);
-
-  for(iterator iter = row_s.begin(), iter_end = row_s.end();
-      iter != iter_end; ++iter){
-    ArithVar x_j = iter->first;
-    Rational a_sj = iter->second;
-    a_sj *= a_rs;
-    CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j);
-
-    if(coeff_iter != d_coeffs.end()){
-      coeff_iter->second += a_sj;
-      if(coeff_iter->second == zero){
-        d_coeffs.erase(coeff_iter);
-      }
-    }else{
-      d_coeffs.insert(std::make_pair(x_j,a_sj));
-    }
-  }
-}
-
-void Row::pivot(ArithVar x_j){
-  Rational negInverseA_rs = -(lookup(x_j).inverse());
-  d_coeffs[d_x_i] = Rational(Integer(-1));
-  d_coeffs.erase(x_j);
-
-  d_x_i = x_j;
-
-  for(iterator nonbasicIter = begin(), nonbasicIter_end = end();
-      nonbasicIter != nonbasicIter_end; ++nonbasicIter){
-    nonbasicIter->second *= negInverseA_rs;
-  }
-
-}
-
-void Row::printRow(){
-  Debug("tableau") << d_x_i << " ";
-  for(iterator nonbasicIter = d_coeffs.begin();
-      nonbasicIter != d_coeffs.end();
-      ++nonbasicIter){
-    ArithVar nb = nonbasicIter->first;
-    Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}";
-  }
-  Debug("tableau") << std::endl;
-}
-
 void Tableau::addRow(ArithVar basicVar,
                      const std::vector<Rational>& coeffs,
                      const std::vector<ArithVar>& variables){
@@ -113,15 +34,15 @@ void Tableau::addRow(ArithVar basicVar,
   //The new basic variable cannot already be a basic variable
   Assert(!isActiveBasicVariable(basicVar));
   d_activeBasicVars.insert(basicVar);
-  Row* row_current = new Row(basicVar,coeffs,variables);
+  ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs);
   d_rowsTable[basicVar] = row_current;
 
   //A variable in the row may have been made non-basic already.
   //If this is the case we fake pivoting this variable
-  std::vector<Rational>::const_iterator coeffsIter = coeffs.begin();
-  std::vector<Rational>::const_iterator coeffsEnd = coeffs.end();
+  vector<Rational>::const_iterator coeffsIter = coeffs.begin();
+  vector<Rational>::const_iterator coeffsEnd = coeffs.end();
 
-  std::vector<ArithVar>::const_iterator varsIter = variables.begin();
+  vector<ArithVar>::const_iterator varsIter = variables.begin();
 
   for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){
     ArithVar var = *varsIter;
@@ -132,7 +53,7 @@ void Tableau::addRow(ArithVar basicVar,
       }
       Assert(isActiveBasicVariable(var));
 
-      Row* row_var = lookup(var);
+      ReducedRowVector* row_var = lookup(var);
       row_current->substitute(*row_var);
     }
   }
@@ -142,7 +63,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
   Assert(d_basicManager.isMember(x_r));
   Assert(!d_basicManager.isMember(x_s));
 
-  Row* row_s = lookup(x_r);
+  ReducedRowVector* row_s = lookup(x_r);
   Assert(row_s->has(x_s));
 
   //Swap x_r and x_s in d_activeRows
@@ -160,7 +81,9 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
   for(ArithVarSet::iterator basicIter = begin(), endIter = end();
       basicIter != endIter; ++basicIter){
     ArithVar basic = *basicIter;
-    Row* row_k = lookup(basic);
+    if(basic == x_s) continue;
+
+    ReducedRowVector* row_k = lookup(basic);
     if(row_k->has(x_s)){
       d_activityMonitor[basic] += 30;
       row_k->substitute(*row_s);
@@ -173,7 +96,7 @@ void Tableau::printTableau(){
   typedef RowsTable::iterator table_iter;
   for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end();
       rowIter != end; ++rowIter){
-    Row* row_k = *rowIter;
+    ReducedRowVector* row_k = *rowIter;
     if(row_k != NULL){
       row_k->printRow();
     }
@@ -181,18 +104,19 @@ void Tableau::printTableau(){
 }
 
 
-void Tableau::updateRow(Row* row){
-  for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){
+void Tableau::updateRow(ReducedRowVector* row){
+  ArithVar basic = row->basic();
+  for(ReducedRowVector::NonZeroIterator i=row->beginNonZero(), endIter = row->endNonZero(); i != endIter; ){
     ArithVar var = i->first;
     ++i;
-    if(d_basicManager.isMember(var)){
-      Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
+    if(var != basic && d_basicManager.isMember(var)){
+      ReducedRowVector* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
 
       Assert(row_var != row);
       row->substitute(*row_var);
 
-      i = row->begin();
-      endIter = row->end();
+      i = row->beginNonZero();
+      endIter = row->endNonZero();
     }
   }
 }
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 588b521b1..758e5d92d 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -25,8 +25,9 @@
 #include "theory/arith/arithvar_dense_set.h"
 #include "theory/arith/normal_form.h"
 
+#include "theory/arith/row_vector.h"
+
 #include <ext/hash_map>
-#include <map>
 #include <set>
 
 #ifndef __CVC4__THEORY__ARITH__TABLEAU_H
@@ -36,57 +37,6 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-
-class Row {
-  ArithVar d_x_i;
-
-  typedef std::map<ArithVar, Rational, std::greater<ArithVar> > CoefficientTable;
-
-  CoefficientTable d_coeffs;
-
-public:
-
-  typedef CoefficientTable::iterator iterator;
-
-  /**
-   * Construct a row equal to:
-   *   basic = \sum_{x_i} c_i * x_i
-   */
-  Row(ArithVar basic,
-      const std::vector< Rational >& coefficients,
-      const std::vector< ArithVar >& variables);
-
-
-  iterator begin(){
-    return d_coeffs.begin();
-  }
-
-  iterator end(){
-    return d_coeffs.end();
-  }
-
-  ArithVar basicVar(){
-    return d_x_i;
-  }
-
-  bool has(ArithVar x_j){
-    CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
-    return x_jPos != d_coeffs.end();
-  }
-
-  const Rational& lookup(ArithVar x_j){
-    CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
-    Assert(x_jPos !=  d_coeffs.end());
-    return (*x_jPos).second;
-  }
-
-  void pivot(ArithVar x_j);
-
-  void substitute(Row& row_s);
-
-  void printRow();
-};
-
 class ArithVarSet {
 private:
   typedef std::list<ArithVar> VarList;
@@ -138,7 +88,7 @@ private:
 class Tableau {
 private:
 
-  typedef std::vector< Row* > RowsTable;
+  typedef std::vector< ReducedRowVector* > RowsTable;
 
   ArithVarSet d_activeBasicVars;
   RowsTable d_rowsTable;
@@ -171,19 +121,21 @@ public:
     return d_activeBasicVars.end();
   }
 
-  Row* lookup(ArithVar var){
+  ReducedRowVector* lookup(ArithVar var){
     Assert(isActiveBasicVariable(var));
     return d_rowsTable[var];
   }
 
 private:
-  Row* lookupEjected(ArithVar var){
+  ReducedRowVector* lookupEjected(ArithVar var){
     Assert(isEjected(var));
     return d_rowsTable[var];
   }
 public:
 
-  void addRow(ArithVar basicVar, const std::vector<Rational>& coeffs, const std::vector<ArithVar>& variables);
+  void addRow(ArithVar basicVar,
+              const std::vector<Rational>& coeffs,
+              const std::vector<ArithVar>& variables);
 
   /**
    * preconditions:
@@ -210,7 +162,7 @@ public:
     Assert(d_basicManager.isMember(basic));
     Assert(isEjected(basic));
 
-    Row* row = lookupEjected(basic);
+    ReducedRowVector* row = lookupEjected(basic);
     d_activeBasicVars.insert(basic);
     updateRow(row);
   }
@@ -219,7 +171,7 @@ private:
     return d_activeBasicVars.inSet(var);
   }
 
-  void updateRow(Row* row);
+  void updateRow(ReducedRowVector* row);
 };
 
 }; /* namespace arith  */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index bd686737a..6efffa21c 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -104,28 +104,6 @@ TheoryArith::Statistics::~Statistics(){
 }
 
 
-bool isBasicSum(TNode n){
-  if(n.getKind() != kind::PLUS) return false;
-
-  for(TNode::const_iterator i=n.begin(); i!=n.end(); ++i){
-    TNode child = *i;
-    if(child.getKind() != MULT) return false;
-    if(child[0].getKind() != CONST_RATIONAL) return false;
-    for(unsigned j=1; j<child.getNumChildren(); ++j){
-      TNode var = child[j];
-      if(var.getMetaKind() != metakind::VARIABLE) return false;
-    }
-  }
-  return true;
-}
-
-bool isNormalAtom(TNode n){
-
-  Comparison parse = Comparison::parseNormalForm(n);
-
-  return parse.isNormalForm();
-}
-
 
 bool TheoryArith::shouldEject(ArithVar var){
   if(d_partialModel.hasEitherBound(var)){
@@ -145,7 +123,7 @@ ArithVar TheoryArith::findBasicRow(ArithVar variable){
       basicIter != d_tableau.end();
       ++basicIter){
     ArithVar x_j = *basicIter;
-    Row* row_j = d_tableau.lookup(x_j);
+    ReducedRowVector* row_j = d_tableau.lookup(x_j);
 
     if(row_j->has(variable)){
       return x_j;
@@ -208,7 +186,7 @@ void TheoryArith::preRegisterTerm(TNode n) {
 
   //TODO is an atom
   if(isRelationOperator(k)){
-    Assert(isNormalAtom(n));
+    Assert(Comparison::isNormalAtom(n));
 
 
     d_propagator.addAtom(n);
@@ -331,10 +309,12 @@ DeltaRational TheoryArith::computeRowValue(ArithVar x, bool useSafe){
   Assert(d_basicManager.isMember(x));
   DeltaRational sum = d_constants.d_ZERO_DELTA;
 
-  Row* row = d_tableau.lookup(x);
-  for(Row::iterator i = row->begin(); i != row->end();++i){
-    ArithVar nonbasic = i->first;
-    const Rational& coeff = i->second;
+  ReducedRowVector* row = d_tableau.lookup(x);
+  for(ReducedRowVector::NonZeroIterator i = row->beginNonZero(), end = row->endNonZero();
+      i != end;++i){
+    ArithVar nonbasic = getArithVar(*i);
+    if(nonbasic == row->basic()) continue;
+    const Rational& coeff = getCoefficient(*i);
 
     const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe);
     sum = sum + (assignment * coeff);
@@ -484,7 +464,7 @@ void TheoryArith::update(ArithVar x_i, const DeltaRational& v){
       basicIter != d_tableau.end();
       ++basicIter){
     ArithVar x_j = *basicIter;
-    Row* row_j = d_tableau.lookup(x_j);
+    ReducedRowVector* row_j = d_tableau.lookup(x_j);
 
     if(row_j->has(x_i)){
       const Rational& a_ji = row_j->lookup(x_i);
@@ -509,7 +489,7 @@ void TheoryArith::update(ArithVar x_i, const DeltaRational& v){
 void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
   Assert(x_i != x_j);
 
-  Row* row_i = d_tableau.lookup(x_i);
+  ReducedRowVector* row_i = d_tableau.lookup(x_i);
   const Rational& a_ij = row_i->lookup(x_j);
 
 
@@ -528,7 +508,7 @@ void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
       basicIter != d_tableau.end();
       ++basicIter){
     ArithVar x_k = *basicIter;
-    Row* row_k = d_tableau.lookup(x_k);
+    ReducedRowVector* row_k = d_tableau.lookup(x_k);
 
     if(x_k != x_i && row_k->has(x_j)){
       const Rational& a_kj = row_k->lookup(x_j);
@@ -585,10 +565,13 @@ ArithVar TheoryArith::selectSmallestInconsistentVar(){
 
 template <bool above>
 ArithVar TheoryArith::selectSlack(ArithVar x_i){
-   Row* row_i = d_tableau.lookup(x_i);
+  ReducedRowVector* row_i = d_tableau.lookup(x_i);
+
+  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero();
+      nbi != end; ++nbi){
+    ArithVar nonbasic = getArithVar(*nbi);
+    if(nonbasic == x_i) continue;
 
-  for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
-    ArithVar nonbasic = nbi->first;
     const Rational& a_ij = nbi->second;
     int cmp = a_ij.cmp(d_constants.d_ZERO);
     if(above){ // beta(x_i) > u_i
@@ -653,7 +636,7 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
 
 Node TheoryArith::generateConflictAbove(ArithVar conflictVar){
 
-  Row* row_i = d_tableau.lookup(conflictVar);
+  ReducedRowVector* row_i = d_tableau.lookup(conflictVar);
 
   NodeBuilder<> nb(kind::AND);
   TNode bound = d_partialModel.getUpperConstraint(conflictVar);
@@ -665,8 +648,11 @@ Node TheoryArith::generateConflictAbove(ArithVar conflictVar){
 
   nb << bound;
 
-  for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
-    ArithVar nonbasic = nbi->first;
+  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero();
+      nbi != end; ++nbi){
+    ArithVar nonbasic = getArithVar(*nbi);
+    if(nonbasic == conflictVar) continue;
+
     const Rational& a_ij = nbi->second;
 
     Assert(a_ij != d_constants.d_ZERO);
@@ -690,7 +676,7 @@ Node TheoryArith::generateConflictAbove(ArithVar conflictVar){
 }
 
 Node TheoryArith::generateConflictBelow(ArithVar conflictVar){
-  Row* row_i = d_tableau.lookup(conflictVar);
+  ReducedRowVector* row_i = d_tableau.lookup(conflictVar);
 
   NodeBuilder<> nb(kind::AND);
   TNode bound = d_partialModel.getLowerConstraint(conflictVar);
@@ -701,8 +687,10 @@ Node TheoryArith::generateConflictBelow(ArithVar conflictVar){
                  << " " << bound << endl;
   nb << bound;
 
-  for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
-    ArithVar nonbasic = nbi->first;
+  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){
+    ArithVar nonbasic = getArithVar(*nbi);
+    if(nonbasic != conflictVar) continue;
+
     const Rational& a_ij = nbi->second;
 
     Assert(a_ij != d_constants.d_ZERO);
@@ -867,13 +855,15 @@ void TheoryArith::checkTableau(){
   for(ArithVarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end(); ++basicIter){
     ArithVar basic = *basicIter;
-    Row* row_k = d_tableau.lookup(basic);
+    ReducedRowVector* row_k = d_tableau.lookup(basic);
     DeltaRational sum;
     Debug("paranoid:check_tableau") << "starting row" << basic << endl;
-    for(Row::iterator nonbasicIter = row_k->begin();
-        nonbasicIter != row_k->end();
+    for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k->beginNonZero();
+        nonbasicIter != row_k->endNonZero();
         ++nonbasicIter){
       ArithVar nonbasic = nonbasicIter->first;
+      if(basic == nonbasic) continue;
+
       const Rational& coeff = nonbasicIter->second;
       DeltaRational beta = d_partialModel.getAssignment(nonbasic);
       Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl;