This commit merges in branches/arithmetic/internalbb up to revision 2831. This is a significant refactoring of code.

- r2820
-- Refactors Simplex so that it does significantly fewer functions.
--  Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model.
-- Some of the code for propagation has moved to TheoryArith.
-r2826
-- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound().
- r2827
-- Adds isZero() to Rational. Adds cmp to DeltaRational.
- r2831
-- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp.
-- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases.

12 files changed, 1050 insertions, 766 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 4ca8aff0b..7934140a0 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -25,6 +25,8 @@ libarith_la_SOURCES = \
 	delta_rational.cpp \
 	partial_model.h \
 	partial_model.cpp \
+	linear_equality.h \
+	linear_equality.cpp \
 	ordered_set.h \
 	arithvar_set.h \
 	tableau.h \
diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index e74a250a3..bd2939df9 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -118,7 +118,7 @@ ArithVar ArithPriorityQueue::dequeueInconsistentBasicVariable(){
 ArithPriorityQueue::VarDRatPair ArithPriorityQueue::computeDiff(ArithVar basic){
   Assert(basicAndInconsistent(basic));
   const DeltaRational& beta = d_partialModel.getAssignment(basic);
-  DeltaRational diff = d_partialModel.belowLowerBound(basic,beta,true) ?
+  DeltaRational diff = d_partialModel.strictlyLessThanLowerBound(basic,beta) ?
     d_partialModel.getLowerBound(basic) - beta:
     beta - d_partialModel.getUpperBound(basic);
 
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 0168ee043..07387c977 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -51,6 +51,12 @@ typedef context::CDSet<Node, NodeHashFunction> CDNodeSet;
 
 typedef context::CDSet<ArithVar> CDArithVarSet;
 
+class ArithVarCallBack {
+public:
+  virtual void callback(ArithVar x) = 0;
+};
+
+
 
 inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 682d13720..c004a681f 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -63,6 +63,15 @@ public:
     }
   }
 
+  int cmp(const DeltaRational& other) const{
+    int cmp = c.cmp(other.c);
+    if(cmp == 0){
+      return k.cmp(other.k);
+    }else{
+      return cmp;
+    }
+  }
+
   DeltaRational operator+(const DeltaRational& other) const{
     CVC4::Rational tmpC = c+other.c;
     CVC4::Rational tmpK = k+other.k;
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
new file mode 100644
index 000000000..c84e61285
--- /dev/null
+++ b/src/theory/arith/linear_equality.cpp
@@ -0,0 +1,302 @@
+/*********************                                                        */
+/*! \file simplex.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This implements the LinearEqualityModule.
+ **
+ ** This implements the LinearEqualityModule.
+ **/
+
+
+#include "theory/arith/linear_equality.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/* Explicitly instatiate this function. */
+template void LinearEqualityModule::explainNonbasics<true>(ArithVar basic, NodeBuilder<>& output);
+template void LinearEqualityModule::explainNonbasics<false>(ArithVar basic, NodeBuilder<>& output);
+
+LinearEqualityModule::Statistics::Statistics():
+  d_statPivots("theory::arith::pivots",0),
+  d_statUpdates("theory::arith::updates",0),
+  d_pivotTime("theory::arith::pivotTime")
+{
+  StatisticsRegistry::registerStat(&d_statPivots);
+  StatisticsRegistry::registerStat(&d_statUpdates);
+
+  StatisticsRegistry::registerStat(&d_pivotTime);
+}
+
+LinearEqualityModule::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_statPivots);
+  StatisticsRegistry::unregisterStat(&d_statUpdates);
+  StatisticsRegistry::unregisterStat(&d_pivotTime);
+}
+
+void LinearEqualityModule::update(ArithVar x_i, const DeltaRational& v){
+  Assert(!d_tableau.isBasic(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;
+
+  //Assert(matchingSets(d_tableau, x_i));
+  Tableau::ColIterator basicIter = d_tableau.colIterator(x_i);
+  for(; !basicIter.atEnd(); ++basicIter){
+    const TableauEntry& entry = *basicIter;
+    Assert(entry.getColVar() == x_i);
+
+    ArithVar x_j = entry.getRowVar();
+    //ReducedRowVector& row_j = d_tableau.lookup(x_j);
+
+    //const Rational& a_ji = row_j.lookup(x_i);
+    const Rational& a_ji = entry.getCoefficient();
+
+    const DeltaRational& assignment = d_partialModel.getAssignment(x_j);
+    DeltaRational  nAssignment = assignment+(diff * a_ji);
+    d_partialModel.setAssignment(x_j, nAssignment);
+
+    d_basicVariableUpdates.callback(x_j);
+  }
+
+  d_partialModel.setAssignment(x_i, v);
+
+  Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_i));
+  //double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_i));
+
+  //(d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference);
+  if(Debug.isOn("paranoid:check_tableau")){  debugCheckTableau(); }
+}
+
+void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
+  Assert(x_i != x_j);
+
+  TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
+
+  if(Debug.isOn("arith::simplex:row")){ debugPivot(x_i, x_j); }
+
+  const TableauEntry& entry_ij =  d_tableau.findEntry(x_i, x_j);
+  Assert(!entry_ij.blank());
+
+
+  const Rational& a_ij = entry_ij.getCoefficient();
+
+
+  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);
+
+
+  //Assert(matchingSets(d_tableau, x_j));
+  for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){
+    const TableauEntry& entry = *iter;
+    Assert(entry.getColVar() == x_j);
+    ArithVar x_k = entry.getRowVar();
+    if(x_k != x_i ){
+      const Rational& a_kj = entry.getCoefficient();
+      DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
+      d_partialModel.setAssignment(x_k, nextAssignment);
+
+      d_basicVariableUpdates.callback(x_k);
+    }
+  }
+
+  // Pivots
+  ++(d_statistics.d_statPivots);
+
+  Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_j));
+  //double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_j));
+  //(d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference);
+  d_tableau.pivot(x_i, x_j);
+
+  d_basicVariableUpdates.callback(x_j);
+
+  if(Debug.isOn("tableau")){
+    d_tableau.printTableau();
+  }
+}
+
+
+void LinearEqualityModule::debugPivot(ArithVar x_i, ArithVar x_j){
+  Debug("arith::pivot") << "debugPivot("<< x_i  <<"|->"<< x_j << ")" << endl;
+
+  for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){
+    const TableauEntry& entry = *iter;
+
+    ArithVar var = entry.getColVar();
+    const Rational& coeff = entry.getCoefficient();
+    DeltaRational beta = d_partialModel.getAssignment(var);
+    Debug("arith::pivot") << var << beta << coeff;
+    if(d_partialModel.hasLowerBound(var)){
+      Debug("arith::pivot") << "(lb " << d_partialModel.getLowerBound(var) << ")";
+    }
+    if(d_partialModel.hasUpperBound(var)){
+      Debug("arith::pivot") << "(up " << d_partialModel.getUpperBound(var) << ")";
+    }
+    Debug("arith::pivot") << endl;
+  }
+  Debug("arith::pivot") << "end row"<< endl;
+}
+
+/**
+ * This check is quite expensive.
+ * It should be wrapped in a Debug.isOn() guard.
+ *   if(Debug.isOn("paranoid:check_tableau")){
+ *      checkTableau();
+ *   }
+ */
+void LinearEqualityModule::debugCheckTableau(){
+  ArithVarSet::const_iterator basicIter = d_tableau.beginBasic();
+  ArithVarSet::const_iterator endIter = d_tableau.endBasic();
+  for(; basicIter != endIter; ++basicIter){
+    ArithVar basic = *basicIter;
+    DeltaRational sum;
+    Debug("paranoid:check_tableau") << "starting row" << basic << endl;
+    Tableau::RowIterator nonbasicIter = d_tableau.rowIterator(basic);
+    for(; !nonbasicIter.atEnd(); ++nonbasicIter){
+      const TableauEntry& entry = *nonbasicIter;
+      ArithVar nonbasic = entry.getColVar();
+      if(basic == nonbasic) continue;
+
+      const Rational& coeff = entry.getCoefficient();
+      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);
+  }
+}
+
+DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){
+  DeltaRational sum(0,0);
+  for(Tableau::RowIterator i = d_tableau.rowIterator(basic); !i.atEnd(); ++i){
+    const TableauEntry& entry = (*i);
+    ArithVar nonbasic = entry.getColVar();
+    if(nonbasic == basic) continue;
+    const Rational& coeff =  entry.getCoefficient();
+    int sgn = coeff.sgn();
+    bool ub = upperBound ? (sgn > 0) : (sgn < 0);
+
+    const DeltaRational& bound = ub ?
+      d_partialModel.getUpperBound(nonbasic):
+      d_partialModel.getLowerBound(nonbasic);
+
+    DeltaRational diff = bound * coeff;
+    sum = sum + diff;
+  }
+  return sum;
+}
+
+/**
+ * Computes the value of a basic variable using the current assignment.
+ */
+DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){
+  Assert(d_tableau.isBasic(x));
+  DeltaRational sum(0);
+
+  for(Tableau::RowIterator i = d_tableau.rowIterator(x); !i.atEnd(); ++i){
+    const TableauEntry& entry = (*i);
+    ArithVar nonbasic = entry.getColVar();
+    if(nonbasic == x) continue;
+    const Rational& coeff = entry.getCoefficient();
+
+    const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe);
+    sum = sum + (assignment * coeff);
+  }
+  return sum;
+}
+
+bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){
+  for(Tableau::RowIterator iter = d_tableau.rowIterator(basic); !iter.atEnd(); ++iter){
+    const TableauEntry& entry = *iter;
+
+    ArithVar var = entry.getColVar();
+    if(var == basic) continue;
+    int sgn = entry.getCoefficient().sgn();
+    if(upperBound){
+      if( (sgn < 0 && !d_partialModel.hasLowerBound(var)) ||
+          (sgn > 0 && !d_partialModel.hasUpperBound(var))){
+        return false;
+      }
+    }else{
+      if( (sgn < 0 && !d_partialModel.hasUpperBound(var)) ||
+          (sgn > 0 && !d_partialModel.hasLowerBound(var))){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
+template <bool upperBound>
+void LinearEqualityModule::explainNonbasics(ArithVar basic, NodeBuilder<>& output){
+  Assert(d_tableau.isBasic(basic));
+
+  Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
+                                   << basic <<") start" << endl;
+
+
+  Tableau::RowIterator iter = d_tableau.rowIterator(basic);
+  for(; !iter.atEnd(); ++iter){
+    const TableauEntry& entry = *iter;
+    ArithVar nonbasic = entry.getColVar();
+    if(nonbasic == basic) continue;
+
+    const Rational& a_ij = entry.getCoefficient();
+    TNode bound = TNode::null();
+
+    int sgn = a_ij.sgn();
+    Assert(sgn != 0);
+    if(upperBound){
+      if(sgn < 0){
+        bound = d_partialModel.getLowerConstraint(nonbasic);
+      }else{
+        Assert(sgn > 0);
+        bound = d_partialModel.getUpperConstraint(nonbasic);
+      }
+    }else{
+      if(sgn < 0){
+        bound =  d_partialModel.getUpperConstraint(nonbasic);
+      }else{
+        Assert(sgn > 0);
+        bound =  d_partialModel.getLowerConstraint(nonbasic);
+      }
+    }
+    Assert(!bound.isNull());
+    Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound
+                                     << endl;
+    output << bound;
+  }
+  Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
+                                   << basic << ") done" << endl;
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
new file mode 100644
index 000000000..aa8a49238
--- /dev/null
+++ b/src/theory/arith/linear_equality.h
@@ -0,0 +1,163 @@
+/*********************                                                        */
+/*! \file linear_equality.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This module maintains the relationship between a Tableau and PartialModel.
+ **
+ ** This shares with the theory a Tableau, and a PartialModel that:
+ **  - satisfies the equalities in the Tableau, and
+ **  - the assignment for the non-basic variables satisfies their bounds.
+ ** This maintains the relationship needed by the SimplexDecisionProcedure.
+ **
+ ** In the language of Simplex for DPLL(T), this provides:
+ ** - update()
+ ** - pivotAndUpdate()
+ **
+ ** This class also provides utility functions that require
+ ** using both the Tableau and PartialModel.
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H
+#define __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H
+
+#include "theory/arith/delta_rational.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/tableau.h"
+
+#include "util/stats.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class LinearEqualityModule {
+private:
+  /**
+   * Manages information about the assignment and upper and lower bounds on the
+   * variables.
+   */
+  ArithPartialModel& d_partialModel;
+
+  /**
+   * Reference to the Tableau to operate upon.
+   */
+  Tableau& d_tableau;
+
+  /** Called whenever the value of a basic variable is updated. */
+  ArithVarCallBack& d_basicVariableUpdates;
+
+public:
+
+  /**
+   * Initailizes a LinearEqualityModule with a partial model, a tableau,
+   * and a callback function for when basic variables update their values.
+   */
+  LinearEqualityModule(ArithPartialModel& pm, Tableau& t, ArithVarCallBack& f):
+    d_partialModel(pm), d_tableau(t), d_basicVariableUpdates(f)
+  {}
+
+  /**
+   * 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);
+
+
+  ArithPartialModel& getPartialModel() const{ return d_partialModel; }
+  Tableau& getTableau() const{ return d_tableau; }
+
+
+  bool hasBounds(ArithVar basic, bool upperBound);
+  bool hasLowerBounds(ArithVar basic){
+    return hasBounds(basic, false);
+  }
+  bool hasUpperBounds(ArithVar basic){
+    return hasBounds(basic, true);
+  }
+
+private:
+  /**
+   * Exports either the explanation of an upperbound or a lower bound
+   * of the basic variable basic, using the non-basic variables in the row.
+   */
+  template <bool upperBound>
+  void explainNonbasics(ArithVar basic, NodeBuilder<>& output);
+
+public:
+  void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){
+    explainNonbasics<false>(basic, output);
+  }
+  void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){
+    explainNonbasics<true>(basic, output);
+  }
+
+  /**
+   * 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);
+
+  inline DeltaRational computeLowerBound(ArithVar basic){
+    return computeBound(basic, false);
+  }
+  inline DeltaRational computeUpperBound(ArithVar basic){
+    return computeBound(basic, true);
+  }
+
+private:
+  DeltaRational computeBound(ArithVar basic, bool upperBound);
+
+public:
+  /**
+   * Checks to make sure the assignment is consistent with the tableau.
+   * This code is for debugging.
+   */
+  void debugCheckTableau();
+
+  /** Debugging information for a pivot. */
+  void debugPivot(ArithVar x_i, ArithVar x_j);
+
+
+private:
+  /** These fields are designed to be accessable to TheoryArith methods. */
+  class Statistics {
+  public:
+    IntStat d_statPivots, d_statUpdates;
+
+    TimerStat d_pivotTime;
+
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
+
+};/* class LinearEqualityModule */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H */
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 4a126ec55..f113c4d34 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -209,21 +209,52 @@ TNode ArithPartialModel::getUpperConstraint(ArithVar x){
   return d_upperConstraint[x];
 }
 
-
-
-bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){
+int ArithPartialModel::cmpToLowerBound(ArithVar x, const DeltaRational& c){
   if(!hasLowerBound(x)){
     // l = -\intfy
     // ? c < -\infty |-  _|_
-    return false;
+    return 1;
+  }else{
+    return c.cmp(d_lowerBound[x]);
   }
-  if(strict){
-    return c < d_lowerBound[x];
+}
+
+int ArithPartialModel::cmpToUpperBound(ArithVar x, const DeltaRational& c){
+  if(!hasUpperBound(x)){
+    //u = \intfy
+    // ? c > \infty |-  _|_
+    return -1;
   }else{
-    return c <= d_lowerBound[x];
+    return c.cmp(d_upperBound[x]);
   }
 }
 
+// bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){
+//   if(!hasLowerBound(x)){
+//     // l = -\intfy
+//     // ? c < -\infty |-  _|_
+//     return false;
+//   }
+//   if(strict){
+//     return c < d_lowerBound[x];
+//   }else{
+//     return c <= d_lowerBound[x];
+//   }
+// }
+
+// bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
+//   if(!hasUpperBound(x)){
+//     // u = \intfy
+//     // ? c > \infty |-  _|_
+//     return false;
+//   }
+//   if(strict){
+//     return c > d_upperBound[x];
+//   }else{
+//     return c >= d_upperBound[x];
+//   }
+// }
+
 bool ArithPartialModel::equalsLowerBound(ArithVar x, const DeltaRational& c){
   if(!hasLowerBound(x)){
     return false;
@@ -239,18 +270,6 @@ bool ArithPartialModel::equalsUpperBound(ArithVar x, const DeltaRational& c){
   }
 }
 
-bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
-  if(!hasUpperBound(x)){
-    // u = \intfy
-    // ? c > \infty |-  _|_
-    return false;
-  }
-  if(strict){
-    return c > d_upperBound[x];
-  }else{
-    return c >= d_upperBound[x];
-  }
-}
 bool ArithPartialModel::hasEitherBound(ArithVar x){
   return hasLowerBound(x) || hasUpperBound(x);
 }
@@ -271,35 +290,35 @@ bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
   return  d_lowerBound[x] < d_assignment[x];
 }
 
-/**
- * x <= u
- * ? c < u
- */
-bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){
-  Assert(inMaps(x));
-  if(!hasUpperBound(x)){ // u = \infty
-    return true;
-  }
-  return c < d_upperBound[x];
-}
-
-/**
- * x <= u
- * ? c < u
- */
-bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){
-  Assert(inMaps(x));
-  if(!hasLowerBound(x)){ // l = -\infty
-    return true;
-  }
-  return  d_lowerBound[x] < c;
-}
+// /**
+//  * x <= u
+//  * ? c < u
+//  */
+// bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){
+//   Assert(inMaps(x));
+//   if(!hasUpperBound(x)){ // u = \infty
+//     return true;
+//   }
+//   return c < d_upperBound[x];
+// }
+
+// /**
+//  * x <= u
+//  * ? c < u
+//  */
+// bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){
+//   Assert(inMaps(x));
+//   if(!hasLowerBound(x)){ // l = -\infty
+//     return true;
+//   }
+//   return  d_lowerBound[x] < c;
+// }
 
 bool ArithPartialModel::assignmentIsConsistent(ArithVar x){
   const DeltaRational& beta = getAssignment(x);
 
   //l_i <= beta(x_i) <= u_i
-  return  !belowLowerBound(x,beta,true) && !aboveUpperBound(x,beta,true);
+  return  cmpToLowerBound(x,beta) >= 0 && cmpToUpperBound(x,beta) <= 0;
 }
 
 
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index cf0fc7d4e..d9fa51d8d 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -132,33 +132,52 @@ public:
   const DeltaRational& getAssignment(ArithVar x) const;
 
 
+  bool equalsLowerBound(ArithVar x, const DeltaRational& c);
+  bool equalsUpperBound(ArithVar x, const DeltaRational& c);
 
   /**
-   * x >= l
-   * ? c < l
+   * If lowerbound > - \infty:
+   *   return getAssignment(x).cmp(getLowerBound(x))
+   * If lowerbound = - \infty:
+   *   return 1
    */
-  bool belowLowerBound(ArithVar x, const DeltaRational& c, bool strict);
+  int cmpToLowerBound(ArithVar x, const DeltaRational& c);
 
-  /**
-   * x <= u
-   * ? c > u
-   */
-  bool aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict);
+  inline bool strictlyLessThanLowerBound(ArithVar x, const DeltaRational& c){
+    return cmpToLowerBound(x, c) < 0;
+  }
+  inline bool lessThanLowerBound(ArithVar x, const DeltaRational& c){
+    return cmpToLowerBound(x, c) <= 0;
+  }
 
-  bool equalsLowerBound(ArithVar x, const DeltaRational& c);
-  bool equalsUpperBound(ArithVar x, const DeltaRational& c);
+  inline bool strictlyGreaterThanLowerBound(ArithVar x, const DeltaRational& c){
+    return cmpToLowerBound(x, c) > 0;
+  }
 
   /**
-   * x <= u
-   * ? c < u
+   * If upperbound < \infty:
+   *   return getAssignment(x).cmp(getUpperBound(x))
+   * If upperbound = \infty:
+   *   return -1
    */
-  bool strictlyBelowUpperBound(ArithVar x, const DeltaRational& c);
+  int cmpToUpperBound(ArithVar x, const DeltaRational& c);
+
+  inline bool strictlyLessThanUpperBound(ArithVar x, const DeltaRational& c){
+    return cmpToUpperBound(x, c) < 0;
+  }
+
+  inline bool lessThanUpperBound(ArithVar x, const DeltaRational& c){
+    return cmpToUpperBound(x, c) <= 0;
+  }
+
+  inline bool strictlyGreaterThanUpperBound(ArithVar x, const DeltaRational& c){
+    return cmpToUpperBound(x, c) > 0;
+  }
+
+  inline bool greaterThanUpperBound(ArithVar x, const DeltaRational& c){
+    return cmpToUpperBound(x, c) >= 0;
+  }
 
-  /**
-   * x <= u
-   * ? c < u
-   */
-  bool strictlyAboveLowerBound(ArithVar x, const DeltaRational& c);
 
   bool strictlyBelowUpperBound(ArithVar x);
   bool strictlyAboveLowerBound(ArithVar x);
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 6f8d02642..7fce748dc 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -34,16 +34,15 @@ static const bool CHECK_AFTER_PIVOT = true;
 static const uint32_t VARORDER_CHECK_PERIOD = 200;
 
 SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager,
-                                                   ArithPartialModel& pm,
-                                                   Tableau& tableau) :
-  d_partialModel(pm),
-  d_tableau(tableau),
-  d_queue(pm, tableau),
+                                                   LinearEqualityModule& linEq) :
+  d_linEq(linEq),
+  d_partialModel(d_linEq.getPartialModel()),
+  d_tableau(d_linEq.getTableau()),
+  d_queue(d_partialModel, d_tableau),
   d_propManager(propManager),
   d_numVariables(0),
   d_delayedLemmas(),
   d_pivotsInRound(),
-  d_ZERO(0),
   d_DELTA_ZERO(0,0)
 {
   switch(Options::ArithPivotRule rule = Options::current()->pivotRule) {
@@ -62,10 +61,6 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager
 }
 
 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),
   d_findConflictOnTheQueueTime("theory::arith::findConflictOnTheQueueTime"),
   d_attemptBeforeDiffSearch("theory::arith::qi::BeforeDiffSearch::attempt",0),
@@ -82,18 +77,8 @@ SimplexDecisionProcedure::Statistics::Statistics():
   d_weakeningSuccesses("theory::arith::weakening::success",0),
   d_weakenings("theory::arith::weakening::total",0),
   d_weakenTime("theory::arith::weakening::time"),
-  d_boundComputationTime("theory::arith::bound::time"),
-  d_boundComputations("theory::arith::bound::boundComputations",0),
-  d_boundPropagations("theory::arith::bound::boundPropagations",0),
-  d_delayedConflicts("theory::arith::delayedConflicts",0),
-  d_pivotTime("theory::arith::pivotTime"),
-  d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"),
-  d_avgNumRowsNotContainingOnPivot("theory::arith::avgNumRowsNotContainingOnPivot")
+  d_delayedConflicts("theory::arith::delayedConflicts",0)
 {
-  StatisticsRegistry::registerStat(&d_statPivots);
-  StatisticsRegistry::registerStat(&d_statUpdates);
-  StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
-  StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
   StatisticsRegistry::registerStat(&d_statUpdateConflicts);
 
   StatisticsRegistry::registerStat(&d_findConflictOnTheQueueTime);
@@ -114,23 +99,10 @@ SimplexDecisionProcedure::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_weakenings);
   StatisticsRegistry::registerStat(&d_weakenTime);
 
-  StatisticsRegistry::registerStat(&d_boundComputationTime);
-  StatisticsRegistry::registerStat(&d_boundComputations);
-  StatisticsRegistry::registerStat(&d_boundPropagations);
-
   StatisticsRegistry::registerStat(&d_delayedConflicts);
-
-  StatisticsRegistry::registerStat(&d_pivotTime);
-
-  StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnUpdate);
-  StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnPivot);
 }
 
 SimplexDecisionProcedure::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_findConflictOnTheQueueTime);
@@ -151,356 +123,14 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_weakenings);
   StatisticsRegistry::unregisterStat(&d_weakenTime);
 
-  StatisticsRegistry::unregisterStat(&d_boundComputationTime);
-  StatisticsRegistry::unregisterStat(&d_boundComputations);
-  StatisticsRegistry::unregisterStat(&d_boundPropagations);
-
   StatisticsRegistry::unregisterStat(&d_delayedConflicts);
-  StatisticsRegistry::unregisterStat(&d_pivotTime);
-
-  StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnUpdate);
-  StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnPivot);
-}
-
-/* procedure AssertLower( x_i >= c_i ) */
-Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
-  Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
-
-  if(d_partialModel.belowLowerBound(x_i, c_i, true)){
-    return Node::null();
-  }
-
-  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 conflict;
-  }
-
-  d_partialModel.setLowerConstraint(x_i,original);
-  d_partialModel.setLowerBound(x_i, c_i);
-
-  d_updatedBounds.softAdd(x_i);
-
-  if(!d_tableau.isBasic(x_i)){
-    if(d_partialModel.getAssignment(x_i) < c_i){
-      update(x_i, c_i);
-    }
-  }else{
-    d_queue.enqueueIfInconsistent(x_i);
-  }
-
-  if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
-
-  return Node::null();
-}
-
-/* procedure AssertUpper( x_i <= c_i) */
-Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
-
-  Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
-
-  if(d_partialModel.aboveUpperBound(x_i, c_i, true) ){ // \upperbound(x_i) <= c_i
-    return Node::null(); //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);
-    return conflict;
-  }
-
-  d_partialModel.setUpperConstraint(x_i,original);
-  d_partialModel.setUpperBound(x_i, c_i);
-
-  d_updatedBounds.softAdd(x_i);
-
-  if(!d_tableau.isBasic(x_i)){
-    if(d_partialModel.getAssignment(x_i) > c_i){
-      update(x_i, c_i);
-    }
-  }else{
-    d_queue.enqueueIfInconsistent(x_i);
-  }
-
-  if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
-
-  return Node::null();
-}
-
-
-/* procedure AssertLower( x_i == c_i ) */
-Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){
-
-  Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
-
-  // 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 Node::null(); //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);
-    Debug("arith") << "AssertLower conflict " << conflict << endl;
-    return conflict;
-  }
-
-  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;
-    return conflict;
-  }
-
-  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_updatedBounds.softAdd(x_i);
-
-  if(!d_tableau.isBasic(x_i)){
-    if(!(d_partialModel.getAssignment(x_i) == c_i)){
-      update(x_i, c_i);
-    }
-  }else{
-    d_queue.enqueueIfInconsistent(x_i);
-  }
-  return Node::null();
-}
-
-void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
-  Assert(!d_tableau.isBasic(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;
-
-  //Assert(matchingSets(d_tableau, x_i));
-  Tableau::ColIterator basicIter = d_tableau.colIterator(x_i);
-  for(; !basicIter.atEnd(); ++basicIter){
-    const TableauEntry& entry = *basicIter;
-    Assert(entry.getColVar() == x_i);
-
-    ArithVar x_j = entry.getRowVar();
-    //ReducedRowVector& row_j = d_tableau.lookup(x_j);
-
-    //const Rational& a_ji = row_j.lookup(x_i);
-    const Rational& a_ji = entry.getCoefficient();
-
-    const DeltaRational& assignment = d_partialModel.getAssignment(x_j);
-    DeltaRational  nAssignment = assignment+(diff * a_ji);
-    d_partialModel.setAssignment(x_j, nAssignment);
-
-    d_queue.enqueueIfInconsistent(x_j);
-  }
-
-  d_partialModel.setAssignment(x_i, v);
-
-  Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_i));
-  double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_i));
-
-  (d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference);
-  if(Debug.isOn("paranoid:check_tableau")){  debugCheckTableau(); }
-}
-
-
-bool SimplexDecisionProcedure::propagateCandidateBound(ArithVar basic, bool upperBound){
-
-  DeltaRational bound = upperBound ?
-    computeUpperBound(basic):
-    computeLowerBound(basic);
-
-  if((upperBound && d_partialModel.strictlyBelowUpperBound(basic, bound)) ||
-     (!upperBound && d_partialModel.strictlyAboveLowerBound(basic, bound))){
-    Node bestImplied = upperBound ?
-      d_propManager.getBestImpliedUpperBound(basic, bound):
-      d_propManager.getBestImpliedLowerBound(basic, bound);
-
-    if(!bestImplied.isNull()){
-      bool asserted = d_propManager.isAsserted(bestImplied);
-      bool propagated = d_propManager.isPropagated(bestImplied);
-      if( !asserted && !propagated){
-
-        NodeBuilder<> nb(kind::AND);
-        if(upperBound){
-          explainNonbasicsUpperBound(basic, nb);
-        }else{
-          explainNonbasicsLowerBound(basic, nb);
-        }
-        Node explanation = nb;
-        d_propManager.propagate(bestImplied, explanation, false);
-        return true;
-      }else{
-        Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl;
-      }
-    }
-  }
-  return false;
-}
-
-
-bool SimplexDecisionProcedure::hasBounds(ArithVar basic, bool upperBound){
-  for(Tableau::RowIterator iter = d_tableau.rowIterator(basic); !iter.atEnd(); ++iter){
-    const TableauEntry& entry = *iter;
-
-    ArithVar var = entry.getColVar();
-    if(var == basic) continue;
-    int sgn = entry.getCoefficient().sgn();
-    if(upperBound){
-      if( (sgn < 0 && !d_partialModel.hasLowerBound(var)) ||
-          (sgn > 0 && !d_partialModel.hasUpperBound(var))){
-        return false;
-      }
-    }else{
-      if( (sgn < 0 && !d_partialModel.hasUpperBound(var)) ||
-          (sgn > 0 && !d_partialModel.hasLowerBound(var))){
-        return false;
-      }
-    }
-  }
-  return true;
 }
-void SimplexDecisionProcedure::propagateCandidate(ArithVar basic){
-  bool success = false;
-  if(d_partialModel.strictlyAboveLowerBound(basic) && hasLowerBounds(basic)){
-    ++d_statistics.d_boundComputations;
-    success |= propagateCandidateLowerBound(basic);
-  }
-  if(d_partialModel.strictlyBelowUpperBound(basic) && hasUpperBounds(basic)){
-    ++d_statistics.d_boundComputations;
-    success |= propagateCandidateUpperBound(basic);
-  }
-  if(success){
-    ++d_statistics.d_boundPropagations;
-  }
-}
-
-void SimplexDecisionProcedure::propagateCandidates(){
-  TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
 
-  Assert(d_candidateBasics.empty());
 
-  if(d_updatedBounds.empty()){ return; }
 
-  PermissiveBackArithVarSet::const_iterator i = d_updatedBounds.begin();
-  PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end();
-  for(; i != end; ++i){
-    ArithVar var = *i;
-    if(d_tableau.isBasic(var) &&
-       d_tableau.getRowLength(var) <= Options::current()->arithPropagateMaxLength){
-      d_candidateBasics.softAdd(var);
-    }else{
-      Tableau::ColIterator basicIter = d_tableau.colIterator(var);
-      for(; !basicIter.atEnd(); ++basicIter){
-        const TableauEntry& entry = *basicIter;
-        ArithVar rowVar = entry.getRowVar();
-        Assert(entry.getColVar() == var);
-        Assert(d_tableau.isBasic(rowVar));
-        if(d_tableau.getRowLength(rowVar) <= Options::current()->arithPropagateMaxLength){
-          d_candidateBasics.softAdd(rowVar);
-        }
-      }
-    }
-  }
-  d_updatedBounds.purge();
-
-  while(!d_candidateBasics.empty()){
-    ArithVar candidate = d_candidateBasics.pop_back();
-    Assert(d_tableau.isBasic(candidate));
-    propagateCandidate(candidate); 
-  }
-}
 
 
-void SimplexDecisionProcedure::debugPivotSimplex(ArithVar x_i, ArithVar x_j){
-  Debug("arith::simplex:row") << "debugRowSimplex("
-                              << x_i  << "|->" << x_j
-                              << ")" << endl;
 
-  for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){
-    const TableauEntry& entry = *iter;
-
-    ArithVar var = entry.getColVar();
-    const Rational& coeff = entry.getCoefficient();
-    DeltaRational beta = d_partialModel.getAssignment(var);
-    Debug("arith::simplex:row") << var << beta << coeff;
-    if(d_partialModel.hasLowerBound(var)){
-      Debug("arith::simplex:row") << "(lb " << d_partialModel.getLowerBound(var) << ")";
-    }
-    if(d_partialModel.hasUpperBound(var)){
-      Debug("arith::simplex:row") << "(up " << d_partialModel.getUpperBound(var) << ")";
-    }
-    Debug("arith::simplex:row") << endl;
-  }
-  Debug("arith::simplex:row") << "end row"<< endl;
-}
-
-void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
-  Assert(x_i != x_j);
-
-  TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
-
-  if(Debug.isOn("arith::simplex:row")){ debugPivotSimplex(x_i, x_j); }
-
-  const TableauEntry& entry_ij =  d_tableau.findEntry(x_i, x_j);
-  Assert(!entry_ij.blank());
-
-
-  const Rational& a_ij = entry_ij.getCoefficient();
-
-
-  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);
-
-
-  //Assert(matchingSets(d_tableau, x_j));
-  for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){
-    const TableauEntry& entry = *iter;
-    Assert(entry.getColVar() == x_j);
-    ArithVar x_k = entry.getRowVar();
-    if(x_k != x_i ){
-      const Rational& a_kj = entry.getCoefficient();
-      DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
-      d_partialModel.setAssignment(x_k, nextAssignment);
-
-      d_queue.enqueueIfInconsistent(x_k);
-    }
-  }
-
-  // Pivots
-  ++(d_statistics.d_statPivots);
-
-  Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_j));
-  double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_j));
-  (d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference);
-  d_tableau.pivot(x_i, x_j);
-
-
-  d_queue.enqueueIfInconsistent(x_j);
-
-  if(Debug.isOn("tableau")){
-    d_tableau.printTableau();
-  }
-}
 
 ArithVar SimplexDecisionProcedure::minVarOrder(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){
   Assert(x != ARITHVAR_SENTINEL);
@@ -615,15 +245,14 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool re
   return firstConflict;
 }
 
-Node SimplexDecisionProcedure::updateInconsistentVars(){
+Node SimplexDecisionProcedure::findModel(){
   if(d_queue.empty()){
     return Node::null();
   }
 
   static CVC4_THREADLOCAL(unsigned int) instance = 0;
   instance = instance + 1;
-  Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() "
-                                         << instance << endl;
+  Debug("arith::findModel") << "begin findModel()" << instance << endl;
 
   d_queue.transitionToDifferenceMode();
 
@@ -678,8 +307,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
 
   Assert(d_queue.inCollectionMode());
 
-  Debug("arith::updateInconsistentVars") << "end updateInconsistentVars() "
-                                         << instance << endl;
+  Debug("arith::findModel") << "end findModel() " << instance << endl;
 
   return possibleConflict;
 }
@@ -689,12 +317,12 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
   Assert(d_tableau.isBasic(basic));
   const DeltaRational& beta = d_partialModel.getAssignment(basic);
 
-  if(d_partialModel.belowLowerBound(basic, beta, true)){
+  if(d_partialModel.strictlyLessThanLowerBound(basic, beta)){
     ArithVar x_j = selectSlackUpperBound(basic);
     if(x_j == ARITHVAR_SENTINEL ){
       return generateConflictBelowLowerBound(basic);
     }
-  }else if(d_partialModel.aboveUpperBound(basic, beta, true)){
+  }else if(d_partialModel.strictlyGreaterThanUpperBound(basic, beta)){
     ArithVar x_j = selectSlackLowerBound(basic);
     if(x_j == ARITHVAR_SENTINEL ){
       return generateConflictAboveUpperBound(basic);
@@ -706,11 +334,11 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
 //corresponds to Check() in dM06
 //template <SimplexDecisionProcedure::PreferenceFunction pf>
 Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
-  Debug("arith") << "updateInconsistentVars" << endl;
+  Debug("arith") << "searchForFeasibleSolution" << endl;
   Assert(remainingIterations > 0);
 
   while(remainingIterations > 0){
-    if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); }
+    if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
     ArithVar x_i = d_queue.dequeueInconsistentBasicVariable();
     Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
@@ -737,23 +365,23 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
     DeltaRational beta_i = d_partialModel.getAssignment(x_i);
     ArithVar x_j = ARITHVAR_SENTINEL;
 
-    if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
+    if(d_partialModel.strictlyLessThanLowerBound(x_i, beta_i)){
       x_j = selectSlackUpperBound(x_i, pf);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         return generateConflictBelowLowerBound(x_i); //unsat
       }
       DeltaRational l_i = d_partialModel.getLowerBound(x_i);
-      pivotAndUpdate(x_i, x_j, l_i);
+      d_linEq.pivotAndUpdate(x_i, x_j, l_i);
 
-    }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
+    }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, beta_i)){
       x_j = selectSlackLowerBound(x_i, pf);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         return generateConflictAboveUpperBound(x_i); //unsat
       }
       DeltaRational u_i = d_partialModel.getUpperBound(x_i);
-      pivotAndUpdate(x_i, x_j, u_i);
+      d_linEq.pivotAndUpdate(x_i, x_j, u_i);
     }
     Assert(x_j != ARITHVAR_SENTINEL);
 
@@ -770,49 +398,6 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
   return Node::null();
 }
 
-template <bool upperBound>
-void SimplexDecisionProcedure::explainNonbasics(ArithVar basic, NodeBuilder<>& output){
-  Assert(d_tableau.isBasic(basic));
-
-  Debug("arith::explainNonbasics") << "SimplexDecisionProcedure::explainNonbasics("
-                                   << basic <<") start" << endl;
-
-
-  Tableau::RowIterator iter = d_tableau.rowIterator(basic);
-  for(; !iter.atEnd(); ++iter){
-    const TableauEntry& entry = *iter;
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == basic) continue;
-
-    const Rational& a_ij = entry.getCoefficient();
-    Assert(a_ij != d_ZERO);
-    TNode bound = TNode::null();
-
-    int sgn = a_ij.sgn();
-    Assert(sgn != 0);
-    if(upperBound){
-      if(sgn < 0){
-        bound = d_partialModel.getLowerConstraint(nonbasic);
-      }else{
-        Assert(sgn > 0);
-        bound = d_partialModel.getUpperConstraint(nonbasic);
-      }
-    }else{
-      if(sgn < 0){
-        bound =  d_partialModel.getUpperConstraint(nonbasic);
-      }else{
-        Assert(sgn > 0);
-        bound =  d_partialModel.getLowerConstraint(nonbasic);
-      }
-    }
-    Assert(!bound.isNull());
-    Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound
-                                     << endl;
-    output << bound;
-  }
-  Debug("arith::explainNonbasics") << "SimplexDecisionProcedure::explainNonbasics("
-                                   << basic << ") done" << endl;
-}
 
 
 TNode SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){
@@ -912,75 +497,3 @@ Node SimplexDecisionProcedure::generateConflictBelowLowerBound(ArithVar conflict
   return weakenConflict(false, conflictVar);
 }
 
-/**
- * Computes the value of a basic variable using the current assignment.
- */
-DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe){
-  Assert(d_tableau.isBasic(x));
-  DeltaRational sum(0);
-
-  for(Tableau::RowIterator i = d_tableau.rowIterator(x); !i.atEnd(); ++i){
-    const TableauEntry& entry = (*i);
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == x) continue;
-    const Rational& coeff = entry.getCoefficient();
-
-    const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe);
-    sum = sum + (assignment * coeff);
-  }
-  return sum;
-}
-
-DeltaRational SimplexDecisionProcedure::computeBound(ArithVar basic, bool upperBound){
-  DeltaRational sum(0,0);
-  for(Tableau::RowIterator i = d_tableau.rowIterator(basic); !i.atEnd(); ++i){
-    const TableauEntry& entry = (*i);
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == basic) continue;
-    const Rational& coeff =  entry.getCoefficient();
-    int sgn = coeff.sgn();
-    bool ub = upperBound ? (sgn > 0) : (sgn < 0);
-
-    const DeltaRational& bound = ub ?
-      d_partialModel.getUpperBound(nonbasic):
-      d_partialModel.getLowerBound(nonbasic);
-
-    DeltaRational diff = bound * coeff;
-    sum = sum + diff;
-  }
-  return sum;
-}
-
-/**
- * This check is quite expensive.
- * It should be wrapped in a Debug.isOn() guard.
- *   if(Debug.isOn("paranoid:check_tableau")){
- *      checkTableau();
- *   }
- */
-void SimplexDecisionProcedure::debugCheckTableau(){
-  ArithVarSet::const_iterator basicIter = d_tableau.beginBasic();
-  ArithVarSet::const_iterator endIter = d_tableau.endBasic();
-  for(; basicIter != endIter; ++basicIter){
-    ArithVar basic = *basicIter;
-    DeltaRational sum;
-    Debug("paranoid:check_tableau") << "starting row" << basic << endl;
-    Tableau::RowIterator nonbasicIter = d_tableau.rowIterator(basic);
-    for(; !nonbasicIter.atEnd(); ++nonbasicIter){
-      const TableauEntry& entry = *nonbasicIter;
-      ArithVar nonbasic = entry.getColVar();
-      if(basic == nonbasic) continue;
-
-      const Rational& coeff = entry.getCoefficient();
-      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
index 04b4ca784..d69de3756 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -11,10 +11,37 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief This is an implementation of the Simplex Module for the Simplex for DPLL(T) decision procedure.
  **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure.
+ ** See the Simplex for DPLL(T) technical report for more background.(citation?)
+ ** This shares with the theory a Tableau, and a PartialModel that:
+ **  - satisfies the equalities in the Tableau, and
+ **  - the assignment for the non-basic variables satisfies their bounds.
+ ** This is required to either produce a conflict or satisifying PartialModel.
+ ** Further, we require being told when a basic variable updates its value.
+ **
+ ** During the Simplex search we maintain a queue of variables.
+ ** The queue is required to contain all of the basic variables that voilate their bounds.
+ ** As elimination from the queue is more efficient to be done lazily,
+ ** we do not maintain that the queue of variables needs to be only basic variables or only variables that satisfy their bounds.
+ **
+ ** The simplex procedure roughly follows Alberto's thesis. (citation?)
+ ** There is one round of selecting using a hueristic pivoting rule. (See PreferenceFunction Documentation for the available options.)
+ ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that Leonardo invented this first.)
+ ** After this, Bland's pivot rule is invoked.
+ **
+ ** During this proccess, we periodically inspect the queue of variables to
+ ** 1) remove now extraneous extries,
+ ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the current queue hueristics, and
+ ** 3) detect multiple conflicts.
+ **
+ ** Conflicts are greedily slackened to use the weakest bounds that still produce the conflict.
+ **
+ ** Extra things tracked atm: (Subject to change at Tim's whims)
+ ** - A superset of all of the newly pivoted variables.
+ ** - A queue of additional conflicts that were discovered by Simplex.
+ **   These are theory valid and are currently turned into lemmas
  **/
 
 
@@ -30,6 +57,7 @@
 #include "theory/arith/tableau.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/arith_prop_manager.h"
+#include "theory/arith/linear_equality.h"
 
 #include "util/options.h"
 
@@ -44,70 +72,69 @@ namespace arith {
 class SimplexDecisionProcedure {
 private:
 
+  /** Linear equality module. */
+  LinearEqualityModule& d_linEq;
+
   /**
    * Manages information about the assignment and upper and lower bounds on
    * variables.
+   * Partial model matches that in LinearEqualityModule.
    */
   ArithPartialModel& d_partialModel;
 
+  /**
+   * Stores the linear equalities used by Simplex.
+   * Tableau from the LinearEquality module.
+   */
   Tableau& d_tableau;
+
+  /** Contains a superset of the basic variables in violation of their bounds. */
   ArithPriorityQueue d_queue;
 
+  /** A link to the propagation manager. This is used to generate weaker conflicts. */
   ArithPropManager& d_propManager;
 
+  /** Number of variables in the system. This is used for tuning heuristics. */
   ArithVar d_numVariables;
 
   std::queue<Node> d_delayedLemmas;
 
-  PermissiveBackArithVarSet d_updatedBounds;
-  PermissiveBackArithVarSet d_candidateBasics;
-
+  /** Maps a variable to how many times they have been used as a pivot in the simplex search. */
   ArithVarMultiset d_pivotsInRound;
 
-  Rational d_ZERO;
+  /** Stores to the DeltaRational constant 0. */
   DeltaRational d_DELTA_ZERO;
 
 public:
   SimplexDecisionProcedure(ArithPropManager& propManager,
-                           ArithPartialModel& pm,
-                           Tableau& tableau);
+                           LinearEqualityModule& linEq);
 
+  /**
+   * This must be called when the value of a basic variable may now voilate one
+   * of its bounds.
+   */
+  void updateBasic(ArithVar x){
+    d_queue.enqueueIfInconsistent(x);
+  }
 
   /**
-   * 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.
+   * Tries to update the assignments of variables such that all of the
+   * assignments are consistent with their bounds.
+   * This is done by a simplex search through the possible bases of the tableau.
    *
-   * orig must be a literal in the SAT solver so that it can be used for
-   * conflict analysis.
+   * If all of the variables can be made consistent with their bounds
+   * Node::null() is returned. Otherwise a minimized conflict is returned.
    *
-   * x is the variable getting the new bound,
-   * c is the value of the new bound.
+   * Tableau pivoting is performed so variables may switch from being basic to
+   * nonbasic and vice versa.
    *
-   * If this new bound is in conflict with the other bound,
-   * a node describing this conflict is returned.
-   * If this new bound is not in conflict, Node::null() is returned.
+   * Corresponds to the "check()" procedure in [Cav06].
    */
-  Node AssertLower(ArithVar x, const DeltaRational& c, TNode orig);
-  Node AssertUpper(ArithVar x, const DeltaRational& c, TNode orig);
-  Node AssertEquality(ArithVar x, const DeltaRational& c, TNode orig);
+  Node findModel();
 
 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);
-
-private:
-  /**
    * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure,
    * and 2 ArithVar variables and returns one of the ArithVar variables potentially
    * using the internals of the SimplexDecisionProcedure.
@@ -119,7 +146,7 @@ private:
   /**
    * minVarOrder is a PreferenceFunction for selecting the smaller of the 2 ArithVars.
    * This PreferenceFunction is used during the VarOrder stage of
-   * updateInconsistentVars.
+   * findModel.
    */
   static ArithVar minVarOrder(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
 
@@ -128,7 +155,7 @@ private:
    * row count in the tableau.
    *
    * This is a hueristic rule and should not be used
-   * during the VarOrder stage of updateInconsistentVars.
+   * during the VarOrder stage of findModel.
    */
   static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
   /**
@@ -138,27 +165,13 @@ private:
    * the rule falls back to minRowCount(...).
    *
    * This is a hueristic rule and should not be used
-   * during the VarOrder stage of updateInconsistentVars.
+   * during the VarOrder stage of findModel.
    */
   static ArithVar minBoundAndRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
 
-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 searchForFeasibleSolution(uint32_t maxIterations);
 
@@ -193,23 +206,6 @@ private:
    */
   ArithVar selectSmallestInconsistentVar();
 
-
-  /**
-   * Exports either the explanation of an upperbound or a lower bound
-   * of the basic variable basic, using the non-basic variables in the row.
-   */
-  template <bool upperBound>
-  void explainNonbasics(ArithVar basic, NodeBuilder<>& output);
-  void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){
-    explainNonbasics<false>(basic, output);
-  }
-  void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){
-    explainNonbasics<true>(basic, output);
-  }
-
-  Node deduceUpperBound(ArithVar basicVar);
-  Node deduceLowerBound(ArithVar basicVar);
-
   /**
    * Given a non-basic variable that is know to not be updatable
    * to a consistent value, construct and return a conflict.
@@ -219,29 +215,6 @@ private:
   Node generateConflictBelowLowerBound(ArithVar conflictVar);
 
 public:
-  /**
-   * Checks to make sure the assignment is consistent with the tableau.
-   * This code is for debugging.
-   */
-  void debugCheckTableau();
-  void debugPivotSimplex(ArithVar x_i, ArithVar x_j);
-
-
-  /**
-   * 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);
-
-  bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
-  void clearUpdates(){
-    d_updatedBounds.purge();
-  }
-  void propagateCandidates();
-
   void increaseMax() {d_numVariables++;}
 
   /** Returns true if the simplex procedure has more delayed lemmas in its queue.*/
@@ -288,39 +261,11 @@ private:
   Node weakenConflict(bool aboveUpper, ArithVar basicVar);
   TNode weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic);
 
-  void propagateCandidate(ArithVar basic);
-  bool propagateCandidateBound(ArithVar basic, bool upperBound);
-
-  inline bool propagateCandidateLowerBound(ArithVar basic){
-    return propagateCandidateBound(basic, false);
-  }
-  inline bool propagateCandidateUpperBound(ArithVar basic){
-    return propagateCandidateBound(basic, true);
-  }
-
-  bool hasBounds(ArithVar basic, bool upperBound);
-  bool hasLowerBounds(ArithVar basic){
-    return hasBounds(basic, false);
-  }
-  bool hasUpperBounds(ArithVar basic){
-    return hasBounds(basic, true);
-  }
-  DeltaRational computeBound(ArithVar basic, bool upperBound);
-
-  inline DeltaRational computeLowerBound(ArithVar basic){
-    return computeBound(basic, false);
-  }
-  inline DeltaRational computeUpperBound(ArithVar basic){
-    return computeBound(basic, true);
-  }
 
 
   /** These fields are designed to be accessable to TheoryArith methods. */
   class Statistics {
   public:
-    IntStat d_statPivots, d_statUpdates;
-
-    IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts;
     IntStat d_statUpdateConflicts;
 
     TimerStat d_findConflictOnTheQueueTime;
@@ -334,16 +279,9 @@ private:
     IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings;
     TimerStat d_weakenTime;
 
-    TimerStat d_boundComputationTime;
-    IntStat d_boundComputations, d_boundPropagations;
 
     IntStat d_delayedConflicts;
 
-    TimerStat d_pivotTime;
-
-    AverageStat d_avgNumRowsNotContainingOnUpdate;
-    AverageStat d_avgNumRowsNotContainingOnPivot;
-
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index b10fc964d..1137ca7b7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -56,6 +56,7 @@ using namespace CVC4::theory::arith;
 
 static const uint32_t RESET_START = 2;
 
+
 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
   Theory(THEORY_ARITH, c, u, out, valuation),
   d_hasDoneWorkSinceCut(false),
@@ -65,9 +66,10 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_constantIntegerVariables(c),
   d_CivIterator(c,0),
   d_varsInDioSolver(c),
-  d_partialModel(c, d_differenceManager),
   d_diseq(c),
+  d_partialModel(c, d_differenceManager),
   d_tableau(),
+  d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack),
   d_diosolver(c),
   d_pbSubstitutions(u),
   d_restartsCounter(0),
@@ -77,7 +79,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_atomDatabase(c, out),
   d_propManager(c, d_arithvarNodeMap, d_atomDatabase, valuation),
   d_differenceManager(c, d_propManager),
-  d_simplex(d_propManager, d_partialModel, d_tableau),
+  d_simplex(d_propManager, d_linEq),
+  d_basicVarModelUpdateCallBack(d_simplex),
   d_DELTA_ZERO(0),
   d_statistics()
 {}
@@ -85,6 +88,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
 TheoryArith::~TheoryArith(){}
 
 TheoryArith::Statistics::Statistics():
+  d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
+  d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
   d_statUserVariables("theory::arith::UserVariables", 0),
   d_statSlackVariables("theory::arith::SlackVariables", 0),
   d_statDisequalitySplits("theory::arith::DisequalitySplits", 0),
@@ -97,8 +102,14 @@ TheoryArith::Statistics::Statistics():
   d_initialTableauSize("theory::arith::initialTableauSize", 0),
   d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
   d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
-  d_restartTimer("theory::arith::restartTimer")
+  d_restartTimer("theory::arith::restartTimer"),
+  d_boundComputationTime("theory::arith::bound::time"),
+  d_boundComputations("theory::arith::bound::boundComputations",0),
+  d_boundPropagations("theory::arith::bound::boundPropagations",0)
 {
+  StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
+  StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
+
   StatisticsRegistry::registerStat(&d_statUserVariables);
   StatisticsRegistry::registerStat(&d_statSlackVariables);
   StatisticsRegistry::registerStat(&d_statDisequalitySplits);
@@ -115,9 +126,16 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_currSetToSmaller);
   StatisticsRegistry::registerStat(&d_smallerSetToCurr);
   StatisticsRegistry::registerStat(&d_restartTimer);
+
+  StatisticsRegistry::registerStat(&d_boundComputationTime);
+  StatisticsRegistry::registerStat(&d_boundComputations);
+  StatisticsRegistry::registerStat(&d_boundPropagations);
 }
 
 TheoryArith::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
+  StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
+
   StatisticsRegistry::unregisterStat(&d_statUserVariables);
   StatisticsRegistry::unregisterStat(&d_statSlackVariables);
   StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
@@ -134,6 +152,186 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
   StatisticsRegistry::unregisterStat(&d_smallerSetToCurr);
   StatisticsRegistry::unregisterStat(&d_restartTimer);
+
+  StatisticsRegistry::unregisterStat(&d_boundComputationTime);
+  StatisticsRegistry::unregisterStat(&d_boundComputations);
+  StatisticsRegistry::unregisterStat(&d_boundPropagations);
+}
+
+/* procedure AssertLower( x_i >= c_i ) */
+Node TheoryArith::AssertLower(ArithVar x_i, DeltaRational& c_i, TNode original){
+  Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
+
+  if(isInteger(x_i)){
+    c_i = DeltaRational(c_i.ceiling());
+  }
+
+  //TODO Relax to less than?
+  if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
+    return Node::null();
+  }
+
+  int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
+  if(cmpToUB > 0){ //  c_i < \lowerbound(x_i)
+    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 conflict;
+  }else if(cmpToUB == 0){
+    if(isInteger(x_i)){
+      d_constantIntegerVariables.push_back(x_i);
+    }
+    //check to make sure x_i != c_i has not been asserted
+    Node left  = d_arithvarNodeMap.asNode(x_i);
+
+    // if lowerbound and upperbound are equal, then the infinitesimal must be 0
+    Assert(c_i.getInfinitesimalPart().isZero());
+    Node right = mkRationalNode(c_i.getNoninfinitesimalPart());
+
+    Node diseq = left.eqNode(right).notNode();
+    if (d_diseq.find(diseq) != d_diseq.end()) {
+      Node lb = d_partialModel.getLowerConstraint(x_i);
+      return disequalityConflict(diseq, lb , original);
+    }
+  }
+
+  d_partialModel.setLowerConstraint(x_i,original);
+  d_partialModel.setLowerBound(x_i, c_i);
+
+  d_updatedBounds.softAdd(x_i);
+
+  if(!d_tableau.isBasic(x_i)){
+    if(d_partialModel.getAssignment(x_i) < c_i){
+      d_linEq.update(x_i, c_i);
+    }
+  }else{
+    d_simplex.updateBasic(x_i);
+  }
+
+  if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
+
+  return Node::null();
+}
+
+/* procedure AssertUpper( x_i <= c_i) */
+Node TheoryArith::AssertUpper(ArithVar x_i, DeltaRational& c_i, TNode original){
+  Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
+
+  if(isInteger(x_i)){
+    c_i = DeltaRational(c_i.floor());
+  }
+
+  Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
+
+  if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
+    return Node::null(); //sat
+  }
+
+  // cmpToLb =  \lowerbound(x_i).cmp(c_i)
+  int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
+  if( cmpToLB < 0 ){ //  \upperbound(x_i) < \lowerbound(x_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);
+    return conflict;
+  }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
+    if(isInteger(x_i)){
+      d_constantIntegerVariables.push_back(x_i);
+    }
+
+    //check to make sure x_i != c_i has not been asserted
+    Node left  = d_arithvarNodeMap.asNode(x_i);
+
+    // if lowerbound and upperbound are equal, then the infinitesimal must be 0
+    Assert(c_i.getInfinitesimalPart().isZero());
+    Node right = mkRationalNode(c_i.getNoninfinitesimalPart());
+
+    Node diseq = left.eqNode(right).notNode();
+    if (d_diseq.find(diseq) != d_diseq.end()) {
+      Node lb = d_partialModel.getLowerConstraint(x_i);
+      return disequalityConflict(diseq, lb , original);
+    }
+  }
+
+  d_partialModel.setUpperConstraint(x_i,original);
+  d_partialModel.setUpperBound(x_i, c_i);
+
+  d_updatedBounds.softAdd(x_i);
+
+  if(!d_tableau.isBasic(x_i)){
+    if(d_partialModel.getAssignment(x_i) > c_i){
+      d_linEq.update(x_i, c_i);
+    }
+  }else{
+    d_simplex.updateBasic(x_i);
+  }
+
+  if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
+
+  return Node::null();
+}
+
+
+/* procedure AssertLower( x_i == c_i ) */
+Node TheoryArith::AssertEquality(ArithVar x_i, DeltaRational& c_i, TNode original){
+
+  Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
+
+  int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
+  int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_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(cmpToUB >= 0 && cmpToLB <= 0){
+    return Node::null(); //sat
+  }
+
+  if(cmpToUB > 0){
+    Node ubc = d_partialModel.getUpperConstraint(x_i);
+    Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
+    Debug("arith") << "AssertLower conflict " << conflict << endl;
+    return conflict;
+  }
+
+  if(cmpToLB < 0){
+    Node lbc = d_partialModel.getLowerConstraint(x_i);
+    Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
+    Debug("arith") << "AssertUpper conflict " << conflict << endl;
+    return conflict;
+  }
+
+  Assert(cmpToUB <= 0);
+  Assert(cmpToLB >= 0);
+  Assert(cmpToUB < 0 || cmpToLB > 0);
+
+
+  if(isInteger(x_i)){
+    d_constantIntegerVariables.push_back(x_i);
+  }
+
+  // Don't bother to check whether x_i != c_i is in d_diseq
+  // The a and (not a) should never be on the fact queue
+
+  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_updatedBounds.softAdd(x_i);
+
+  if(!d_tableau.isBasic(x_i)){
+    if(!(d_partialModel.getAssignment(x_i) == c_i)){
+      d_linEq.update(x_i, c_i);
+    }
+  }else{
+    d_simplex.updateBasic(x_i);
+  }
+  return Node::null();
 }
 
 
@@ -482,8 +680,8 @@ void TheoryArith::setupInitialValue(ArithVar x){
 
     //This can go away if the tableau creation is done at preregister
     //time instead of register
-    DeltaRational safeAssignment = d_simplex.computeRowValue(x, true);
-    DeltaRational assignment = d_simplex.computeRowValue(x, false);
+    DeltaRational safeAssignment = d_linEq.computeRowValue(x, true);
+    DeltaRational assignment = d_linEq.computeRowValue(x, false);
     d_partialModel.initialize(x,safeAssignment);
     d_partialModel.setAssignment(x,assignment);
   }
@@ -634,69 +832,33 @@ Node TheoryArith::assertionCases(TNode assertion){
   ArithVar x_i = determineLeftVariable(assertion, simpleKind);
   DeltaRational c_i = determineRightConstant(assertion, simpleKind);
 
-  bool tightened = false;
+  // bool tightened = false;
 
-  //If the variable is an integer tighen the constraint.
-  if(isInteger(x_i)){
-    if(simpleKind == LT){
-      tightened = true;
-      c_i = DeltaRational(c_i.floor());
-    }else if(simpleKind == GT){
-      tightened = true;
-      c_i = DeltaRational(c_i.ceiling());
-    }
-  }
+  // //If the variable is an integer tighen the constraint.
+  // if(isInteger(x_i)){
+  //   if(simpleKind == LT){
+  //     tightened = true;
+  //     c_i = DeltaRational(c_i.floor());
+  //   }else if(simpleKind == GT){
+  //     tightened = true;
+  //     c_i = DeltaRational(c_i.ceiling());
+  //   }
+  // }
 
   Debug("arith::assertions")  << "arith assertion @" << getContext()->getLevel()
                               <<"(" << assertion
-			     << " \\-> "
-			     << x_i<<" "<< simpleKind <<" "<< c_i << ")" << std::endl;
+                              << " \\-> "
+                              << x_i<<" "<< simpleKind <<" "<< c_i << ")" << std::endl;
 
   switch(simpleKind){
   case LEQ:
   case LT:
-    if(simpleKind == LEQ || (simpleKind == LT && tightened)){
-      if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) {
-        //If equal
-        TNode left  = getSide<false>(assertion, simpleKind);
-        TNode right = getSide<true>(assertion, simpleKind);
-
-        Node diseq = left.eqNode(right).notNode();
-        if (d_diseq.find(diseq) != d_diseq.end()) {
-          Node lb = d_partialModel.getLowerConstraint(x_i);
-          return disequalityConflict(diseq, lb , assertion);
-        }
-
-        if(isInteger(x_i)){
-          d_constantIntegerVariables.push_back(x_i);
-        }
-      }
-    }
-    return  d_simplex.AssertUpper(x_i, c_i, assertion);
+    return  AssertUpper(x_i, c_i, assertion);
   case GEQ:
   case GT:
-    if(simpleKind == GEQ || (simpleKind == GT && tightened)){
-      if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) {
-        //If equal
-        TNode left  = getSide<false>(assertion, simpleKind);
-        TNode right = getSide<true>(assertion, simpleKind);
-
-        Node diseq = left.eqNode(right).notNode();
-        if (d_diseq.find(diseq) != d_diseq.end()) {
-          Node ub = d_partialModel.getUpperConstraint(x_i);
-          return disequalityConflict(diseq, assertion, ub);
-        }
-        if(isInteger(x_i)){
-          d_constantIntegerVariables.push_back(x_i);
-        }
-      }
-    }
-    return d_simplex.AssertLower(x_i, c_i, assertion);
+    return AssertLower(x_i, c_i, assertion);
   case EQUAL:
-    if(isInteger(x_i)){
-      d_constantIntegerVariables.push_back(x_i);
-    }
-    return d_simplex.AssertEquality(x_i, c_i, assertion);
+    return AssertEquality(x_i, c_i, assertion);
   case DISTINCT:
     {
       d_diseq.insert(assertion);
@@ -760,7 +922,7 @@ void TheoryArith::check(Effort effortLevel){
     if(!possibleConflict.isNull()){
       d_partialModel.revertAssignmentChanges();
       Debug("arith::conflict") << "conflict   " << possibleConflict << endl;
-      d_simplex.clearUpdates();
+      clearUpdates();
       d_out->conflict(possibleConflict);
       return;
     }
@@ -771,10 +933,10 @@ void TheoryArith::check(Effort effortLevel){
   }
 
   bool emmittedConflictOrSplit = false;
-  Node possibleConflict = d_simplex.updateInconsistentVars();
+  Node possibleConflict = d_simplex.findModel();
   if(possibleConflict != Node::null()){
     d_partialModel.revertAssignmentChanges();
-    d_simplex.clearUpdates();
+    clearUpdates();
     Debug("arith::conflict") << "conflict   " << possibleConflict << endl;
 
     d_out->conflict(possibleConflict);
@@ -818,7 +980,7 @@ void TheoryArith::check(Effort effortLevel){
     }
   }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
 
-  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
+  if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
   if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
   Debug("arith") << "TheoryArith::check end" << std::endl;
 }
@@ -958,10 +1120,10 @@ Node flattenAnd(Node n){
 void TheoryArith::propagate(Effort e) {
   if(quickCheckOrMore(e)){
     bool propagated = false;
-    if(Options::current()->arithPropagation && d_simplex.hasAnyUpdates()){
-      d_simplex.propagateCandidates();
+    if(Options::current()->arithPropagation && hasAnyUpdates()){
+      propagateCandidates();
     }else{
-      d_simplex.clearUpdates();
+      clearUpdates();
     }
 
     while(d_propManager.hasMorePropagations()){
@@ -1106,7 +1268,7 @@ void TheoryArith::notifyEq(TNode lhs, TNode rhs) {
 void TheoryArith::notifyRestart(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
 
-  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
+  if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
   ++d_restartsCounter;
 
@@ -1225,7 +1387,7 @@ void TheoryArith::presolve(){
 
   d_statistics.d_initialTableauSize.setData(d_tableau.size());
 
-  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
+  if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
   static CVC4_THREADLOCAL(unsigned) callCount = 0;
   if(Debug.isOn("arith::presolve")) {
@@ -1245,3 +1407,87 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
   }
 
 }
+
+bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){
+  ++d_statistics.d_boundComputations;
+
+  DeltaRational bound = upperBound ?
+    d_linEq.computeUpperBound(basic):
+    d_linEq.computeLowerBound(basic);
+
+  if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) ||
+     (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){
+    Node bestImplied = upperBound ?
+      d_propManager.getBestImpliedUpperBound(basic, bound):
+      d_propManager.getBestImpliedLowerBound(basic, bound);
+
+    if(!bestImplied.isNull()){
+      bool asserted = d_propManager.isAsserted(bestImplied);
+      bool propagated = d_propManager.isPropagated(bestImplied);
+      if( !asserted && !propagated){
+
+        NodeBuilder<> nb(kind::AND);
+        if(upperBound){
+          d_linEq.explainNonbasicsUpperBound(basic, nb);
+        }else{
+          d_linEq.explainNonbasicsLowerBound(basic, nb);
+        }
+        Node explanation = nb;
+        d_propManager.propagate(bestImplied, explanation, false);
+        return true;
+      }else{
+        Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl;
+      }
+    }
+  }
+  return false;
+}
+
+void TheoryArith::propagateCandidate(ArithVar basic){
+  bool success = false;
+  if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasLowerBounds(basic)){
+    success |= propagateCandidateLowerBound(basic);
+  }
+  if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasUpperBounds(basic)){
+    success |= propagateCandidateUpperBound(basic);
+  }
+  if(success){
+    ++d_statistics.d_boundPropagations;
+  }
+}
+
+void TheoryArith::propagateCandidates(){
+  TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
+
+  Assert(d_candidateBasics.empty());
+
+  if(d_updatedBounds.empty()){ return; }
+
+  PermissiveBackArithVarSet::const_iterator i = d_updatedBounds.begin();
+  PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end();
+  for(; i != end; ++i){
+    ArithVar var = *i;
+    if(d_tableau.isBasic(var) &&
+       d_tableau.getRowLength(var) <= Options::current()->arithPropagateMaxLength){
+      d_candidateBasics.softAdd(var);
+    }else{
+      Tableau::ColIterator basicIter = d_tableau.colIterator(var);
+      for(; !basicIter.atEnd(); ++basicIter){
+        const TableauEntry& entry = *basicIter;
+        ArithVar rowVar = entry.getRowVar();
+        Assert(entry.getColVar() == var);
+        Assert(d_tableau.isBasic(rowVar));
+        if(d_tableau.getRowLength(rowVar) <= Options::current()->arithPropagateMaxLength){
+          d_candidateBasics.softAdd(rowVar);
+        }
+      }
+    }
+  }
+  d_updatedBounds.purge();
+
+  while(!d_candidateBasics.empty()){
+    ArithVar candidate = d_candidateBasics.pop_back();
+    Assert(d_tableau.isBasic(candidate));
+    propagateCandidate(candidate);
+  }
+}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index c19a20ead..f364885c2 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -32,6 +32,7 @@
 #include "theory/arith/tableau.h"
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/partial_model.h"
+#include "theory/arith/linear_equality.h"
 #include "theory/arith/atom_database.h"
 #include "theory/arith/simplex.h"
 #include "theory/arith/arith_static_learner.h"
@@ -180,20 +181,25 @@ private:
   std::map<ArithVar, Node> d_removedRows;
 
   /**
+   * List of all of the inequalities asserted in the current context.
+   */
+  context::CDSet<Node, NodeHashFunction> d_diseq;
+
+  /**
    * Manages information about the assignment and upper and lower bounds on
    * variables.
    */
   ArithPartialModel d_partialModel;
 
   /**
-   * List of all of the inequalities asserted in the current context.
+   * The tableau for all of the constraints seen thus far in the system.
    */
-  context::CDSet<Node, NodeHashFunction> d_diseq;
+  Tableau d_tableau;
 
   /**
-   * The tableau for all of the constraints seen thus far in the system.
+   * Maintains the relationship between the PartialModel and the Tableau.
    */
-  Tableau d_tableau;
+  LinearEqualityModule d_linEq;
 
   /**
    * A Diophantine equation solver.  Accesses the tableau and partial
@@ -279,6 +285,23 @@ public:
   void addSharedTerm(TNode n);
 
 private:
+
+  class BasicVarModelUpdateCallBack : public ArithVarCallBack{
+  private:
+    SimplexDecisionProcedure& d_simplex;
+
+  public:
+    BasicVarModelUpdateCallBack(SimplexDecisionProcedure& s):
+      d_simplex(s)
+    {}
+
+    void callback(ArithVar x){
+      d_simplex.updateBasic(x);
+    }
+  };
+
+  BasicVarModelUpdateCallBack d_basicVarModelUpdateCallBack;
+
   /** The constant zero. */
   DeltaRational d_DELTA_ZERO;
 
@@ -331,6 +354,45 @@ private:
 
 
   /**
+   * 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.
+   *
+   * orig must be a literal in the SAT solver so that it can be used for
+   * conflict analysis.
+   *
+   * x is the variable getting the new bound,
+   * c is the value of the new bound.
+   *
+   * If this new bound is in conflict with the other bound,
+   * a node describing this conflict is returned.
+   * If this new bound is not in conflict, Node::null() is returned.
+   */
+  Node AssertLower(ArithVar x, DeltaRational& c, TNode orig);
+  Node AssertUpper(ArithVar x, DeltaRational& c, TNode orig);
+  Node AssertEquality(ArithVar x, DeltaRational& c, TNode orig);
+
+  /** Tracks the bounds that were updated in the current round. */
+  PermissiveBackArithVarSet d_updatedBounds;
+
+  /** Tracks the basic variables where propagatation might be possible. */
+  PermissiveBackArithVarSet d_candidateBasics;
+
+  bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
+  void clearUpdates(){ d_updatedBounds.purge(); }
+
+  void propagateCandidates();
+  void propagateCandidate(ArithVar basic);
+  bool propagateCandidateBound(ArithVar basic, bool upperBound);
+
+  inline bool propagateCandidateLowerBound(ArithVar basic){
+    return propagateCandidateBound(basic, false);
+  }
+  inline bool propagateCandidateUpperBound(ArithVar basic){
+    return propagateCandidateBound(basic, true);
+  }
+
+  /**
    * Performs a check to see if it is definitely true that setup can be avoided.
    */
   bool canSafelyAvoidEqualitySetup(TNode equality);
@@ -383,6 +445,8 @@ private:
   /** These fields are designed to be accessable to TheoryArith methods. */
   class Statistics {
   public:
+    IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts;
+
     IntStat d_statUserVariables, d_statSlackVariables;
     IntStat d_statDisequalitySplits;
     IntStat d_statDisequalityConflicts;
@@ -399,6 +463,9 @@ private:
     IntStat d_smallerSetToCurr;
     TimerStat d_restartTimer;
 
+    TimerStat d_boundComputationTime;
+    IntStat d_boundComputations, d_boundPropagations;
+
     Statistics();
     ~Statistics();
   };