Merged the branch sparse-tableau into trunk.

11 files changed, 1019 insertions, 919 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 2c00f5d4d..12088b493 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -26,8 +26,6 @@ libarith_la_SOURCES = \
 	arith_priority_queue.cpp \
 	simplex.h \
 	simplex.cpp \
-	row_vector.h \
-	row_vector.cpp \
 	unate_propagator.h \
 	unate_propagator.cpp \
 	theory_arith.h \
diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
index 89b1c9507..0d59e3aea 100644
--- a/src/theory/arith/arithvar_set.h
+++ b/src/theory/arith/arithvar_set.h
@@ -57,7 +57,7 @@ private:
   std::vector<unsigned> d_posVector;
 
 public:
-  typedef VarList::const_iterator iterator;
+  typedef VarList::const_iterator const_iterator;
 
   ArithVarSetImpl() :  d_list(), d_posVector() {}
 
@@ -114,8 +114,8 @@ public:
     d_list.push_back(x);
   }
 
-  iterator begin() const{ return d_list.begin(); }
-  iterator end() const{ return d_list.end(); }
+  const_iterator begin() const{ return d_list.begin(); }
+  const_iterator end() const{ return d_list.end(); }
 
   const VarList& getList() const{
     return d_list;
diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
deleted file mode 100644
index 8edfb8612..000000000
--- a/src/theory/arith/row_vector.cpp
+++ /dev/null
@@ -1,316 +0,0 @@
-
-#include "theory/arith/row_vector.h"
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
-
-using namespace std;
-
-bool ReducedRowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) {
-  if(arr.size() >= 2){
-    const_iterator curr = arr.begin();
-    const_iterator end = arr.end();
-    ArithVar prev = (*curr).getArithVar();
-    ++curr;
-    for(;curr != end; ++curr){
-      ArithVar v = (*curr).getArithVar();
-      if(strictlySorted && prev > v) return false;
-      if(!strictlySorted && prev >= v) return false;
-      prev = v;
-    }
-  }
-  return true;
-}
-
-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 = (*curr).getArithVar();
-    Assert(d_rowCount[v] >= 1);
-    d_columnMatrix[v].remove(basic());
-    --(d_rowCount[v]);
-  }
-
-  Assert(matchingCounts());
-}
-
-
-bool ReducedRowVector::matchingCounts() const{
-  for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
-    ArithVar v = (*i).getArithVar();
-    if(d_columnMatrix[v].size() != d_rowCount[v]){
-      return false;
-    }
-  }
-  return true;
-}
-
-bool ReducedRowVector::noZeroCoefficients(const VarCoeffArray& arr){
-  for(const_iterator curr = arr.begin(), endEntries = arr.end();
-      curr != endEntries; ++curr){
-    const Rational& coeff = (*curr).getCoefficient();
-    if(coeff == 0) return false;
-  }
-  return true;
-}
-
-void ReducedRowVector::zip(const std::vector< ArithVar >& variables,
-                           const std::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(VarCoeffPair(var_i, coeff));
-  }
-}
-
-void ReducedRowVector::addArithVar(ArithVarContainsSet& contains, ArithVar v){
-  if(v >= contains.size()){
-    contains.resize(v+1, false);
-  }
-  contains[v] = true;
-}
-
-void ReducedRowVector::removeArithVar(ArithVarContainsSet& contains, ArithVar v){
-  Assert(v < contains.size());
-  Assert(contains[v]);
-  contains[v] = false;
-}
-
-void ReducedRowVector::multiply(const Rational& c){
-  Assert(c != 0);
-
-  for(iterator i = d_entries.begin(), end = d_entries.end(); i != end; ++i){
-    (*i).getCoefficient() *= c;
-  }
-}
-
-void ReducedRowVector::addRowTimesConstant(const Rational& c, const ReducedRowVector& other){
-  Assert(c != 0);
-  Assert(d_buffer.empty());
-  Assert(wellFormed());
-
-  d_buffer.reserve(other.d_entries.size());
-
-  iterator curr1 = d_entries.begin();
-  iterator end1 = d_entries.end();
-
-  const_iterator curr2 = other.d_entries.begin();
-  const_iterator end2 = other.d_entries.end();
-
-  while(curr1 != end1 && curr2 != end2){
-    ArithVar var1 = (*curr1).getArithVar();
-    ArithVar var2 = (*curr2).getArithVar();
-
-    if(var1 < var2){
-      d_buffer.push_back(*curr1);
-      ++curr1;
-    }else if(var1 > var2){
-
-      ++d_rowCount[var2];
-      d_columnMatrix[var2].add(d_basic);
-
-      addArithVar(d_contains, var2);
-      const Rational& coeff2 = (*curr2).getCoefficient();
-      d_buffer.push_back( VarCoeffPair(var2, c * coeff2));
-      ++curr2;
-    }else{
-      Assert(var1 == var2);
-      const Rational& coeff1 = (*curr1).getCoefficient();
-      const Rational& coeff2 = (*curr2).getCoefficient();
-      Rational res = coeff1 + (c * coeff2);
-      if(res != 0){
-        //The variable is not new so the count stays the same
-        d_buffer.push_back(VarCoeffPair(var1, res));
-      }else{
-        removeArithVar(d_contains, var1);
-
-        --d_rowCount[var1];
-        d_columnMatrix[var1].remove(d_basic);
-      }
-      ++curr1;
-      ++curr2;
-    }
-  }
-  while(curr1 != end1){
-    d_buffer.push_back(*curr1);
-    ++curr1;
-  }
-  while(curr2 != end2){
-    ArithVar var2 = (*curr2).getArithVar();
-    const Rational& coeff2 = (*curr2).getCoefficient();
-    ++d_rowCount[var2];
-    d_columnMatrix[var2].add(d_basic);
-
-    addArithVar(d_contains, var2);
-
-    d_buffer.push_back(VarCoeffPair(var2, c * coeff2));
-    ++curr2;
-  }
-
-  d_buffer.swap(d_entries);
-  d_buffer.clear();
-
-  Assert(d_buffer.empty());
-}
-
-void ReducedRowVector::printRow(){
-  for(const_iterator i = begin(); i != end(); ++i){
-    ArithVar nb = (*i).getArithVar();
-    const Rational& coeff = (*i).getCoefficient();
-    Debug("row::print") << "{" << nb << "," << coeff << "}";
-  }
-  Debug("row::print") << std::endl;
-}
-
-
-ReducedRowVector::ReducedRowVector(ArithVar basic,
-                                   const std::vector<ArithVar>& variables,
-                                   const std::vector<Rational>& coefficients,
-                                   std::vector<uint32_t>& counts,
-                                   std::vector<PermissiveBackArithVarSet>& cm):
-  d_basic(basic), d_rowCount(counts),  d_columnMatrix(cm)
-{
-  zip(variables, coefficients, d_entries);
-  d_entries.push_back(VarCoeffPair(basic, Rational(-1)));
-
-  std::sort(d_entries.begin(), d_entries.end());
-
-  for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
-    ArithVar var = (*i).getArithVar();
-    ++d_rowCount[var];
-    addArithVar(d_contains, var);
-    d_columnMatrix[var].add(d_basic);
-  }
-
-  Assert(isSorted(d_entries, true));
-  Assert(noZeroCoefficients(d_entries));
-
-  Assert(matchingCounts());
-  Assert(wellFormed());
-  Assert(d_rowCount[d_basic] == 1);
-}
-
-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());
-  Assert(matchingCounts());
-  Assert(d_rowCount[basic()] == 1);
-}
-
-void ReducedRowVector::pivot(ArithVar x_j){
-  Assert(has(x_j));
-  Assert(basic() != x_j);
-  Rational negInverseA_rs = -(lookup(x_j).inverse());
-  multiply(negInverseA_rs);
-
-  for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
-    ArithVar var = (*i).getArithVar();
-    d_columnMatrix[var].remove(d_basic);
-    d_columnMatrix[var].add(x_j);
-  }
-
-  d_basic = x_j;
-
-  Assert(matchingCounts());
-  Assert(wellFormed());
-  //The invariant Assert(d_rowCount[basic()] == 1); does not hold.
-  //This is because the pivot is within the row first then
-  //is moved through the propagated through the rest of the tableau.
-}
-
-
-Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{
-  using namespace CVC4::kind;
-
-  Assert(size() >= 2);
-
-  vector<Node> nonBasicPairs;
-  for(const_iterator i = begin(); i != end(); ++i){
-    ArithVar nb = (*i).getArithVar();
-    if(nb == basic()) continue;
-    Node var = (map.find(nb))->second;
-    Node coeff = mkRationalNode((*i).getCoefficient());
-
-    Node mult = NodeBuilder<2>(MULT) << coeff << var;
-    nonBasicPairs.push_back(mult);
-  }
-
-  Node sum = Node::null();
-  if(nonBasicPairs.size() == 1 ){
-    sum = nonBasicPairs.front();
-  }else{
-    Assert(nonBasicPairs.size() >= 2);
-    NodeBuilder<> sumBuilder(PLUS);
-    sumBuilder.append(nonBasicPairs);
-    sum = sumBuilder;
-  }
-  Node basicVar = (map.find(basic()))->second;
-  return NodeBuilder<2>(EQUAL) << basicVar << sum;
-
-  /*
-  Node sum = Node::null();
-  if(size() > 2){
-    NodeBuilder<> sumBuilder(PLUS);
-
-    for(const_iterator i = begin(); i != end(); ++i){
-      ArithVar nb = (*i).getArithVar();
-      if(nb == basic()) continue;
-      Node var = (map.find(nb))->second;
-      Node coeff = mkRationalNode((*i).getCoefficient());
-
-      Node mult = NodeBuilder<2>(MULT) << coeff << var;
-      sumBuilder << mult;
-    }
-    sum = sumBuilder;
-  }else{
-    Assert(size() == 2);
-    const_iterator i = begin();
-    if((*i).getArithVar() == basic()){
-      ++i;
-    }
-    Assert((*i).getArithVar() != basic());
-    Node var = (map.find((*i).getArithVar()))->second;
-    Node coeff = mkRationalNode((*i).getCoefficient());
-    sum = NodeBuilder<2>(MULT) << coeff << var;
-  }
-  Node basicVar = (map.find(basic()))->second;
-  return NodeBuilder<2>(EQUAL) << basicVar << sum;
-*/
-}
-
-void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,std::vector< Rational >& coefficients) const{
-  for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
-    ArithVar var = (*i).getArithVar();
-    const Rational& q = (*i).getCoefficient();
-    if(var != basic()){
-      variables.push_back(var);
-      coefficients.push_back(q);
-    }
-  }
-}
diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
deleted file mode 100644
index 5fd471700..000000000
--- a/src/theory/arith/row_vector.h
+++ /dev/null
@@ -1,233 +0,0 @@
-
-
-#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 "theory/arith/arithvar_set.h"
-#include "util/rational.h"
-#include <vector>
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class VarCoeffPair {
-private:
-  ArithVar d_variable;
-  Rational d_coeff;
-
-public:
-  VarCoeffPair(ArithVar v, const Rational& q): d_variable(v), d_coeff(q) {}
-
-  ArithVar getArithVar() const { return d_variable; }
-  Rational& getCoefficient() { return d_coeff; }
-  const Rational& getCoefficient() const { return d_coeff; }
-
-  bool operator<(const VarCoeffPair& other) const{
-    return getArithVar() < other.getArithVar();
-  }
-
-  static bool variableLess(const VarCoeffPair& a, const VarCoeffPair& b){
-    return a < b;
-  }
-};
-
-/**
- * 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 ReducedRowVector {
-public:
-  typedef std::vector<VarCoeffPair> VarCoeffArray;
-  typedef VarCoeffArray::const_iterator const_iterator;
-
-private:
-  typedef std::vector<bool> ArithVarContainsSet;
-  typedef VarCoeffArray::iterator iterator;
-
-  /**
-   * Invariants:
-   * - isSorted(d_entries, true)
-   * - noZeroCoefficients(d_entries)
-   */
-  VarCoeffArray d_entries;
-
-  /**
-   * Buffer for d_entries to reduce allocations by addRowTimesConstant.
-   */
-  VarCoeffArray d_buffer;
-
-  /**
-   * 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.
-   */
-  ArithVarContainsSet d_contains;
-
-  std::vector<uint32_t>& d_rowCount;
-  std::vector<PermissiveBackArithVarSet>& d_columnMatrix;
-
-
-public:
-
-  ReducedRowVector(ArithVar basic,
-                   const std::vector< ArithVar >& variables,
-                   const std::vector< Rational >& coefficients,
-                   std::vector<uint32_t>& count,
-                   std::vector< PermissiveBackArithVarSet >& columnMatrix);
-  ~ReducedRowVector();
-
-  void enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,
-                                               std::vector< Rational >& coefficients) const;
-
-  /** Returns the basic variable.*/
-  ArithVar basic() const{
-    Assert(basicIsSet());
-    return d_basic;
-  }
-
-  /** Returns the number of nonzero variables in the vector. */
-  uint32_t size() const {
-    return d_entries.size();
-  }
-
-  /** Iterates over the nonzero entries in the vector. */
-  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{
-    if(x_j >= d_contains.size()){
-      return false;
-    }else{
-      return d_contains[x_j];
-    }
-  }
-
-  /**
-   * Returns the coefficient of a variable in the row.
-   */
-  const Rational& lookup(ArithVar x_j) const{
-    Assert(has(x_j));
-    Assert(hasInEntries(x_j));
-    const_iterator lb = lower_bound(x_j);
-    return (*lb).getCoefficient();
-  }
-
-
-  /** Prints the row to the buffer Debug("row::print"). */
-  void printRow();
-
-  /**
-   * Changes the basic variable to x_j.
-   * Precondition: has(x_j)
-   */
-  void pivot(ArithVar x_j);
-
-  /**
-   * Replaces other.basic() in the current row using the other row.
-   * This assumes the other row represents an equality equal to zero.
-   *
-   *   \sum(this->entries) -= this->lookup(other.basic()) * (\sum(other.d_entries))
-   * Precondition:
-   *  has(other.basic())
-   *  basic != other.basic()
-   */
-  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:
-
-  /**
-   * \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 ReducedRowVector& other);
-
-
-  /** Multiplies the coefficients of the RowVector by c (where c != 0). */
-  void multiply(const Rational& c);
-
-  /**
-   * Adds v to d_contains.
-   * This may resize d_contains.
-   */
-  static void addArithVar(ArithVarContainsSet& contains, ArithVar v);
-
-  /** Removes v from d_contains. */
-  static void removeArithVar(ArithVarContainsSet& contains, ArithVar v);
-
-
-  /**
-   * 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);
-
-  /**
-   * 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(), VarCoeffPair(x_j, 0));
-  }
-
-  /** Debugging code */
-  bool wellFormed() const{
-    return
-      isSorted(d_entries, true) &&
-      noZeroCoefficients(d_entries) &&
-      basicIsSet() &&
-      has(basic()) &&
-      lookup(basic()) == Rational(-1);
-  }
-
-  bool basicIsSet() const { return d_basic != ARITHVAR_SENTINEL; }
-
-  /** Debugging code. */
-  bool hasInEntries(ArithVar x_j) const {
-    return std::binary_search(d_entries.begin(), d_entries.end(), VarCoeffPair(x_j,0));
-  }
-
-}; /* class ReducedRowVector */
-
-
-}/* namespace CVC4::theory::arith */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
-
-#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 6e73ca999..1a9c39984 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -209,36 +209,38 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
   return Node::null();
 }
 
-set<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){
-  set<ArithVar> has;
-  for(ArithVarSet::iterator basicIter = tab.begin();
-      basicIter != tab.end();
-      ++basicIter){
-    ArithVar basic = *basicIter;
-    ReducedRowVector& row = tab.lookup(basic);
-
-    if(row.has(v)){
-      has.insert(basic);
-    }
-  }
-  return has;
-}
-
-set<ArithVar> columnIteratorSet(Tableau& tab,ArithVar v){
-  set<ArithVar> has;
-  Column::iterator basicIter = tab.beginColumn(v);
-  Column::iterator endIter = tab.endColumn(v);
-  for(; basicIter != endIter; ++basicIter){
-    ArithVar basic = *basicIter;
-    has.insert(basic);
-  }
-  return has;
-}
-
-
+// set<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){
+//   set<ArithVar> has;
+//   for(ArithVarSet::const_iterator basicIter = tab.beginBasic();
+//       basicIter != tab.endBasic();
+//       ++basicIter){
+//     ArithVar basic = *basicIter;
+//     ReducedRowVector& row = tab.lookup(basic);
+
+//     if(row.has(v)){
+//       has.insert(basic);
+//     }
+//   }
+//   return has;
+// }
+
+// set<ArithVar> columnIteratorSet(Tableau& tab,ArithVar v){
+//   set<ArithVar> has;
+//   Column::iterator basicIter = tab.beginColumn(v);
+//   Column::iterator endIter = tab.endColumn(v);
+//   for(; basicIter != endIter; ++basicIter){
+//     ArithVar basic = *basicIter;
+//     has.insert(basic);
+//   }
+//   return has;
+// }
+
+
+/*
 bool matchingSets(Tableau& tab, ArithVar v){
   return tableauAndHasSet(tab, v) == columnIteratorSet(tab, v);
 }
+*/
 
 void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
   Assert(!d_tableau.isBasic(x_i));
@@ -249,15 +251,17 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
                  << assignment_x_i << "|-> " << v << endl;
   DeltaRational diff = v - assignment_x_i;
 
-  Assert(matchingSets(d_tableau, x_i));
-  Column::iterator basicIter = d_tableau.beginColumn(x_i);
-  Column::iterator endIter   = d_tableau.endColumn(x_i);
-  for(; basicIter != endIter; ++basicIter){
-    ArithVar x_j = *basicIter;
-    ReducedRowVector& row_j = d_tableau.lookup(x_j);
+  //Assert(matchingSets(d_tableau, x_i));
+  Tableau::ColIterator basicIter = d_tableau.colIterator(x_i);
+  for(; !basicIter.atEnd(); ++basicIter){
+    const TableauEntry& entry = *basicIter;
+    Assert(entry.getColVar() == x_i);
+
+    ArithVar x_j = entry.getRowVar();
+    //ReducedRowVector& row_j = d_tableau.lookup(x_j);
 
-    Assert(row_j.has(x_i));
-    const Rational& a_ji = row_j.lookup(x_i);
+    //const Rational& a_ji = row_j.lookup(x_i);
+    const Rational& a_ji = entry.getCoefficient();
 
     const DeltaRational& assignment = d_partialModel.getAssignment(x_j);
     DeltaRational  nAssignment = assignment+(diff * a_ji);
@@ -268,13 +272,34 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
 
   d_partialModel.setAssignment(x_i, v);
 
-  Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_i));
-  double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_i));
+  Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_i));
+  double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_i));
 
   (d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference);
-  if(Debug.isOn("paranoid:check_tableau")){
-    checkTableau();
+  if(Debug.isOn("paranoid:check_tableau")){  debugCheckTableau(); }
+}
+
+void SimplexDecisionProcedure::debugPivotSimplex(ArithVar x_i, ArithVar x_j){
+  Debug("arith::simplex:row") << "debugRowSimplex("
+                              << x_i  << "|->" << x_j
+                              << ")" << endl;
+
+  for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){
+    const TableauEntry& entry = *iter;
+
+    ArithVar var = entry.getColVar();
+    const Rational& coeff = entry.getCoefficient();
+    DeltaRational beta = d_partialModel.getAssignment(var);
+    Debug("arith::simplex:row") << var << beta << coeff;
+    if(d_partialModel.hasLowerBound(var)){
+      Debug("arith::simplex:row") << "(lb " << d_partialModel.getLowerBound(var) << ")";
+    }
+    if(d_partialModel.hasUpperBound(var)){
+      Debug("arith::simplex:row") << "(up " << d_partialModel.getUpperBound(var) << ")";
+    }
+    Debug("arith::simplex:row") << endl;
   }
+  Debug("arith::simplex:row") << "end row"<< endl;
 }
 
 void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
@@ -282,32 +307,13 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
 
   TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
 
-  if(Debug.isOn("arith::pivotAndUpdate")){
-    Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl;
-    ReducedRowVector& row_k = d_tableau.lookup(x_i);
-    for(ReducedRowVector::const_iterator varIter = row_k.begin();
-        varIter != row_k.end();
-        ++varIter){
-
-      ArithVar var = (*varIter).getArithVar();
-      const Rational& coeff = (*varIter).getCoefficient();
-      DeltaRational beta = d_partialModel.getAssignment(var);
-      Debug("arith::pivotAndUpdate") << var << beta << coeff;
-      if(d_partialModel.hasLowerBound(var)){
-        Debug("arith::pivotAndUpdate") << "(lb " << d_partialModel.getLowerBound(var) << ")";
-      }
-      if(d_partialModel.hasUpperBound(var)){
-        Debug("arith::pivotAndUpdate") << "(up " << d_partialModel.getUpperBound(var)
-                                       << ")";
-      }
-      Debug("arith::pivotAndUpdate") << endl;
-    }
-    Debug("arith::pivotAndUpdate") << "end row"<< endl;
-  }
+  if(Debug.isOn("arith::simplex:row")){ debugPivotSimplex(x_i, x_j); }
+
+  const TableauEntry& entry_ij =  d_tableau.findEntry(x_i, x_j);
+  Assert(!entry_ij.blank());
 
 
-  ReducedRowVector& row_i = d_tableau.lookup(x_i);
-  const Rational& a_ij = row_i.lookup(x_j);
+  const Rational& a_ij = entry_ij.getCoefficient();
 
 
   const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i);
@@ -322,16 +328,13 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
   d_partialModel.setAssignment(x_j, tmp);
 
 
-  Assert(matchingSets(d_tableau, x_j));
-  Column::iterator basicIter = d_tableau.beginColumn(x_j);
-  Column::iterator endIter   = d_tableau.endColumn(x_j);
-  for(; basicIter != endIter; ++basicIter){
-    ArithVar x_k = *basicIter;
-    ReducedRowVector& row_k = d_tableau.lookup(x_k);
-
-    Assert(row_k.has(x_j));
+  //Assert(matchingSets(d_tableau, x_j));
+  for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){
+    const TableauEntry& entry = *iter;
+    Assert(entry.getColVar() == x_j);
+    ArithVar x_k = entry.getRowVar();
     if(x_k != x_i ){
-      const Rational& a_kj = row_k.lookup(x_j);
+      const Rational& a_kj = entry.getCoefficient();
       DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
       d_partialModel.setAssignment(x_k, nextAssignment);
 
@@ -342,8 +345,8 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
   // Pivots
   ++(d_statistics.d_statPivots);
 
-  Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_j));
-  double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_j));
+  Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_j));
+  double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_j));
   (d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference);
   d_tableau.pivot(x_i, x_j);
 
@@ -367,14 +370,18 @@ ArithVar SimplexDecisionProcedure::minVarOrder(const SimplexDecisionProcedure& s
   }
 }
 
-ArithVar SimplexDecisionProcedure::minRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){
+ArithVar SimplexDecisionProcedure::minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){
   Assert(x != ARITHVAR_SENTINEL);
   Assert(y != ARITHVAR_SENTINEL);
   Assert(!simp.d_tableau.isBasic(x));
   Assert(!simp.d_tableau.isBasic(y));
-  if(simp.d_tableau.getRowCount(x) > simp.d_tableau.getRowCount(y)){
-    return y;
-  } else {
+  uint32_t xLen = simp.d_tableau.getColLength(x);
+  uint32_t yLen = simp.d_tableau.getColLength(y);
+  if( xLen > yLen){
+     return y;
+  } else if( xLen== yLen ){
+    return minVarOrder(simp,x,y);
+  }else{
     return x;
   }
 }
@@ -389,27 +396,22 @@ ArithVar SimplexDecisionProcedure::minBoundAndRowCount(const SimplexDecisionProc
   }else if(!simp.d_partialModel.hasEitherBound(x) && simp.d_partialModel.hasEitherBound(y)){
     return x;
   }else {
-    return minRowCount(simp, x, y);
+    return minColLength(simp, x, y);
   }
 }
 
 template <bool above, SimplexDecisionProcedure::PreferenceFunction pref>
 ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
-  ReducedRowVector& row_i = d_tableau.lookup(x_i);
-
   ArithVar slack = ARITHVAR_SENTINEL;
 
-  for(ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
-      nbi != end; ++nbi){
-    ArithVar nonbasic = (*nbi).getArithVar();
+  for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd();  ++iter){
+    const TableauEntry& entry = *iter;
+    ArithVar nonbasic = entry.getColVar();
     if(nonbasic == x_i) continue;
 
-    const Rational& a_ij = (*nbi).getCoefficient();
+    const Rational& a_ij = entry.getCoefficient();
     int sgn = a_ij.sgn();
-    if(( above && sgn < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
-       ( above && sgn > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)) ||
-       (!above && sgn > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
-       (!above && sgn < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic))) {
+    if(isAcceptableSlack<above>(sgn, nonbasic)){
       //If one of the above conditions is met, we have found an acceptable
       //nonbasic variable to pivot x_i with.  We can now choose which one we
       //prefer the most.
@@ -563,7 +565,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
   Assert(remainingIterations > 0);
 
   while(remainingIterations > 0){
-    if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
+    if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); }
 
     ArithVar x_i = d_queue.dequeueInconsistentBasicVariable();
     Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
@@ -612,8 +614,6 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
 
 Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
 
-  ReducedRowVector& row_i = d_tableau.lookup(conflictVar);
-
   NodeBuilder<> nb(kind::AND);
   TNode bound = d_partialModel.getUpperConstraint(conflictVar);
 
@@ -624,13 +624,13 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
 
   nb << bound;
 
-  ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
-
-  for(; nbi != end; ++nbi){
-    ArithVar nonbasic = (*nbi).getArithVar();
+  Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar);
+  for(; !iter.atEnd(); ++iter){
+    const TableauEntry& entry = *iter;
+    ArithVar nonbasic = entry.getColVar();
     if(nonbasic == conflictVar) continue;
 
-    const Rational& a_ij = (*nbi).getCoefficient();
+    const Rational& a_ij = entry.getCoefficient();
     Assert(a_ij != d_ZERO);
 
     int sgn = a_ij.sgn();
@@ -655,8 +655,6 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
 }
 
 Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
-  ReducedRowVector& row_i = d_tableau.lookup(conflictVar);
-
   NodeBuilder<> nb(kind::AND);
   TNode bound = d_partialModel.getLowerConstraint(conflictVar);
 
@@ -667,12 +665,13 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
   nb << bound;
 
 
-  ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
-  for(; nbi != end; ++nbi){
-    ArithVar nonbasic = (*nbi).getArithVar();
+  Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar);
+  for(; !iter.atEnd(); ++iter){
+    const TableauEntry& entry = *iter;
+    ArithVar nonbasic = entry.getColVar();
     if(nonbasic == conflictVar) continue;
 
-    const Rational& a_ij = (*nbi).getCoefficient();
+    const Rational& a_ij = entry.getCoefficient();
 
     int sgn = a_ij.sgn();
     Assert(a_ij != d_ZERO);
@@ -706,12 +705,11 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe
   Assert(d_tableau.isBasic(x));
   DeltaRational sum(0);
 
-  ReducedRowVector& row = d_tableau.lookup(x);
-  for(ReducedRowVector::const_iterator i = row.begin(), end = row.end();
-      i != end;++i){
-    ArithVar nonbasic = (*i).getArithVar();
-    if(nonbasic == row.basic()) continue;
-    const Rational& coeff = (*i).getCoefficient();
+  for(Tableau::RowIterator i = d_tableau.rowIterator(x); !i.atEnd(); ++i){
+    const TableauEntry& entry = (*i);
+    ArithVar nonbasic = entry.getColVar();
+    if(nonbasic == x) continue;
+    const Rational& coeff = entry.getCoefficient();
 
     const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe);
     sum = sum + (assignment * coeff);
@@ -726,21 +724,20 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe
  *      checkTableau();
  *   }
  */
-void SimplexDecisionProcedure::checkTableau(){
-
-  for(ArithVarSet::iterator basicIter = d_tableau.begin();
-      basicIter != d_tableau.end(); ++basicIter){
+void SimplexDecisionProcedure::debugCheckTableau(){
+  ArithVarSet::const_iterator basicIter = d_tableau.beginBasic();
+  ArithVarSet::const_iterator endIter = d_tableau.endBasic();
+  for(; basicIter != endIter; ++basicIter){
     ArithVar basic = *basicIter;
-    ReducedRowVector& row_k = d_tableau.lookup(basic);
     DeltaRational sum;
     Debug("paranoid:check_tableau") << "starting row" << basic << endl;
-    for(ReducedRowVector::const_iterator nonbasicIter = row_k.begin();
-        nonbasicIter != row_k.end();
-        ++nonbasicIter){
-      ArithVar nonbasic = (*nonbasicIter).getArithVar();
+    Tableau::RowIterator nonbasicIter = d_tableau.rowIterator(basic);
+    for(; !nonbasicIter.atEnd(); ++nonbasicIter){
+      const TableauEntry& entry = *nonbasicIter;
+      ArithVar nonbasic = entry.getColVar();
       if(basic == nonbasic) continue;
 
-      const Rational& coeff = (*nonbasicIter).getCoefficient();
+      const Rational& coeff = entry.getCoefficient();
       DeltaRational beta = d_partialModel.getAssignment(nonbasic);
       Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl;
       sum = sum + (beta*coeff);
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 93574b3da..91f0bccfc 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -107,7 +107,7 @@ private:
    * This is a hueristic rule and should not be used
    * during the VarOrder stage of updateInconsistentVars.
    */
-  static ArithVar minRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
+  static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
   /**
    * minBoundAndRowCount is a PreferenceFunction for preferring a variable
    * without an asserted bound over variables with an asserted bound.
@@ -201,7 +201,9 @@ public:
    * Checks to make sure the assignment is consistent with the tableau.
    * This code is for debugging.
    */
-  void checkTableau();
+  void debugCheckTableau();
+  void debugPivotSimplex(ArithVar x_i, ArithVar x_j);
+
 
   /**
    * Computes the value of a basic variable using the assignments
@@ -240,6 +242,15 @@ private:
     pushLemma(negatedConflict);
   }
 
+  template <bool above>
+  inline bool isAcceptableSlack(int sgn, ArithVar nonbasic){
+    return
+      ( above && sgn < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
+      ( above && sgn > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)) ||
+      (!above && sgn > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
+      (!above && sgn < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic));
+  }
+
   /**
    * Checks a basic variable, b, to see if it is in conflict.
    * If a conflict is discovered a node summarizing the conflict is returned.
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index cb1364488..367e90301 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -26,80 +26,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
 
-Tableau::Tableau(const Tableau& tab){
-  internalCopy(tab);
-}
-
-void Tableau::internalCopy(const Tableau& tab){
-  uint32_t N = tab.d_rowsTable.size();
-
-  Debug("tableau::copy") << "tableau copy "<< N << endl;
-
-  if(N > 1){
-    d_columnMatrix.insert(d_columnMatrix.end(), N, Column());
-    d_rowsTable.insert(d_rowsTable.end(), N, NULL);
-    d_basicVariables.increaseSize(N-1);
-
-    Assert(d_basicVariables.allocated() == tab.d_basicVariables.allocated());
-
-    d_rowCount.insert(d_rowCount.end(), N, 0);
-  }
-
-  ColumnMatrix::const_iterator otherIter = tab.d_columnMatrix.begin();
-  ColumnMatrix::iterator i_colIter = d_columnMatrix.begin();
-  ColumnMatrix::iterator end_colIter = d_columnMatrix.end();
-  for(; i_colIter != end_colIter; ++i_colIter, ++otherIter){
-    Assert(otherIter != tab.d_columnMatrix.end());
-    Column& col = *i_colIter;
-    const Column& otherCol = *otherIter;
-    col.increaseSize(otherCol.allocated());
-  }
-
-  ArithVarSet::iterator i_basicIter = tab.d_basicVariables.begin();
-  ArithVarSet::iterator i_basicEnd = tab.d_basicVariables.end();
-  for(; i_basicIter != i_basicEnd; ++i_basicIter){
-    ArithVar basicVar = *i_basicIter;
-    const ReducedRowVector* otherRow = tab.d_rowsTable[basicVar];
-
-    Assert(otherRow != NULL);
-
-    std::vector< ArithVar > variables;
-    std::vector< Rational > coefficients;
-    otherRow->enqueueNonBasicVariablesAndCoefficients(variables, coefficients);
-
-    ReducedRowVector* copy = new ReducedRowVector(basicVar, variables, coefficients, d_rowCount, d_columnMatrix);
-
-    Debug("tableau::copy") << "copying " << basicVar << endl;
-    copy->printRow();
-
-    d_basicVariables.add(basicVar);
-    d_rowsTable[basicVar] = copy;
-  }
-}
-
-Tableau& Tableau::operator=(const Tableau& other){
-  clear();
-  internalCopy(other);
-  return (*this);
-}
-
-Tableau::~Tableau(){
-  clear();
-}
-
-void Tableau::clear(){
-  while(!d_basicVariables.empty()){
-    ArithVar curr = *(d_basicVariables.begin());
-    ReducedRowVector* vec = removeRow(curr);
-    delete vec;
-  }
-
-  d_rowsTable.clear();
-  d_basicVariables.clear();
-  d_rowCount.clear();
-  d_columnMatrix.clear();
-}
-
+/*
 void Tableau::addRow(ArithVar basicVar,
                      const std::vector<Rational>& coeffs,
                      const std::vector<ArithVar>& variables){
@@ -121,14 +48,21 @@ void Tableau::addRow(ArithVar basicVar,
     ArithVar var = *varsIter;
 
     if(d_basicVariables.isMember(var)){
-      ReducedRowVector& row_var = lookup(var);
-      row_current->substitute(row_var);
+      EntryID varID = find(basicVar, var);
+      TableauEntry& entry = d_entryManager.get(varID);
+      const Rational& coeff = entry.getCoefficient();
+
+      loadRowIntoMergeBuffer(var);
+      rowPlusRowTimesConstant(coeff, basicVar, var);
+      emptyRowFromMergeBuffer(var);
     }
   }
 }
+*/
 
+/*
 ReducedRowVector* Tableau::removeRow(ArithVar basic){
-  Assert(d_basicVariables.isMember(basic));
+  Assert(isBasic(basic));
 
   ReducedRowVector* row = d_rowsTable[basic];
 
@@ -137,73 +71,502 @@ ReducedRowVector* Tableau::removeRow(ArithVar basic){
 
   return row;
 }
+*/
 
-void Tableau::pivot(ArithVar x_r, ArithVar x_s){
-  Assert(d_basicVariables.isMember(x_r));
-  Assert(!d_basicVariables.isMember(x_s));
+void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic){
+  Assert(isBasic(oldBasic));
+  Assert(!isBasic(newBasic));
+  Assert(mergeBufferIsEmpty());
 
-  Debug("tableau") << "Tableau::pivot(" <<  x_r <<", " <<x_s <<")"  << endl;
+  //cout << oldBasic << "," << newBasic << endl;
+  Debug("tableau") << "Tableau::pivot(" <<  oldBasic <<", " << newBasic <<")"  << endl;
 
-  ReducedRowVector* row_s = d_rowsTable[x_r];
-  Assert(row_s != NULL);
-  Assert(row_s->has(x_s));
+  rowPivot(oldBasic, newBasic);
+  loadRowIntoMergeBuffer(newBasic);
 
-  //Swap x_r and x_s in d_activeRows
-  d_rowsTable[x_s] = row_s;
-  d_rowsTable[x_r] = NULL;
+  ColIterator colIter = colIterator(newBasic);
+  while(!colIter.atEnd()){
+    EntryID id = colIter.getID();
+    TableauEntry& entry = d_entryManager.get(id);
 
-  d_basicVariables.remove(x_r);
+    ++colIter; //needs to be incremented before the variable is removed
+    if(entry.getRowVar() == newBasic){ continue; }
 
-  d_basicVariables.add(x_s);
+    ArithVar basicTo = entry.getRowVar();
+    Rational coeff = entry.getCoefficient();
 
-  row_s->pivot(x_s);
+    rowPlusRowTimesConstant(basicTo, coeff, newBasic);
+  }
+  emptyRowFromMergeBuffer(newBasic);
 
-  Column::VarList copy(getColumn(x_s).getList());
-  vector<ArithVar>::iterator basicIter = copy.begin(), endIter = copy.end();
+  //Clear the column for used for this variable
 
-  for(; basicIter != endIter; ++basicIter){
-    ArithVar basic = *basicIter;
-    if(basic == x_s) continue;
+  Assert(mergeBufferIsEmpty());
+  Assert(!isBasic(oldBasic));
+  Assert(isBasic(newBasic));
+  Assert(getColLength(newBasic) == 1);
+}
 
-    ReducedRowVector& row_k = lookup(basic);
-    Assert(row_k.has(x_s));
+Tableau::~Tableau(){}
 
-    row_k.substitute(*row_s);
+void Tableau::setColumnUnused(ArithVar v){
+  ColIterator colIter = colIterator(v);
+  while(!colIter.atEnd()){
+    ++colIter;
   }
-  Assert(getColumn(x_s).size() == 1);
-  Assert(getRowCount(x_s) == 1);
 }
-
 void Tableau::printTableau(){
   Debug("tableau") << "Tableau::d_activeRows"  << endl;
 
-  typedef RowsTable::iterator table_iter;
-  for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end();
-      rowIter != end; ++rowIter){
-    ReducedRowVector* row_k = *rowIter;
-    if(row_k != NULL){
-      row_k->printRow();
-    }
+  ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic();
+  for(; basicIter != endIter; ++basicIter){
+    ArithVar basic = *basicIter;
+    printRow(basic);
   }
 }
 
-uint32_t Tableau::numNonZeroEntries() const {
-  uint32_t colSum = 0;
-  ColumnMatrix::const_iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end();
-  for(; i != end; ++i){
-    const Column& col = *i;
-    colSum += col.size();
+void Tableau::printRow(ArithVar basic){
+  Debug("tableau") << "{" << basic << ":";
+  for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){
+    const TableauEntry& entry = *entryIter;
+    printEntry(entry);
+    Debug("tableau") << ",";
   }
-  return colSum;
+  Debug("tableau") << "}" << endl;
+}
+
+void Tableau::printEntry(const TableauEntry& entry){
+  Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient();
 }
 
 uint32_t Tableau::numNonZeroEntriesByRow() const {
   uint32_t rowSum = 0;
-  ArithVarSet::iterator i = d_basicVariables.begin(), end = d_basicVariables.end();
+  ArithVarSet::const_iterator i = d_basicVariables.begin(), end = d_basicVariables.end();
   for(; i != end; ++i){
     ArithVar basic = *i;
-    const ReducedRowVector& row = *(d_rowsTable[basic]);
-    rowSum += row.size();
+    rowSum += getRowLength(basic);
   }
   return rowSum;
 }
+
+uint32_t Tableau::numNonZeroEntriesByCol() const {
+  uint32_t colSum = 0;
+  VectorSizeTable::const_iterator i = d_colLengths.begin();
+  VectorSizeTable::const_iterator end = d_colLengths.end();
+  for(; i != end; ++i){
+    colSum += *i;
+  }
+  return colSum;
+}
+
+
+EntryID Tableau::findOnRow(ArithVar row, ArithVar col){
+  for(RowIterator i = rowIterator(row); !i.atEnd(); ++i){
+    EntryID id = i.getID();
+    const TableauEntry& entry = *i;
+    ArithVar colVar = entry.getColVar();
+
+    if(colVar == col){
+      return id;
+    }
+  }
+  return ENTRYID_SENTINEL;
+}
+
+EntryID Tableau::findOnCol(ArithVar row, ArithVar col){
+  for(ColIterator i = colIterator(col); !i.atEnd(); ++i){
+    EntryID id = i.getID();
+    const TableauEntry& entry = *i;
+    ArithVar rowVar = entry.getRowVar();
+
+    if(rowVar == row){
+      return id;
+    }
+  }
+  return ENTRYID_SENTINEL;
+}
+
+const TableauEntry& Tableau::findEntry(ArithVar row, ArithVar col){
+  bool colIsShorter = getColLength(col) < getRowLength(row);
+  EntryID id = colIsShorter ? findOnCol(row,col) : findOnRow(row,col);
+  if(id == ENTRYID_SENTINEL){
+    return d_failedFind;
+  }else{
+    return d_entryManager.get(id);
+  }
+}
+
+void Tableau::removeRow(ArithVar basic){
+  RowIterator i = rowIterator(basic);
+  while(!i.atEnd()){
+    EntryID id = i.getID();
+    ++i;
+    removeEntry(id);
+  }
+  d_basicVariables.remove(basic);
+}
+
+void Tableau::loadRowIntoMergeBuffer(ArithVar basic){
+  Assert(mergeBufferIsEmpty());
+  for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
+    EntryID id = i.getID();
+    const TableauEntry& entry = *i;
+    ArithVar colVar = entry.getColVar();
+    d_mergeBuffer[colVar] = make_pair(id, false);
+  }
+}
+
+void Tableau::emptyRowFromMergeBuffer(ArithVar basic){
+  Assert(isBasic(basic));
+  for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
+    const TableauEntry& entry = *i;
+    ArithVar colVar = entry.getColVar();
+    Assert(d_mergeBuffer[colVar].first == i.getID());
+    d_mergeBuffer[colVar] = make_pair(ENTRYID_SENTINEL, false);
+  }
+
+  Assert(mergeBufferIsEmpty());
+}
+
+
+/**
+ * Changes basic to newbasic (a variable on the row).
+ */
+void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew){
+  Assert(mergeBufferIsEmpty());
+  Assert(isBasic(basicOld));
+  Assert(!isBasic(basicNew));
+
+  EntryID newBasicID = findOnRow(basicOld, basicNew);
+
+  Assert(newBasicID != ENTRYID_SENTINEL);
+
+  TableauEntry& newBasicEntry = d_entryManager.get(newBasicID);
+  Rational negInverseA_rs = -(newBasicEntry.getCoefficient().inverse());
+
+  for(RowIterator i = rowIterator(basicOld); !i.atEnd(); ++i){
+    EntryID id = i.getID();
+    TableauEntry& entry = d_entryManager.get(id);
+
+    entry.getCoefficient() *=  negInverseA_rs;
+    entry.setRowVar(basicNew);
+  }
+
+  d_rowHeads[basicNew] = d_rowHeads[basicOld];
+  d_rowHeads[basicOld] = ENTRYID_SENTINEL;
+
+  d_rowLengths[basicNew] = d_rowLengths[basicOld];
+  d_rowLengths[basicOld] = 0;
+
+  d_basicVariables.remove(basicOld);
+  d_basicVariables.add(basicNew);
+}
+
+void Tableau::addEntry(ArithVar row, ArithVar col, const Rational& coeff){
+  Assert(coeff != 0);
+
+  EntryID newId = d_entryManager.newEntry();
+  TableauEntry& newEntry =  d_entryManager.get(newId);
+  newEntry = TableauEntry( row, col,
+                           d_rowHeads[row], d_colHeads[col],
+                           ENTRYID_SENTINEL, ENTRYID_SENTINEL,
+                           coeff);
+  Assert(newEntry.getCoefficient() != 0);
+
+  Debug("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << endl;
+
+  ++d_entriesInUse;
+
+  if(d_rowHeads[row] != ENTRYID_SENTINEL)
+    d_entryManager.get(d_rowHeads[row]).setPrevRowID(newId);
+
+  if(d_colHeads[col] != ENTRYID_SENTINEL)
+    d_entryManager.get(d_colHeads[col]).setPrevColID(newId);
+
+  d_rowHeads[row] = newId;
+  d_colHeads[col] = newId;
+  ++d_rowLengths[row];
+  ++d_colLengths[col];
+}
+
+void Tableau::removeEntry(EntryID id){
+  Assert(d_entriesInUse > 0);
+  --d_entriesInUse;
+
+  TableauEntry& entry = d_entryManager.get(id);
+
+  ArithVar row = entry.getRowVar();
+  ArithVar col = entry.getColVar();
+
+  Assert(d_rowLengths[row] > 0);
+  Assert(d_colLengths[col] > 0);
+
+
+  --d_rowLengths[row];
+  --d_colLengths[col];
+
+  EntryID prevRow = entry.getPrevRowID();
+  EntryID prevCol = entry.getPrevColID();
+
+  EntryID nextRow = entry.getNextRowID();
+  EntryID nextCol = entry.getNextColID();
+
+  if(d_rowHeads[row] == id){
+    d_rowHeads[row] = nextRow;
+  }
+  if(d_colHeads[col] == id){
+    d_colHeads[col] = nextCol;
+  }
+
+  entry.markBlank();
+
+  if(prevRow != ENTRYID_SENTINEL){
+    d_entryManager.get(prevRow).setNextRowID(nextRow);
+  }
+  if(nextRow != ENTRYID_SENTINEL){
+    d_entryManager.get(nextRow).setPrevRowID(prevRow);
+  }
+
+  if(prevCol != ENTRYID_SENTINEL){
+    d_entryManager.get(prevCol).setNextColID(nextCol);
+  }
+  if(nextCol != ENTRYID_SENTINEL){
+    d_entryManager.get(nextCol).setPrevColID(prevCol);
+  }
+
+  d_entryManager.freeEntry(id);
+}
+
+void Tableau::rowPlusRowTimesConstant(ArithVar basicTo, const Rational& c, ArithVar basicFrom){
+
+  Debug("tableau") << "rowPlusRowTimesConstant("
+                   << basicTo << "," << c << "," << basicFrom << ")"
+                   << endl;
+
+  Assert(debugNoZeroCoefficients(basicTo));
+  Assert(debugNoZeroCoefficients(basicFrom));
+
+  Assert(c != 0);
+  Assert(isBasic(basicTo));
+  Assert(isBasic(basicFrom));
+  Assert( d_usedList.empty() );
+
+
+  RowIterator i = rowIterator(basicTo);
+  while(!i.atEnd()){
+    EntryID id = i.getID();
+    TableauEntry& entry = d_entryManager.get(id);
+    ArithVar colVar = entry.getColVar();
+
+    ++i;
+    if(bufferPairIsNotEmpty(d_mergeBuffer[colVar])){
+      d_mergeBuffer[colVar].second = true;
+      d_usedList.push_back(colVar);
+
+      EntryID inOtherRow = d_mergeBuffer[colVar].first;
+      const TableauEntry& other = d_entryManager.get(inOtherRow);
+      entry.getCoefficient() += c * other.getCoefficient();
+
+      if(entry.getCoefficient().sgn() == 0){
+        removeEntry(id);
+      }
+    }
+  }
+
+  for(RowIterator i = rowIterator(basicFrom); !i.atEnd(); ++i){
+    const TableauEntry& entry = *i;
+    ArithVar colVar = entry.getColVar();
+
+    if(!(d_mergeBuffer[colVar]).second){
+      Rational newCoeff =  c * entry.getCoefficient();
+      addEntry(basicTo, colVar, newCoeff);
+    }
+  }
+
+  clearUsedList();
+
+  if(Debug.isOn("tableau")) { printTableau(); }
+}
+
+void Tableau::clearUsedList(){
+  ArithVarArray::iterator i, end;
+  for(i = d_usedList.begin(), end = d_usedList.end(); i != end; ++i){
+    ArithVar pos = *i;
+    d_mergeBuffer[pos].second = false;
+  }
+  d_usedList.clear();
+}
+
+void Tableau::addRow(ArithVar basic,
+                     const std::vector<Rational>& coefficients,
+                     const std::vector<ArithVar>& variables)
+{
+  Assert(coefficients.size() == variables.size() );
+  Assert(!isBasic(basic));
+
+  d_basicVariables.add(basic);
+
+  if(Debug.isOn("tableau")){ printTableau(); }
+
+  addEntry(basic, basic, Rational(-1));
+
+  vector<Rational>::const_iterator coeffIter = coefficients.begin();
+  vector<ArithVar>::const_iterator varsIter = variables.begin();
+  vector<ArithVar>::const_iterator varsEnd = variables.end();
+
+  for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
+    const Rational& coeff = *coeffIter;
+    ArithVar var_i = *varsIter;
+    addEntry(basic, var_i, coeff);
+  }
+
+  varsIter = variables.begin();
+  coeffIter = coefficients.begin();
+  for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
+    ArithVar var = *varsIter;
+
+    if(isBasic(var)){
+      Rational coeff = *coeffIter;
+
+      loadRowIntoMergeBuffer(var);
+      rowPlusRowTimesConstant(basic, coeff,  var);
+      emptyRowFromMergeBuffer(var);
+    }
+  }
+
+  if(Debug.isOn("tableau")) { printTableau(); }
+
+  Assert(debugNoZeroCoefficients(basic));
+
+  Assert(debugMatchingCountsForRow(basic));
+  Assert(getColLength(basic) == 1);
+}
+
+bool Tableau::debugNoZeroCoefficients(ArithVar basic){
+  for(RowIterator i=rowIterator(basic); !i.atEnd(); ++i){
+    const TableauEntry& entry = *i;
+    if(entry.getCoefficient() == 0){
+      return false;
+    }
+  }
+  return true;
+}
+bool Tableau::debugMatchingCountsForRow(ArithVar basic){
+  for(RowIterator i=rowIterator(basic); !i.atEnd(); ++i){
+    const TableauEntry& entry = *i;
+    ArithVar colVar = entry.getColVar();
+    uint32_t count = debugCountColLength(colVar);
+    Debug("tableau") << "debugMatchingCountsForRow "
+                     << basic << ":" << colVar << " " << count
+                     <<" "<< d_colLengths[colVar] << endl;
+    if( count != d_colLengths[colVar] ){
+      return false;
+    }
+  }
+  return true;
+}
+
+
+uint32_t Tableau::debugCountColLength(ArithVar var){
+  Debug("tableau") << var << " ";
+  uint32_t count = 0;
+  for(ColIterator i=colIterator(var); !i.atEnd(); ++i){
+    const TableauEntry& entry = *i;
+    Debug("tableau") << "(" << entry.getRowVar() << ", " << i.getID() << ") ";
+    ++count;
+  }
+  Debug("tableau") << endl;
+  return count;
+}
+
+uint32_t Tableau::debugCountRowLength(ArithVar var){
+  uint32_t count = 0;
+  for(RowIterator i=rowIterator(var); !i.atEnd(); ++i){
+    ++count;
+  }
+  return count;
+}
+
+/*
+void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,std::vector< Rational >& coefficients) const{
+  for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
+    ArithVar var = (*i).getArithVar();
+    const Rational& q = (*i).getCoefficient();
+    if(var != basic()){
+      variables.push_back(var);
+      coefficients.push_back(q);
+    }
+  }
+  }*/
+
+Node Tableau::rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map){
+  using namespace CVC4::kind;
+
+  Assert(getRowLength(basic) >= 2);
+
+  vector<Node> nonBasicPairs;
+  for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
+    const TableauEntry& entry = *i;
+    ArithVar colVar = entry.getColVar();
+    if(colVar == basic) continue;
+    Node var = (map.find(colVar))->second;
+    Node coeff = mkRationalNode(entry.getCoefficient());
+
+    Node mult = NodeBuilder<2>(MULT) << coeff << var;
+    nonBasicPairs.push_back(mult);
+  }
+
+  Node sum = Node::null();
+  if(nonBasicPairs.size() == 1 ){
+    sum = nonBasicPairs.front();
+  }else{
+    Assert(nonBasicPairs.size() >= 2);
+    NodeBuilder<> sumBuilder(PLUS);
+    sumBuilder.append(nonBasicPairs);
+    sum = sumBuilder;
+  }
+  Node basicVar = (map.find(basic))->second;
+  return NodeBuilder<2>(EQUAL) << basicVar << sum;
+}
+
+double Tableau::densityMeasure() const{
+  Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
+  Assert(numNonZeroEntriesByCol() == numNonZeroEntries());
+
+  uint32_t n = getNumRows();
+  if(n == 0){
+    return 1.0;
+  }else {
+    uint32_t s = numNonZeroEntries();
+    uint32_t m = d_colHeads.size();
+    uint32_t divisor = (n *(m - n + 1));
+
+    Assert(n >= 1);
+    Assert(m >= n);
+    Assert(divisor > 0);
+    Assert(divisor >= s);
+
+    return (double(s)) / divisor;
+  }
+}
+
+void TableauEntryManager::freeEntry(EntryID id){
+  Assert(get(id).blank());
+  Assert(d_size > 0);
+
+  d_freedEntries.push(id);
+  --d_size;
+}
+
+EntryID TableauEntryManager::newEntry(){
+  EntryID newId;
+  if(d_freedEntries.empty()){
+    newId = d_entries.size();
+    d_entries.push_back(TableauEntry());
+  }else{
+    newId = d_freedEntries.front();
+    d_freedEntries.pop();
+  }
+  ++d_size;
+  return newId;
+}
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 31f7cfa5a..fa227757a 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -25,10 +25,9 @@
 #include "theory/arith/arithvar_set.h"
 #include "theory/arith/normal_form.h"
 
-#include "theory/arith/row_vector.h"
-
-#include <ext/hash_map>
-#include <set>
+#include <queue>
+#include <vector>
+#include <utility>
 
 #ifndef __CVC4__THEORY__ARITH__TABLEAU_H
 #define __CVC4__THEORY__ARITH__TABLEAU_H
@@ -37,38 +36,229 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-typedef PermissiveBackArithVarSet Column;
+typedef uint32_t EntryID;
+#define ENTRYID_SENTINEL std::numeric_limits<ArithVar>::max()
+
+class TableauEntry {
+private:
+  ArithVar d_rowVar;
+  ArithVar d_colVar;
+
+  EntryID d_nextRow;
+  EntryID d_nextCol;
+
+  EntryID d_prevRow;
+  EntryID d_prevCol;
+
+  Rational d_coefficient;
+
+public:
+  TableauEntry():
+    d_rowVar(ARITHVAR_SENTINEL),
+    d_colVar(ARITHVAR_SENTINEL),
+    d_nextRow(ENTRYID_SENTINEL),
+    d_nextCol(ENTRYID_SENTINEL),
+    d_prevRow(ENTRYID_SENTINEL),
+    d_prevCol(ENTRYID_SENTINEL),
+    d_coefficient(0)
+  {}
+
+  TableauEntry(ArithVar row, ArithVar col,
+               EntryID nextRowEntry, EntryID nextColEntry,
+               EntryID prevRowEntry, EntryID prevColEntry,
+               const Rational& coeff):
+    d_rowVar(row),
+    d_colVar(col),
+    d_nextRow(nextRowEntry),
+    d_nextCol(nextColEntry),
+    d_prevRow(prevRowEntry),
+    d_prevCol(prevColEntry),
+    d_coefficient(coeff)
+  {}
+
+private:
+  bool unusedConsistent() const {
+    return
+      (d_rowVar == ARITHVAR_SENTINEL && d_colVar == ARITHVAR_SENTINEL) ||
+      (d_rowVar != ARITHVAR_SENTINEL && d_colVar != ARITHVAR_SENTINEL);
+  }
+
+public:
+
+  EntryID getNextRowID() const {
+    return d_nextRow;
+  }
+
+  EntryID getNextColID() const {
+    return d_nextCol;
+  }
+  EntryID getPrevRowID() const {
+    return d_prevRow;
+  }
+
+  EntryID getPrevColID() const {
+    return d_prevCol;
+  }
+
+  void setNextRowID(EntryID id) {
+    d_nextRow = id;
+  }
+  void setNextColID(EntryID id) {
+    d_nextCol = id;
+  }
+  void setPrevRowID(EntryID id) {
+    d_prevRow = id;
+  }
+  void setPrevColID(EntryID id) {
+    d_prevCol = id;
+  }
+
+  void setRowVar(ArithVar newRowVar){
+    d_rowVar = newRowVar;
+  }
+
+  ArithVar getRowVar() const{
+    return d_rowVar;
+  }
+  ArithVar getColVar() const{
+    return d_colVar;
+  }
+
+  const Rational& getCoefficient() const {
+    return d_coefficient;
+  }
+
+  Rational& getCoefficient(){
+    return d_coefficient;
+  }
+
+  void markBlank() {
+    d_rowVar = ARITHVAR_SENTINEL;
+    d_colVar = ARITHVAR_SENTINEL;
+  }
+
+  bool blank() const{
+    Assert(unusedConsistent());
+
+    return d_rowVar == ARITHVAR_SENTINEL;
+  }
+};
+
+class TableauEntryManager {
+private:
+  typedef std::vector<TableauEntry> EntryArray;
+
+  EntryArray d_entries;
+  std::queue<EntryID> d_freedEntries;
+
+  uint32_t d_size;
+
+public:
+  TableauEntryManager():
+    d_entries(), d_freedEntries(), d_size(0)
+  {}
+
+  const TableauEntry& get(EntryID id) const{
+    Assert(inBounds(id));
+    return d_entries[id];
+  }
+
+  TableauEntry& get(EntryID id){
+    Assert(inBounds(id));
+    return d_entries[id];
+  }
+
+  void freeEntry(EntryID id);
+
+  EntryID newEntry();
 
-typedef std::vector<Column> ColumnMatrix;
+  uint32_t size() const{ return d_size; }
+  uint32_t capacity() const{ return d_entries.capacity(); }
+
+
+private:
+  bool inBounds(EntryID id) const{
+    return id <  d_entries.size();
+  }
+};
 
 class Tableau {
 private:
 
-  typedef std::vector< ReducedRowVector* > RowsTable;
+  // VectorHeadTable : ArithVar |-> EntryID of the head of the vector
+  typedef std::vector<EntryID> VectorHeadTable;
+  VectorHeadTable d_rowHeads;
+  VectorHeadTable d_colHeads;
 
-  RowsTable d_rowsTable;
+  // VectorSizeTable : ArithVar |-> length of the vector
+  typedef std::vector<uint32_t> VectorSizeTable;
+  VectorSizeTable d_colLengths;
+  VectorSizeTable d_rowLengths;
 
+  // Set of all of the basic variables in the tableau.
   ArithVarSet d_basicVariables;
 
-  std::vector<uint32_t> d_rowCount;
-  ColumnMatrix d_columnMatrix;
+  typedef std::pair<EntryID, bool> PosUsedPair;
+  typedef std::vector<PosUsedPair> PosUsedPairArray;
+  PosUsedPairArray d_mergeBuffer;
+
+  typedef std::vector<ArithVar> ArithVarArray;
+  ArithVarArray d_usedList;
+
+
+  uint32_t d_entriesInUse;
+  TableauEntryManager d_entryManager;
 
 public:
   /**
    * Constructs an empty tableau.
    */
-  Tableau() :
-    d_rowsTable(),
-    d_basicVariables(),
-    d_rowCount(),
-    d_columnMatrix()
-  {}
-
-  /** Copy constructor. */
-  Tableau(const Tableau& tab);
+  Tableau() : d_entriesInUse(0) {}
   ~Tableau();
 
-  Tableau& operator=(const Tableau& tab);
+private:
+  void addEntry(ArithVar row, ArithVar col, const Rational& coeff);
+  void removeEntry(EntryID id);
+
+  template <bool isRowIterator>
+  class Iterator {
+  private:
+    EntryID d_curr;
+    TableauEntryManager& d_entryManager;
+
+  public:
+    Iterator(EntryID start, TableauEntryManager& manager) :
+      d_curr(start), d_entryManager(manager)
+    {}
+
+  public:
+
+    EntryID getID() const {
+      return d_curr;
+    }
+
+    const TableauEntry& operator*() const{
+      Assert(!atEnd());
+      return d_entryManager.get(d_curr);
+    }
+
+    Iterator& operator++(){
+      Assert(!atEnd());
+      TableauEntry& entry = d_entryManager.get(d_curr);
+      d_curr = isRowIterator ? entry.getNextRowID() : entry.getNextColID();
+      return *this;
+    }
+
+    bool atEnd() const {
+      return d_curr == ENTRYID_SENTINEL;
+    }
+  };
+
+public:
+  typedef Iterator<true> RowIterator;
+  typedef Iterator<false> ColIterator;
+
+  double densityMeasure() const;
 
   size_t getNumRows() const {
     return d_basicVariables.size();
@@ -76,56 +266,49 @@ public:
 
   void increaseSize(){
     d_basicVariables.increaseSize();
-    d_rowsTable.push_back(NULL);
-    d_rowCount.push_back(0);
 
-    d_columnMatrix.push_back(PermissiveBackArithVarSet());
+    d_rowHeads.push_back(ENTRYID_SENTINEL);
+    d_colHeads.push_back(ENTRYID_SENTINEL);
+
+    d_colLengths.push_back(0);
+    d_rowLengths.push_back(0);
 
-    //TODO replace with version of ArithVarSet that handles misses as non-entries
-    // not as buffer overflows
-    // ColumnMatrix::iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end();
-    // for(; i != end; ++i){
-    //   Column& col = *i;
-    //   col.increaseSize(d_columnMatrix.size());
-    // }
+    d_mergeBuffer.push_back(std::make_pair(ENTRYID_SENTINEL, false));
   }
 
   bool isBasic(ArithVar v) const {
     return d_basicVariables.isMember(v);
   }
 
-  ArithVarSet::iterator begin(){
+  ArithVarSet::const_iterator beginBasic() const{
     return d_basicVariables.begin();
   }
 
-  ArithVarSet::iterator end(){
+  ArithVarSet::const_iterator endBasic() const{
     return d_basicVariables.end();
   }
 
-  const Column& getColumn(ArithVar v){
-    Assert(v < d_columnMatrix.size());
-    return d_columnMatrix[v];
+  RowIterator rowIterator(ArithVar v){
+    Assert(v < d_rowHeads.size());
+    EntryID head = d_rowHeads[v];
+    return RowIterator(head, d_entryManager);
   }
 
-  Column::iterator beginColumn(ArithVar v){
-    return getColumn(v).begin();
-  }
-  Column::iterator endColumn(ArithVar v){
-    return getColumn(v).end();
+  ColIterator colIterator(ArithVar v){
+    Assert(v < d_colHeads.size());
+    EntryID head = d_colHeads[v];
+    return ColIterator(head, d_entryManager);
   }
 
 
-  ReducedRowVector& lookup(ArithVar var){
-    Assert(d_basicVariables.isMember(var));
-    Assert(d_rowsTable[var] != NULL);
-    return *(d_rowsTable[var]);
+  uint32_t getRowLength(ArithVar x) const{
+    Assert(x < d_rowLengths.size());
+    return d_rowLengths[x];
   }
 
-  uint32_t getRowCount(ArithVar x){
-    Assert(x < d_rowCount.size());
-    AlwaysAssert(d_rowCount[x] == getColumn(x).size());
-
-    return d_rowCount[x];
+  uint32_t getColLength(ArithVar x) const{
+    Assert(x < d_colLengths.size());
+    return d_colLengths[x];
   }
 
   /**
@@ -149,49 +332,73 @@ public:
    *   x_s is non-basic, and
    *   a_rs != 0.
    */
-  void pivot(ArithVar x_r, ArithVar x_s);
+  void pivot(ArithVar basicOld, ArithVar basicNew);
+private:
+  void rowPivot(ArithVar basicOld, ArithVar basicNew);
+  /** Requires merge buffer to be loaded with basicFrom and used to be empty. */
+  void rowPlusRowTimesConstant(ArithVar basicTo, const Rational& coeff, ArithVar basicFrom);
 
-  void printTableau();
+  EntryID findOnRow(ArithVar basic, ArithVar find);
+  EntryID findOnCol(ArithVar basic, ArithVar find);
 
-  ReducedRowVector* removeRow(ArithVar basic);
+  TableauEntry d_failedFind;
+public:
 
+  /** If the find fails, isUnused is true on the entry. */
+  const TableauEntry& findEntry(ArithVar row, ArithVar col);
 
   /**
-   * Let s = numNonZeroEntries(), n = getNumRows(), and m = d_columnMatrix.size().
-   * When n >= 1,
-   *   densityMeasure() := s / (n*m - n**2 + n)
-   *                    := s / (n *(m - n + 1))
-   * When n = 0, densityMeasure() := 1
+   * Prints the contents of the Tableau to Debug("tableau::print")
    */
-  double densityMeasure() const{
-    Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
-    uint32_t n = getNumRows();
-    if(n == 0){
-      return 1.0;
-    }else {
-      uint32_t s = numNonZeroEntries();
-      uint32_t m = d_columnMatrix.size();
-      uint32_t divisor = (n *(m - n + 1));
-
-      Assert(n >= 1);
-      Assert(m >= n);
-      Assert(divisor > 0);
-      Assert(divisor >= s);
-
-      return (double(s)) / divisor;
-    }
-  }
+  void printTableau();
+  void printRow(ArithVar basic);
+  void printEntry(const TableauEntry& entry);
+
 
 private:
+  void loadRowIntoMergeBuffer(ArithVar basic);
+  void emptyRowFromMergeBuffer(ArithVar basic);
+  void clearUsedList();
 
-  uint32_t numNonZeroEntries() const;
+  static bool bufferPairIsNotEmpty(const PosUsedPair& p){
+    return !(p.first == ENTRYID_SENTINEL && p.second == false);
+  }
+
+  static bool bufferPairIsEmpty(const PosUsedPair& p){
+    return (p.first == ENTRYID_SENTINEL && p.second == false);
+  }
+  bool mergeBufferIsEmpty() const {
+    return d_mergeBuffer.end() == std::find_if(d_mergeBuffer.begin(),
+                                               d_mergeBuffer.end(),
+                                               bufferPairIsNotEmpty);
+  }
+
+  void setColumnUnused(ArithVar v);
+
+public:
+  uint32_t size() const {
+    return d_entriesInUse;
+  }
+  uint32_t getNumEntriesInTableau() const {
+    return d_entryManager.size();
+  }
+  uint32_t getEntryCapacity() const {
+    return d_entryManager.capacity();
+  }
+
+  void removeRow(ArithVar basic);
+  Node rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map);
+private:
+  uint32_t numNonZeroEntries() const { return size(); }
   uint32_t numNonZeroEntriesByRow() const;
+  uint32_t numNonZeroEntriesByCol() const;
+
 
-  /** Copies the datastructures in tab to this.*/
-  void internalCopy(const Tableau& tab);
+  bool debugNoZeroCoefficients(ArithVar basic);
+  bool debugMatchingCountsForRow(ArithVar basic);
+  uint32_t debugCountColLength(ArithVar var);
+  uint32_t debugCountRowLength(ArithVar var);
 
-  /** Clears the structures in the tableau. */
-  void clear();
 };
 
 }; /* namespace arith  */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4b40e582c..c22b0019d 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -41,7 +41,6 @@
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/normal_form.h"
 
-#include <map>
 #include <stdint.h>
 
 using namespace std;
@@ -52,6 +51,8 @@ using namespace CVC4::kind;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
+static const uint32_t RESET_START = 2;
+
 struct SlackAttrID;
 typedef expr::Attribute<SlackAttrID, Node> Slack;
 
@@ -62,8 +63,8 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valu
   d_diseq(c),
   d_tableau(),
   d_restartsCounter(0),
-  d_initialDensity(1.0),
-  d_tableauResetDensity(2.0),
+  d_presolveHasBeenCalled(false),
+  d_tableauResetDensity(1.6),
   d_tableauResetPeriod(10),
   d_propagator(c, out),
   d_simplex(d_partialModel, d_tableau),
@@ -81,9 +82,10 @@ TheoryArith::Statistics::Statistics():
   d_staticLearningTimer("theory::arith::staticLearningTimer"),
   d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
   d_presolveTime("theory::arith::presolveTime"),
-  d_initialTableauDensity("theory::arith::initialTableauDensity", 0.0),
-  d_avgTableauDensityAtRestart("theory::arith::avgTableauDensityAtRestarts"),
-  d_tableauResets("theory::arith::tableauResets", 0),
+  d_initialTableauSize("theory::arith::initialTableauSize", 0),
+  //d_tableauSizeHistory("theory::arith::tableauSizeHistory"),
+  d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
+  d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
   d_restartTimer("theory::arith::restartTimer")
 {
   StatisticsRegistry::registerStat(&d_statUserVariables);
@@ -96,9 +98,10 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_presolveTime);
 
 
-  StatisticsRegistry::registerStat(&d_initialTableauDensity);
-  StatisticsRegistry::registerStat(&d_avgTableauDensityAtRestart);
-  StatisticsRegistry::registerStat(&d_tableauResets);
+  StatisticsRegistry::registerStat(&d_initialTableauSize);
+  //StatisticsRegistry::registerStat(&d_tableauSizeHistory);
+  StatisticsRegistry::registerStat(&d_currSetToSmaller);
+  StatisticsRegistry::registerStat(&d_smallerSetToCurr);
   StatisticsRegistry::registerStat(&d_restartTimer);
 }
 
@@ -113,9 +116,10 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_presolveTime);
 
 
-  StatisticsRegistry::unregisterStat(&d_initialTableauDensity);
-  StatisticsRegistry::unregisterStat(&d_avgTableauDensityAtRestart);
-  StatisticsRegistry::unregisterStat(&d_tableauResets);
+  StatisticsRegistry::unregisterStat(&d_initialTableauSize);
+  //StatisticsRegistry::unregisterStat(&d_tableauSizeHistory);
+  StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
+  StatisticsRegistry::unregisterStat(&d_smallerSetToCurr);
   StatisticsRegistry::unregisterStat(&d_restartTimer);
 }
 
@@ -129,21 +133,21 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
 
 ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){
   ArithVar bestBasic = ARITHVAR_SENTINEL;
-  uint64_t rowLength = std::numeric_limits<uint64_t>::max();
-
-  Column::iterator basicIter = d_tableau.beginColumn(variable);
-  Column::iterator end = d_tableau.endColumn(variable);
-  for(; basicIter != end; ++basicIter){
-    ArithVar x_j = *basicIter;
-    ReducedRowVector& row_j = d_tableau.lookup(x_j);
-
-    Assert(row_j.has(variable));
-    if((row_j.size() < rowLength) ||
-       (row_j.size() == rowLength && x_j < bestBasic)){
-      bestBasic = x_j;
-      rowLength = row_j.size();
+  uint64_t bestRowLength = std::numeric_limits<uint64_t>::max();
+
+  Tableau::ColIterator basicIter = d_tableau.colIterator(variable);
+  for(; !basicIter.atEnd(); ++basicIter){
+    const TableauEntry& entry = *basicIter;
+    Assert(entry.getColVar() == variable);
+    ArithVar basic = entry.getRowVar();
+    uint32_t rowLength = d_tableau.getRowLength(basic);
+    if((rowLength < bestRowLength) ||
+       (rowLength == bestRowLength && basic < bestBasic)){
+      bestBasic = basic;
+      bestRowLength = rowLength;
     }
   }
+  Assert(bestBasic == ARITHVAR_SENTINEL || bestRowLength < std::numeric_limits<uint32_t>::max());
   return bestBasic;
 }
 
@@ -409,7 +413,7 @@ void TheoryArith::check(Effort effortLevel){
     }
   }
 
-  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
   if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
   Debug("arith") << "TheoryArith::check end" << std::endl;
 }
@@ -579,15 +583,15 @@ Node TheoryArith::getValue(TNode n) {
 }
 
 void TheoryArith::notifyEq(TNode lhs, TNode rhs) {
-
 }
 
 void TheoryArith::notifyRestart(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
 
-  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
 
   ++d_restartsCounter;
+  /*
   if(d_restartsCounter % d_tableauResetPeriod == 0){
     double currentDensity = d_tableau.densityMeasure();
     d_statistics.d_avgTableauDensityAtRestart.addEntry(currentDensity);
@@ -599,6 +603,32 @@ void TheoryArith::notifyRestart(){
       d_tableau = d_initialTableau;
     }
   }
+  */
+  static const bool debugResetPolicy = false;
+
+  uint32_t currSize = d_tableau.size();
+  uint32_t copySize = d_smallTableauCopy.size();
+
+  //d_statistics.d_tableauSizeHistory << currSize;
+  if(debugResetPolicy){
+    cout << "curr " << currSize << " copy " << copySize << endl;
+  }
+  if(d_presolveHasBeenCalled && copySize == 0 && currSize > 0){
+    if(debugResetPolicy){
+      cout << "initial copy " << d_restartsCounter << endl;
+    }
+    d_smallTableauCopy = d_tableau; // The initial copy
+  }
+
+  if(d_presolveHasBeenCalled && d_restartsCounter >= RESET_START){
+    if(copySize >= currSize * 1.1 ){
+      ++d_statistics.d_smallerSetToCurr;
+      d_smallTableauCopy = d_tableau;
+    }else if(d_tableauResetDensity * copySize <=  currSize){
+      ++d_statistics.d_currSetToSmaller;
+      d_tableau = d_smallTableauCopy;
+    }
+  }
 }
 
 bool TheoryArith::entireStateIsConsistent(){
@@ -639,15 +669,14 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){
     Assert(!noRow);
 
     //remove the row from the tableau
-    ReducedRowVector* row  = d_tableau.removeRow(v);
-    Node eq = row->asEquality(d_arithVarToNodeMap);
+    Node eq =  d_tableau.rowAsEquality(v, d_arithVarToNodeMap);
+    d_tableau.removeRow(v);
 
-    if(Debug.isOn("row::print")) row->printRow();
     if(Debug.isOn("tableau")) d_tableau.printTableau();
     Debug("arith::permanentlyRemoveVariable") << eq << endl;
-    delete row;
 
-    Assert(d_tableau.getRowCount(v) == 0);
+    Assert(d_tableau.getRowLength(v) == 0);
+    Assert(d_tableau.getColLength(v) == 0);
     Assert(d_removedRows.find(v) ==  d_removedRows.end());
     d_removedRows[v] = eq;
   }
@@ -671,16 +700,15 @@ void TheoryArith::presolve(){
     }
   }
 
-  d_initialTableau = d_tableau;
-  d_initialDensity = d_initialTableau.densityMeasure();
-  d_statistics.d_initialTableauDensity.setData(d_initialDensity);
+  d_statistics.d_initialTableauSize.setData(d_tableau.size());
 
-  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
 
   static int callCount = 0;
   Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
 
   learner.clear();
 
+  d_presolveHasBeenCalled = true;
   check(FULL_EFFORT);
 }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 11cbfb425..a90e37bdc 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -119,11 +119,6 @@ private:
    */
   Tableau d_tableau;
 
-  /**
-   * A copy of the tableau immediately after removing variables
-   * without bounds in presolve().
-   */
-  Tableau d_initialTableau;
 
   /** Counts the number of notifyRestart() calls to the theory. */
   uint32_t d_restartsCounter;
@@ -134,11 +129,16 @@ private:
    * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau
    * is set to d_initialTableau.
    */
-  double d_initialDensity;
+  bool d_presolveHasBeenCalled;
   double d_tableauResetDensity;
   uint32_t d_tableauResetPeriod;
   static const uint32_t s_TABLEAU_RESET_INCREMENT = 5;
 
+  /**
+   * A copy of the tableau immediately after removing variables
+   * without bounds in presolve().
+   */
+  Tableau d_smallTableauCopy;
 
   ArithUnatePropagator d_propagator;
   SimplexDecisionProcedure d_simplex;
@@ -252,9 +252,10 @@ private:
     IntStat d_permanentlyRemovedVariables;
     TimerStat d_presolveTime;
 
-    BackedStat<double> d_initialTableauDensity;
-    AverageStat d_avgTableauDensityAtRestart;
-    IntStat d_tableauResets;
+    IntStat d_initialTableauSize;
+    //ListStat<uint32_t> d_tableauSizeHistory;
+    IntStat d_currSetToSmaller;
+    IntStat d_smallerSetToCurr;
     TimerStat d_restartTimer;
 
     Statistics();
diff --git a/src/util/stats.h b/src/util/stats.h
index a78070de4..bf962d02b 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -29,6 +29,7 @@
 #include <iomanip>
 #include <set>
 #include <ctime>
+#include <vector>
 
 #include "util/Assert.h"
 #include "lib/clock_gettime.h"
@@ -502,6 +503,49 @@ public:
 
 };/* class AverageStat */
 
+template <class T>
+class ListStat : public Stat{
+private:
+  typedef std::vector<T> List;
+  List d_list;
+public:
+
+  /**
+   * Construct an integer-valued statistic with the given name and
+   * initial value.
+   */
+  ListStat(const std::string& name) : Stat(name) {}
+  ~ListStat() {}
+
+  void flushInformation(std::ostream& out) const{
+    if(__CVC4_USE_STATISTICS) {
+      typename List::const_iterator i = d_list.begin(), end =  d_list.end();
+      out << "[";
+      if(i != end){
+        out << *i;
+        ++i;
+        for(; i != end; ++i){
+          out << ", " << *i;
+        }
+      }
+      out << "]";
+    }
+  }
+
+  ListStat& operator<<(const T& val){
+    if(__CVC4_USE_STATISTICS) {
+      d_list.push_back(val);
+    }
+    return (*this);
+  }
+
+  std::string getValue() const {
+    std::stringstream ss;
+    flushInformation(ss);
+    return ss.str();
+  }
+
+};/* class ListStat */
 
 /****************************************************************************/
 /* Some utility functions for ::timespec                                    */