Factors out the QF_LRA decision procedure from TheoryArith and puts this into its own class SimplexDecisionProcedure. Implements about 1/2 of the pivoting rule from Alberto's thesis (section2.5.3).

5 files changed, 781 insertions, 612 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 907c8820f..7d78b1e6c 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -21,6 +21,8 @@ libarith_la_SOURCES = \
 	arithvar_dense_set.h \
 	tableau.h \
 	tableau.cpp \
+	simplex.h \
+	simplex.cpp \
 	row_vector.h \
 	row_vector.cpp \
 	arith_propagator.h \
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
new file mode 100644
index 000000000..be2b87252
--- /dev/null
+++ b/src/theory/arith/simplex.cpp
@@ -0,0 +1,549 @@
+
+#include "theory/arith/simplex.h"
+
+using namespace std;
+
+using namespace CVC4;
+using namespace CVC4::kind;
+
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+const static uint64_t ACTIVITY_THRESHOLD = 100;
+
+SimplexDecisionProcedure::Statistics::Statistics():
+  d_statPivots("theory::arith::pivots",0),
+  d_statUpdates("theory::arith::updates",0),
+  d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
+  d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
+  d_statUpdateConflicts("theory::arith::UpdateConflicts", 0)
+{
+  StatisticsRegistry::registerStat(&d_statPivots);
+  StatisticsRegistry::registerStat(&d_statUpdates);
+  StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
+  StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
+  StatisticsRegistry::registerStat(&d_statUpdateConflicts);
+}
+
+SimplexDecisionProcedure::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_statPivots);
+  StatisticsRegistry::unregisterStat(&d_statUpdates);
+  StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
+  StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
+  StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
+}
+
+
+void SimplexDecisionProcedure::ejectInactiveVariables(){
+  Debug("decay") << "begin ejectInactiveVariables()" << endl;
+  for(ArithVar variable = 0, end = d_numVariables; variable != end; ++variable){
+
+    if(shouldEject(variable)){
+      if(d_basicManager.isMember(variable)){
+        Debug("decay") << "ejecting basic " << variable << endl;;
+        d_tableau.ejectBasic(variable);
+      }
+    }
+  }
+}
+
+void SimplexDecisionProcedure::reinjectVariable(ArithVar x){
+  d_tableau.reinjectBasic(x);
+
+
+  DeltaRational safeAssignment = computeRowValue(x, true);
+  DeltaRational assignment = computeRowValue(x, false);
+  d_partialModel.setAssignment(x,safeAssignment,assignment);
+}
+
+bool SimplexDecisionProcedure::shouldEject(ArithVar var){
+  if(d_partialModel.hasEitherBound(var)){
+    return false;
+  }else if(d_tableau.isEjected(var)) {
+    return false;
+  }else if(!d_partialModel.hasEverHadABound(var)){
+    return true;
+  }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){
+    return true;
+  }
+  return false;
+}
+
+/* procedure AssertLower( x_i >= c_i ) */
+bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
+  Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
+
+  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
+    reinjectVariable(x_i);
+  }
+
+  if(d_partialModel.belowLowerBound(x_i, c_i, false)){
+    return false; //sat
+  }
+  if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
+    Node ubc = d_partialModel.getUpperConstraint(x_i);
+    Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
+    d_out->conflict(conflict);
+    Debug("arith") << "AssertLower conflict " << conflict << endl;
+    ++(d_statistics.d_statAssertLowerConflicts);
+    return true;
+  }
+
+  d_partialModel.setLowerConstraint(x_i,original);
+  d_partialModel.setLowerBound(x_i, c_i);
+  d_activityMonitor[x_i] = 0;
+
+  if(!d_basicManager.isMember(x_i)){
+    if(d_partialModel.getAssignment(x_i) < c_i){
+      update(x_i, c_i);
+    }
+  }else{
+    checkBasicVariable(x_i);
+  }
+
+  return false;
+}
+
+/* procedure AssertUpper( x_i <= c_i) */
+bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
+
+  Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
+  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
+    reinjectVariable(x_i);
+  }
+
+  if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i
+    return false; //sat
+  }
+  if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i
+    Node lbc = d_partialModel.getLowerConstraint(x_i);
+    Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
+    Debug("arith") << "AssertUpper conflict " << conflict << endl;
+    ++(d_statistics.d_statAssertUpperConflicts);
+    d_out->conflict(conflict);
+    return true;
+  }
+
+  d_partialModel.setUpperConstraint(x_i,original);
+  d_partialModel.setUpperBound(x_i, c_i);
+
+  d_activityMonitor[x_i] = 0;
+
+  if(!d_basicManager.isMember(x_i)){
+    if(d_partialModel.getAssignment(x_i) > c_i){
+      update(x_i, c_i);
+    }
+  }else{
+    checkBasicVariable(x_i);
+  }
+  d_partialModel.printModel(x_i);
+  return false;
+}
+
+
+/* procedure AssertLower( x_i == c_i ) */
+bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){
+
+  Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
+
+  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
+    reinjectVariable(x_i);
+  }
+
+  // u_i <= c_i <= l_i
+  // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
+  if(d_partialModel.belowLowerBound(x_i, c_i, false) &&
+     d_partialModel.aboveUpperBound(x_i, c_i, false)){
+    return false; //sat
+  }
+
+  if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
+    Node ubc = d_partialModel.getUpperConstraint(x_i);
+    Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
+    d_out->conflict(conflict);
+    Debug("arith") << "AssertLower conflict " << conflict << endl;
+    return true;
+  }
+
+  if(d_partialModel.belowLowerBound(x_i, c_i, true)){
+    Node lbc = d_partialModel.getLowerConstraint(x_i);
+    Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
+    Debug("arith") << "AssertUpper conflict " << conflict << endl;
+    d_out->conflict(conflict);
+    return true;
+  }
+
+  d_partialModel.setLowerConstraint(x_i,original);
+  d_partialModel.setLowerBound(x_i, c_i);
+
+  d_partialModel.setUpperConstraint(x_i,original);
+  d_partialModel.setUpperBound(x_i, c_i);
+  d_activityMonitor[x_i] = 0;
+
+  if(!d_basicManager.isMember(x_i)){
+    if(!(d_partialModel.getAssignment(x_i) == c_i)){
+      update(x_i, c_i);
+    }
+  }else{
+    checkBasicVariable(x_i);
+  }
+
+  return false;
+}
+
+void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
+  Assert(!d_basicManager.isMember(x_i));
+  DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
+  ++(d_statistics.d_statUpdates);
+
+  Debug("arith") <<"update " << x_i << ": "
+                 << assignment_x_i << "|-> " << v << endl;
+  DeltaRational diff = v - assignment_x_i;
+
+  for(ArithVarSet::iterator basicIter = d_tableau.begin();
+      basicIter != d_tableau.end();
+      ++basicIter){
+    ArithVar x_j = *basicIter;
+    ReducedRowVector* row_j = d_tableau.lookup(x_j);
+
+    if(row_j->has(x_i)){
+      const Rational& a_ji = row_j->lookup(x_i);
+
+      const DeltaRational& assignment = d_partialModel.getAssignment(x_j);
+      DeltaRational  nAssignment = assignment+(diff * a_ji);
+      d_partialModel.setAssignment(x_j, nAssignment);
+
+      d_activityMonitor[x_j] += 1;
+
+      checkBasicVariable(x_j);
+    }
+  }
+
+  d_partialModel.setAssignment(x_i, v);
+
+  if(Debug.isOn("paranoid:check_tableau")){
+    checkTableau();
+  }
+}
+
+void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
+  Assert(x_i != x_j);
+
+  ReducedRowVector* row_i = d_tableau.lookup(x_i);
+  const Rational& a_ij = row_i->lookup(x_j);
+
+
+  const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i);
+
+  Rational inv_aij = a_ij.inverse();
+  DeltaRational theta = (v - betaX_i)*inv_aij;
+
+  d_partialModel.setAssignment(x_i, v);
+
+
+  DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta;
+  d_partialModel.setAssignment(x_j, tmp);
+
+  for(ArithVarSet::iterator basicIter = d_tableau.begin();
+      basicIter != d_tableau.end();
+      ++basicIter){
+    ArithVar x_k = *basicIter;
+    ReducedRowVector* row_k = d_tableau.lookup(x_k);
+
+    if(x_k != x_i && row_k->has(x_j)){
+      const Rational& a_kj = row_k->lookup(x_j);
+      DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
+      d_partialModel.setAssignment(x_k, nextAssignment);
+
+      d_activityMonitor[x_j] += 1;
+
+      checkBasicVariable(x_k);
+    }
+  }
+
+  ++(d_statistics.d_statPivots);
+  d_tableau.pivot(x_i, x_j);
+
+  checkBasicVariable(x_j);
+
+  if(Debug.isOn("tableau")){
+    d_tableau.printTableau();
+  }
+}
+
+ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){
+  Debug("arith_update") << "selectSmallestInconsistentVar()" << endl;
+  Debug("arith_update") << "possiblyInconsistent.size()"
+                        << d_possiblyInconsistent.size() << endl;
+
+  if(d_pivotStage){
+    while(!d_griggioRuleQueue.empty()){
+      ArithVar var = d_griggioRuleQueue.top().first;
+      Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl;
+      if(d_basicManager.isMember(var)){
+        if(!d_partialModel.assignmentIsConsistent(var)){
+          return var;
+        }
+      }
+      d_griggioRuleQueue.pop();
+    }
+  }else{
+    while(!d_possiblyInconsistent.empty()){
+      ArithVar var = d_possiblyInconsistent.top();
+      Debug("arith_update") << "possiblyInconsistent var" << var << endl;
+      if(d_basicManager.isMember(var)){
+        if(!d_partialModel.assignmentIsConsistent(var)){
+          return var;
+        }
+      }
+      d_possiblyInconsistent.pop();
+    }
+  }
+  return ARITHVAR_SENTINEL;
+}
+
+template <bool above>
+ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
+  ReducedRowVector* row_i = d_tableau.lookup(x_i);
+
+  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero();
+      nbi != end; ++nbi){
+    ArithVar nonbasic = getArithVar(*nbi);
+    if(nonbasic == x_i) continue;
+
+    const Rational& a_ij = nbi->second;
+    int cmp = a_ij.cmp(d_constants.d_ZERO);
+    if(above){ // beta(x_i) > u_i
+      if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){
+        return nonbasic;
+      }else if( cmp > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
+        return nonbasic;
+      }
+    }else{ //beta(x_i) < l_i
+      if(cmp > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){
+        return nonbasic;
+      }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
+        return nonbasic;
+      }
+    }
+  }
+  return ARITHVAR_SENTINEL;
+}
+
+Node SimplexDecisionProcedure::updateInconsistentVars(){
+  d_pivotStage = true;
+  return privateUpdateInconsistentVars();
+}
+
+//corresponds to Check() in dM06
+Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
+  Assert(d_pivotStage || d_griggioRuleQueue.empty());
+
+  Debug("arith") << "updateInconsistentVars" << endl;
+
+  uint32_t iteratationNum = 0;
+  static const int EJECT_FREQUENCY = 10;
+
+  while(!d_pivotStage || iteratationNum <= d_numVariables){
+    if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
+
+    ArithVar x_i = selectSmallestInconsistentVar();
+    Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
+    if(x_i == ARITHVAR_SENTINEL){
+      Debug("arith_update") << "No inconsistent variables" << endl;
+      return Node::null(); //sat
+    }
+
+    ++iteratationNum;
+    if(iteratationNum % EJECT_FREQUENCY == 0)
+      ejectInactiveVariables();
+
+    DeltaRational beta_i = d_partialModel.getAssignment(x_i);
+
+    if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
+      DeltaRational l_i = d_partialModel.getLowerBound(x_i);
+      ArithVar x_j = selectSlackBelow(x_i);
+      if(x_j == ARITHVAR_SENTINEL ){
+        ++(d_statistics.d_statUpdateConflicts);
+        return generateConflictBelow(x_i); //unsat
+      }
+      pivotAndUpdate(x_i, x_j, l_i);
+
+    }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
+      DeltaRational u_i = d_partialModel.getUpperBound(x_i);
+      ArithVar x_j = selectSlackAbove(x_i);
+      if(x_j == ARITHVAR_SENTINEL ){
+        ++(d_statistics.d_statUpdateConflicts);
+        return generateConflictAbove(x_i); //unsat
+      }
+      pivotAndUpdate(x_i, x_j, u_i);
+    }
+  }
+
+  if(d_pivotStage && iteratationNum >= d_numVariables){
+    while(!d_griggioRuleQueue.empty()){
+      ArithVar var = d_griggioRuleQueue.top().first;
+      if(d_basicManager.isMember(var)){
+        d_possiblyInconsistent.push(var);
+      }
+      d_griggioRuleQueue.pop();
+    }
+    d_pivotStage = false;
+    return updateInconsistentVars();
+  }
+
+  Unreachable();
+}
+
+
+Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
+
+  ReducedRowVector* row_i = d_tableau.lookup(conflictVar);
+
+  NodeBuilder<> nb(kind::AND);
+  TNode bound = d_partialModel.getUpperConstraint(conflictVar);
+
+  Debug("arith")  << "generateConflictAbove "
+                  << "conflictVar " << conflictVar
+                  << " " << d_partialModel.getAssignment(conflictVar)
+                  << " " << bound << endl;
+
+  nb << bound;
+
+  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero();
+      nbi != end; ++nbi){
+    ArithVar nonbasic = getArithVar(*nbi);
+    if(nonbasic == conflictVar) continue;
+
+    const Rational& a_ij = nbi->second;
+
+    Assert(a_ij != d_constants.d_ZERO);
+
+    if(a_ij < d_constants.d_ZERO){
+      bound =  d_partialModel.getUpperConstraint(nonbasic);
+      Debug("arith") << "below 0 " << nonbasic << " "
+                     << d_partialModel.getAssignment(nonbasic)
+                     << " " << bound << endl;
+      nb << bound;
+    }else{
+      bound =  d_partialModel.getLowerConstraint(nonbasic);
+      Debug("arith") << " above 0 " << nonbasic << " "
+                     << d_partialModel.getAssignment(nonbasic)
+                     << " " << bound << endl;
+      nb << bound;
+    }
+  }
+  Node conflict = nb;
+  return conflict;
+}
+
+Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
+  ReducedRowVector* row_i = d_tableau.lookup(conflictVar);
+
+  NodeBuilder<> nb(kind::AND);
+  TNode bound = d_partialModel.getLowerConstraint(conflictVar);
+
+  Debug("arith") << "generateConflictBelow "
+                 << "conflictVar " << conflictVar
+                 << d_partialModel.getAssignment(conflictVar) << " "
+                 << " " << bound << endl;
+  nb << bound;
+
+  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){
+    ArithVar nonbasic = getArithVar(*nbi);
+    if(nonbasic != conflictVar) continue;
+
+    const Rational& a_ij = nbi->second;
+
+    Assert(a_ij != d_constants.d_ZERO);
+
+    if(a_ij < d_constants.d_ZERO){
+      TNode bound = d_partialModel.getLowerConstraint(nonbasic);
+      Debug("arith") << "Lower "<< nonbasic << " "
+                     << d_partialModel.getAssignment(nonbasic) << " "
+                     << bound << endl;
+
+      nb << bound;
+    }else{
+      TNode bound = d_partialModel.getUpperConstraint(nonbasic);
+      Debug("arith") << "Upper "<< nonbasic << " "
+                     << d_partialModel.getAssignment(nonbasic) << " "
+                     << bound << endl;
+
+      nb << bound;
+    }
+  }
+  Node conflict (nb.constructNode());
+  return conflict;
+}
+
+/**
+ * Computes the value of a basic variable using the current assignment.
+ */
+DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe){
+  Assert(d_basicManager.isMember(x));
+  DeltaRational sum = d_constants.d_ZERO_DELTA;
+
+  ReducedRowVector* row = d_tableau.lookup(x);
+  for(ReducedRowVector::NonZeroIterator i = row->beginNonZero(), end = row->endNonZero();
+      i != end;++i){
+    ArithVar nonbasic = getArithVar(*i);
+    if(nonbasic == row->basic()) continue;
+    const Rational& coeff = getCoefficient(*i);
+
+    const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe);
+    sum = sum + (assignment * coeff);
+  }
+  return sum;
+}
+
+
+void SimplexDecisionProcedure::checkBasicVariable(ArithVar basic){
+  Assert(d_basicManager.isMember(basic));
+  if(!d_partialModel.assignmentIsConsistent(basic)){
+    if(d_pivotStage){
+      const DeltaRational& beta = d_partialModel.getAssignment(basic);
+      DeltaRational diff = d_partialModel.belowLowerBound(basic,beta,true) ?
+        d_partialModel.getLowerBound(basic) - beta:
+        beta - d_partialModel.getUpperBound(basic);
+      d_griggioRuleQueue.push(make_pair(basic,diff));
+    }else{
+      d_possiblyInconsistent.push(basic);
+    }
+  }
+}
+
+/**
+ * This check is quite expensive.
+ * It should be wrapped in a Debug.isOn() guard.
+ *   if(Debug.isOn("paranoid:check_tableau")){
+ *      checkTableau();
+ *   }
+ */
+void SimplexDecisionProcedure::checkTableau(){
+
+  for(ArithVarSet::iterator basicIter = d_tableau.begin();
+      basicIter != d_tableau.end(); ++basicIter){
+    ArithVar basic = *basicIter;
+    ReducedRowVector* row_k = d_tableau.lookup(basic);
+    DeltaRational sum;
+    Debug("paranoid:check_tableau") << "starting row" << basic << endl;
+    for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k->beginNonZero();
+        nonbasicIter != row_k->endNonZero();
+        ++nonbasicIter){
+      ArithVar nonbasic = nonbasicIter->first;
+      if(basic == nonbasic) continue;
+
+      const Rational& coeff = nonbasicIter->second;
+      DeltaRational beta = d_partialModel.getAssignment(nonbasic);
+      Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl;
+      sum = sum + (beta*coeff);
+    }
+    DeltaRational shouldBe = d_partialModel.getAssignment(basic);
+    Debug("paranoid:check_tableau") << "ending row" << sum
+                                    << "," << shouldBe << endl;
+
+    Assert(sum == shouldBe);
+  }
+}
+
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
new file mode 100644
index 000000000..440d7063c
--- /dev/null
+++ b/src/theory/arith/simplex.h
@@ -0,0 +1,211 @@
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__SIMPLEX_H
+#define __CVC4__THEORY__ARITH__SIMPLEX_H
+
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar_dense_set.h"
+#include "theory/arith/delta_rational.h"
+#include "theory/arith/tableau.h"
+#include "theory/arith/partial_model.h"
+#include "theory/output_channel.h"
+
+#include "util/stats.h"
+
+#include <queue>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class SimplexDecisionProcedure {
+private:
+  typedef std::pair<ArithVar, DeltaRational> VarDRatPair;
+
+  struct VarDRatPairCompare{
+    inline bool operator()(const VarDRatPair& a, const VarDRatPair& b){
+      return a.second > b.second;
+    }
+  };
+
+  std::priority_queue<VarDRatPair, std::vector<VarDRatPair>, VarDRatPairCompare> d_griggioRuleQueue;
+
+  /**
+   * Priority Queue of the basic variables that may be inconsistent.
+   *
+   * This is required to contain at least 1 instance of every inconsistent
+   * 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<ArithVar> d_possiblyInconsistent;
+
+  /** Stores system wide constants to avoid unnessecary reconstruction. */
+  const ArithConstants& d_constants;
+
+  /**
+   * Manages information about the assignment and upper and lower bounds on
+   * variables.
+   */
+  ArithPartialModel& d_partialModel;
+
+  ArithVarDenseSet& d_basicManager;
+  ActivityMonitor& d_activityMonitor;
+
+  OutputChannel* d_out;
+
+
+  Tableau& d_tableau;
+
+  ArithVar d_numVariables;
+
+  bool d_pivotStage;
+
+public:
+  SimplexDecisionProcedure(const ArithConstants& constants,
+                           ArithPartialModel& pm,
+                           ArithVarDenseSet& bm,
+                           OutputChannel* out,
+                           ActivityMonitor& am,
+                           Tableau& tableau) :
+    d_possiblyInconsistent(),
+    d_constants(constants),
+    d_partialModel(pm),
+    d_basicManager(bm),
+    d_activityMonitor(am),
+    d_out(out),
+    d_tableau(tableau),
+    d_numVariables(0)
+  {}
+
+  void increaseMax() {d_numVariables++;}
+
+  /**
+   * 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
+   * and updates the value of a basic variable if needed.
+   * If this new bound is in conflict with the other bound,
+   * a conflict is created and asserted to the output channel.
+   *
+   * orig must be an atom in the SAT solver so that it can be used for
+   * conflict analysis.
+   *
+   * n is of the form (x =?= c) where x is a variable,
+   * c is a constant and =?= is either LT, LEQ, EQ, GEQ, or GT.
+   *
+   * returns true if a conflict was asserted.
+   */
+  bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig);
+  bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig);
+  bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig);
+
+private:
+  /**
+   * Updates the assignment of a nonbasic variable x_i to v.
+   * Also updates the assignment of basic variables accordingly.
+   */
+  void update(ArithVar x_i, const 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(ArithVar x_i, ArithVar x_j, DeltaRational& v);
+
+public:
+  /**
+   * Tries to update the assignments of variables such that all of the
+   * assignments are consistent with their bounds.
+   *
+   * This is done by searching through the tableau.
+   * If all of the variables can be made consistent with their bounds
+   * Node::null() is returned. Otherwise a minimized conflict is returned.
+   *
+   * If a conflict is found, changes to the assignments need to be reverted.
+   *
+   * Tableau pivoting is performed so variables may switch from being basic to
+   * nonbasic and vice versa.
+   *
+   * Corresponds to the "check()" procedure in [Cav06].
+   */
+  Node updateInconsistentVars();
+private:
+  Node privateUpdateInconsistentVars();
+
+private:
+  /**
+   * Given the basic variable x_i,
+   * this function finds the smallest nonbasic variable x_j in the row of x_i
+   * in the tableau that can "take up the slack" to let x_i satisfy its bounds.
+   * This returns TNode::null() if none exists.
+   *
+   * More formally one of the following conditions must be satisfied:
+   * -  above && a_ij < 0 && assignment(x_j) < upperbound(x_j)
+   * -  above && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
+   * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j)
+   * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
+   */
+  template <bool above>  ArithVar selectSlack(ArithVar 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.
+   */
+  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(ArithVar conflictVar);
+  Node generateConflictBelow(ArithVar conflictVar);
+
+public:
+  /** Checks to make sure the assignment is consistent with the tableau. */
+  void checkTableau();
+
+private:
+  bool shouldEject(ArithVar var);
+  void ejectInactiveVariables();
+
+public:
+  void reinjectVariable(ArithVar x);
+
+  /**
+   * Computes the value of a basic variable using the assignments
+   * of the values of the variables in the basic variable's row tableau.
+   * This can compute the value using either:
+   * - the the current assignment (useSafe=false) or
+   * - the safe assignment (useSafe = true).
+   */
+  DeltaRational computeRowValue(ArithVar x, bool useSafe);
+
+private:
+  /** Check to make sure all of the basic variables are within their bounds. */
+  void checkBasicVariable(ArithVar basic);
+
+
+  /** 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;
+
+    Statistics();
+    ~Statistics();
+  };
+
+  Statistics d_statistics;
+
+};/* class SimplexDecisionProcedure */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__SIMPLEX_H */
+
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6efffa21c..e691788fa 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -53,8 +53,6 @@ using namespace CVC4::theory::arith;
 struct SlackAttrID;
 typedef expr::Attribute<SlackAttrID, Node> Slack;
 
-const static uint64_t ACTIVITY_THRESHOLD = 100;
-
 TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) :
   Theory(id, c, out),
   d_constants(NodeManager::currentNM()),
@@ -65,58 +63,27 @@ TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) :
   d_tableau(d_activityMonitor, d_basicManager),
   d_rewriter(&d_constants),
   d_propagator(c),
+  d_simplex(d_constants, d_partialModel, d_basicManager,  d_out, d_activityMonitor, d_tableau),
   d_statistics()
 {}
 
-TheoryArith::~TheoryArith(){
-  for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
-    Node var = *i;
-    Debug("arithgc") << var << endl;
-  }
-}
+TheoryArith::~TheoryArith(){}
 
 TheoryArith::Statistics::Statistics():
-  d_statPivots("theory::arith::pivots",0),
-  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_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(){
-  StatisticsRegistry::unregisterStat(&d_statPivots);
-  StatisticsRegistry::unregisterStat(&d_statUpdates);
-  StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
-  StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
-  StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
   StatisticsRegistry::unregisterStat(&d_statUserVariables);
   StatisticsRegistry::unregisterStat(&d_statSlackVariables);
 }
 
 
 
-bool TheoryArith::shouldEject(ArithVar var){
-  if(d_partialModel.hasEitherBound(var)){
-    return false;
-  }else if(d_tableau.isEjected(var)) {
-    return false;
-  }else if(!d_partialModel.hasEverHadABound(var)){
-    return true;
-  }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){
-    return true;
-  }
-  return false;
-}
 
 ArithVar TheoryArith::findBasicRow(ArithVar variable){
   for(ArithVarSet::iterator basicIter = d_tableau.begin();
@@ -132,28 +99,6 @@ ArithVar TheoryArith::findBasicRow(ArithVar variable){
   return ARITHVAR_SENTINEL;
 }
 
-void TheoryArith::ejectInactiveVariables(){
-  Debug("decay") << "begin ejectInactiveVariables()" << endl;
-  for(ArithVar variable = 0, end = d_variables.size(); variable != end; ++variable){
-    //TNode var = *i;
-    //ArithVar variable = asArithVar(var);
-    if(shouldEject(variable)){
-      if(d_basicManager.isMember(variable)){
-        Debug("decay") << "ejecting basic " << variable << endl;;
-        d_tableau.ejectBasic(variable);
-      }
-    }
-  }
-}
-
-void TheoryArith::reinjectVariable(ArithVar x){
-  d_tableau.reinjectBasic(x);
-
-
-  DeltaRational safeAssignment = computeRowValue(x, true);
-  DeltaRational assignment = computeRowValue(x, false);
-  d_partialModel.setAssignment(x,safeAssignment,assignment);
-}
 
 void TheoryArith::preRegisterTerm(TNode n) {
   Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
@@ -206,13 +151,6 @@ void TheoryArith::preRegisterTerm(TNode n) {
 
 
 
-void TheoryArith::checkBasicVariable(ArithVar basic){
-  Assert(d_basicManager.isMember(basic));
-  if(!d_partialModel.assignmentIsConsistent(basic)){
-    d_possiblyInconsistent.push(basic);
-  }
-}
-
 bool TheoryArith::isTheoryLeaf(TNode x) const{
   return x.getMetaKind() == kind::metakind::VARIABLE;
 }
@@ -224,6 +162,8 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
   ArithVar varX = d_variables.size();
   d_variables.push_back(Node(x));
 
+  d_simplex.increaseMax();
+
   setArithVar(x,varX);
 
   Assert(varX == d_activityMonitor.size());
@@ -288,12 +228,15 @@ void TheoryArith::setupInitialValue(ArithVar x){
 
     //This can go away if the tableau creation is done at preregister
     //time instead of register
-    DeltaRational safeAssignment = computeRowValue(x, true);
-    DeltaRational assignment = computeRowValue(x, false);
+    DeltaRational safeAssignment = d_simplex.computeRowValue(x, true);
+    DeltaRational assignment = d_simplex.computeRowValue(x, false);
     d_partialModel.initialize(x,safeAssignment);
     d_partialModel.setAssignment(x,assignment);
 
-    checkBasicVariable(x);
+
+    //d_simplex.checkBasicVariable(x);
+    //Conciously violating unneeded check
+
     //Strictly speaking checking x is unnessecary as it cannot have an upper or
     //lower bound. This is done to strongly enforce the notion that basic
     //variables should not be changed without begin checked.
@@ -302,27 +245,6 @@ void TheoryArith::setupInitialValue(ArithVar x){
   Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
 };
 
-/**
- * Computes the value of a basic variable using the current assignment.
- */
-DeltaRational TheoryArith::computeRowValue(ArithVar x, bool useSafe){
-  Assert(d_basicManager.isMember(x));
-  DeltaRational sum = d_constants.d_ZERO_DELTA;
-
-  ReducedRowVector* row = d_tableau.lookup(x);
-  for(ReducedRowVector::NonZeroIterator i = row->beginNonZero(), end = row->endNonZero();
-      i != end;++i){
-    ArithVar nonbasic = getArithVar(*i);
-    if(nonbasic == row->basic()) continue;
-    const Rational& coeff = getCoefficient(*i);
-
-    const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe);
-    sum = sum + (assignment * coeff);
-  }
-  return sum;
-}
-
-
 RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) {
   return d_rewriter.preRewrite(n);
 }
@@ -331,390 +253,6 @@ void TheoryArith::registerTerm(TNode tn){
   Debug("arith") << "registerTerm(" << tn << ")" << endl;
 }
 
-/* procedure AssertUpper( x_i <= c_i) */
-bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
-
-  Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
-  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
-    reinjectVariable(x_i);
-  }
-
-  if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i
-    return false; //sat
-  }
-  if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i
-    Node lbc = d_partialModel.getLowerConstraint(x_i);
-    Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
-    Debug("arith") << "AssertUpper conflict " << conflict << endl;
-    ++(d_statistics.d_statAssertUpperConflicts);
-    d_out->conflict(conflict);
-    return true;
-  }
-
-  d_partialModel.setUpperConstraint(x_i,original);
-  d_partialModel.setUpperBound(x_i, c_i);
-
-  d_activityMonitor[x_i] = 0;
-
-  if(!d_basicManager.isMember(x_i)){
-    if(d_partialModel.getAssignment(x_i) > c_i){
-      update(x_i, c_i);
-    }
-  }else{
-    checkBasicVariable(x_i);
-  }
-  d_partialModel.printModel(x_i);
-  return false;
-}
-
-/* procedure AssertLower( x_i >= c_i ) */
-bool TheoryArith::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
-  Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
-
-  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
-    reinjectVariable(x_i);
-  }
-
-  if(d_partialModel.belowLowerBound(x_i, c_i, false)){
-    return false; //sat
-  }
-  if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
-    Node ubc = d_partialModel.getUpperConstraint(x_i);
-    Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
-    d_out->conflict(conflict);
-    Debug("arith") << "AssertLower conflict " << conflict << endl;
-    ++(d_statistics.d_statAssertLowerConflicts);
-    return true;
-  }
-
-  d_partialModel.setLowerConstraint(x_i,original);
-  d_partialModel.setLowerBound(x_i, c_i);
-  d_activityMonitor[x_i] = 0;
-
-  if(!d_basicManager.isMember(x_i)){
-    if(d_partialModel.getAssignment(x_i) < c_i){
-      update(x_i, c_i);
-    }
-  }else{
-    checkBasicVariable(x_i);
-  }
-
-  return false;
-}
-
-/* procedure AssertLower( x_i == c_i ) */
-bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){
-
-  Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
-
-  if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){
-    reinjectVariable(x_i);
-  }
-
-  // u_i <= c_i <= l_i
-  // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
-  if(d_partialModel.belowLowerBound(x_i, c_i, false) &&
-     d_partialModel.aboveUpperBound(x_i, c_i, false)){
-    return false; //sat
-  }
-
-  if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
-    Node ubc = d_partialModel.getUpperConstraint(x_i);
-    Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
-    d_out->conflict(conflict);
-    Debug("arith") << "AssertLower conflict " << conflict << endl;
-    return true;
-  }
-
-  if(d_partialModel.belowLowerBound(x_i, c_i, true)){
-    Node lbc = d_partialModel.getLowerConstraint(x_i);
-    Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
-    Debug("arith") << "AssertUpper conflict " << conflict << endl;
-    d_out->conflict(conflict);
-    return true;
-  }
-
-  d_partialModel.setLowerConstraint(x_i,original);
-  d_partialModel.setLowerBound(x_i, c_i);
-
-  d_partialModel.setUpperConstraint(x_i,original);
-  d_partialModel.setUpperBound(x_i, c_i);
-  d_activityMonitor[x_i] = 0;
-
-  if(!d_basicManager.isMember(x_i)){
-    if(!(d_partialModel.getAssignment(x_i) == c_i)){
-      update(x_i, c_i);
-    }
-  }else{
-    checkBasicVariable(x_i);
-  }
-
-  return false;
-}
-void TheoryArith::update(ArithVar x_i, const DeltaRational& v){
-  Assert(!d_basicManager.isMember(x_i));
-  DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
-  ++(d_statistics.d_statUpdates);
-
-  Debug("arith") <<"update " << x_i << ": "
-                 << assignment_x_i << "|-> " << v << endl;
-  DeltaRational diff = v - assignment_x_i;
-
-  for(ArithVarSet::iterator basicIter = d_tableau.begin();
-      basicIter != d_tableau.end();
-      ++basicIter){
-    ArithVar x_j = *basicIter;
-    ReducedRowVector* row_j = d_tableau.lookup(x_j);
-
-    if(row_j->has(x_i)){
-      const Rational& a_ji = row_j->lookup(x_i);
-
-      const DeltaRational& assignment = d_partialModel.getAssignment(x_j);
-      DeltaRational  nAssignment = assignment+(diff * a_ji);
-      d_partialModel.setAssignment(x_j, nAssignment);
-
-      d_activityMonitor[x_j] += 1;
-
-      checkBasicVariable(x_j);
-    }
-  }
-
-  d_partialModel.setAssignment(x_i, v);
-
-  if(Debug.isOn("paranoid:check_tableau")){
-    checkTableau();
-  }
-}
-
-void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
-  Assert(x_i != x_j);
-
-  ReducedRowVector* row_i = d_tableau.lookup(x_i);
-  const Rational& a_ij = row_i->lookup(x_j);
-
-
-  const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i);
-
-  Rational inv_aij = a_ij.inverse();
-  DeltaRational theta = (v - betaX_i)*inv_aij;
-
-  d_partialModel.setAssignment(x_i, v);
-
-
-  DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta;
-  d_partialModel.setAssignment(x_j, tmp);
-
-  for(ArithVarSet::iterator basicIter = d_tableau.begin();
-      basicIter != d_tableau.end();
-      ++basicIter){
-    ArithVar x_k = *basicIter;
-    ReducedRowVector* row_k = d_tableau.lookup(x_k);
-
-    if(x_k != x_i && row_k->has(x_j)){
-      const Rational& a_kj = row_k->lookup(x_j);
-      DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
-      d_partialModel.setAssignment(x_k, nextAssignment);
-
-      d_activityMonitor[x_j] += 1;
-
-      checkBasicVariable(x_k);
-    }
-  }
-
-  ++(d_statistics.d_statPivots);
-  d_tableau.pivot(x_i, x_j);
-
-  checkBasicVariable(x_j);
-
-  if(Debug.isOn("tableau")){
-    d_tableau.printTableau();
-  }
-}
-
-ArithVar TheoryArith::selectSmallestInconsistentVar(){
-  Debug("arith_update") << "selectSmallestInconsistentVar()" << endl;
-  Debug("arith_update") << "possiblyInconsistent.size()"
-                        << d_possiblyInconsistent.size() << endl;
-
-  while(!d_possiblyInconsistent.empty()){
-    ArithVar var = d_possiblyInconsistent.top();
-    Debug("arith_update") << "possiblyInconsistent var" << var << endl;
-    if(d_basicManager.isMember(var)){
-      if(!d_partialModel.assignmentIsConsistent(var)){
-        return var;
-      }
-    }
-    d_possiblyInconsistent.pop();
-  }
-
-  if(Debug.isOn("paranoid:variables")){
-    for(ArithVarSet::iterator basicIter = d_tableau.begin();
-        basicIter != d_tableau.end();
-        ++basicIter){
-
-      ArithVar basic = *basicIter;
-      Assert(d_partialModel.assignmentIsConsistent(basic));
-      if(!d_partialModel.assignmentIsConsistent(basic)){
-        return basic;
-      }
-    }
-  }
-
-  return ARITHVAR_SENTINEL;
-}
-
-template <bool above>
-ArithVar TheoryArith::selectSlack(ArithVar x_i){
-  ReducedRowVector* row_i = d_tableau.lookup(x_i);
-
-  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero();
-      nbi != end; ++nbi){
-    ArithVar nonbasic = getArithVar(*nbi);
-    if(nonbasic == x_i) continue;
-
-    const Rational& a_ij = nbi->second;
-    int cmp = a_ij.cmp(d_constants.d_ZERO);
-    if(above){ // beta(x_i) > u_i
-      if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){
-        return nonbasic;
-      }else if( cmp > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
-        return nonbasic;
-      }
-    }else{ //beta(x_i) < l_i
-      if(cmp > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){
-        return nonbasic;
-      }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
-        return nonbasic;
-      }
-    }
-  }
-  return ARITHVAR_SENTINEL;
-}
-
-
-Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
-  Debug("arith") << "updateInconsistentVars" << endl;
-
-  static int iteratationNum = 0;
-  static const int EJECT_FREQUENCY = 10;
-  while(true){
-    if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
-
-    ArithVar x_i = selectSmallestInconsistentVar();
-    Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
-    if(x_i == ARITHVAR_SENTINEL){
-      Debug("arith_update") << "No inconsistent variables" << endl;
-      return Node::null(); //sat
-    }
-
-    ++iteratationNum;
-    if(iteratationNum % EJECT_FREQUENCY == 0)
-      ejectInactiveVariables();
-
-    DeltaRational beta_i = d_partialModel.getAssignment(x_i);
-
-    if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
-      DeltaRational l_i = d_partialModel.getLowerBound(x_i);
-      ArithVar x_j = selectSlackBelow(x_i);
-      if(x_j == ARITHVAR_SENTINEL ){
-        ++(d_statistics.d_statUpdateConflicts);
-        return generateConflictBelow(x_i); //unsat
-      }
-      pivotAndUpdate(x_i, x_j, l_i);
-
-    }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
-      DeltaRational u_i = d_partialModel.getUpperBound(x_i);
-      ArithVar x_j = selectSlackAbove(x_i);
-      if(x_j == ARITHVAR_SENTINEL ){
-        ++(d_statistics.d_statUpdateConflicts);
-        return generateConflictAbove(x_i); //unsat
-      }
-      pivotAndUpdate(x_i, x_j, u_i);
-    }
-  }
-}
-
-Node TheoryArith::generateConflictAbove(ArithVar conflictVar){
-
-  ReducedRowVector* row_i = d_tableau.lookup(conflictVar);
-
-  NodeBuilder<> nb(kind::AND);
-  TNode bound = d_partialModel.getUpperConstraint(conflictVar);
-
-  Debug("arith")  << "generateConflictAbove "
-                  << "conflictVar " << conflictVar
-                  << " " << d_partialModel.getAssignment(conflictVar)
-                  << " " << bound << endl;
-
-  nb << bound;
-
-  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero();
-      nbi != end; ++nbi){
-    ArithVar nonbasic = getArithVar(*nbi);
-    if(nonbasic == conflictVar) continue;
-
-    const Rational& a_ij = nbi->second;
-
-    Assert(a_ij != d_constants.d_ZERO);
-
-    if(a_ij < d_constants.d_ZERO){
-      bound =  d_partialModel.getUpperConstraint(nonbasic);
-      Debug("arith") << "below 0 " << nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic)
-                     << " " << bound << endl;
-      nb << bound;
-    }else{
-      bound =  d_partialModel.getLowerConstraint(nonbasic);
-      Debug("arith") << " above 0 " << nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic)
-                     << " " << bound << endl;
-      nb << bound;
-    }
-  }
-  Node conflict = nb;
-  return conflict;
-}
-
-Node TheoryArith::generateConflictBelow(ArithVar conflictVar){
-  ReducedRowVector* row_i = d_tableau.lookup(conflictVar);
-
-  NodeBuilder<> nb(kind::AND);
-  TNode bound = d_partialModel.getLowerConstraint(conflictVar);
-
-  Debug("arith") << "generateConflictBelow "
-                 << "conflictVar " << conflictVar
-                 << d_partialModel.getAssignment(conflictVar) << " "
-                 << " " << bound << endl;
-  nb << bound;
-
-  for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){
-    ArithVar nonbasic = getArithVar(*nbi);
-    if(nonbasic != conflictVar) continue;
-
-    const Rational& a_ij = nbi->second;
-
-    Assert(a_ij != d_constants.d_ZERO);
-
-    if(a_ij < d_constants.d_ZERO){
-      TNode bound = d_partialModel.getLowerConstraint(nonbasic);
-      Debug("arith") << "Lower "<< nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic) << " "
-                     << bound << endl;
-
-      nb << bound;
-    }else{
-      TNode bound = d_partialModel.getUpperConstraint(nonbasic);
-      Debug("arith") << "Upper "<< nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic) << " "
-                     << bound << endl;
-
-      nb << bound;
-    }
-  }
-  Node conflict (nb.constructNode());
-  return conflict;
-}
-
 template <bool selectLeft>
 TNode getSide(TNode assertion, Kind simpleKind){
   switch(simpleKind){
@@ -766,12 +304,12 @@ bool TheoryArith::assertionCases(TNode assertion){
   switch(simpKind){
   case LEQ:
   case LT:
-    return AssertUpper(x_i, c_i, assertion);
+    return d_simplex.AssertUpper(x_i, c_i, assertion);
   case GT:
   case GEQ:
-    return AssertLower(x_i, c_i, assertion);
+    return d_simplex.AssertLower(x_i, c_i, assertion);
   case EQUAL:
-    return AssertEquality(x_i, c_i, assertion);
+    return d_simplex.AssertEquality(x_i, c_i, assertion);
   case DISTINCT:
     d_diseq.push_back(assertion);
     return false;
@@ -798,9 +336,9 @@ void TheoryArith::check(Effort level){
   }
 
   //TODO This must be done everytime for the time being
-  if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
+  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
 
-  Node possibleConflict = updateInconsistentVars();
+  Node possibleConflict = d_simplex.updateInconsistentVars();
   if(possibleConflict != Node::null()){
 
     d_partialModel.revertAssignmentChanges();
@@ -814,7 +352,7 @@ void TheoryArith::check(Effort level){
   }else{
     d_partialModel.commitAssignmentChanges();
   }
-  if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); }
+  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
 
 
   Debug("arith") << "TheoryArith::check end" << std::endl;
@@ -843,41 +381,6 @@ void TheoryArith::check(Effort level){
   }
 }
 
-/**
- * This check is quite expensive.
- * It should be wrapped in a Debug.isOn() guard.
- *   if(Debug.isOn("paranoid:check_tableau")){
- *      checkTableau();
- *   }
- */
-void TheoryArith::checkTableau(){
-
-  for(ArithVarSet::iterator basicIter = d_tableau.begin();
-      basicIter != d_tableau.end(); ++basicIter){
-    ArithVar basic = *basicIter;
-    ReducedRowVector* row_k = d_tableau.lookup(basic);
-    DeltaRational sum;
-    Debug("paranoid:check_tableau") << "starting row" << basic << endl;
-    for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k->beginNonZero();
-        nonbasicIter != row_k->endNonZero();
-        ++nonbasicIter){
-      ArithVar nonbasic = nonbasicIter->first;
-      if(basic == nonbasic) continue;
-
-      const Rational& coeff = nonbasicIter->second;
-      DeltaRational beta = d_partialModel.getAssignment(nonbasic);
-      Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl;
-      sum = sum + (beta*coeff);
-    }
-    DeltaRational shouldBe = d_partialModel.getAssignment(basic);
-    Debug("paranoid:check_tableau") << "ending row" << sum
-                                    << "," << shouldBe << endl;
-
-    Assert(sum == shouldBe);
-  }
-}
-
-
 void TheoryArith::explain(TNode n, Effort e) {
   Node explanation = d_propagator.explain(n);
   Debug("arith") << "arith::explain("<<explanation<<")->"
@@ -904,7 +407,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
   case kind::VARIABLE: {
     ArithVar var = asArithVar(n);
     if(d_tableau.isEjected(var)){
-      reinjectVariable(var);
+      d_simplex.reinjectVariable(var);
     }
 
     DeltaRational drat = d_partialModel.getAssignment(var);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 5395327c0..af52da444 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -33,6 +33,7 @@
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/arith_propagator.h"
+#include "theory/arith/simplex.h"
 
 #include "util/stats.h"
 
@@ -98,6 +99,7 @@ private:
   ArithRewriter d_rewriter;
 
   ArithUnatePropagator d_propagator;
+  SimplexDecisionProcedure d_simplex;
 
 public:
   TheoryArith(int id, context::Context* c, OutputChannel& out);
@@ -137,91 +139,10 @@ 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
-   * and updates the value of a basic variable if needed.
-   * If this new bound is in conflict with the other bound,
-   * a conflict is created and asserted to the output channel.
-   *
-   * orig must be an atom in the SAT solver so that it can be used for
-   * conflict analysis.
-   *
-   * n is of the form (x =?= c) where x is a variable,
-   * c is a constant and =?= is either LT, LEQ, EQ, GEQ, or GT.
-   *
-   * returns true if a conflict was asserted.
-   */
-  bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig);
-  bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig);
-  bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig);
-
   ArithVar determineLeftVariable(TNode assertion, Kind simpleKind);
 
 
   /**
-   * Updates the assignment of a nonbasic variable x_i to v.
-   * Also updates the assignment of basic variables accordingly.
-   */
-  void update(ArithVar x_i, const 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(ArithVar x_i, ArithVar x_j, DeltaRational& v);
-
-  /**
-   * Tries to update the assignments of variables such that all of the
-   * assignments are consistent with their bounds.
-   *
-   * This is done by searching through the tableau.
-   * If all of the variables can be made consistent with their bounds
-   * Node::null() is returned. Otherwise a minimized conflict is returned.
-   *
-   * If a conflict is found, changes to the assignments need to be reverted.
-   *
-   * Tableau pivoting is performed so variables may switch from being basic to
-   * nonbasic and vice versa.
-   *
-   * Corresponds to the "check()" procedure in [Cav06].
-   */
-  Node updateInconsistentVars();
-
-  /**
-   * Given the basic variable x_i,
-   * this function finds the smallest nonbasic variable x_j in the row of x_i
-   * in the tableau that can "take up the slack" to let x_i satisfy its bounds.
-   * This returns TNode::null() if none exists.
-   *
-   * More formally one of the following conditions must be satisfied:
-   * -  above && a_ij < 0 && assignment(x_j) < upperbound(x_j)
-   * -  above && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
-   * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j)
-   * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
-   */
-  template <bool above>  ArithVar selectSlack(ArithVar 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.
-   */
-  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(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.
@@ -234,20 +155,8 @@ private:
   /** Initial (not context dependent) sets up for a new slack variable.*/
   void setupSlack(TNode left);
 
-  /**
-   * Computes the value of a basic variable using the assignments
-   * of the values of the variables in the basic variable's row tableau.
-   * This can compute the value using either:
-   * - the the current assignment (useSafe=false) or
-   * - the safe assignment (useSafe = true).
-   */
-  DeltaRational computeRowValue(ArithVar x, bool useSafe);
 
-  /** 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(ArithVar basic);
 
   /**
    * Handles the case splitting for check() for a new assertion.
@@ -256,9 +165,6 @@ private:
   bool assertionCases(TNode assertion);
 
   ArithVar findBasicRow(ArithVar variable);
-  bool shouldEject(ArithVar var);
-  void ejectInactiveVariables();
-  void reinjectVariable(ArithVar x);
 
   void asVectors(Polynomial& p,
                  std::vector<Rational>& coeffs,
@@ -268,8 +174,6 @@ private:
   /** 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();