branches/arith-indexed-variables merged into the main trunk.

12 files changed, 851 insertions, 551 deletions

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index d9cc5b1a3..b7fc5dcc6 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -340,19 +340,17 @@ public:
   }
 
   void clear() throw(AssertionException) {
-    Debug("gc") << "clearing cdmap " << this << std::endl;
-
-    Debug("gc") << "cdmap " << this << " cleared, emptying trash" << std::endl;
+    Debug("gc") << "clearing cdmap " << this << ", emptying trash" << std::endl;
     emptyTrash();
     Debug("gc") << "done emptying trash for " << this << std::endl;
 
-    for(typename table_type::iterator i = d_map.begin();
-        i != d_map.end();
-        ++i) {
+    for(Element* i = d_first; i != NULL;) {
       // mark it as being a destruction (short-circuit restore())
-      (*i).second->d_map = NULL;
-      if(!(*i).second->d_noTrash) {
-        (*i).second->deleteSelf();
+      Element* thisOne = i;
+      i = i->next();
+      thisOne->d_map = NULL;
+      if(!thisOne->d_noTrash) {
+        thisOne->deleteSelf();
       }
     }
     d_map.clear();
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index ead39082c..665b9be4b 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -22,6 +22,7 @@ libarith_la_SOURCES = \
 	basic.h \
 	slack.h \
 	tableau.h \
+	tableau.cpp \
 	arith_propagator.h \
 	arith_propagator.cpp \
 	theory_arith.h \
diff --git a/src/theory/arith/arith_activity.h b/src/theory/arith/arith_activity.h
index f336237a4..7db3d7d8f 100644
--- a/src/theory/arith/arith_activity.h
+++ b/src/theory/arith/arith_activity.h
@@ -30,27 +30,34 @@ namespace theory {
 namespace arith {
 
 
-struct ArithActivityID {};
-typedef expr::Attribute<ArithActivityID, uint64_t> ArithActivity;
-
-inline void resetActivity(TNode var){
-  var.setAttribute(ArithActivity(), 0);
-}
-inline void initActivity(TNode var){
-  resetActivity(var);
-}
-
-inline uint64_t getActivity(TNode var){
-  return var.getAttribute(ArithActivity());
-}
-
-inline void increaseActivity(TNode var, uint64_t x){
-  Assert(var.hasAttribute(ArithActivity()));
-  uint64_t newValue = x + getActivity(var);
-  var.setAttribute(ArithActivity(), newValue);
-}
-
-const static uint64_t ACTIVITY_THRESHOLD = 100;
+class ActivityMonitor {
+private:
+  std::vector<uint64_t> d_activities;
+
+public:
+  const static uint64_t ACTIVITY_THRESHOLD = 100;
+
+  ActivityMonitor() : d_activities() {}
+
+  void resetActivity(ArithVar var){
+    d_activities[var] = 0;
+  }
+
+  void initActivity(ArithVar var){
+    Assert(var == d_activities.size());
+    d_activities.push_back(0);
+  }
+
+  uint64_t getActivity(ArithVar var) const{
+    return d_activities[var];
+  }
+
+  inline void increaseActivity(ArithVar var, uint64_t x){
+    d_activities[var] += x;
+  }
+
+};
+
 
 }; /* namesapce arith */
 }; /* namespace theory */
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index d2c07900d..4ae0e44ef 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -24,11 +24,27 @@
 
 #include "util/rational.h"
 #include "expr/node.h"
+#include "expr/attribute.h"
+#include <stdint.h>
+#include <limits>
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
+
+typedef uint64_t ArithVar;
+//static const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
+#define ARITHVAR_SENTINEL std::numeric_limits<ArithVar>::max()
+
+struct ArithVarAttrID{};
+typedef expr::Attribute<ArithVarAttrID,ArithVar> ArithVarAttr;
+
+inline ArithVar asArithVar(TNode x){
+  Assert(x.hasAttribute(ArithVarAttr()));
+  return x.getAttribute(ArithVarAttr());
+}
+
 inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
 }
diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h
index 11f0f71f0..c52e0881d 100644
--- a/src/theory/arith/basic.h
+++ b/src/theory/arith/basic.h
@@ -29,22 +29,32 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-struct IsBasicAttrID;
-
-typedef expr::Attribute<IsBasicAttrID, bool> IsBasic;
-
-
-inline bool isBasic(TNode x){
-  return x.getAttribute(IsBasic());
-}
-
-inline void makeBasic(TNode x){
-  return x.setAttribute(IsBasic(), true);
-}
-
-inline void makeNonbasic(TNode x){
-  return x.setAttribute(IsBasic(), false);
-}
+class IsBasicManager {
+private:
+  std::vector<bool> d_basic;
+
+public:
+  IsBasicManager() : d_basic() {}
+
+  void init(ArithVar var, bool value){
+    Assert(var == d_basic.size());
+    d_basic.push_back(value);
+  }
+
+  bool isBasic(ArithVar x) const{
+    return d_basic[x];
+  }
+
+  void makeBasic(ArithVar x){
+    Assert(!isBasic(x));
+    d_basic[x] = true;
+  }
+
+  void makeNonbasic(ArithVar x){
+    Assert(isBasic(x));
+    d_basic[x] = false;
+  }
+};
 
 }; /* namespace arith */
 }; /* namespace theory */
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 7baacd4f5..14c525267 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -244,8 +244,8 @@ Comparison Comparison::parseNormalForm(TNode n) {
 Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right) {
   Assert(isRelationOperator(k));
   if(left.isConstant()) {
-    const Rational& rConst =  left.getNode().getConst<Rational>();
-    const Rational& lConst = right.getNode().getConst<Rational>();
+    const Rational& lConst =  left.getNode().getConst<Rational>();
+    const Rational& rConst = right.getNode().getConst<Rational>();
     bool res = evaluateConstantPredicate(k, lConst, rConst);
     return Comparison(res);
   } else {
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 18993c748..6f0ded9e5 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -28,267 +28,368 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 using namespace CVC4::theory::arith::partial_model;
 
-void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){
+  //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
   Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl;
-  x.setAttribute(partial_model::HasHadABound(), true);
+  //x.setAttribute(partial_model::HasHadABound(), true);
+  d_hasHadABound[x] = true;
 
-  d_UpperBoundMap[x] = r;
+  d_upperBound.set(x,r);
 }
 
-void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-  Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
-  x.setAttribute(partial_model::HasHadABound(), true);
+void ArithPartialModel::setLowerBound(ArithVar x, const DeltaRational& r){
+  //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+  // Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
+//   x.setAttribute(partial_model::HasHadABound(), true);
 
-  d_LowerBoundMap[x] = r;
+//   d_LowerBoundMap[x] = r;
+  d_hasHadABound[x] = true;
+  d_lowerBound.set(x,r);
 }
 
-void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-  Assert(x.hasAttribute(partial_model::Assignment()));
-  Assert(x.hasAttribute(partial_model::SafeAssignment()));
-
-  DeltaRational* curr = x.getAttribute(partial_model::Assignment());
-
-  DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
-  if(saved == NULL){
-    saved = new DeltaRational(*curr);
-    x.setAttribute(partial_model::SafeAssignment(), saved);
+void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){
+  //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+  //Assert(x.hasAttribute(partial_model::Assignment()));
+  //Assert(x.hasAttribute(partial_model::SafeAssignment()));
+
+//   DeltaRational* curr = x.getAttribute(partial_model::Assignment());
+
+//   DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
+//   if(saved == NULL){
+//     saved = new DeltaRational(*curr);
+//     x.setAttribute(partial_model::SafeAssignment(), saved);
+//     d_history.push_back(x);
+//   }
+
+//   *curr = r;
+   Debug("partial_model") << "pm: updating the assignment to" << x
+                          << " now " << r <<endl;
+  if(!d_hasSafeAssignment[x]){
+    d_safeAssignment[x] = d_assignment[x];
+    d_hasSafeAssignment[x] = true;
     d_history.push_back(x);
   }
-
-  *curr = r;
-  Debug("partial_model") << "pm: updating the assignment to" << x
-                         << " now " << r <<endl;
+  d_assignment[x] = r;
 }
-void ArithPartialModel::setAssignment(TNode x, const DeltaRational& safe, const DeltaRational& r){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-  Assert(x.hasAttribute(partial_model::Assignment()));
-  Assert(x.hasAttribute(partial_model::SafeAssignment()));
-
-  DeltaRational* curr = x.getAttribute(partial_model::Assignment());
-  DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
-
+void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
+  // Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+//   Assert(x.hasAttribute(partial_model::Assignment()));
+//   Assert(x.hasAttribute(partial_model::SafeAssignment()));
+
+//   DeltaRational* curr = x.getAttribute(partial_model::Assignment());
+//   DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
+
+
+
+//   if(safe == r){
+//     if(saved != NULL){
+//       x.setAttribute(partial_model::SafeAssignment(), NULL);
+//       delete saved;
+//     }
+//   }else{
+//     if(saved == NULL){
+//       saved = new DeltaRational(safe);
+//       x.setAttribute(partial_model::SafeAssignment(), saved);
+//     }else{
+//       *saved = safe;
+//     }
+//     d_history.push_back(x);
+//   }
+//   *curr = r;
+
+   Debug("partial_model") << "pm: updating the assignment to" << x
+                          << " now " << r <<endl;
   if(safe == r){
-    if(saved != NULL){
-      x.setAttribute(partial_model::SafeAssignment(), NULL);
-      delete saved;
-    }
+    d_hasSafeAssignment[x] = false;
   }else{
-    if(saved == NULL){
-      saved = new DeltaRational(safe);
-      x.setAttribute(partial_model::SafeAssignment(), saved);
-    }else{
-      *saved = safe;
+    d_safeAssignment[x] = safe;
+
+    if(!d_hasSafeAssignment[x]){
+      d_hasSafeAssignment[x] = true;
+      d_history.push_back(x);
     }
-    d_history.push_back(x);
   }
-  *curr = r;
+  d_assignment[x] = r;
+}
 
-  Debug("partial_model") << "pm: updating the assignment to" << x
-                         << " now " << r <<endl;
+bool ArithPartialModel::equalSizes(){
+  return d_mapSize == d_hasHadABound.size() &&
+    d_mapSize == d_hasSafeAssignment.size() &&
+    d_mapSize == d_assignment.size() &&
+    d_mapSize == d_safeAssignment.size() &&
+    d_mapSize == d_upperBound.size() &&
+    d_mapSize == d_lowerBound.size() &&
+    d_mapSize == d_upperConstraint.size() &&
+    d_mapSize == d_lowerConstraint.size();
 }
 
-void ArithPartialModel::initialize(TNode x, const DeltaRational& r){
-   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){
+//    Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+//    Assert(!x.hasAttribute(partial_model::Assignment()));
+//    Assert(!x.hasAttribute(partial_model::SafeAssignment()));
+
+//    DeltaRational* c = new DeltaRational(r);
+//    x.setAttribute(partial_model::Assignment(), c);
+//    x.setAttribute(partial_model::SafeAssignment(), NULL);
+
+//    Debug("partial_model") << "pm: constructing an assignment for " << x
+//                           << " initially " << (*c) <<endl;
 
-   Assert(!x.hasAttribute(partial_model::Assignment()));
-   Assert(!x.hasAttribute(partial_model::SafeAssignment()));
+  Assert(x == d_mapSize);
+  Assert(equalSizes());
+  ++d_mapSize;
 
-   DeltaRational* c = new DeltaRational(r);
-   x.setAttribute(partial_model::Assignment(), c);
-   x.setAttribute(partial_model::SafeAssignment(), NULL);
 
-   Debug("partial_model") << "pm: constructing an assignment for " << x
-                          << " initially " << (*c) <<endl;
+  d_hasHadABound.push_back( false );
+
+  d_hasSafeAssignment.push_back( false );
+  d_assignment.push_back( r );
+  d_safeAssignment.push_back( DeltaRational(0) );
+
+  d_upperBound.push_back( DeltaRational(0) );
+  d_lowerBound.push_back( DeltaRational(0) );
+
+  d_upperConstraint.push_back( TNode::null() );
+  d_lowerConstraint.push_back( TNode::null() );
 }
 
 /** Must know that the bound exists both calling this! */
-DeltaRational ArithPartialModel::getUpperBound(TNode x) const {
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) {
+  Assert(inMaps(x));
+  Assert(!d_upperConstraint[x].isNull());
 
-  CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
-  Assert(i != d_UpperBoundMap.end());
+  return d_upperBound[x];
 
-  return DeltaRational((*i).second);
+//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+//   CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+//   Assert(i != d_UpperBoundMap.end());
+
+//   return DeltaRational((*i).second);
 }
 
-DeltaRational ArithPartialModel::getLowerBound(TNode x) const{
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) {
+  Assert(inMaps(x));
+  Assert(!d_lowerConstraint[x].isNull());
 
-  CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-  Assert(i != d_LowerBoundMap.end());
+  return d_lowerBound[x];
 
-  return DeltaRational((*i).second);
-}
+//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
-DeltaRational ArithPartialModel::getSafeAssignment(TNode x) const{
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-  Assert( x.hasAttribute(SafeAssignment()));
+//   CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+//   Assert(i != d_LowerBoundMap.end());
 
-  DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
-  if(safeAssignment != NULL){
-    return *safeAssignment;
+//   return DeltaRational((*i).second);
+}
+
+const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{
+  Assert(inMaps(x));
+  if(d_hasSafeAssignment[x]){
+    return d_safeAssignment[x];
   }else{
-    return getAssignment(x); //The current assignment is safe.
+    return d_assignment[x];
   }
+//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+//   Assert( x.hasAttribute(SafeAssignment()));
+
+//   DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
+//   if(safeAssignment != NULL){
+//     return *safeAssignment;
+//   }else{
+//     return getAssignment(x); //The current assignment is safe.
+//   }
 }
 
-const DeltaRational& ArithPartialModel::getAssignment(TNode x) const{
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{
+//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
-  DeltaRational* assign;
-  AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
-  return *assign;
+//   DeltaRational* assign;
+//   AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+//   return *assign;
+  Assert(inMaps(x));
+  return d_assignment[x];
 }
 
 
 
-void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+void ArithPartialModel::setLowerConstraint(ArithVar x, TNode constraint){
+//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
   Debug("partial_model") << "setLowerConstraint("
                          << x << ":" << constraint << ")" << endl;
 
-  x.setAttribute(partial_model::LowerConstraint(),constraint);
-}
+//   x.setAttribute(partial_model::LowerConstraint(),constraint);
 
-void ArithPartialModel::setUpperConstraint(TNode x, TNode constraint){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+  Assert(inMaps(x));
+  d_lowerConstraint.set(x,constraint);
 
-  Debug("partial_model") << "setUpperConstraint("
-                         << x << ":" << constraint << ")" << endl;
-
-  x.setAttribute(partial_model::UpperConstraint(),constraint);
 }
 
-TNode ArithPartialModel::getLowerConstraint(TNode x){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
-  TNode ret;
-  AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
-  return ret;
-}
+void ArithPartialModel::setUpperConstraint(ArithVar x, TNode constraint){
+//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
-TNode ArithPartialModel::getUpperConstraint(TNode x){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+  Debug("partial_model") << "setUpperConstraint("
+                         << x << ":" << constraint << ")" << endl;
 
-  TNode ret;
-  AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
-  return ret;
+//   x.setAttribute(partial_model::UpperConstraint(),constraint);
+  Assert(inMaps(x));
+  d_upperConstraint.set(x, constraint);
 }
 
-// TNode CVC4::theory::arith::getLowerConstraint(TNode x){
+TNode ArithPartialModel::getLowerConstraint(ArithVar x){
 //   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
 //   TNode ret;
 //   AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
 //   return ret;
-// }
 
-// TNode CVC4::theory::arith::getUpperConstraint(TNode x){
+  Assert(inMaps(x));
+  Assert(!d_lowerConstraint[x].isNull());
+  return d_lowerConstraint[x];
+}
+
+TNode ArithPartialModel::getUpperConstraint(ArithVar x){
 //   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
 //   TNode ret;
 //   AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
 //   return ret;
-// }
+  Assert(inMaps(x));
+  Assert(!d_upperConstraint[x].isNull());
+  return d_upperConstraint[x];
+}
 
 
-bool ArithPartialModel::belowLowerBound(TNode x, const DeltaRational& c, bool strict){
-  CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-  if(i == d_LowerBoundMap.end()){
+
+bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){
+  if(d_lowerConstraint[x].isNull()){
     // l = -\intfy
     // ? c < -\infty |-  _|_
     return false;
   }
-
-  const DeltaRational& l = (*i).second;
-
   if(strict){
-    return c < l;
+    return c < d_lowerBound[x];
   }else{
-    return c <= l;
+    return c <= d_lowerBound[x];
   }
+//   CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+//   if(i == d_LowerBoundMap.end()){
+//     // l = -\intfy
+//     // ? c < -\infty |-  _|_
+//     return false;
+//   }
+
+//   const DeltaRational& l = (*i).second;
+
+//   if(strict){
+//     return c < l;
+//   }else{
+//     return c <= l;
+//   }
 }
 
-bool ArithPartialModel::aboveUpperBound(TNode x, const DeltaRational& c, bool strict){
-  CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
-  if(i == d_UpperBoundMap.end()){
-    // u = -\intfy
-    // ? u < -\infty |-  _|_
+bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
+  if(d_upperConstraint[x].isNull()){
+    // u = \intfy
+    // ? c > \infty |-  _|_
     return false;
   }
-  const DeltaRational& u = (*i).second;
-
   if(strict){
-    return c > u;
+    return c > d_upperBound[x];
   }else{
-    return c >= u;
+    return c >= d_upperBound[x];
   }
+//   CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+//   if(i == d_UpperBoundMap.end()){
+//     // u = -\intfy
+//     // ? u < -\infty |-  _|_
+//     return false;
+//   }
+//   const DeltaRational& u = (*i).second;
+
+//   if(strict){
+//     return c > u;
+//   }else{
+//     return c >= u;
+//   }
 }
 
-bool ArithPartialModel::hasBounds(TNode x){
+bool ArithPartialModel::hasBounds(ArithVar x){
   return
-    d_UpperBoundMap.find(x) != d_UpperBoundMap.end() ||
-    d_LowerBoundMap.find(x) != d_LowerBoundMap.end();
+    !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull();
+  // return
+//     d_UpperBoundMap.find(x) != d_UpperBoundMap.end() ||
+//     d_LowerBoundMap.find(x) != d_LowerBoundMap.end();
 }
 
-bool ArithPartialModel::strictlyBelowUpperBound(TNode x){
-  DeltaRational* assign;
-  AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
-
-  CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
-  if(i == d_UpperBoundMap.end()){// u = \infty
+bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){
+  Assert(inMaps(x));
+  if(d_upperConstraint[x].isNull()){ // u = \infty
     return true;
   }
+  return d_assignment[x] < d_upperBound[x];
+//   DeltaRational* assign;
+//   AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
 
-  const DeltaRational& u = (*i).second;
-  return (*assign) < u;
-}
+//   CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+//   if(i == d_UpperBoundMap.end()){// u = \infty
+//     return true;
+//   }
 
-bool ArithPartialModel::strictlyAboveLowerBound(TNode x){
-  DeltaRational* assign;
-  AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+//   const DeltaRational& u = (*i).second;
+//   return (*assign) < u;
+}
 
-  CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-  if(i == d_LowerBoundMap.end()){// l = \infty
+bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
+  Assert(inMaps(x));
+  if(d_lowerConstraint[x].isNull()){ // l = -\infty
     return true;
   }
+  return  d_lowerBound[x] < d_assignment[x];
+
+//   DeltaRational* assign;
+//   AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
 
-  const DeltaRational& l = (*i).second;
-  return l < *assign;
+//   CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+//   if(i == d_LowerBoundMap.end()){// l = \infty
+//     return true;
+//   }
+
+//   const DeltaRational& l = (*i).second;
+//   return l < *assign;
 }
 
-bool ArithPartialModel::assignmentIsConsistent(TNode x){
+bool ArithPartialModel::assignmentIsConsistent(ArithVar x){
   const DeltaRational& beta = getAssignment(x);
 
-  bool above_li = !belowLowerBound(x,beta,true);
-  bool below_ui = !aboveUpperBound(x,beta,true);
-
   //l_i <= beta(x_i) <= u_i
-  return  above_li && below_ui;
+  return  !belowLowerBound(x,beta,true) && !aboveUpperBound(x,beta,true);
 }
 
 
 void ArithPartialModel::clearSafeAssignments(bool revert){
 
   for(HistoryList::iterator i = d_history.begin(); i != d_history.end(); ++i){
-    TNode x = *i;
-
-    Assert(x.hasAttribute(SafeAssignment()));
-    Assert(x.hasAttribute(Assignment()));
-
-    DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
+    ArithVar x = *i;
+    Assert(d_hasSafeAssignment[x]);
+    d_hasSafeAssignment[x] = false;
 
     if(revert){
-      DeltaRational* assign = x.getAttribute(Assignment());
-      *assign = *safeAssignment;
+      d_assignment[x] = d_safeAssignment[x];
     }
-    x.setAttribute(partial_model::SafeAssignment(), NULL);
-    delete safeAssignment;
+//     Assert(x.hasAttribute(SafeAssignment()));
+//     Assert(x.hasAttribute(Assignment()));
+
+//     DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
+
+//     if(revert){
+//       DeltaRational* assign = x.getAttribute(Assignment());
+//       *assign = *safeAssignment;
+//     }
+//     x.setAttribute(partial_model::SafeAssignment(), NULL);
+//     delete safeAssignment;
   }
 
   d_history.clear();
@@ -301,26 +402,38 @@ void ArithPartialModel::commitAssignmentChanges(){
   clearSafeAssignments(false);
 }
 
-void ArithPartialModel::printModel(TNode x){
-
+void ArithPartialModel::printModel(ArithVar x){
   Debug("model") << "model" << x << ":"<< getAssignment(x) << " ";
-
-  CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-  if(i != d_LowerBoundMap.end()){
-    DeltaRational l = (*i).second;
-    Debug("model") << l << " ";
-    Debug("model") << getLowerConstraint(x) << " ";
-  }else{
+  if(d_lowerConstraint[x].isNull()){
     Debug("model") << "no lb ";
-  }
-
-  i = d_UpperBoundMap.find(x);
-  if(i != d_UpperBoundMap.end()){
-    DeltaRational u = (*i).second;
-    Debug("model") << u << " ";
-    Debug("model") << getUpperConstraint(x) << " ";
   }else{
+    Debug("model") << getLowerBound(x) << " ";
+    Debug("model") << getLowerConstraint(x) << " ";
+  }
+  if(d_upperConstraint[x].isNull()){
     Debug("model") << "no ub ";
+  }else{
+    Debug("model") << getUpperBound(x) << " ";
+    Debug("model") << getUpperConstraint(x) << " ";
   }
-  Debug("model") << endl;
+//   Debug("model") << "model" << x << ":"<< getAssignment(x) << " ";
+
+//   CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+//   if(i != d_LowerBoundMap.end()){
+//     DeltaRational l = (*i).second;
+//     Debug("model") << l << " ";
+//     Debug("model") << getLowerConstraint(x) << " ";
+//   }else{
+//     Debug("model") << "no lb ";
+//   }
+
+//   i = d_UpperBoundMap.find(x);
+//   if(i != d_UpperBoundMap.end()){
+//     DeltaRational u = (*i).second;
+//     Debug("model") << u << " ";
+//     Debug("model") << getUpperConstraint(x) << " ";
+//   }else{
+//     Debug("model") << "no ub ";
+//   }
+//   Debug("model") << endl;
 }
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index bd945002e..bec703369 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -19,7 +19,8 @@
 
 
 #include "context/context.h"
-#include "context/cdmap.h"
+#include "context/cdvector.h"
+#include "theory/arith/arith_utilities.h"
 #include "theory/arith/delta_rational.h"
 #include "expr/attribute.h"
 #include "expr/node.h"
@@ -34,32 +35,35 @@ namespace theory {
 namespace arith {
 
 namespace partial_model {
-struct DeltaRationalCleanupStrategy{
-  static void cleanup(DeltaRational* dq){
-    Debug("arithgc") << "cleaning up  " << dq << "\n";
-    if(dq != NULL){
-      delete dq;
-    }
-  }
-};
+// struct DeltaRationalCleanupStrategy{
+//   static void cleanup(DeltaRational* dq){
+//     Debug("arithgc") << "cleaning up  " << dq << "\n";
+//     if(dq != NULL){
+//       delete dq;
+//     }
+//   }
+// };
+
+
+// struct AssignmentAttrID {};
+// typedef expr::Attribute<AssignmentAttrID,
+//                         DeltaRational*,
+//                         DeltaRationalCleanupStrategy> Assignment;
 
-struct AssignmentAttrID {};
-typedef expr::Attribute<AssignmentAttrID,
-                        DeltaRational*,
-                        DeltaRationalCleanupStrategy> Assignment;
+
+// struct SafeAssignmentAttrID {};
+// typedef expr::Attribute<SafeAssignmentAttrID,
+//                         DeltaRational*,
+//                         DeltaRationalCleanupStrategy> SafeAssignment;
 
 
-struct SafeAssignmentAttrID {};
-typedef expr::Attribute<SafeAssignmentAttrID,
-                        DeltaRational*,
-                        DeltaRationalCleanupStrategy> SafeAssignment;
 
 /**
  * This defines a context dependent delta rational map.
  * This is used to keep track of the current lower and upper bounds on
  * each variable.  This information is conext dependent.
  */
-typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
+//typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
 /* Side disucssion for why new tables are introduced instead of using the
  * attribute framework.
  * It comes down to that the obvious ways to use the current attribute
@@ -95,20 +99,20 @@ typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
  * Note the strong correspondence between this and LowerBoundMap.
  * This is used during conflict analysis.
  */
-struct LowerConstraintAttrID {};
-typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint;
+// struct LowerConstraintAttrID {};
+// typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint;
 
 /**
  * See the documentation for LowerConstraint.
  */
-struct UpperConstraintAttrID {};
-typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint;
+// struct UpperConstraintAttrID {};
+// typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint;
 
-struct TheoryArithPropagatedID {};
-typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
+// struct TheoryArithPropagatedID {};
+// typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
 
-struct HasHadABoundID {};
-typedef expr::Attribute<HasHadABoundID, bool> HasHadABound;
+// struct HasHadABoundID {};
+// typedef expr::Attribute<HasHadABoundID, bool> HasHadABound;
 
 }; /*namespace partial_model*/
 
@@ -116,36 +120,55 @@ typedef expr::Attribute<HasHadABoundID, bool> HasHadABound;
 
 class ArithPartialModel {
 private:
-  partial_model::CDDRationalMap d_LowerBoundMap;
-  partial_model::CDDRationalMap d_UpperBoundMap;
+
+  unsigned d_mapSize;
+  //Maps from ArithVar -> T
+
+  std::vector<bool> d_hasHadABound;
+
+  std::vector<bool> d_hasSafeAssignment;
+  std::vector<DeltaRational> d_assignment;
+  std::vector<DeltaRational> d_safeAssignment;
+
+  context::CDVector<DeltaRational> d_upperBound;
+  context::CDVector<DeltaRational> d_lowerBound;
+  context::CDVector<TNode> d_upperConstraint;
+  context::CDVector<TNode> d_lowerConstraint;
 
 
   /**
    * List contains all of the variables that have an unsafe assignment.
    */
-  typedef std::vector<TNode> HistoryList;
+  typedef std::vector<ArithVar> HistoryList;
   HistoryList d_history;
 
 public:
 
   ArithPartialModel(context::Context* c):
-    d_LowerBoundMap(c),
-    d_UpperBoundMap(c),
+    d_mapSize(0),
+    d_hasHadABound(),
+    d_hasSafeAssignment(),
+    d_assignment(),
+    d_safeAssignment(),
+    d_upperBound(c, false),
+    d_lowerBound(c, false),
+    d_upperConstraint(c,false),
+    d_lowerConstraint(c,false),
     d_history()
   { }
 
-  void setLowerConstraint(TNode x, TNode constraint);
-  void setUpperConstraint(TNode x, TNode constraint);
-  TNode getLowerConstraint(TNode x);
-  TNode getUpperConstraint(TNode x);
+  void setLowerConstraint(ArithVar x, TNode constraint);
+  void setUpperConstraint(ArithVar x, TNode constraint);
+  TNode getLowerConstraint(ArithVar x);
+  TNode getUpperConstraint(ArithVar x);
 
 
 
   /* Initializes a variable to a safe value.*/
-  void initialize(TNode x, const DeltaRational& r);
+  void initialize(ArithVar x, const DeltaRational& r);
 
   /* Gets the last assignment to a variable that is known to be conistent. */
-  DeltaRational getSafeAssignment(TNode x) const;
+  const DeltaRational& getSafeAssignment(ArithVar x) const;
 
   /* Reverts all variable assignments to their safe values. */
   void revertAssignmentChanges();
@@ -156,41 +179,42 @@ public:
 
 
 
-  void setUpperBound(TNode x, const DeltaRational& r);
-  void setLowerBound(TNode x, const DeltaRational& r);
+  void setUpperBound(ArithVar x, const DeltaRational& r);
+  void setLowerBound(ArithVar x, const DeltaRational& r);
 
   /* Sets an unsafe variable assignment */
-  void setAssignment(TNode x, const DeltaRational& r);
-  void setAssignment(TNode x, const DeltaRational& safe, const DeltaRational& r);
+  void setAssignment(ArithVar x, const DeltaRational& r);
+  void setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r);
 
 
   /** Must know that the bound exists before calling this! */
-  DeltaRational getUpperBound(TNode x) const;
-  DeltaRational getLowerBound(TNode x) const;
-  const DeltaRational& getAssignment(TNode x) const;
+  const DeltaRational& getUpperBound(ArithVar x);
+  const DeltaRational& getLowerBound(ArithVar x);
+  const DeltaRational& getAssignment(ArithVar x) const;
 
 
   /**
    * x <= l
    * ? c < l
    */
-  bool belowLowerBound(TNode x, const DeltaRational& c, bool strict);
+  bool belowLowerBound(ArithVar x, const DeltaRational& c, bool strict);
 
   /**
    * x <= u
    * ? c < u
    */
-  bool aboveUpperBound(TNode x, const DeltaRational& c, bool strict);
+  bool aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict);
 
-  bool strictlyBelowUpperBound(TNode x);
-  bool strictlyAboveLowerBound(TNode x);
-  bool assignmentIsConsistent(TNode x);
+  bool strictlyBelowUpperBound(ArithVar x);
+  bool strictlyAboveLowerBound(ArithVar x);
+  bool assignmentIsConsistent(ArithVar x);
 
-  void printModel(TNode x);
+  void printModel(ArithVar x);
 
-  bool hasBounds(TNode x);
-  bool hasEverHadABound(TNode var){
-    return var.getAttribute(partial_model::HasHadABound());
+  bool hasBounds(ArithVar x);
+
+  bool hasEverHadABound(ArithVar var){
+    return d_hasHadABound[var];
   }
 
 private:
@@ -200,6 +224,13 @@ private:
    * revertAssignmentChanges() and commitAssignmentChanges().
    */
   void clearSafeAssignments(bool revert);
+
+  bool equalSizes();
+
+  bool inMaps(ArithVar x) const{
+    return 0 <= x && x < d_mapSize;
+  }
+
 };
 
 
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
new file mode 100644
index 000000000..e43458a23
--- /dev/null
+++ b/src/theory/arith/tableau.cpp
@@ -0,0 +1,184 @@
+
+#include "theory/arith/tableau.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+Row::Row(ArithVar basic,
+         const std::vector< Rational >& coefficients,
+         const std::vector< ArithVar >& variables):
+  d_x_i(basic),
+  d_coeffs(){
+
+  Assert(coefficients.size() == variables.size() );
+
+  std::vector<Rational>::const_iterator coeffIter = coefficients.begin();
+  std::vector<Rational>::const_iterator coeffEnd = coefficients.end();
+  std::vector<ArithVar>::const_iterator varIter = variables.begin();
+
+  for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){
+    const Rational& coeff = *coeffIter;
+    ArithVar var_i = *varIter;
+
+    Assert(var_i != d_x_i);
+    Assert(!has(var_i));
+    Assert(coeff != Rational(0,1));
+
+    d_coeffs[var_i] = coeff;
+    Assert(d_coeffs[var_i] != Rational(0,1));
+  }
+}
+
+void Row::subsitute(Row& row_s){
+  ArithVar x_s = row_s.basicVar();
+
+  Assert(has(x_s));
+  Assert(x_s != d_x_i);
+
+  Rational zero(0,1);
+
+  Rational a_rs = lookup(x_s);
+  Assert(a_rs != zero);
+  d_coeffs.erase(x_s);
+
+  for(iterator iter = row_s.begin(), iter_end = row_s.end();
+      iter != iter_end; ++iter){
+    ArithVar x_j = iter->first;
+    Rational a_sj = iter->second;
+    a_sj *= a_rs;
+    CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j);
+
+    if(coeff_iter != d_coeffs.end()){
+      coeff_iter->second += a_sj;
+      if(coeff_iter->second == zero){
+        d_coeffs.erase(coeff_iter);
+      }
+    }else{
+      d_coeffs.insert(std::make_pair(x_j,a_sj));
+    }
+  }
+}
+
+void Row::pivot(ArithVar x_j){
+  Rational negInverseA_rs = -(lookup(x_j).inverse());
+  d_coeffs[d_x_i] = Rational(Integer(-1));
+  d_coeffs.erase(x_j);
+
+  d_x_i = x_j;
+
+  for(iterator nonbasicIter = begin(), nonbasicIter_end = end();
+      nonbasicIter != nonbasicIter_end; ++nonbasicIter){
+    nonbasicIter->second *= negInverseA_rs;
+  }
+
+}
+
+void Row::printRow(){
+  Debug("tableau") << d_x_i << " ";
+  for(iterator nonbasicIter = d_coeffs.begin();
+      nonbasicIter != d_coeffs.end();
+      ++nonbasicIter){
+    ArithVar nb = nonbasicIter->first;
+    Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}";
+  }
+  Debug("tableau") << std::endl;
+}
+
+void Tableau::addRow(ArithVar basicVar,
+                     const std::vector<Rational>& coeffs,
+                     const std::vector<ArithVar>& variables){
+
+  Assert(coeffs.size() == variables.size());
+  Assert(d_basicManager.isBasic(basicVar));
+
+  //The new basic variable cannot already be a basic variable
+  Assert(!isActiveBasicVariable(basicVar));
+  d_activeBasicVars.insert(basicVar);
+  Row* row_current = new Row(basicVar,coeffs,variables);
+  d_activeRows[basicVar] = row_current;
+
+  //A variable in the row may have been made non-basic already.
+  //If this is the case we fake pivoting this variable
+  std::vector<Rational>::const_iterator coeffsIter = coeffs.begin();
+  std::vector<Rational>::const_iterator coeffsEnd = coeffs.end();
+
+  std::vector<ArithVar>::const_iterator varsIter = variables.begin();
+
+  for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){
+    ArithVar var = *varsIter;
+
+    if(d_basicManager.isBasic(var)){
+      if(!isActiveBasicVariable(var)){
+        reinjectBasic(var);
+      }
+      Assert(isActiveBasicVariable(var));
+
+      Row* row_var = lookup(var);
+      row_current->subsitute(*row_var);
+    }
+  }
+}
+
+void Tableau::pivot(ArithVar x_r, ArithVar x_s){
+  Assert(d_basicManager.isBasic(x_r));
+  Assert(!d_basicManager.isBasic(x_s));
+
+  RowsTable::iterator ptrRow_r = d_activeRows.find(x_r);
+  Assert(ptrRow_r != d_activeRows.end());
+
+  Row* row_s = (*ptrRow_r).second;
+
+  Assert(row_s->has(x_s));
+  row_s->pivot(x_s);
+
+  d_activeRows.erase(ptrRow_r);
+  d_activeBasicVars.erase(x_r);
+  d_basicManager.makeNonbasic(x_r);
+
+  d_activeRows.insert(std::make_pair(x_s,row_s));
+  d_activeBasicVars.insert(x_s);
+  d_basicManager.makeBasic(x_s);
+
+  for(VarSet::iterator basicIter = begin(), endIter = end();
+      basicIter != endIter; ++basicIter){
+    ArithVar basic = *basicIter;
+    Row* row_k = lookup(basic);
+    if(row_k->has(x_s)){
+      d_activityMonitor.increaseActivity(basic, 30);
+      row_k->subsitute(*row_s);
+    }
+  }
+}
+
+void Tableau::printTableau(){
+  for(VarSet::iterator basicIter = begin(), endIter = end();
+      basicIter != endIter; ++basicIter){
+    ArithVar basic = *basicIter;
+    Row* row_k = lookup(basic);
+    row_k->printRow();
+  }
+  for(RowsTable::iterator basicIter = d_inactiveRows.begin(), endIter =  d_inactiveRows.end();
+      basicIter != endIter; ++basicIter){
+    ArithVar basic = (*basicIter).first;
+    Row* row_k = lookupEjected(basic);
+    row_k->printRow();
+  }
+}
+
+
+void Tableau::updateRow(Row* row){
+  for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){
+    ArithVar var = i->first;
+    ++i;
+    if(d_basicManager.isBasic(var)){
+      Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
+
+      Assert(row_var != row);
+      row->subsitute(*row_var);
+
+      i = row->begin();
+      endIter = row->end();
+    }
+  }
+}
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 768d9f39d..dc2c19936 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -21,8 +21,9 @@
 #include "expr/node.h"
 #include "expr/attribute.h"
 
-#include "theory/arith/basic.h"
+#include "theory/arith/arith_utilities.h"
 #include "theory/arith/arith_activity.h"
+#include "theory/arith/basic.h"
 #include "theory/arith/normal_form.h"
 
 #include <ext/hash_map>
@@ -38,9 +39,9 @@ namespace arith {
 
 
 class Row {
-  TNode d_x_i;
+  ArithVar d_x_i;
 
-  typedef std::map<TNode, Rational> CoefficientTable;
+  typedef std::map<ArithVar, Rational, std::greater<ArithVar> > CoefficientTable;
 
   CoefficientTable d_coeffs;
 
@@ -52,28 +53,10 @@ public:
    * Construct a row equal to:
    *   basic = \sum_{x_i} c_i * x_i
    */
-  Row(TNode basic, const Polynomial& sum):
-    d_x_i(basic),
-    d_coeffs(){
-
-    Assert(d_x_i.getMetaKind() == kind::metakind::VARIABLE);
-
-    for(Polynomial::iterator iter=sum.begin(), end = sum.end(); iter != end; ++iter){
-      const Monomial& mono = *iter;
-
-      Assert(!mono.isConstant());
-
-      TNode coeff = mono.getConstant().getNode();
-      TNode var_i =  mono.getVarList().getNode();
-
-      Assert(coeff.getKind() == kind::CONST_RATIONAL);
+  Row(ArithVar basic,
+      const std::vector< Rational >& coefficients,
+      const std::vector< ArithVar >& variables);
 
-      Assert(!has(var_i));
-      d_coeffs[var_i] = coeff.getConst<Rational>();
-      Assert(coeff.getConst<Rational>() != Rational(0,1));
-      Assert(d_coeffs[var_i] != Rational(0,1));
-    }
-  }
 
   iterator begin(){
     return d_coeffs.begin();
@@ -83,93 +66,53 @@ public:
     return d_coeffs.end();
   }
 
-  TNode basicVar(){
+  ArithVar basicVar(){
     return d_x_i;
   }
 
-  bool has(TNode x_j){
+  bool has(ArithVar x_j){
     CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
     return x_jPos != d_coeffs.end();
   }
 
-  const Rational& lookup(TNode x_j){
+  const Rational& lookup(ArithVar x_j){
     CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
     Assert(x_jPos !=  d_coeffs.end());
     return (*x_jPos).second;
   }
 
-  void pivot(TNode x_j){
-    Rational negInverseA_rs = -(lookup(x_j).inverse());
-    d_coeffs[d_x_i] = Rational(Integer(-1));
-    d_coeffs.erase(x_j);
-
-    d_x_i = x_j;
+  void pivot(ArithVar x_j);
 
-    for(iterator nonbasicIter = begin(), nonbasicIter_end = end();
-        nonbasicIter != nonbasicIter_end; ++nonbasicIter){
-      nonbasicIter->second *= negInverseA_rs;
-    }
-
-  }
+  void subsitute(Row& row_s);
 
-  void subsitute(Row& row_s){
-    TNode x_s = row_s.basicVar();
-
-    Assert(has(x_s));
-    Assert(x_s != d_x_i);
-
-    Rational zero(0,1);
-
-    Rational a_rs = lookup(x_s);
-    Assert(a_rs != zero);
-    d_coeffs.erase(x_s);
-
-    for(iterator iter = row_s.begin(), iter_end = row_s.end();
-        iter != iter_end; ++iter){
-      TNode x_j = iter->first;
-      Rational a_sj = iter->second;
-      a_sj *= a_rs;
-      CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j);
-
-      if(coeff_iter != d_coeffs.end()){
-        coeff_iter->second += a_sj;
-        if(coeff_iter->second == zero){
-          d_coeffs.erase(coeff_iter);
-        }
-      }else{
-        d_coeffs.insert(std::make_pair(x_j,a_sj));
-      }
-    }
-  }
-
-  void printRow(){
-    Debug("tableau") << d_x_i << " ";
-    for(iterator nonbasicIter = d_coeffs.begin();
-        nonbasicIter != d_coeffs.end();
-        ++nonbasicIter){
-      TNode nb = nonbasicIter->first;
-      Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}";
-    }
-    Debug("tableau") << std::endl;
-  }
+  void printRow();
 };
 
 class Tableau {
 public:
-  typedef std::set<TNode> VarSet;
+  typedef std::set<ArithVar> VarSet;
 
 private:
-  typedef __gnu_cxx::hash_map<TNode, Row*, NodeHashFunction> RowsTable;
+  typedef __gnu_cxx::hash_map<ArithVar, Row*> RowsTable;
 
   VarSet d_activeBasicVars;
   RowsTable d_activeRows, d_inactiveRows;
 
+  ActivityMonitor& d_activityMonitor;
+  IsBasicManager& d_basicManager;
+
 
 public:
   /**
    * Constructs an empty tableau.
    */
-  Tableau() : d_activeBasicVars(), d_activeRows(), d_inactiveRows() {}
+  Tableau(ActivityMonitor &am, IsBasicManager& bm) :
+    d_activeBasicVars(),
+    d_activeRows(),
+    d_inactiveRows(),
+    d_activityMonitor(am),
+    d_basicManager(bm)
+  {}
 
   VarSet::iterator begin(){
     return d_activeBasicVars.begin();
@@ -179,45 +122,19 @@ public:
     return d_activeBasicVars.end();
   }
 
-  Row* lookup(TNode var){
+  Row* lookup(ArithVar var){
     Assert(isActiveBasicVariable(var));
     return d_activeRows[var];
   }
 
 private:
-  Row* lookupEjected(TNode var){
+  Row* lookupEjected(ArithVar var){
     Assert(isEjected(var));
     return d_inactiveRows[var];
   }
 public:
 
-  void addRow(TNode eq){
-    TNode var = eq[0];
-    TNode sumNode = eq[1];
-
-    Assert(var.getAttribute(IsBasic()));
-
-    Polynomial sum = Polynomial::parsePolynomial(sumNode);
-
-    //The new basic variable cannot already be a basic variable
-    Assert(!isActiveBasicVariable(var));
-    d_activeBasicVars.insert(var);
-    Row* row_var = new Row(var,sum);
-    d_activeRows[var] = row_var;
-
-    //A variable in the row may have been made non-basic already.
-    //If this is the case we fake pivoting this variable
-    for(Polynomial::iterator sumIter = sum.begin(); sumIter!= sum.end(); ++sumIter){
-      const Monomial& child = *sumIter;
-
-      Assert(!child.isConstant());
-      TNode c = child.getVarList().getNode();
-      if(isActiveBasicVariable(c)){
-        Row* row_c = lookup(c);
-        row_var->subsitute(*row_c);
-      }
-    }
-  }
+  void addRow(ArithVar basicVar, const std::vector<Rational>& coeffs, const std::vector<ArithVar>& variables);
 
   /**
    * preconditions:
@@ -225,47 +142,16 @@ public:
    *   x_s is non-basic, and
    *   a_rs != 0.
    */
-  void pivot(TNode x_r, TNode x_s){
-    RowsTable::iterator ptrRow_r = d_activeRows.find(x_r);
-    Assert(ptrRow_r != d_activeRows.end());
-
-    Row* row_s = (*ptrRow_r).second;
-
-    Assert(row_s->has(x_s));
-    row_s->pivot(x_s);
-
-    d_activeRows.erase(ptrRow_r);
-    d_activeBasicVars.erase(x_r);
-    makeNonbasic(x_r);
-
-    d_activeRows.insert(std::make_pair(x_s,row_s));
-    d_activeBasicVars.insert(x_s);
-    makeBasic(x_s);
-
-    for(VarSet::iterator basicIter = begin(), endIter = end();
-        basicIter != endIter; ++basicIter){
-      TNode basic = *basicIter;
-      Row* row_k = lookup(basic);
-      if(row_k->has(x_s)){
-         increaseActivity(basic, 30);
-        row_k->subsitute(*row_s);
-      }
-    }
-  }
-  void printTableau(){
-    for(VarSet::iterator basicIter = begin(), endIter = end();
-        basicIter != endIter; ++basicIter){
-      TNode basic = *basicIter;
-      Row* row_k = lookup(basic);
-      row_k->printRow();
-    }
-  }
+  void pivot(ArithVar x_r, ArithVar x_s);
+
+  void printTableau();
 
-  bool isEjected(TNode var){
+  bool isEjected(ArithVar var){
     return d_inactiveRows.find(var) != d_inactiveRows.end();
   }
 
-  void ejectBasic(TNode basic){
+  void ejectBasic(ArithVar basic){
+    Assert(d_basicManager.isBasic(basic));
     Assert(isActiveBasicVariable(basic));
 
     Row* row = lookup(basic);
@@ -275,7 +161,8 @@ public:
     d_inactiveRows.insert(std::make_pair(basic, row));
   }
 
-  void reinjectBasic(TNode basic){
+  void reinjectBasic(ArithVar basic){
+    Assert(d_basicManager.isBasic(basic));
     Assert(isEjected(basic));
 
     Row* row = lookupEjected(basic);
@@ -287,25 +174,11 @@ public:
     updateRow(row);
   }
 private:
-  inline bool isActiveBasicVariable(TNode var){
+  inline bool isActiveBasicVariable(ArithVar var){
     return d_activeBasicVars.find(var) != d_activeBasicVars.end();
   }
 
-  void updateRow(Row* row){
-    for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){
-      TNode var = i->first;
-      ++i;
-      if(isBasic(var)){
-        Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
-
-        Assert(row_var != row);
-        row->subsitute(*row_var);
-
-        i = row->begin();
-        endIter = row->end();
-      }
-    }
-  }
+  void updateRow(Row* row);
 };
 
 }; /* namespace arith  */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 41882e87c..be40472b6 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -56,14 +56,15 @@ TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) :
   Theory(id, c, out),
   d_constants(NodeManager::currentNM()),
   d_partialModel(c),
+  d_basicManager(),
+  d_activityMonitor(),
   d_diseq(c),
+  d_tableau(d_activityMonitor, d_basicManager),
   d_nextRewriter(&d_constants),
   d_propagator(c),
   d_statistics()
-{
-  uint64_t ass_id = partial_model::Assignment::getId();
-  Debug("arithsetup") << "Assignment: " << ass_id << std::endl;
-}
+{}
+
 TheoryArith::~TheoryArith(){
   for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
     Node var = *i;
@@ -76,13 +77,17 @@ TheoryArith::Statistics::Statistics():
   d_statUpdates("theory::arith::updates",0),
   d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
   d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
-  d_statUpdateConflicts("theory::arith::UpdateConflicts", 0)
+  d_statUpdateConflicts("theory::arith::UpdateConflicts", 0),
+  d_statUserVariables("theory::arith::UserVariables", 0),
+  d_statSlackVariables("theory::arith::SlackVariables", 0)
 {
   StatisticsRegistry::registerStat(&d_statPivots);
   StatisticsRegistry::registerStat(&d_statUpdates);
   StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
   StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
   StatisticsRegistry::registerStat(&d_statUpdateConflicts);
+  StatisticsRegistry::registerStat(&d_statUserVariables);
+  StatisticsRegistry::registerStat(&d_statSlackVariables);
 }
 
 TheoryArith::Statistics::~Statistics(){
@@ -91,6 +96,8 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
   StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
   StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
+  StatisticsRegistry::unregisterStat(&d_statUserVariables);
+  StatisticsRegistry::unregisterStat(&d_statSlackVariables);
 }
 
 
@@ -117,40 +124,40 @@ bool isNormalAtom(TNode n){
 }
 
 
-bool TheoryArith::shouldEject(TNode var){
+bool TheoryArith::shouldEject(ArithVar var){
   if(d_partialModel.hasBounds(var)){
     return false;
   }else if(d_tableau.isEjected(var)) {
     return false;
   }else if(!d_partialModel.hasEverHadABound(var)){
     return true;
-  }else if(getActivity(var) >= ACTIVITY_THRESHOLD){
+  }else if(d_activityMonitor.getActivity(var) >= ActivityMonitor::ACTIVITY_THRESHOLD){
     return true;
   }
   return false;
 }
 
-TNode TheoryArith::findBasicRow(TNode variable){
+ArithVar TheoryArith::findBasicRow(ArithVar variable){
   for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end();
       ++basicIter){
-    TNode x_j = *basicIter;
+    ArithVar x_j = *basicIter;
     Row* row_j = d_tableau.lookup(x_j);
 
     if(row_j->has(variable)){
       return x_j;
     }
   }
-  return TNode::null();
+  return ARITHVAR_SENTINEL;
 }
 
 void TheoryArith::ejectInactiveVariables(){
   Debug("decay") << "begin ejectInactiveVariables()" << endl;
-  for(std::vector<Node>::iterator i = d_variables.begin(),
-        end = d_variables.end(); i != end; ++i){
-    TNode variable = *i;
+  for(ArithVar variable = 0, end = d_variables.size(); variable != end; ++variable){
+    //TNode var = *i;
+    //ArithVar variable = asArithVar(var);
     if(shouldEject(variable)){
-      if(isBasic(variable)){
+      if(d_basicManager.isBasic(variable)){
         Debug("decay") << "ejecting basic " << variable << endl;;
         d_tableau.ejectBasic(variable);
       }
@@ -158,7 +165,7 @@ void TheoryArith::ejectInactiveVariables(){
   }
 }
 
-void TheoryArith::reinjectVariable(TNode x){
+void TheoryArith::reinjectVariable(ArithVar x){
   d_tableau.reinjectBasic(x);
 
 
@@ -184,9 +191,9 @@ void TheoryArith::preRegisterTerm(TNode n) {
     d_out->augmentingLemma(eagerSplit);
   }
 
-  if(n.getMetaKind() == metakind::VARIABLE){
-
-    setupVariable(n);
+  if(isTheoryLeaf(n)){
+    ArithVar varN = requestArithVar(n,false);
+    setupInitialValue(varN);
   }
 
 
@@ -210,38 +217,81 @@ void TheoryArith::preRegisterTerm(TNode n) {
   Debug("arith_preregister") << "end arith::preRegisterTerm("<< n <<")"<< endl;
 }
 
+
+
+void TheoryArith::checkBasicVariable(ArithVar basic){
+  Assert(d_basicManager.isBasic(basic));
+  if(!d_partialModel.assignmentIsConsistent(basic)){
+    d_possiblyInconsistent.push(basic);
+  }
+}
+
+bool TheoryArith::isTheoryLeaf(TNode x) const{
+  return x.getMetaKind() == kind::metakind::VARIABLE;
+}
+
+ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
+  Assert(isTheoryLeaf(x));
+  Assert(!x.hasAttribute(ArithVarAttr()));
+
+  ArithVar varX = d_variables.size();
+  d_variables.push_back(Node(x));
+
+  x.setAttribute(ArithVarAttr(), varX);
+
+
+  d_activityMonitor.initActivity(varX);
+  d_basicManager.init(varX, basic);
+
+  Debug("arith::arithvar") << x << " |-> " << varX << endl;
+
+  return varX;
+}
+
+void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::vector<ArithVar>& variables) const{
+  for(Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i){
+    const Monomial& mono = *i;
+    const Constant& constant = mono.getConstant();
+    const VarList& variable = mono.getVarList();
+
+    Node n = variable.getNode();
+
+    Assert(isTheoryLeaf(n));
+    Assert(n.hasAttribute(ArithVarAttr()));
+
+    ArithVar av = n.getAttribute(ArithVarAttr());
+
+    coeffs.push_back(constant.getValue());
+    variables.push_back(av);
+  }
+}
+
 void TheoryArith::setupSlack(TNode left){
+
   TypeNode real_type = NodeManager::currentNM()->realType();
   Node slack = NodeManager::currentNM()->mkVar(real_type);
-
   left.setAttribute(Slack(), slack);
-  makeBasic(slack);
 
-  Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, slack, left);
+  ArithVar varSlack = requestArithVar(slack, true);
 
-  d_tableau.addRow(eq);
+  Polynomial polyLeft = Polynomial::parsePolynomial(left);
 
-  setupVariable(slack);
-}
+  vector<ArithVar> variables;
+  vector<Rational> coefficients;
 
+  asVectors(polyLeft, coefficients, variables);
 
-void TheoryArith::checkBasicVariable(TNode basic){
-  Assert(isBasic(basic));
-  if(!d_partialModel.assignmentIsConsistent(basic)){
-    d_possiblyInconsistent.push(basic);
-  }
+  d_tableau.addRow(varSlack, coefficients, variables);
+
+  setupInitialValue(varSlack);
 }
 
 /* Requirements:
  * For basic variables the row must have been added to the tableau.
  */
-void TheoryArith::setupVariable(TNode x){
-  Assert(x.getMetaKind() == kind::metakind::VARIABLE);
-  d_variables.push_back(Node(x));
-
-  initActivity(x);
+void TheoryArith::setupInitialValue(ArithVar x){
 
-  if(!isBasic(x)){
+  if(!d_basicManager.isBasic(x)){
     d_partialModel.initialize(x,d_constants.d_ZERO_DELTA);
   }else{
     //If the variable is basic, assertions may have already happened and updates
@@ -270,13 +320,13 @@ void TheoryArith::setupVariable(TNode x){
 /**
  * Computes the value of a basic variable using the current assignment.
  */
-DeltaRational TheoryArith::computeRowValueUsingAssignment(TNode x){
-  Assert(isBasic(x));
+DeltaRational TheoryArith::computeRowValueUsingAssignment(ArithVar x){
+  Assert(d_basicManager.isBasic(x));
   DeltaRational sum = d_constants.d_ZERO_DELTA;
 
   Row* row = d_tableau.lookup(x);
   for(Row::iterator i = row->begin(); i != row->end();++i){
-    TNode nonbasic = i->first;
+    ArithVar nonbasic = i->first;
     const Rational& coeff = i->second;
     const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic);
     sum = sum + (assignment * coeff);
@@ -287,13 +337,13 @@ DeltaRational TheoryArith::computeRowValueUsingAssignment(TNode x){
 /**
  * Computes the value of a basic variable using the current assignment.
  */
-DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){
-  Assert(isBasic(x));
+DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(ArithVar x){
+  Assert(d_basicManager.isBasic(x));
   DeltaRational sum = d_constants.d_ZERO_DELTA;
 
   Row* row = d_tableau.lookup(x);
   for(Row::iterator i = row->begin(); i != row->end();++i){
-    TNode nonbasic = i->first;
+    ArithVar nonbasic = i->first;
     const Rational& coeff = i->second;
     const DeltaRational& assignment = d_partialModel.getSafeAssignment(nonbasic);
     sum = sum + (assignment * coeff);
@@ -311,13 +361,14 @@ void TheoryArith::registerTerm(TNode tn){
 
 /* procedure AssertUpper( x_i <= c_i) */
 bool TheoryArith::AssertUpper(TNode n, TNode original){
-  TNode x_i = n[0];
+  TNode nodeX_i = n[0];
+  ArithVar x_i = nodeX_i.getAttribute(ArithVarAttr());
   Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
   DeltaRational c_i(n[1].getConst<Rational>(), dcoeff);
 
 
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
-  if(isBasic(x_i) && d_tableau.isEjected(x_i)){
+  if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
     reinjectVariable(x_i);
   }
 
@@ -336,9 +387,9 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
 
-  resetActivity(x_i);
+  d_activityMonitor.resetActivity(x_i);
 
-  if(!isBasic(x_i)){
+  if(!d_basicManager.isBasic(x_i)){
     if(d_partialModel.getAssignment(x_i) > c_i){
       update(x_i, c_i);
     }
@@ -351,13 +402,14 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){
 
 /* procedure AssertLower( x_i >= c_i ) */
 bool TheoryArith::AssertLower(TNode n, TNode original){
-  TNode x_i = n[0];
+  TNode nodeX_i = n[0];
+  ArithVar x_i = nodeX_i.getAttribute(ArithVarAttr());
   Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
   DeltaRational c_i(n[1].getConst<Rational>(),dcoeff);
 
   Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
 
-  if(isBasic(x_i) && d_tableau.isEjected(x_i)){
+  if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
     reinjectVariable(x_i);
   }
 
@@ -375,9 +427,9 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
 
   d_partialModel.setLowerConstraint(x_i,original);
   d_partialModel.setLowerBound(x_i, c_i);
-  resetActivity(x_i);
+  d_activityMonitor.resetActivity(x_i);
 
-  if(!isBasic(x_i)){
+  if(!d_basicManager.isBasic(x_i)){
     if(d_partialModel.getAssignment(x_i) < c_i){
       update(x_i, c_i);
     }
@@ -391,12 +443,13 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
 /* procedure AssertLower( x_i == c_i ) */
 bool TheoryArith::AssertEquality(TNode n, TNode original){
   Assert(n.getKind() == EQUAL);
-  TNode x_i = n[0];
+  TNode nodeX_i = n[0];
+  ArithVar x_i = nodeX_i.getAttribute(ArithVarAttr());
   DeltaRational c_i(n[1].getConst<Rational>());
 
   Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
 
-  if(isBasic(x_i) && d_tableau.isEjected(x_i)){
+  if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){
     reinjectVariable(x_i);
   }
 
@@ -428,9 +481,9 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){
 
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
-  resetActivity(x_i);
+  d_activityMonitor.resetActivity(x_i);
 
-  if(!isBasic(x_i)){
+  if(!d_basicManager.isBasic(x_i)){
     if(!(d_partialModel.getAssignment(x_i) == c_i)){
       update(x_i, c_i);
     }
@@ -440,8 +493,8 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){
 
   return false;
 }
-void TheoryArith::update(TNode x_i, DeltaRational& v){
-  Assert(!isBasic(x_i));
+void TheoryArith::update(ArithVar x_i, DeltaRational& v){
+  Assert(!d_basicManager.isBasic(x_i));
   DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
   ++(d_statistics.d_statUpdates);
 
@@ -452,7 +505,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
   for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end();
       ++basicIter){
-    TNode x_j = *basicIter;
+    ArithVar x_j = *basicIter;
     Row* row_j = d_tableau.lookup(x_j);
 
     if(row_j->has(x_i)){
@@ -462,7 +515,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
       DeltaRational  nAssignment = assignment+(diff * a_ji);
       d_partialModel.setAssignment(x_j, nAssignment);
 
-      increaseActivity(x_j, 1);
+      d_activityMonitor.increaseActivity(x_j, 1);
 
       checkBasicVariable(x_j);
     }
@@ -475,7 +528,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
   }
 }
 
-void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
+void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
   Assert(x_i != x_j);
 
   Row* row_i = d_tableau.lookup(x_i);
@@ -496,7 +549,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
   for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end();
       ++basicIter){
-    TNode x_k = *basicIter;
+    ArithVar x_k = *basicIter;
     Row* row_k = d_tableau.lookup(x_k);
 
     if(x_k != x_i && row_k->has(x_j)){
@@ -504,7 +557,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
       DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
       d_partialModel.setAssignment(x_k, nextAssignment);
 
-      increaseActivity(x_j, 1);
+      d_activityMonitor.increaseActivity(x_j, 1);
 
       checkBasicVariable(x_k);
     }
@@ -520,15 +573,15 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
   }
 }
 
-TNode TheoryArith::selectSmallestInconsistentVar(){
+ArithVar TheoryArith::selectSmallestInconsistentVar(){
   Debug("arith_update") << "selectSmallestInconsistentVar()" << endl;
   Debug("arith_update") << "possiblyInconsistent.size()"
                         << d_possiblyInconsistent.size() << endl;
 
   while(!d_possiblyInconsistent.empty()){
-    TNode var = d_possiblyInconsistent.top();
+    ArithVar var = d_possiblyInconsistent.top();
     Debug("arith_update") << "possiblyInconsistent var" << var << endl;
-    if(isBasic(var)){
+    if(d_basicManager.isBasic(var)){
       if(!d_partialModel.assignmentIsConsistent(var)){
         return var;
       }
@@ -541,7 +594,7 @@ TNode TheoryArith::selectSmallestInconsistentVar(){
         basicIter != d_tableau.end();
         ++basicIter){
 
-      TNode basic = *basicIter;
+      ArithVar basic = *basicIter;
       Assert(d_partialModel.assignmentIsConsistent(basic));
       if(!d_partialModel.assignmentIsConsistent(basic)){
         return basic;
@@ -549,15 +602,15 @@ TNode TheoryArith::selectSmallestInconsistentVar(){
     }
   }
 
-  return TNode::null();
+  return ARITHVAR_SENTINEL;
 }
 
 template <bool above>
-TNode TheoryArith::selectSlack(TNode x_i){
+ArithVar TheoryArith::selectSlack(ArithVar x_i){
    Row* row_i = d_tableau.lookup(x_i);
 
   for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
-    TNode nonbasic = nbi->first;
+    ArithVar nonbasic = nbi->first;
     const Rational& a_ij = nbi->second;
     int cmp = a_ij.cmp(d_constants.d_ZERO);
     if(above){ // beta(x_i) > u_i
@@ -574,7 +627,7 @@ TNode TheoryArith::selectSlack(TNode x_i){
       }
     }
   }
-  return TNode::null();
+  return ARITHVAR_SENTINEL;
 }
 
 
@@ -586,9 +639,9 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
   while(true){
     if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
 
-    TNode x_i = selectSmallestInconsistentVar();
+    ArithVar x_i = selectSmallestInconsistentVar();
     Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
-    if(x_i == Node::null()){
+    if(x_i == ARITHVAR_SENTINEL){
       Debug("arith_update") << "No inconsistent variables" << endl;
       return Node::null(); //sat
     }
@@ -601,8 +654,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
 
     if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
       DeltaRational l_i = d_partialModel.getLowerBound(x_i);
-      TNode x_j = selectSlackBelow(x_i);
-      if(x_j == TNode::null() ){
+      ArithVar x_j = selectSlackBelow(x_i);
+      if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         return generateConflictBelow(x_i); //unsat
       }
@@ -610,8 +663,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
 
     }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
       DeltaRational u_i = d_partialModel.getUpperBound(x_i);
-      TNode x_j = selectSlackAbove(x_i);
-      if(x_j == TNode::null() ){
+      ArithVar x_j = selectSlackAbove(x_i);
+      if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         return generateConflictAbove(x_i); //unsat
       }
@@ -620,7 +673,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
   }
 }
 
-Node TheoryArith::generateConflictAbove(TNode conflictVar){
+Node TheoryArith::generateConflictAbove(ArithVar conflictVar){
+
   Row* row_i = d_tableau.lookup(conflictVar);
 
   NodeBuilder<> nb(kind::AND);
@@ -634,7 +688,7 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){
   nb << bound;
 
   for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
-    TNode nonbasic = nbi->first;
+    ArithVar nonbasic = nbi->first;
     const Rational& a_ij = nbi->second;
 
     Assert(a_ij != d_constants.d_ZERO);
@@ -657,7 +711,7 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){
   return conflict;
 }
 
-Node TheoryArith::generateConflictBelow(TNode conflictVar){
+Node TheoryArith::generateConflictBelow(ArithVar conflictVar){
   Row* row_i = d_tableau.lookup(conflictVar);
 
   NodeBuilder<> nb(kind::AND);
@@ -670,7 +724,7 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){
   nb << bound;
 
   for(Row::iterator nbi = row_i->begin(); nbi != row_i->end(); ++nbi){
-    TNode nonbasic = nbi->first;
+    ArithVar nonbasic = nbi->first;
     const Rational& a_ij = nbi->second;
 
     Assert(a_ij != d_constants.d_ZERO);
@@ -801,26 +855,23 @@ void TheoryArith::check(Effort level){
   if(Debug.isOn("arith::print_model")) {
     Debug("arith::print_model") << "Model:" << endl;
 
-    for (unsigned i = 0; i < d_variables.size(); ++ i) {
+    for (ArithVar i = 0; i < d_variables.size(); ++ i) {
       Debug("arith::print_model") << d_variables[i] << " : " <<
-        d_partialModel.getAssignment(d_variables[i]);
-      if(isBasic(d_variables[i]))
+        d_partialModel.getAssignment(i);
+      if(d_basicManager.isBasic(i))
         Debug("arith::print_model") << " (basic)";
       Debug("arith::print_model") << endl;
     }
   }
   if(Debug.isOn("arith::print_assertions")) {
     Debug("arith::print_assertions") << "Assertions:" << endl;
-    for (unsigned i = 0; i < d_variables.size(); ++ i) {
-      Node x = d_variables[i];
-      if (x.hasAttribute(partial_model::LowerConstraint())) {
-        Node constr = d_partialModel.getLowerConstraint(x);
-        Debug("arith::print_assertions") << constr.toString() << endl;
-      }
-      if (x.hasAttribute(partial_model::UpperConstraint())) {
-        Node constr = d_partialModel.getUpperConstraint(x);
-        Debug("arith::print_assertions") << constr.toString() << endl;
-      }
+    for (ArithVar i = 0; i < d_variables.size(); ++ i) {
+      Node lConstr = d_partialModel.getLowerConstraint(i);
+      Debug("arith::print_assertions") << lConstr.toString() << endl;
+
+      Node uConstr = d_partialModel.getUpperConstraint(i);
+      Debug("arith::print_assertions") << uConstr.toString() << endl;
+
     }
   }
 }
@@ -836,14 +887,14 @@ void TheoryArith::checkTableau(){
 
   for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end(); ++basicIter){
-    TNode basic = *basicIter;
+    ArithVar basic = *basicIter;
     Row* row_k = d_tableau.lookup(basic);
     DeltaRational sum;
     Debug("paranoid:check_tableau") << "starting row" << basic << endl;
     for(Row::iterator nonbasicIter = row_k->begin();
         nonbasicIter != row_k->end();
         ++nonbasicIter){
-      TNode nonbasic = nonbasicIter->first;
+      ArithVar nonbasic = nonbasicIter->first;
       const Rational& coeff = nonbasicIter->second;
       DeltaRational beta = d_partialModel.getAssignment(nonbasic);
       Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 450d5c608..cbfdf27f3 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -26,6 +26,9 @@
 #include "context/cdlist.h"
 #include "expr/node.h"
 
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/basic.h"
+#include "theory/arith/arith_activity.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
 #include "theory/arith/next_arith_rewriter.h"
@@ -55,12 +58,9 @@ private:
   std::vector<Node> d_splits;
   //This stores the eager splits sent out of the theory.
 
-  std::vector<Node> d_variables;
-  // Currently forces every variable and skolem constant that
-  // can hit the tableau to stay alive forever!
-
   /* Chopping block ends */
 
+  std::vector<Node> d_variables;
 
   /**
    * Priority Queue of the basic variables that may be inconsistent.
@@ -69,7 +69,7 @@ private:
    * basic variable. This is only required to be a superset though so its
    * contents must be checked to still be basic and inconsistent.
    */
-  std::priority_queue<Node> d_possiblyInconsistent;
+  std::priority_queue<ArithVar> d_possiblyInconsistent;
 
   /** Stores system wide constants to avoid unnessecary reconstruction. */
   ArithConstants d_constants;
@@ -80,6 +80,8 @@ private:
    */
   ArithPartialModel d_partialModel;
 
+  IsBasicManager d_basicManager;
+  ActivityMonitor d_activityMonitor;
 
   /**
    * List of all of the inequalities asserted in the current context.
@@ -131,6 +133,9 @@ public:
   std::string identify() const { return std::string("TheoryArith"); }
 
 private:
+
+  bool isTheoryLeaf(TNode x) const;
+
   /**
    * Assert*(n, orig) takes an bound n that is implied by orig.
    * and asserts that as a new bound if it is tighter than the current bound
@@ -155,14 +160,14 @@ private:
    * Updates the assignment of a nonbasic variable x_i to v.
    * Also updates the assignment of basic variables accordingly.
    */
-  void update(TNode x_i, DeltaRational& v);
+  void update(ArithVar x_i, DeltaRational& v);
 
   /**
    * Updates the value of a basic variable x_i to v,
    * and then pivots x_i with the nonbasic variable in its row x_j.
    * Updates the assignment of the other basic variables accordingly.
    */
-  void pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v);
+  void pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v);
 
   /**
    * Tries to update the assignments of variables such that all of the
@@ -193,45 +198,51 @@ private:
    * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j)
    * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
    */
-  template <bool above>
-  TNode selectSlack(TNode x_i);
+  template <bool above>  ArithVar selectSlack(ArithVar x_i);
 
-  TNode selectSlackBelow(TNode x_i) { return selectSlack<false>(x_i); }
-  TNode selectSlackAbove(TNode x_i) { return selectSlack<true>(x_i);  }
+  ArithVar selectSlackBelow(ArithVar x_i) { return selectSlack<false>(x_i); }
+  ArithVar selectSlackAbove(ArithVar x_i) { return selectSlack<true>(x_i);  }
 
   /**
    * Returns the smallest basic variable whose assignment is not consistent
    * with its upper and lower bounds.
    */
-  TNode selectSmallestInconsistentVar();
+  ArithVar selectSmallestInconsistentVar();
 
   /**
    * Given a non-basic variable that is know to not be updatable
    * to a consistent value, construct and return a conflict.
    * Follows section 4.2 in the CAV06 paper.
    */
-  Node generateConflictAbove(TNode conflictVar);
-  Node generateConflictBelow(TNode conflictVar);
+  Node generateConflictAbove(ArithVar conflictVar);
+  Node generateConflictBelow(ArithVar conflictVar);
 
 
+  /**
+   * This requests a new unique ArithVar value for x.
+   * This also does initial (not context dependent) set up for a variable,
+   * except for setting up the initial.
+   */
+  ArithVar requestArithVar(TNode x, bool basic);
+
   /** Initial (not context dependent) sets up for a variable.*/
-  void setupVariable(TNode x);
+  void setupInitialValue(ArithVar x);
 
   /** Initial (not context dependent) sets up for a new slack variable.*/
   void setupSlack(TNode left);
 
 
   /** Computes the value of a row in the tableau using the current assignment.*/
-  DeltaRational computeRowValueUsingAssignment(TNode x);
+  DeltaRational computeRowValueUsingAssignment(ArithVar x);
 
   /** Computes the value of a row in the tableau using the safe assignment.*/
-  DeltaRational computeRowValueUsingSavedAssignment(TNode x);
+  DeltaRational computeRowValueUsingSavedAssignment(ArithVar x);
 
   /** Checks to make sure the assignment is consistent with the tableau. */
   void checkTableau();
 
   /** Check to make sure all of the basic variables are within their bounds. */
-  void checkBasicVariable(TNode basic);
+  void checkBasicVariable(ArithVar basic);
 
   /**
    * Handles the case splitting for check() for a new assertion.
@@ -239,20 +250,25 @@ private:
    */
   bool assertionCases(TNode original, TNode assertion);
 
-  TNode findBasicRow(TNode variable);
-  bool shouldEject(TNode var);
+  ArithVar findBasicRow(ArithVar variable);
+  bool shouldEject(ArithVar var);
   void ejectInactiveVariables();
-  void reinjectVariable(TNode x);
+  void reinjectVariable(ArithVar x);
 
   //TODO get rid of this!
   Node simulatePreprocessing(TNode n);
 
+  void asVectors(Polynomial& p,
+                 std::vector<Rational>& coeffs,
+                 std::vector<ArithVar>& variables) const;
+
 
   /** These fields are designed to be accessable to TheoryArith methods. */
   class Statistics {
   public:
     IntStat d_statPivots, d_statUpdates, d_statAssertUpperConflicts;
     IntStat d_statAssertLowerConflicts, d_statUpdateConflicts;
+    IntStat d_statUserVariables, d_statSlackVariables;
 
     Statistics();
     ~Statistics();