This merges in the branch cvc4/branches/arithmetic/matrix into trunk.

- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau.
- Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code.
- No performance loss!
 

16 files changed, 1544 insertions, 1414 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index f9c423ef7..a029bc97b 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -27,9 +27,8 @@ libarith_la_SOURCES = \
 	partial_model.cpp \
 	linear_equality.h \
 	linear_equality.cpp \
-	arithvar_set.h \
-	tableau.h \
-	tableau.cpp \
+	matrix.h \
+	matrix.cpp \
 	arith_priority_queue.h \
 	arith_priority_queue.cpp \
 	simplex.h \
diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index 9dd8e588a..e11a8ba53 100644
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -25,7 +25,7 @@
 
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/arith/tableau.h"
+#include "theory/arith/matrix.h"
 #include "theory/arith/partial_model.h"
 
 #include "util/stats.h"
@@ -136,7 +136,7 @@ private:
    */
   ArithVarArray d_varOrderQueue;
 
-  PermissiveBackArithVarSet d_varSet;
+  DenseSet d_varSet;
 
   /**
    * Reference to the arithmetic partial model for checking if a variable
diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index 432f9f0c2..924e91bf5 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -14,7 +14,7 @@
  ** \brief Defines ArithVar which is the internal representation of variables in arithmetic
  **
  ** This defines ArithVar which is the internal representation of variables in
- ** arithmetic. This is a typedef from uint32_t to ArithVar.
+ ** arithmetic. This is a typedef from Index to ArithVar.
  ** This file also provides utilities for ArithVars.
  **/
 
@@ -25,16 +25,18 @@
 #define __CVC4__THEORY__ARITH__ARITHVAR_H
 
 #include <limits>
-#include <stdint.h>
 #include <ext/hash_map>
 #include "expr/node.h"
 #include "context/cdhashset.h"
+#include "context/cdhashset.h"
+
+#include "util/index.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
-typedef uint32_t ArithVar;
+typedef Index ArithVar;
 const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
 
 //Maps from Nodes -> ArithVars, and vice versa
diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
deleted file mode 100644
index b9ae48b16..000000000
--- a/src/theory/arith/arithvar_set.h
+++ /dev/null
@@ -1,372 +0,0 @@
-/*********************                                                        */
-/*! \file arithvar_set.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
-#define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
-
-#include <vector>
-#include "theory/arith/arithvar.h"
-#include "context/context.h"
-#include "context/cdlist.h"
-
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-/**
- * This is an abstraction of a set of ArithVars.
- * This class is designed to provide constant time insertion, deletion, and element_of
- * and fast iteration.
- *
- * ArithVarSets come in 2 varieties: ArithVarSet, and PermissiveBackArithVarSet.
- * The default ArithVarSet assumes that there is no knowledge assumed about ArithVars
- * that are greater than allocated(). Asking isMember() of such an ArithVar
- * is an assertion failure. The cost of doing this is that it takes O(M)
- * where M is the total number of ArithVars in memory.
- *
- * PermissiveBackArithVarSet means that all ArithVars are implicitly not in the set,
- * and any ArithVar past the end of d_posVector is not in the set.
- * A permissiveBack allows for less memory to be consumed on average.
- *
- */
-template <bool permissiveBack>
-class ArithVarSetImpl {
-public:
-  typedef std::vector<ArithVar> VarList;
-private:
-  //List of the ArithVars in the set.
-  VarList d_list;
-
-  //Each ArithVar in the set is mapped to its position in d_list.
-  //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL
-  std::vector<unsigned> d_posVector;
-
-public:
-  typedef VarList::const_iterator const_iterator;
-
-  ArithVarSetImpl() :  d_list(), d_posVector() {}
-
-  size_t size() const {
-    return d_list.size();
-  }
-  bool empty() const {
-    return d_list.empty();
-  }
-
-  size_t allocated() const {
-    return d_posVector.size();
-  }
-
-  void purge() {
-    for(VarList::const_iterator i=d_list.begin(), endIter=d_list.end();i!= endIter; ++i){
-      d_posVector[*i] = ARITHVAR_SENTINEL;
-    }
-    d_list.clear();
-    Assert(empty());
-  }
-
-  void increaseSize(ArithVar max){
-    Assert(max >= allocated());
-    d_posVector.resize(max+1, ARITHVAR_SENTINEL);
-  }
-
-  void increaseSize(){
-    increaseSize(allocated());
-  }
-
-  bool isMember(ArithVar x) const{
-    if(permissiveBack && x >=  allocated()){
-      return false;
-    }else{
-      Assert(x <  allocated());
-      return d_posVector[x] != ARITHVAR_SENTINEL;
-    }
-  }
-
-  /** Invalidates iterators */
-  void init(ArithVar x, bool val) {
-    Assert(x >= allocated());
-    increaseSize(x);
-    if(val){
-      add(x);
-    }
-  }
-
-  /** Invalidates iterators */
-  void add(ArithVar x){
-    Assert(!isMember(x));
-    if(permissiveBack && x >=  allocated()){
-      increaseSize(x);
-    }
-    d_posVector[x] = size();
-    d_list.push_back(x);
-  }
-
-  const_iterator begin() const{ return d_list.begin(); }
-  const_iterator end() const{ return d_list.end(); }
-
-  /**
-   * Invalidates iterators.
-   * Adds x to the set if it is not already in the set.
-   */
-  void softAdd(ArithVar x){
-    if(!isMember(x)){
-      add(x);
-    }
-  }
-
-  const VarList& getList() const{
-    return d_list;
-  }
-
-  /** Invalidates iterators */
-  void remove(ArithVar x){
-    Assert(isMember(x));
-    swapToBack(x);
-    Assert(d_list.back() == x);
-    pop_back();
-  }
-
-  ArithVar pop_back() {
-    Assert(!empty());
-    ArithVar atBack = d_list.back();
-    d_posVector[atBack] = ARITHVAR_SENTINEL;
-    d_list.pop_back();
-    return atBack;
-  }
-
- private:
-
-  /** This should be true of all x < allocated() after every operation. */
-  bool wellFormed(ArithVar x){
-    if(d_posVector[x] == ARITHVAR_SENTINEL){
-      return true;
-    }else{
-      return d_list[d_posVector[x]] == x;
-    }
-  }
-
-  /** Swaps a member x to the back of d_list. */
-  void swapToBack(ArithVar x){
-    Assert(isMember(x));
-
-    unsigned currentPos = d_posVector[x];
-    ArithVar atBack = d_list.back();
-
-    d_list[currentPos] = atBack;
-    d_posVector[atBack] = currentPos;
-
-    d_list[size() - 1] = x;
-    d_posVector[x] = size() - 1;
-  }
-};
-
-typedef ArithVarSetImpl<false> ArithVarSet;
-typedef ArithVarSetImpl<true> PermissiveBackArithVarSet;
-
-
-/**
- * ArithVarMultiset
- */
-class ArithVarMultiset {
-public:
-  typedef std::vector<ArithVar> VarList;
-private:
-  //List of the ArithVars in the multi set.
-  VarList d_list;
-
-  //Each ArithVar in the set is mapped to its position in d_list.
-  //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL
-  std::vector<unsigned> d_posVector;
-
-  //Count of the number of elements in the array
-  std::vector<unsigned> d_counts;
-
-public:
-  typedef VarList::const_iterator const_iterator;
-
-  ArithVarMultiset() :  d_list(), d_posVector() {}
-
-  size_t size() const {
-    return d_list.size();
-  }
-
-  bool empty() const {
-    return d_list.empty();
-  }
-
-  size_t allocated() const {
-    Assert(d_posVector.size() == d_counts.size());
-    return d_posVector.size();
-  }
-
-  void purge() {
-    for(VarList::const_iterator i=d_list.begin(), endIter=d_list.end(); i!= endIter; ++i){
-      d_posVector[*i] = ARITHVAR_SENTINEL;
-      d_counts[*i] = 0;
-    }
-    d_list.clear();
-    Assert(empty());
-  }
-
-  void increaseSize(ArithVar max){
-    Assert(max >= allocated());
-    d_posVector.resize(max+1, ARITHVAR_SENTINEL);
-    d_counts.resize(max+1, 0);
-  }
-
-  void increaseSize(){
-    increaseSize(allocated());
-  }
-
-  bool isMember(ArithVar x) const{
-    if( x >=  allocated()){
-      return false;
-    }else{
-      Assert(x <  allocated());
-      return d_posVector[x] != ARITHVAR_SENTINEL;
-    }
-  }
-
-  /**
-   * Invalidates iterators.
-   */
-  void addMultiset(ArithVar x){
-    if( x >=  allocated()){
-      increaseSize(x);
-    }
-    if(d_counts[x] == 0){
-      d_posVector[x] = size();
-      d_list.push_back(x);
-    }
-    d_counts[x]++;
-  }
-
-  unsigned count(ArithVar x){
-    if( x >=  allocated()){
-      return 0;
-    }else{
-      return d_counts[x];
-    }
-  }
-
-  const_iterator begin() const{ return d_list.begin(); }
-  const_iterator end() const{ return d_list.end(); }
-
-  const VarList& getList() const{
-    return d_list;
-  }
-
-  /** Invalidates iterators */
-  void remove(ArithVar x){
-    Assert(isMember(x));
-    swapToBack(x);
-    Assert(d_list.back() == x);
-    pop_back();
-  }
-
-  ArithVar pop_back() {
-    Assert(!empty());
-    ArithVar atBack = d_list.back();
-    d_posVector[atBack] = ARITHVAR_SENTINEL;
-    d_counts[atBack] = 0;
-    d_list.pop_back();
-    return atBack;
-  }
-
- private:
-
-  /** This should be true of all x < allocated() after every operation. */
-  bool wellFormed(ArithVar x){
-    if(d_posVector[x] == ARITHVAR_SENTINEL){
-      return true;
-    }else{
-      return d_list[d_posVector[x]] == x;
-    }
-  }
-
-  /** Swaps a member x to the back of d_list. */
-  void swapToBack(ArithVar x){
-    Assert(isMember(x));
-
-    unsigned currentPos = d_posVector[x];
-    ArithVar atBack = d_list.back();
-
-    d_list[currentPos] = atBack;
-    d_posVector[atBack] = currentPos;
-
-    d_list[size() - 1] = x;
-    d_posVector[x] = size() - 1;
-  }
-};
-
-class CDArithVarSet {
-private:
-
-  class RemoveIntCleanup {
-  private:
-    std::vector<bool>& d_set;
-  public:
-    RemoveIntCleanup(std::vector<bool>& set)
-      : d_set(set)
-    {}
-
-    void operator()(ArithVar* p){
-      ArithVar x = *p;
-      Assert(d_set[x]);
-      d_set[x] = false;
-    }
-  };
-
-  std::vector<bool> d_set;
-  context::CDList<ArithVar, RemoveIntCleanup> d_list;
-
-public:
-  CDArithVarSet(context::Context* c)
-    : d_set(), d_list(c, true, RemoveIntCleanup(d_set))
-  { }
-
-  /** This cannot be const as garbage collection is done lazily. */
-  bool contains(ArithVar x) const{
-    if(x < d_set.size()){
-      return d_set[x];
-    }else{
-      return false;
-    }
-  }
-
-  void insert(ArithVar x){
-    Assert(!contains(x));
-    if(x >= d_set.size()){
-      d_set.resize(x+1, false);
-    }
-    d_list.push_back(x);
-    d_set[x] = true;
-  }
-};
-
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_SET_H */
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index e70773030..a72989498 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -5,7 +5,6 @@
 #pragma once
 
 #include "theory/arith/arithvar.h"
-#include "theory/arith/arithvar_set.h"
 #include "theory/arith/arithvar_node_map.h"
 #include "theory/arith/constraint_forward.h"
 
@@ -18,6 +17,7 @@
 #include "context/cdmaybe.h"
 
 #include "util/stats.h"
+#include "util/dense_map.h"
 
 namespace CVC4 {
 namespace theory {
@@ -32,7 +32,7 @@ private:
    * If this is 0 or cannot be 0, this can be signalled.
    * The pair of terms for the congruence is stored in watched equalities.
    */
-  PermissiveBackArithVarSet d_watchedVariables;
+  DenseSet d_watchedVariables;
   /** d_watchedVariables |-> (= x y) */
   ArithVarToNodeMap d_watchedEqualities;
 
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index c5a0f534f..b92aced4e 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -23,7 +23,7 @@
 
 #include "context/context.h"
 
-#include "theory/arith/tableau.h"
+#include "theory/arith/matrix.h"
 #include "theory/arith/partial_model.h"
 #include "util/rational.h"
 
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index ca7cd69c4..964d27464 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -58,10 +58,10 @@ void LinearEqualityModule::update(ArithVar x_i, const DeltaRational& v){
   //Assert(matchingSets(d_tableau, x_i));
   Tableau::ColIterator basicIter = d_tableau.colIterator(x_i);
   for(; !basicIter.atEnd(); ++basicIter){
-    const TableauEntry& entry = *basicIter;
+    const Tableau::Entry& entry = *basicIter;
     Assert(entry.getColVar() == x_i);
 
-    ArithVar x_j = entry.getRowVar();
+    ArithVar x_j = d_tableau.rowIndexToBasic(entry.getRowIndex());
     //ReducedRowVector& row_j = d_tableau.lookup(x_j);
 
     //const Rational& a_ji = row_j.lookup(x_i);
@@ -76,7 +76,6 @@ void LinearEqualityModule::update(ArithVar x_i, const DeltaRational& v){
 
   d_partialModel.setAssignment(x_i, v);
 
-  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);
@@ -90,7 +89,8 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRatio
 
   if(Debug.isOn("arith::simplex:row")){ debugPivot(x_i, x_j); }
 
-  const TableauEntry& entry_ij =  d_tableau.findEntry(x_i, x_j);
+  RowIndex ridx = d_tableau.basicToRowIndex(x_i);
+  const Tableau::Entry& entry_ij =  d_tableau.findEntry(ridx, x_j);
   Assert(!entry_ij.blank());
 
 
@@ -111,10 +111,11 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRatio
 
   //Assert(matchingSets(d_tableau, x_j));
   for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){
-    const TableauEntry& entry = *iter;
+    const Tableau::Entry& entry = *iter;
     Assert(entry.getColVar() == x_j);
-    ArithVar x_k = entry.getRowVar();
-    if(x_k != x_i ){
+    RowIndex currRow = entry.getRowIndex();
+    if(ridx != currRow ){
+      ArithVar x_k = d_tableau.rowIndexToBasic(currRow);
       const Rational& a_kj = entry.getCoefficient();
       DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
       d_partialModel.setAssignment(x_k, nextAssignment);
@@ -126,15 +127,12 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRatio
   // Pivots
   ++(d_statistics.d_statPivots);
 
-  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);
 
   d_basicVariableUpdates(x_j);
 
-  if(Debug.isOn("tableau")){
-    d_tableau.printTableau();
+  if(Debug.isOn("matrix")){
+    d_tableau.printMatrix();
   }
 }
 
@@ -142,8 +140,8 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRatio
 void LinearEqualityModule::debugPivot(ArithVar x_i, ArithVar x_j){
   Debug("arith::pivot") << "debugPivot("<< x_i  <<"|->"<< x_j << ")" << endl;
 
-  for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){
-    const TableauEntry& entry = *iter;
+  for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){
+    const Tableau::Entry& entry = *iter;
 
     ArithVar var = entry.getColVar();
     const Rational& coeff = entry.getCoefficient();
@@ -168,15 +166,15 @@ void LinearEqualityModule::debugPivot(ArithVar x_i, ArithVar x_j){
  *   }
  */
 void LinearEqualityModule::debugCheckTableau(){
-  ArithVarSet::const_iterator basicIter = d_tableau.beginBasic();
-  ArithVarSet::const_iterator endIter = d_tableau.endBasic();
+  Tableau::BasicIterator basicIter = d_tableau.beginBasic(),
+    endIter = d_tableau.endBasic();
   for(; basicIter != endIter; ++basicIter){
     ArithVar basic = *basicIter;
     DeltaRational sum;
     Debug("paranoid:check_tableau") << "starting row" << basic << endl;
-    Tableau::RowIterator nonbasicIter = d_tableau.rowIterator(basic);
+    Tableau::RowIterator nonbasicIter = d_tableau.basicRowIterator(basic);
     for(; !nonbasicIter.atEnd(); ++nonbasicIter){
-      const TableauEntry& entry = *nonbasicIter;
+      const Tableau::Entry& entry = *nonbasicIter;
       ArithVar nonbasic = entry.getColVar();
       if(basic == nonbasic) continue;
 
@@ -195,8 +193,8 @@ void LinearEqualityModule::debugCheckTableau(){
 
 DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){
   DeltaRational sum(0,0);
-  for(Tableau::RowIterator i = d_tableau.rowIterator(basic); !i.atEnd(); ++i){
-    const TableauEntry& entry = (*i);
+  for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
+    const Tableau::Entry& entry = (*i);
     ArithVar nonbasic = entry.getColVar();
     if(nonbasic == basic) continue;
     const Rational& coeff =  entry.getCoefficient();
@@ -220,8 +218,8 @@ DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){
   Assert(d_tableau.isBasic(x));
   DeltaRational sum(0);
 
-  for(Tableau::RowIterator i = d_tableau.rowIterator(x); !i.atEnd(); ++i){
-    const TableauEntry& entry = (*i);
+  for(Tableau::RowIterator i = d_tableau.basicRowIterator(x); !i.atEnd(); ++i){
+    const Tableau::Entry& entry = (*i);
     ArithVar nonbasic = entry.getColVar();
     if(nonbasic == x) continue;
     const Rational& coeff = entry.getCoefficient();
@@ -233,8 +231,8 @@ DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){
 }
 
 bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){
-  for(Tableau::RowIterator iter = d_tableau.rowIterator(basic); !iter.atEnd(); ++iter){
-    const TableauEntry& entry = *iter;
+  for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd(); ++iter){
+    const Tableau::Entry& entry = *iter;
 
     ArithVar var = entry.getColVar();
     if(var == basic) continue;
@@ -267,9 +265,9 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
 
   vector<Constraint> bounds;
 
-  Tableau::RowIterator iter = d_tableau.rowIterator(basic);
+  Tableau::RowIterator iter = d_tableau.basicRowIterator(basic);
   for(; !iter.atEnd(); ++iter){
-    const TableauEntry& entry = *iter;
+    const Tableau::Entry& entry = *iter;
     ArithVar nonbasic = entry.getColVar();
     if(nonbasic == basic) continue;
 
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index b5d439769..7cac4c871 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -35,7 +35,7 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/tableau.h"
+#include "theory/arith/matrix.h"
 #include "theory/arith/constraint.h"
 
 #include "util/stats.h"
diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp
new file mode 100644
index 000000000..18fbf395e
--- /dev/null
+++ b/src/theory/arith/matrix.cpp
@@ -0,0 +1,564 @@
+/*********************                                                        */
+/*! \file tableau.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+
+#include "theory/arith/matrix.h"
+
+using namespace std;
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+
+/*
+void Tableau::addRow(ArithVar basicVar,
+                     const std::vector<Rational>& coeffs,
+                     const std::vector<ArithVar>& variables){
+
+  Assert(coeffs.size() == variables.size());
+
+  //The new basic variable cannot already be a basic variable
+  Assert(!d_basicVariables.isMember(basicVar));
+  d_basicVariables.add(basicVar);
+  ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount, d_columnMatrix);
+  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
+  vector<ArithVar>::const_iterator varsIter = variables.begin();
+  vector<ArithVar>::const_iterator varsEnd = variables.end();
+
+  for( ; varsIter != varsEnd; ++varsIter){
+    ArithVar var = *varsIter;
+
+    if(d_basicVariables.isMember(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(isBasic(basic));
+
+  ReducedRowVector* row = d_rowsTable[basic];
+
+  d_basicVariables.remove(basic);
+  d_rowsTable[basic] = NULL;
+
+  return row;
+}
+*/
+
+void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic){
+  Assert(isBasic(oldBasic));
+  Assert(!isBasic(newBasic));
+  Assert(d_mergeBuffer.empty());
+
+  Debug("tableau") << "Tableau::pivot(" <<  oldBasic <<", " << newBasic <<")"  << endl;
+
+  RowIndex ridx = basicToRowIndex(oldBasic);
+
+  rowPivot(oldBasic, newBasic);
+  Assert(ridx == basicToRowIndex(newBasic));
+
+  loadRowIntoBuffer(ridx);
+
+  ColIterator colIter = colIterator(newBasic);
+  while(!colIter.atEnd()){
+    EntryID id = colIter.getID();
+    Entry& entry = d_entries.get(id);
+
+    ++colIter; //needs to be incremented before the variable is removed
+    if(entry.getRowIndex() == ridx){ continue; }
+
+    RowIndex to = entry.getRowIndex();
+    Rational coeff = entry.getCoefficient();
+
+    rowPlusBufferTimesConstant(to, coeff);
+  }
+  clearBuffer();
+
+  //Clear the column for used for this variable
+
+  Assert(d_mergeBuffer.empty());
+  Assert(!isBasic(oldBasic));
+  Assert(isBasic(newBasic));
+  Assert(getColLength(newBasic) == 1);
+}
+
+// void Tableau::printTableau() const {
+//   Debug("tableau") << "Tableau::d_activeRows"  << endl;
+
+//   ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic();
+//   for(; basicIter != endIter; ++basicIter){
+//     ArithVar basic = *basicIter;
+//     printRow(basic);
+//   }
+// }
+
+// void Tableau::printRow(ArithVar basic) const {
+//   Debug("tableau") << "{" << basic << ":";
+//   for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){
+//     const TableauEntry& entry = *entryIter;
+//     printEntry(entry);
+//     Debug("tableau") << ",";
+//   }
+//   Debug("tableau") << "}" << endl;
+// }
+
+// void Tableau::printEntry(const TableauEntry& entry) const {
+//   Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient();
+// }
+
+// uint32_t Tableau::numNonZeroEntriesByRow() const {
+//   uint32_t rowSum = 0;
+//   ArithVarSet::const_iterator i = d_basicVariables.begin(), end = d_basicVariables.end();
+//   for(; i != end; ++i){
+//     ArithVar basic = *i;
+//     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(isBasic(basicOld));
+  Assert(!isBasic(basicNew));
+
+  RowIndex rid = basicToRowIndex(basicOld);
+
+  EntryID newBasicID = findOnRow(rid, basicNew);
+
+  Assert(newBasicID != ENTRYID_SENTINEL);
+
+  Tableau::Entry& newBasicEntry = d_entries.get(newBasicID);
+  Rational negInverseA_rs = -(newBasicEntry.getCoefficient().inverse());
+
+  for(RowIterator i = basicRowIterator(basicOld); !i.atEnd(); ++i){
+    EntryID id = i.getID();
+    Tableau::Entry& entry = d_entries.get(id);
+
+    entry.getCoefficient() *=  negInverseA_rs;
+  }
+
+  d_basic2RowIndex.remove(basicOld);
+  d_basic2RowIndex.set(basicNew, rid);
+  d_rowIndex2basic[rid] = 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));
+
+  RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
+  addEntry(newRow, basic, Rational(-1));
+
+  Assert(d_rowIndex2basic.size() == newRow);
+
+  d_basic2RowIndex.set(basic, newRow);
+  d_rowIndex2basic.push_back(basic);
+
+
+  if(Debug.isOn("matrix")){ printMatrix(); }
+
+  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){
+    ArithVar var = *varsIter;
+
+    if(isBasic(var)){
+      Rational coeff = *coeffIter;
+
+      RowIndex ri = basicToRowIndex(var);
+
+      loadRowIntoBuffer(ri);
+      rowPlusBufferTimesConstant(newRow, coeff);
+      clearBuffer();
+    }
+  }
+
+  if(Debug.isOn("matrix")) { printMatrix(); }
+
+  Assert(debugNoZeroCoefficients(newRow));
+  Assert(debugMatchingCountsForRow(newRow));
+  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;
+// }
+
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
new file mode 100644
index 000000000..b1be48828
--- /dev/null
+++ b/src/theory/arith/matrix.h
@@ -0,0 +1,915 @@
+/*********************                                                        */
+/*! \file matrix.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sparse matrix implementations for different types.
+ **
+ ** Sparse matrix implementations for different types.
+ ** This defines Matrix<T>, IntegerEqualityTables and Tableau.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+#include "util/index.h"
+#include "util/dense_map.h"
+
+#include "theory/arith/arithvar.h"
+#include "theory/arith/normal_form.h"
+
+#include <queue>
+#include <vector>
+#include <utility>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+typedef Index EntryID;
+const EntryID ENTRYID_SENTINEL = std::numeric_limits<EntryID>::max();
+
+typedef Index RowIndex;
+const RowIndex ROW_INDEX_SENTINEL  = std::numeric_limits<RowIndex>::max();
+
+template<class T>
+class MatrixEntry {
+private:
+  RowIndex d_rowIndex;
+  ArithVar d_colVar;
+
+  EntryID d_nextRow;
+  EntryID d_nextCol;
+
+  EntryID d_prevRow;
+  EntryID d_prevCol;
+
+  T d_coefficient;
+
+public:
+  MatrixEntry():
+    d_rowIndex(ROW_INDEX_SENTINEL),
+    d_colVar(ARITHVAR_SENTINEL),
+    d_nextRow(ENTRYID_SENTINEL),
+    d_nextCol(ENTRYID_SENTINEL),
+    d_prevRow(ENTRYID_SENTINEL),
+    d_prevCol(ENTRYID_SENTINEL),
+    d_coefficient()
+  {}
+
+  MatrixEntry(RowIndex row, ArithVar col, const T& coeff):
+     d_rowIndex(row),
+     d_colVar(col),
+     d_nextRow(ENTRYID_SENTINEL),
+     d_nextCol(ENTRYID_SENTINEL),
+     d_prevRow(ENTRYID_SENTINEL),
+     d_prevCol(ENTRYID_SENTINEL),
+     d_coefficient(coeff)
+  {}
+
+private:
+  bool unusedConsistent() const {
+    return
+      (d_rowIndex == ROW_INDEX_SENTINEL && d_colVar == ARITHVAR_SENTINEL) ||
+      (d_rowIndex != ROW_INDEX_SENTINEL && d_colVar != ARITHVAR_SENTINEL);
+  }
+
+public:
+
+  EntryID getNextRowEntryID() const {
+    return d_nextRow;
+  }
+
+  EntryID getNextColEntryID() const {
+    return d_nextCol;
+  }
+  EntryID getPrevRowEntryID() const {
+    return d_prevRow;
+  }
+
+  EntryID getPrevColEntryID() const {
+    return d_prevCol;
+  }
+
+  void setNextRowEntryID(EntryID id) {
+    d_nextRow = id;
+  }
+  void setNextColEntryID(EntryID id) {
+    d_nextCol = id;
+  }
+  void setPrevRowEntryID(EntryID id) {
+    d_prevRow = id;
+  }
+  void setPrevColEntryID(EntryID id) {
+    d_prevCol = id;
+  }
+
+  RowIndex getRowIndex() const{
+    return d_rowIndex;
+  }
+
+  ArithVar getColVar() const{
+    return d_colVar;
+  }
+
+  const T& getCoefficient() const {
+    return d_coefficient;
+  }
+
+  T& getCoefficient(){
+    return d_coefficient;
+  }
+
+  void setCoefficient(const T& t){
+    d_coefficient = t;
+  }
+
+  void markBlank() {
+    d_rowIndex = ROW_INDEX_SENTINEL;
+    d_colVar = ARITHVAR_SENTINEL;
+  }
+
+  bool blank() const{
+    Assert(unusedConsistent());
+
+    return d_rowIndex == ROW_INDEX_SENTINEL;
+  }
+}; /* class MatrixEntry<T> */
+
+template<class T>
+class MatrixEntryVector {
+private:
+  typedef MatrixEntry<T> EntryType;
+  typedef std::vector<EntryType> EntryArray;
+
+  EntryArray d_entries;
+  std::queue<EntryID> d_freedEntries;
+
+  uint32_t d_size;
+
+public:
+  MatrixEntryVector():
+    d_entries(), d_freedEntries(), d_size(0)
+  {}
+
+  const EntryType& operator[](EntryID id) const{
+    Assert(inBounds(id));
+    return d_entries[id];
+  }
+
+  EntryType& get(EntryID id){
+    Assert(inBounds(id));
+    return d_entries[id];
+  }
+
+  void freeEntry(EntryID id){
+    Assert(get(id).blank());
+    Assert(d_size > 0);
+
+    d_freedEntries.push(id);
+    --d_size;
+  }
+
+  EntryID newEntry(){
+    EntryID newId;
+    if(d_freedEntries.empty()){
+      newId = d_entries.size();
+      d_entries.push_back(MatrixEntry<T>());
+    }else{
+      newId = d_freedEntries.front();
+      d_freedEntries.pop();
+    }
+    ++d_size;
+    return newId;
+  }
+
+  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 MatrixEntryVector<T> */
+
+template <class T, bool isRow>
+class MatrixVector {
+private:
+  EntryID d_head;
+  uint32_t d_size;
+
+  MatrixEntryVector<T>* d_entries;
+
+  class Iterator {
+  private:
+    EntryID d_curr;
+    const MatrixEntryVector<T>* d_entries;
+
+  public:
+    Iterator(EntryID start, const MatrixEntryVector<T>* entries) :
+      d_curr(start), d_entries(entries)
+    {}
+
+  public:
+
+    EntryID getID() const {
+      return d_curr;
+    }
+
+    const MatrixEntry<T>& operator*() const{
+      Assert(!atEnd());
+      return (*d_entries)[d_curr];
+    }
+
+    Iterator& operator++(){
+      Assert(!atEnd());
+      const MatrixEntry<T>& entry = (*d_entries)[d_curr];
+      d_curr = isRow ? entry.getNextRowEntryID() : entry.getNextColEntryID();
+      return *this;
+    }
+
+    bool atEnd() const {
+      return d_curr == ENTRYID_SENTINEL;
+    }
+
+    bool operator==(const Iterator& i) const{
+      return d_curr == i.d_curr && d_entries == i.d_entries;
+    }
+
+    bool operator!=(const Iterator& i) const{
+      return !(d_curr == i.d_curr && d_entries == i.d_entries);
+    }
+  }; /* class MatrixVector<T, isRow>::Iterator */
+
+public:
+  MatrixVector(MatrixEntryVector<T>* mev)
+    : d_head(ENTRYID_SENTINEL), d_size(0), d_entries(mev)
+  {}
+
+  MatrixVector(EntryID head, uint32_t size, MatrixEntryVector<T>* mev)
+    : d_head(head), d_size(size), d_entries(mev)
+  {}
+
+  typedef Iterator const_iterator;
+  const_iterator begin() const {
+    return Iterator(d_head, d_entries);
+  }
+  const_iterator end() const {
+    return Iterator(ENTRYID_SENTINEL, d_entries);
+  }
+
+  EntryID getHead() const { return d_head; }
+
+  uint32_t getSize() const { return d_size; }
+
+  void insert(EntryID newId){
+    if(isRow){
+      d_entries->get(newId).setNextRowEntryID(d_head);
+
+      if(d_head != ENTRYID_SENTINEL){
+        d_entries->get(d_head).setPrevRowEntryID(newId);
+      }
+    }else{
+      d_entries->get(newId).setNextColEntryID(d_head);
+
+      if(d_head != ENTRYID_SENTINEL){
+        d_entries->get(d_head).setPrevColEntryID(newId);
+      }
+    }
+
+    d_head = newId;
+    ++d_size;
+  }
+  void remove(EntryID id){
+    Assert(d_size > 0);
+    --d_size;
+    if(isRow){
+      EntryID prevRow = d_entries->get(id).getPrevRowEntryID();
+      EntryID nextRow = d_entries->get(id).getNextRowEntryID();
+
+      if(d_head == id){
+        d_head = nextRow;
+      }
+      if(prevRow != ENTRYID_SENTINEL){
+        d_entries->get(prevRow).setNextRowEntryID(nextRow);
+      }
+      if(nextRow != ENTRYID_SENTINEL){
+        d_entries->get(nextRow).setPrevRowEntryID(prevRow);
+      }
+    }else{
+      EntryID prevCol = d_entries->get(id).getPrevColEntryID();
+      EntryID nextCol = d_entries->get(id).getNextColEntryID();
+
+      if(d_head == id){
+        d_head = nextCol;
+      }
+
+      if(prevCol != ENTRYID_SENTINEL){
+        d_entries->get(prevCol).setNextColEntryID(nextCol);
+      }
+      if(nextCol != ENTRYID_SENTINEL){
+        d_entries->get(nextCol).setPrevColEntryID(prevCol);
+      }
+    }
+  }
+}; /* class MatrixVector<T, isRow> */
+
+template <class T>
+  class RowVector : public MatrixVector<T, true>
+{
+private:
+  typedef MatrixVector<T, true> SuperT;
+public:
+  typedef typename SuperT::const_iterator const_iterator;
+
+  RowVector(MatrixEntryVector<T>* mev) : SuperT(mev){}
+};
+
+template <class T>
+  class ColumnVector : public MatrixVector<T, false>
+{
+private:
+  typedef MatrixVector<T, false> SuperT;
+public:
+  typedef typename SuperT::const_iterator const_iterator;
+
+  ColumnVector(MatrixEntryVector<T>* mev) : SuperT(mev){}
+};
+
+template <class T>
+class Matrix {
+protected:
+
+  typedef MatrixEntry<T> Entry;
+
+  typedef CVC4::theory::arith::RowVector<T> RowVectorT;
+  typedef typename RowVectorT::const_iterator RowIterator;
+
+  typedef CVC4::theory::arith::ColumnVector<T> ColumnVectorT;
+  typedef typename ColumnVectorT::const_iterator ColIterator;
+
+  // RowTable : RowID |-> RowVector
+  typedef std::vector< RowVectorT > RowTable;
+  RowTable d_rows;
+
+  // ColumnTable : ArithVar |-> ColumnVector
+  typedef std::vector< ColumnVectorT > ColumnTable;
+  ColumnTable d_columns;
+
+  /* The merge buffer is used to store a row in order to optimize row addition. */
+  typedef std::pair<EntryID, bool> PosUsedPair;
+  typedef DenseMap< PosUsedPair > RowToPosUsedPairMap;
+  RowToPosUsedPairMap d_mergeBuffer;
+
+  /* The row that is in the merge buffer. */
+  RowIndex d_rowInMergeBuffer;
+
+  uint32_t d_entriesInUse;
+  MatrixEntryVector<T> d_entries;
+
+  T d_zero;
+
+public:
+  /**
+   * Constructs an empty Matrix.
+   */
+  Matrix()
+  : d_rows(),
+    d_columns(),
+    d_mergeBuffer(),
+    d_rowInMergeBuffer(ROW_INDEX_SENTINEL),
+    d_entriesInUse(0),
+    d_entries(),
+    d_zero(0)
+  {}
+
+  Matrix(const T& zero)
+  : d_rows(),
+    d_columns(),
+    d_mergeBuffer(),
+    d_rowInMergeBuffer(ROW_INDEX_SENTINEL),
+    d_entriesInUse(0),
+    d_entries(),
+    d_zero(zero)
+  {}
+
+
+protected:
+
+  void addEntry(RowIndex row, ArithVar col, const T& coeff){
+    Assert(coeff != 0);
+
+    EntryID newId = d_entries.newEntry();
+    Entry& newEntry = d_entries.get(newId);
+    newEntry = Entry(row, col, coeff);
+
+    Assert(newEntry.getCoefficient() != 0);
+
+    Debug("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << std::endl;
+
+    ++d_entriesInUse;
+
+    d_rows[row].insert(newId);
+    d_columns[col].insert(newId);
+  }
+
+  void removeEntry(EntryID id){
+    Assert(d_entriesInUse > 0);
+    --d_entriesInUse;
+
+    Entry& entry = d_entries.get(id);
+
+    RowIndex ridx = entry.getRowIndex();
+    ArithVar col = entry.getColVar();
+
+    Assert(d_rows[ridx].getSize() > 0);
+    Assert(d_columns[col].getSize() > 0);
+
+    d_rows[ridx].remove(id);
+    d_columns[col].remove(id);
+
+    entry.markBlank();
+
+    d_entries.freeEntry(id);
+}
+
+public:
+
+  size_t getNumRows() const {
+    return d_rows.size();
+  }
+
+  size_t getNumColumns() const {
+    return d_columns.size();
+  }
+
+  void increaseSize(){
+    d_columns.push_back(ColumnVector<T>(&d_entries));
+  }
+
+  const RowVector<T>& getRow(RowIndex r) const {
+    Assert(r < d_rows.size());
+    return d_rows[r];
+  }
+
+  const ColumnVector<T>& getColumn(ArithVar v) const {
+    Assert(v < d_columns.size());
+    return d_columns[v];
+  }
+
+  uint32_t getRowLength(RowIndex r) const{
+    return getRow(r).getSize();
+  }
+
+  uint32_t getColLength(ArithVar x) const{
+    return getColumn(x).getSize();
+  }
+
+  /**
+   * Adds a row to the matrix.
+   * The new row is equivalent to:
+   *   \f$\sum_i\f$ coeffs[i] * variables[i]
+   */
+  RowIndex addRow(const std::vector<T>& coeffs,
+                  const std::vector<ArithVar>& variables){
+    RowIndex ridx = d_rows.size();
+    d_rows.push_back(RowVectorT(&d_entries));
+
+    std::vector<Rational>::const_iterator coeffIter = coeffs.begin();
+    std::vector<ArithVar>::const_iterator varsIter = variables.begin();
+    std::vector<ArithVar>::const_iterator varsEnd = variables.end();
+
+    for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
+      const Rational& coeff = *coeffIter;
+      ArithVar var_i = *varsIter;
+      addEntry(ridx, var_i, coeff);
+    }
+
+    return ridx;
+  }
+
+
+  void loadRowIntoBuffer(RowIndex rid){
+    Assert(d_mergeBuffer.empty());
+    Assert(d_rowInMergeBuffer == ROW_INDEX_SENTINEL);
+
+    RowIterator i = getRow(rid).begin(), i_end = getRow(rid).end();
+    for(; i != i_end; ++i){
+      EntryID id = i.getID();
+      const MatrixEntry<T>& entry = *i;
+      ArithVar colVar = entry.getColVar();
+      d_mergeBuffer.set(colVar, std::make_pair(id, false));
+    }
+
+    d_rowInMergeBuffer = rid;
+  }
+
+  void clearBuffer() {
+    Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
+
+    d_rowInMergeBuffer = ROW_INDEX_SENTINEL;
+    d_mergeBuffer.purge();
+  }
+
+  /**  to += mult * buffer. */
+  void rowPlusBufferTimesConstant(RowIndex to, const T& mult){
+    Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
+    Assert(to != ROW_INDEX_SENTINEL);
+
+    Debug("tableau") << "rowPlusRowTimesConstant("
+                     << to << "," << mult << "," << d_rowInMergeBuffer << ")"
+                     << std::endl;
+
+    Assert(debugNoZeroCoefficients(to));
+    Assert(debugNoZeroCoefficients(d_rowInMergeBuffer));
+
+    Assert(mult != 0);
+
+
+    RowIterator i = getRow(to).begin();
+    RowIterator i_end = getRow(to).end();
+    while(i != i_end){
+      EntryID id = i.getID();
+      Entry& entry = d_entries.get(id);
+      ArithVar colVar = entry.getColVar();
+
+      ++i;
+
+      if(d_mergeBuffer.isKey(colVar)){
+        EntryID bufferEntry = d_mergeBuffer[colVar].first;
+        Assert(!d_mergeBuffer[colVar].second);
+        d_mergeBuffer.get(colVar).second = true;
+
+        const Entry& other = d_entries.get(bufferEntry);
+        entry.getCoefficient() += mult * other.getCoefficient();
+
+        if(entry.getCoefficient() == d_zero){
+          removeEntry(id);
+        }
+      }
+    }
+
+    i = getRow(d_rowInMergeBuffer).begin();
+    i_end = getRow(d_rowInMergeBuffer).end();
+
+    for(; i != i_end; ++i){
+      const Entry& entry = *i;
+      ArithVar colVar = entry.getColVar();
+
+      if(d_mergeBuffer[colVar].second){
+        d_mergeBuffer.get(colVar).second = false;
+      }else{
+        Assert(!(d_mergeBuffer[colVar]).second);
+        T newCoeff =  mult * entry.getCoefficient();
+        addEntry(to, colVar, newCoeff);
+      }
+    }
+
+    Assert(mergeBufferIsClear());
+
+    if(Debug.isOn("matrix")) { printMatrix(); }
+  }
+
+  bool mergeBufferIsClear() const{
+    RowToPosUsedPairMap::const_iterator i = d_mergeBuffer.begin();
+    RowToPosUsedPairMap::const_iterator i_end = d_mergeBuffer.end();
+    for(; i != i_end; ++i){
+      RowIndex rid = *i;
+      if(d_mergeBuffer[rid].second){
+        return false;
+      }
+    }
+    return true;
+  }
+
+protected:
+
+  EntryID findOnRow(RowIndex rid, ArithVar column){
+    RowIterator i = d_rows[rid].begin(), i_end = d_rows[rid].end();
+    for(; i != i_end; ++i){
+      EntryID id = i.getID();
+      const MatrixEntry<T>& entry = *i;
+      ArithVar colVar = entry.getColVar();
+
+      if(colVar == column){
+        return id;
+      }
+    }
+    return ENTRYID_SENTINEL;
+  }
+
+  EntryID findOnCol(RowIndex rid, ArithVar column){
+    ColIterator i = d_columns[column].begin(), i_end = d_columns[column].end();
+    for(; i != i_end; ++i){
+      EntryID id = i.getID();
+      const MatrixEntry<T>& entry = *i;
+      RowIndex currRow = entry.getRowIndex();
+
+      if(currRow == rid){
+        return id;
+      }
+    }
+    return ENTRYID_SENTINEL;
+  }
+
+  MatrixEntry<T> d_failedFind;
+public:
+
+  /** If the find fails, isUnused is true on the entry. */
+  const MatrixEntry<T>& findEntry(RowIndex rid, ArithVar col){
+    bool colIsShorter = getColLength(col) < getRowLength(rid);
+    EntryID id = colIsShorter ? findOnCol(rid, col) : findOnRow(rid,col);
+    if(id == ENTRYID_SENTINEL){
+      return d_failedFind;
+    }else{
+      return d_entries.get(id);
+    }
+  }
+
+  /**
+   * Prints the contents of the Matrix to Debug("matrix")
+   */
+  void printMatrix() const {
+    Debug("matrix") << "Matrix::printMatrix"  << std::endl;
+
+    for(RowIndex i = 0, N = d_rows.size(); i < N; ++i){
+      printRow(i);
+    }
+  }
+
+  void printRow(RowIndex rid) const {
+    Debug("matrix") << "{" << rid << ":";
+    const RowVector<T>& row = getRow(rid);
+    RowIterator i = row.begin();
+    RowIterator i_end = row.end();
+    for(; i != i_end; ++i){
+      printEntry(*i);
+      Debug("matrix") << ",";
+    }
+    Debug("matrix") << "}" << std::endl;
+  }
+
+  void printEntry(const MatrixEntry<T>& entry) const {
+    Debug("matrix") << entry.getColVar() << "*" << entry.getCoefficient();
+  }
+
+
+protected:
+
+  // 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);
+  // }
+
+public:
+  uint32_t size() const {
+    return d_entriesInUse;
+  }
+  uint32_t getNumEntriesInTableau() const {
+    return d_entries.size();
+  }
+  uint32_t getEntryCapacity() const {
+    return d_entries.capacity();
+  }
+
+  void removeRow(RowIndex rid){
+    RowIterator i = getRow(rid).begin();
+    RowIterator i_end = getRow(rid).end();
+    for(; i != i_end; ++i){
+      EntryID id = i.getID();
+      removeEntry(id);
+    }
+  }
+
+
+  Node rowAsEquality(RowIndex rid, const ArithVarToNodeMap& map){
+    using namespace CVC4::kind;
+
+    Assert(getRowLength(rid) >= 2);
+
+    std::vector<Node> pairs;
+    for(RowIterator i = getRow(rid); !i.atEnd(); ++i){
+      const Entry& entry = *i;
+      ArithVar colVar = entry.getColVar();
+
+      Node var = (map.find(colVar))->second;
+      Node coeff = mkRationalNode(entry.getCoefficient());
+
+      Node mult = NodeBuilder<2>(MULT) << coeff << var;
+      pairs.push_back(mult);
+    }
+
+    Node sum = Node::null();
+    if(pairs.size() == 1 ){
+      sum = pairs.front();
+    }else{
+      Assert(pairs.size() >= 2);
+      NodeBuilder<> sumBuilder(PLUS);
+      sumBuilder.append(pairs);
+      sum = sumBuilder;
+    }
+    return NodeBuilder<2>(EQUAL) << sum << mkRationalNode(d_zero);
+  }
+
+  double 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_columns.size();
+      uint32_t divisor = (n *(m - n + 1));
+
+      Assert(n >= 1);
+      Assert(m >= n);
+      Assert(divisor > 0);
+      Assert(divisor >= s);
+
+      return (double(s)) / divisor;
+    }
+  }
+
+protected:
+  uint32_t numNonZeroEntries() const { return size(); }
+
+  uint32_t numNonZeroEntriesByRow() const {
+    uint32_t rowSum = 0;
+    for(RowIndex rid = 0, N = d_rows.size(); rid < N; ++rid){
+      rowSum += getRowLength(rid);
+    }
+    return rowSum;
+  }
+
+  uint32_t numNonZeroEntriesByCol() const {
+    uint32_t colSum = 0;
+    for(ArithVar v = 0, N = d_columns.size(); v < N; ++v){
+      colSum += getColLength(v);
+    }
+    return colSum;
+  }
+
+
+  bool debugNoZeroCoefficients(RowIndex ridx){
+    for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
+      const Entry& entry = *i;
+      if(entry.getCoefficient() == 0){
+        return false;
+      }
+    }
+    return true;
+  }
+  bool debugMatchingCountsForRow(RowIndex ridx){
+    for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
+      const Entry& entry = *i;
+      ArithVar colVar = entry.getColVar();
+      uint32_t count = debugCountColLength(colVar);
+      Debug("tableau") << "debugMatchingCountsForRow "
+                       << ridx << ":" << colVar << " " << count
+                       <<" "<< getColLength(colVar) << std::endl;
+      if( count != getColLength(colVar) ){
+        return false;
+      }
+    }
+    return true;
+  }
+
+  uint32_t debugCountColLength(ArithVar var){
+    Debug("tableau") << var << " ";
+    uint32_t count = 0;
+    for(ColIterator i=getColumn(var).begin(); !i.atEnd(); ++i){
+      const Entry& entry = *i;
+      Debug("tableau") << "(" << entry.getRowIndex() << ", " << i.getID() << ") ";
+      ++count;
+    }
+    Debug("tableau") << std::endl;
+    return count;
+  }
+  uint32_t debugCountRowLength(RowIndex ridx){
+    uint32_t count = 0;
+    for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
+      ++count;
+    }
+    return count;
+  }
+
+};/* class Matrix<T> */
+
+
+/**
+ * A Tableau is a Rational matrix that keeps its rows in solved form.
+ * Each row has a basic variable with coefficient -1 that is solved.
+ * Tableau is optimized for pivoting.
+ * The tableau should only be updated via pivot calls.
+ */
+class Tableau : public Matrix<Rational> {
+public:
+private:
+  typedef DenseMap<RowIndex> BasicToRowMap;
+  // Set of all of the basic variables in the tableau.
+  // ArithVarMap<RowIndex> : ArithVar |-> RowIndex
+  BasicToRowMap d_basic2RowIndex;
+  // RowIndex |-> Basic Variable
+  std::vector<ArithVar> d_rowIndex2basic;
+
+public:
+
+  Tableau() : Matrix<Rational>(Rational(0)) {}
+
+  typedef Matrix<Rational>::ColIterator ColIterator;
+  typedef Matrix<Rational>::RowIterator RowIterator;
+  typedef BasicToRowMap::const_iterator BasicIterator;
+
+  typedef MatrixEntry<Rational> Entry;
+
+  bool isBasic(ArithVar v) const{
+    return d_basic2RowIndex.isKey(v);
+  }
+
+  BasicIterator beginBasic() const {
+    return d_basic2RowIndex.begin();
+  }
+  BasicIterator endBasic() const {
+    return d_basic2RowIndex.end();
+  }
+
+  RowIndex basicToRowIndex(ArithVar x) const {
+    return d_basic2RowIndex[x];
+  }
+
+  ArithVar rowIndexToBasic(RowIndex rid) const {
+    Assert(rid < d_rowIndex2basic.size());
+    return d_rowIndex2basic[rid];
+  }
+
+  ColIterator colIterator(ArithVar x) const {
+    return getColumn(x).begin();
+  }
+
+  RowIterator basicRowIterator(ArithVar basic) const {
+    return getRow(basicToRowIndex(basic)).begin();
+  }
+
+  // RowIterator rowIterator(RowIndex r) const {
+  //   return getRow(r).begin();
+  // }
+
+  /**
+   * Adds a row to the tableau.
+   * The new row is equivalent to:
+   *   basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
+   * preconditions:
+   *   basicVar is already declared to be basic
+   *   basicVar does not have a row associated with it in the tableau.
+   *
+   * Note: each variables[i] does not have to be non-basic.
+   * Pivoting will be mimicked if it is basic.
+   */
+  void addRow(ArithVar basicVar,
+              const std::vector<Rational>& coeffs,
+              const std::vector<ArithVar>& variables);
+
+  /**
+   * preconditions:
+   *   x_r is basic,
+   *   x_s is non-basic, and
+   *   a_rs != 0.
+   */
+  void pivot(ArithVar basicOld, ArithVar basicNew);
+
+  void removeBasicRow(ArithVar basic);
+
+
+private:
+  /* Changes the basic variable on the row for basicOld to basicNew. */
+  void rowPivot(ArithVar basicOld, ArithVar basicNew);
+
+};
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 9f48dad77..d3092c044 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -176,8 +176,8 @@ template <bool above>
 ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, SimplexDecisionProcedure::PreferenceFunction pref){
   ArithVar slack = ARITHVAR_SENTINEL;
 
-  for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd();  ++iter){
-    const TableauEntry& entry = *iter;
+  for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd();  ++iter){
+    const Tableau::Entry& entry = *iter;
     ArithVar nonbasic = entry.getColVar();
     if(nonbasic == x_i) continue;
 
@@ -344,7 +344,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
 
     bool useVarOrderPivot = d_pivotsInRound.count(x_i) >=  Options::current()->arithPivotThreshold;
     if(!useVarOrderPivot){
-      d_pivotsInRound.addMultiset(x_i);
+      d_pivotsInRound.add(x_i);
     }
 
 
@@ -476,8 +476,8 @@ Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar
 
   NodeBuilder<> conflict(kind::AND);
   bool anyWeakenings = false;
-  for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){
-    const TableauEntry& entry = *i;
+  for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){
+    const Tableau::Entry& entry = *i;
     ArithVar v = entry.getColVar();
     const Rational& coeff = entry.getCoefficient();
     bool weakening = false;
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 7ad7734c7..6dcfccb8e 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -52,14 +52,14 @@
 
 #include "theory/arith/arithvar.h"
 #include "theory/arith/arith_priority_queue.h"
-#include "theory/arith/arithvar_set.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/arith/tableau.h"
+#include "theory/arith/matrix.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/linear_equality.h"
 
 #include "context/cdlist.h"
 
+#include "util/dense_map.h"
 #include "util/options.h"
 #include "util/stats.h"
 
@@ -98,7 +98,7 @@ private:
   NodeCallBack& d_conflictChannel;
 
   /** Maps a variable to how many times they have been used as a pivot in the simplex search. */
-  ArithVarMultiset d_pivotsInRound;
+  DenseMultiset d_pivotsInRound;
 
   /** Stores to the DeltaRational constant 0. */
   DeltaRational d_DELTA_ZERO;
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
deleted file mode 100644
index 567d8215e..000000000
--- a/src/theory/arith/tableau.cpp
+++ /dev/null
@@ -1,571 +0,0 @@
-/*********************                                                        */
-/*! \file tableau.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-#include "theory/arith/tableau.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
-
-
-/*
-void Tableau::addRow(ArithVar basicVar,
-                     const std::vector<Rational>& coeffs,
-                     const std::vector<ArithVar>& variables){
-
-  Assert(coeffs.size() == variables.size());
-
-  //The new basic variable cannot already be a basic variable
-  Assert(!d_basicVariables.isMember(basicVar));
-  d_basicVariables.add(basicVar);
-  ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount, d_columnMatrix);
-  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
-  vector<ArithVar>::const_iterator varsIter = variables.begin();
-  vector<ArithVar>::const_iterator varsEnd = variables.end();
-
-  for( ; varsIter != varsEnd; ++varsIter){
-    ArithVar var = *varsIter;
-
-    if(d_basicVariables.isMember(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(isBasic(basic));
-
-  ReducedRowVector* row = d_rowsTable[basic];
-
-  d_basicVariables.remove(basic);
-  d_rowsTable[basic] = NULL;
-
-  return row;
-}
-*/
-
-void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic){
-  Assert(isBasic(oldBasic));
-  Assert(!isBasic(newBasic));
-  Assert(mergeBufferIsEmpty());
-
-  Debug("tableau") << "Tableau::pivot(" <<  oldBasic <<", " << newBasic <<")"  << endl;
-
-  rowPivot(oldBasic, newBasic);
-  loadRowIntoMergeBuffer(newBasic);
-
-  ColIterator colIter = colIterator(newBasic);
-  while(!colIter.atEnd()){
-    EntryID id = colIter.getID();
-    TableauEntry& entry = d_entryManager.get(id);
-
-    ++colIter; //needs to be incremented before the variable is removed
-    if(entry.getRowVar() == newBasic){ continue; }
-
-    ArithVar basicTo = entry.getRowVar();
-    Rational coeff = entry.getCoefficient();
-
-    rowPlusRowTimesConstant(basicTo, coeff, newBasic);
-  }
-  emptyRowFromMergeBuffer(newBasic);
-
-  //Clear the column for used for this variable
-
-  Assert(mergeBufferIsEmpty());
-  Assert(!isBasic(oldBasic));
-  Assert(isBasic(newBasic));
-  Assert(getColLength(newBasic) == 1);
-}
-
-Tableau::~Tableau(){}
-
-void Tableau::setColumnUnused(ArithVar v){
-  ColIterator colIter = colIterator(v);
-  while(!colIter.atEnd()){
-    ++colIter;
-  }
-}
-void Tableau::printTableau() const {
-  Debug("tableau") << "Tableau::d_activeRows"  << endl;
-
-  ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic();
-  for(; basicIter != endIter; ++basicIter){
-    ArithVar basic = *basicIter;
-    printRow(basic);
-  }
-}
-
-void Tableau::printRow(ArithVar basic) const {
-  Debug("tableau") << "{" << basic << ":";
-  for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){
-    const TableauEntry& entry = *entryIter;
-    printEntry(entry);
-    Debug("tableau") << ",";
-  }
-  Debug("tableau") << "}" << endl;
-}
-
-void Tableau::printEntry(const TableauEntry& entry) const {
-  Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient();
-}
-
-uint32_t Tableau::numNonZeroEntriesByRow() const {
-  uint32_t rowSum = 0;
-  ArithVarSet::const_iterator i = d_basicVariables.begin(), end = d_basicVariables.end();
-  for(; i != end; ++i){
-    ArithVar basic = *i;
-    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
deleted file mode 100644
index 1fcbdf13d..000000000
--- a/src/theory/arith/tableau.h
+++ /dev/null
@@ -1,409 +0,0 @@
-/*********************                                                        */
-/*! \file tableau.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#include "expr/node.h"
-#include "expr/attribute.h"
-
-#include "theory/arith/arithvar.h"
-#include "theory/arith/arithvar_set.h"
-#include "theory/arith/normal_form.h"
-
-#include <queue>
-#include <vector>
-#include <utility>
-
-#ifndef __CVC4__THEORY__ARITH__TABLEAU_H
-#define __CVC4__THEORY__ARITH__TABLEAU_H
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-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();
-
-  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:
-
-  // VectorHeadTable : ArithVar |-> EntryID of the head of the vector
-  typedef std::vector<EntryID> VectorHeadTable;
-  VectorHeadTable d_rowHeads;
-  VectorHeadTable d_colHeads;
-
-  // 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;
-
-  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_entriesInUse(0) {}
-  ~Tableau();
-
-private:
-  void addEntry(ArithVar row, ArithVar col, const Rational& coeff);
-  void removeEntry(EntryID id);
-
-  template <bool isRowIterator>
-  class Iterator {
-  private:
-    EntryID d_curr;
-    const TableauEntryManager& d_entryManager;
-
-  public:
-    Iterator(EntryID start, const 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());
-      const 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();
-  }
-
-  void increaseSize(){
-    d_basicVariables.increaseSize();
-
-    d_rowHeads.push_back(ENTRYID_SENTINEL);
-    d_colHeads.push_back(ENTRYID_SENTINEL);
-
-    d_colLengths.push_back(0);
-    d_rowLengths.push_back(0);
-
-    d_mergeBuffer.push_back(std::make_pair(ENTRYID_SENTINEL, false));
-  }
-
-  bool isBasic(ArithVar v) const {
-    return d_basicVariables.isMember(v);
-  }
-
-  ArithVarSet::const_iterator beginBasic() const{
-    return d_basicVariables.begin();
-  }
-
-  ArithVarSet::const_iterator endBasic() const{
-    return d_basicVariables.end();
-  }
-
-  RowIterator rowIterator(ArithVar v) const {
-    Assert(v < d_rowHeads.size());
-    EntryID head = d_rowHeads[v];
-    return RowIterator(head, d_entryManager);
-  }
-
-  ColIterator colIterator(ArithVar v) const {
-    Assert(v < d_colHeads.size());
-    EntryID head = d_colHeads[v];
-    return ColIterator(head, d_entryManager);
-  }
-
-
-  uint32_t getRowLength(ArithVar x) const{
-    Assert(x < d_rowLengths.size());
-    return d_rowLengths[x];
-  }
-
-  uint32_t getColLength(ArithVar x) const{
-    Assert(x < d_colLengths.size());
-    return d_colLengths[x];
-  }
-
-  /**
-   * Adds a row to the tableau.
-   * The new row is equivalent to:
-   *   basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
-   * preconditions:
-   *   basicVar is already declared to be basic
-   *   basicVar does not have a row associated with it in the tableau.
-   *
-   * Note: each variables[i] does not have to be non-basic.
-   * Pivoting will be mimicked if it is basic.
-   */
-  void addRow(ArithVar basicVar,
-              const std::vector<Rational>& coeffs,
-              const std::vector<ArithVar>& variables);
-
-  /**
-   * preconditions:
-   *   x_r is basic,
-   *   x_s is non-basic, and
-   *   a_rs != 0.
-   */
-  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);
-
-  EntryID findOnRow(ArithVar basic, ArithVar find);
-  EntryID findOnCol(ArithVar basic, ArithVar find);
-
-  TableauEntry d_failedFind;
-public:
-
-  /** If the find fails, isUnused is true on the entry. */
-  const TableauEntry& findEntry(ArithVar row, ArithVar col);
-
-  /**
-   * Prints the contents of the Tableau to Debug("tableau::print")
-   */
-  void printTableau() const;
-  void printRow(ArithVar basic) const;
-  void printEntry(const TableauEntry& entry) const;
-
-
-private:
-  void loadRowIntoMergeBuffer(ArithVar basic);
-  void emptyRowFromMergeBuffer(ArithVar basic);
-  void clearUsedList();
-
-  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;
-
-
-  bool debugNoZeroCoefficients(ArithVar basic);
-  bool debugMatchingCountsForRow(ArithVar basic);
-  uint32_t debugCountColLength(ArithVar var);
-  uint32_t debugCountRowLength(ArithVar var);
-
-};/* class Tableau */
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__TABLEAU_H */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index bc8861996..e183e0e1b 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -28,13 +28,13 @@
 #include "util/rational.h"
 #include "util/integer.h"
 #include "util/boolean_simplification.h"
+#include "util/dense_map.h"
 
 
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/tableau.h"
-#include "theory/arith/arithvar_set.h"
+#include "theory/arith/matrix.h"
 
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/constraint.h"
@@ -632,10 +632,11 @@ ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){
 
   Tableau::ColIterator basicIter = d_tableau.colIterator(variable);
   for(; !basicIter.atEnd(); ++basicIter){
-    const TableauEntry& entry = *basicIter;
+    const Tableau::Entry& entry = *basicIter;
     Assert(entry.getColVar() == variable);
-    ArithVar basic = entry.getRowVar();
-    uint32_t rowLength = d_tableau.getRowLength(basic);
+    RowIndex ridx = entry.getRowIndex();
+    ArithVar basic = d_tableau.rowIndexToBasic(ridx);
+    uint32_t rowLength = d_tableau.getRowLength(ridx);
     if((rowLength < bestRowLength) ||
        (rowLength == bestRowLength && basic < bestBasic)){
       bestBasic = basic;
@@ -1762,21 +1763,22 @@ void TheoryArith::propagateCandidates(){
 
   if(d_updatedBounds.empty()){ return; }
 
-  PermissiveBackArithVarSet::const_iterator i = d_updatedBounds.begin();
-  PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end();
+  DenseSet::const_iterator i = d_updatedBounds.begin();
+  DenseSet::const_iterator end = d_updatedBounds.end();
   for(; i != end; ++i){
     ArithVar var = *i;
     if(d_tableau.isBasic(var) &&
-       d_tableau.getRowLength(var) <= Options::current()->arithPropagateMaxLength){
+       d_tableau.getRowLength(d_tableau.basicToRowIndex(var)) <= Options::current()->arithPropagateMaxLength){
       d_candidateBasics.softAdd(var);
     }else{
       Tableau::ColIterator basicIter = d_tableau.colIterator(var);
       for(; !basicIter.atEnd(); ++basicIter){
-        const TableauEntry& entry = *basicIter;
-        ArithVar rowVar = entry.getRowVar();
+        const Tableau::Entry& entry = *basicIter;
+        RowIndex ridx = entry.getRowIndex();
+        ArithVar rowVar = d_tableau.rowIndexToBasic(ridx);
         Assert(entry.getColVar() == var);
         Assert(d_tableau.isBasic(rowVar));
-        if(d_tableau.getRowLength(rowVar) <= Options::current()->arithPropagateMaxLength){
+        if(d_tableau.getRowLength(ridx) <= Options::current()->arithPropagateMaxLength){
           d_candidateBasics.softAdd(rowVar);
         }
       }
@@ -1785,7 +1787,8 @@ void TheoryArith::propagateCandidates(){
   d_updatedBounds.purge();
 
   while(!d_candidateBasics.empty()){
-    ArithVar candidate = d_candidateBasics.pop_back();
+    ArithVar candidate = d_candidateBasics.back();
+    d_candidateBasics.pop_back();
     Assert(d_tableau.isBasic(candidate));
     propagateCandidate(candidate);
   }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 3ed1d1941..aa7740c37 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -27,10 +27,11 @@
 #include "context/cdqueue.h"
 #include "expr/node.h"
 
+#include "util/dense_map.h"
+
 #include "theory/arith/arithvar.h"
-#include "theory/arith/arithvar_set.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/arith/tableau.h"
+#include "theory/arith/matrix.h"
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/linear_equality.h"
@@ -380,10 +381,10 @@ private:
   Node AssertDisequality(Constraint constraint);
 
   /** Tracks the bounds that were updated in the current round. */
-  PermissiveBackArithVarSet d_updatedBounds;
+  DenseSet d_updatedBounds;
 
   /** Tracks the basic variables where propagatation might be possible. */
-  PermissiveBackArithVarSet d_candidateBasics;
+  DenseSet d_candidateBasics;
 
   bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
   void clearUpdates(){ d_updatedBounds.purge(); }