More misc. arithmetic cleanup. Removing unused files and functions. Also removing an ugly forward declaration that was needed to get error set bound information on basic variables.

16 files changed, 33 insertions, 2853 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index e6ef6fdc2..ed14e972b 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -11,7 +11,6 @@ libarith_la_SOURCES = \
 	arithvar.h \
 	arithvar.cpp \
 	bound_counts.h \
-	bound_counts.cpp \
 	arith_rewriter.h \
 	arith_rewriter.cpp \
 	arith_static_learner.h \
@@ -52,8 +51,6 @@ libarith_la_SOURCES = \
 	soi_simplex.cpp \
 	approx_simplex.h \
 	approx_simplex.cpp \
-	pure_update_simplex.h \
-	pure_update_simplex.cpp \
 	theory_arith.h \
 	theory_arith.cpp \
 	theory_arith_private_forward.h \
diff --git a/src/theory/arith/bound_counts.cpp b/src/theory/arith/bound_counts.cpp
deleted file mode 100644
index 27e9a35dc..000000000
--- a/src/theory/arith/bound_counts.cpp
+++ /dev/null
@@ -1,16 +0,0 @@
-#include "theory/arith/bound_counts.h"
-#include "theory/arith/tableau.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const {
-  RowIndex ridx = d_tab->basicToRowIndex(basic);
-  Assert(d_bc->isKey(ridx));
-  return (*d_bc)[ridx];
-}
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index d82fff3eb..1ee6ada06 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -198,23 +198,6 @@ public:
 /** This is intended to map each row to its relevant bound information. */
 typedef DenseMap<BoundsInfo> BoundInfoMap;
 
-class Tableau;
-
-class BoundCountingLookup {
-private:
-  BoundInfoMap* d_bc;
-  Tableau* d_tab;
-public:
-  BoundCountingLookup(BoundInfoMap* bc, Tableau* tab) : d_bc(bc), d_tab(tab) {}
-  const BoundsInfo& boundsInfo(ArithVar basic) const;
-  BoundCounts atBounds(ArithVar basic) const{
-    return boundsInfo(basic).atBounds();
-  }
-  BoundCounts hasBounds(ArithVar basic) const {
-    return boundsInfo(basic).hasBounds();
-  }
-};
-
 inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc){
   os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]";
   return os;
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 6b6170b20..1e827d316 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -32,6 +32,10 @@ void RaiseConflict::operator()(Node n){
   d_ta.raiseConflict(n);
 }
 
+const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const{
+  return d_ta.boundsInfo(basic);
+}
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 0d754d159..718799e9f 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -3,10 +3,10 @@
 
 #include "expr/node.h"
 #include "util/rational.h"
-#include "context/cdlist.h"
 
 #include "theory/arith/theory_arith_private_forward.h"
 #include "theory/arith/arithvar.h"
+#include "theory/arith/bound_counts.h"
 
 namespace CVC4 {
 namespace theory {
@@ -87,6 +87,20 @@ public:
   void operator()(Node n);
 };
 
+class BoundCountingLookup {
+private:
+  TheoryArithPrivate& d_ta;
+public:
+  BoundCountingLookup(TheoryArithPrivate& ta) : d_ta(ta) {}
+  const BoundsInfo& boundsInfo(ArithVar basic) const;
+  BoundCounts atBounds(ArithVar basic) const{
+    return boundsInfo(basic).atBounds();
+  }
+  BoundCounts hasBounds(ArithVar basic) const {
+    return boundsInfo(basic).hasBounds();
+  }
+};
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 27ac6ccd2..c5174a86a 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -26,9 +26,9 @@
 #include "theory/arith/partial_model.h"
 #include "theory/arith/arith_heuristic_pivot_rule.h"
 #include "theory/arith/tableau_sizes.h"
+#include "theory/arith/callbacks.h"
 
 #include "util/statistics_registry.h"
-//#include <boost/heap/d_ary_heap.hpp>
 
 #if CVC4_GCC_HAS_PB_DS_BUG
    // Unfortunate bug in some older GCCs (e.g., v4.2):
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index d264be978..e99e62505 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -358,18 +358,9 @@ UpdateInfo FCSimplexDecisionProcedure::selectPrimalUpdate(ArithVar basic, Linear
     ArithVar curr = cand.d_nb;
     const Rational& coeff = *cand.d_coeff;
 
-#warning "Who is using computeSafeUpdate?"
     LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc = selectLeavingFunction(curr);
     UpdateInfo currProposal = d_linEq.speculativeUpdate(curr, coeff, leavingPrefFunc);
 
-    //int curr_movement = cand.d_sgn;
-    // if(isFocus){
-    //   currProposal = d_linEq.speculativeUpdate(curr, coeff, upf);
-    // }else{
-    //   currProposal = UpdateInfo(curr, curr_movement);
-    //   d_linEq.computeSafeUpdate(currProposal, bpf);
-    // }
-
     Debug("arith::selectPrimalUpdate")
       << "selected " << selected << endl
       << "currProp " << currProposal << endl
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index b1dfa8705..1c32f80e4 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -55,7 +55,6 @@ LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, Bou
   d_basicVariableUpdates(f),
   d_increasing(1),
   d_decreasing(-1),
-  d_relevantErrorBuffer(),
   d_btracking(boundsTracking),
   d_areTracking(false),
   d_trackCallback(this)
@@ -851,213 +850,6 @@ void LinearEqualityModule::trackingCoefficientChange(RowIndex ridx, ArithVar nb,
   row_bi.addInSgn(nb_inf, oldSgn, currSgn);
 }
 
-void LinearEqualityModule::computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction pref){
-  ArithVar nb = inf.nonbasic();
-  int sgn = inf.nonbasicDirection();
-  Assert(sgn != 0);
-  Assert(!d_tableau.isBasic(nb));
-
-
-  // Error variables moving in the correct direction
-  Assert(d_relevantErrorBuffer.empty());
-
-  // phases :
-  enum ComputeSafePhase {
-    NoBoundSelected,
-    NbsBoundSelected,
-    BasicBoundSelected,
-    DegenerateBoundSelected
-  } phase;
-
-  phase = NoBoundSelected;
-
-  static int instance = 0;
-  Debug("computeSafeUpdate") << "computeSafeUpdate " <<  (++instance) << endl;
-
-  if(sgn > 0 && d_variables.hasUpperBound(nb)){
-    Constraint ub = d_variables.getUpperBoundConstraint(nb);
-    inf.updatePureFocus(ub->getValue() - d_variables.getAssignment(nb), ub);
-
-    Assert(inf.nonbasicDelta().sgn() == sgn);
-    Debug("computeSafeUpdate") << "computeSafeUpdate " <<  inf.limiting() << endl;
-    phase = NbsBoundSelected;
-  }else if(sgn < 0 && d_variables.hasLowerBound(nb)){
-    Constraint lb = d_variables.getLowerBoundConstraint(nb);
-    inf.updatePureFocus(lb->getValue() - d_variables.getAssignment(nb), lb);
-
-    Assert(inf.nonbasicDelta().sgn() == sgn);
-
-    Debug("computeSafeUpdate") << "computeSafeUpdate " <<  inf.limiting() << endl;
-    phase = NbsBoundSelected;
-  }
-
-  Tableau::ColIterator basicIter = d_tableau.colIterator(nb);
-  for(; !basicIter.atEnd(); ++basicIter){
-    const Tableau::Entry& entry = *basicIter;
-    Assert(entry.getColVar() == nb);
-
-    ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex());
-    const Rational& a_ji = entry.getCoefficient();
-    int basic_movement = sgn * a_ji.sgn();
-
-    Debug("computeSafeUpdate")
-      << "computeSafeUpdate: "
-      << basic << ", "
-      << basic_movement << ", "
-      << d_variables.cmpAssignmentUpperBound(basic) << ", "
-      << d_variables.cmpAssignmentLowerBound(basic) << ", "
-      << a_ji << ", "
-      << d_variables.getAssignment(basic) << endl;
-
-    Constraint proposal = NullConstraint;
-
-    if(basic_movement > 0){
-      if(d_variables.cmpAssignmentLowerBound(basic) < 0){
-        d_relevantErrorBuffer.push_back(&entry);
-      }
-      if(d_variables.hasUpperBound(basic) &&
-         d_variables.cmpAssignmentUpperBound(basic) <= 0){
-        proposal = d_variables.getUpperBoundConstraint(basic);
-      }
-    }else if(basic_movement < 0){
-      if(d_variables.cmpAssignmentUpperBound(basic) > 0){
-        d_relevantErrorBuffer.push_back(&entry);
-      }
-      if(d_variables.hasLowerBound(basic) &&
-         d_variables.cmpAssignmentLowerBound(basic) >= 0){
-        proposal = d_variables.getLowerBoundConstraint(basic);
-      }
-    }
-    if(proposal != NullConstraint){
-      const Rational& coeff = entry.getCoefficient();
-      DeltaRational diff = proposal->getValue() - d_variables.getAssignment(basic);
-      diff /= coeff;
-      int cmp = phase == NoBoundSelected ? 0 : diff.cmp(inf.nonbasicDelta());
-      Assert(diff.sgn() == sgn || diff.sgn() == 0);
-      bool prefer = false;
-      switch(phase){
-      case NoBoundSelected:
-        prefer = true;
-        break;
-      case NbsBoundSelected:
-        prefer = (sgn > 0 && cmp < 0 ) || (sgn < 0 && cmp > 0);
-        break;
-      case BasicBoundSelected:
-        prefer =
-          (sgn > 0 && cmp < 0 ) ||
-          (sgn < 0 && cmp > 0) ||
-          (cmp == 0 && basic == (this->*pref)(basic, inf.leaving()));
-        break;
-      case DegenerateBoundSelected:
-        prefer = cmp == 0 && basic == (this->*pref)(basic, inf.leaving());
-        break;
-      }
-      if(prefer){
-        inf.updatePivot(diff, coeff, proposal);
-
-        phase = (diff.sgn() != 0) ? BasicBoundSelected : DegenerateBoundSelected;
-      }
-    }
-  }
-
-  if(phase == DegenerateBoundSelected){
-    inf.setErrorsChange(0);
-  }else{
-    computedFixed(inf);
-  }
-  inf.determineFocusDirection();
-
-  d_relevantErrorBuffer.clear();
-}
-
-void LinearEqualityModule::computedFixed(UpdateInfo& proposal){
-  Assert(proposal.nonbasicDirection() != 0);
-  Assert(!d_tableau.isBasic(proposal.nonbasic()));
-
-  //bool unconstrained = (proposal.d_limiting == NullConstraint);
-
-  Assert(!proposal.unbounded() || !d_relevantErrorBuffer.empty());
-
-  Assert(proposal.unbounded() ||
-         proposal.nonbasicDelta().sgn() == proposal.nonbasicDirection());
-
-  // proposal.d_value is the max
-
-  UpdateInfo max;
-  int dropped = 0;
-  //Constraint maxFix = NullConstraint;
-  //DeltaRational maxAmount;
-
-  EntryPointerVector::const_iterator i = d_relevantErrorBuffer.begin();
-  EntryPointerVector::const_iterator i_end = d_relevantErrorBuffer.end();
-  for(; i != i_end; ++i){
-    const Tableau::Entry& entry = *(*i);
-    Assert(entry.getColVar() == proposal.nonbasic());
-
-    ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex());
-    const Rational& a_ji = entry.getCoefficient();
-    int basic_movement = proposal.nonbasicDirection() * a_ji.sgn();
-
-    DeltaRational theta;
-    DeltaRational proposedValue;
-    if(!proposal.unbounded()){
-      theta = proposal.nonbasicDelta() * a_ji;
-      proposedValue = theta + d_variables.getAssignment(basic);
-    }
-
-    Constraint fixed = NullConstraint;
-
-    if(basic_movement < 0){
-      Assert(d_variables.cmpAssignmentUpperBound(basic) > 0);
-
-      if(proposal.unbounded() || d_variables.cmpToUpperBound(basic, proposedValue) <= 0){
-        --dropped;
-        fixed = d_variables.getUpperBoundConstraint(basic);
-      }
-    }else if(basic_movement > 0){
-      Assert(d_variables.cmpAssignmentLowerBound(basic) < 0);
-
-      if(proposal.unbounded() || d_variables.cmpToLowerBound(basic, proposedValue) >= 0){
-        --dropped;
-        fixed = d_variables.getLowerBoundConstraint(basic);
-      }
-    }
-    if(fixed != NullConstraint){
-      DeltaRational amount = fixed->getValue() - d_variables.getAssignment(basic);
-      amount /= a_ji;
-      Assert(amount.sgn() == proposal.nonbasicDirection());
-
-      if(max.uninitialized()){
-        max = UpdateInfo(proposal.nonbasic(), proposal.nonbasicDirection());
-        max.updatePivot(amount, a_ji, fixed, dropped);
-      }else{
-        int cmp = amount.cmp(max.nonbasicDelta());
-        bool prefer =
-          (proposal.nonbasicDirection() < 0 && cmp < 0) ||
-          (proposal.nonbasicDirection() > 0 && cmp > 0) ||
-          (cmp == 0 && fixed->getVariable() < max.limiting()->getVariable());
-
-        if(prefer){
-          max.updatePivot(amount, a_ji, fixed, dropped);
-        }else{
-          max.setErrorsChange(dropped);
-        }
-      }
-    }
-  }
-  Assert(dropped < 0 || !proposal.unbounded());
-
-  if(dropped < 0){
-    proposal = max;
-  }else{
-    Assert(dropped == 0);
-    Assert(proposal.nonbasicDelta().sgn() != 0);
-    Assert(proposal.nonbasicDirection() != 0);
-    proposal.setErrorsChange(0);
-  }
-  Assert(proposal.errorsChange() == dropped);
-}
-
 ArithVar LinearEqualityModule::minBy(const ArithVarVec& vec, VarPreferenceFunction pf) const{
   if(vec.empty()) {
     return ARITHVAR_SENTINEL;
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 4d18d5c81..607ee6244 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -277,8 +277,6 @@ public:
 
   void includeBoundUpdate(ArithVar nb, const BoundsInfo& prev);
 
-  void computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction basic);
-
 
   uint32_t updateProduct(const UpdateInfo& inf) const;
 
@@ -400,16 +398,12 @@ public:
   }
 
 private:
-  typedef std::vector<const Tableau::Entry*> EntryPointerVector;
-  EntryPointerVector d_relevantErrorBuffer;
-
-  //uint32_t computeUnconstrainedUpdate(ArithVar nb, int sgn,  DeltaRational& am);
-  //uint32_t computedFixed(ArithVar nb, int sgn, const DeltaRational& am);
-  void computedFixed(UpdateInfo&);
 
   /**
    * This maps each row index to its relevant bounds info.
-   * This tracks the */
+   * This tracks the count for how many variables on a row have bounds
+   * and how many are assigned at their bounds.
+   */
   BoundInfoMap& d_btracking;
   bool d_areTracking;
 
diff --git a/src/theory/arith/pure_update_simplex.cpp b/src/theory/arith/pure_update_simplex.cpp
deleted file mode 100644
index 233fc292f..000000000
--- a/src/theory/arith/pure_update_simplex.cpp
+++ /dev/null
@@ -1,261 +0,0 @@
-/*********************                                                        */
-/*! \file simplex.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-#include "theory/arith/pure_update_simplex.h"
-#include "theory/arith/options.h"
-#include "theory/arith/constraint.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-PureUpdateSimplexDecisionProcedure::PureUpdateSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
-  : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
-{ }
-
-Result::Sat PureUpdateSimplexDecisionProcedure::findModel(bool exactResult){
-  Assert(d_conflictVariables.empty());
-
-  static CVC4_THREADLOCAL(unsigned int) instance = 0;
-  instance = instance + 1;
-
-  if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
-    Debug("arith::findModel") << "puFindModel("<< instance <<") "
-                              << "trivial" << endl;
-    return Result::SAT;
-  }
-
-  // We need to reduce this because of
-  d_errorSet.reduceToSignals();
-  d_errorSet.setSelectionRule(VAR_ORDER);
-
-  if(processSignals()){
-    d_conflictVariables.purge();
-
-    Debug("arith::findModel") << "puFindModel("<< instance <<") "
-                              << "early conflict" << endl;
-    return Result::UNSAT;
-  }else if(d_errorSet.errorEmpty()){
-    Debug("arith::findModel") << "puFindModel("<< instance <<") "
-                              << "fixed itself" << endl;
-    Assert(!d_errorSet.moreSignals());
-    return Result::SAT;
-  }
-
-  Debug("arith::findModel") << "puFindModel(" << instance <<") "
-                            << "start non-trivial" << endl;
-
-  static const bool verbose = false;
-  Result::Sat result = Result::SAT_UNKNOWN;
-
-  if(result == Result::SAT_UNKNOWN){
-    if(attemptPureUpdates()){
-      result = Result::UNSAT;
-    }
-    if(result ==  Result::UNSAT){
-      ++(d_statistics.d_pureUpdateFoundUnsat);
-      if(verbose){ Message() << "pure updates found unsat" << endl; }
-    }else if(d_errorSet.errorEmpty()){
-      ++(d_statistics.d_pureUpdateFoundSat);
-      if(verbose){ Message() << "pure updates found model" << endl; }
-    }else{
-      ++(d_statistics.d_pureUpdateMissed);
-      if(verbose){ Message() << "pure updates missed" << endl; }
-    }
-  }
-
-  Assert(!d_errorSet.moreSignals());
-  if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
-    result = Result::SAT;
-  }
-
-  // ensure that the conflict variable is still in the queue.
-  d_conflictVariables.purge();
-
-  Assert(d_focusErrorVar == ARITHVAR_SENTINEL);
-  Debug("arith::findModel") << "end findModel() " << instance << " "
-                            << result <<  endl;
-
-  return result;
-}
-
-
-
-PureUpdateSimplexDecisionProcedure::Statistics::Statistics():
-  d_pureUpdateFoundUnsat("theory::arith::PureUpdate::FoundUnsat", 0),
-  d_pureUpdateFoundSat("theory::arith::PureUpdate::FoundSat", 0),
-  d_pureUpdateMissed("theory::arith::PureUpdate::Missed", 0),
-  d_pureUpdates("theory::arith::PureUpdate::updates", 0),
-  d_pureUpdateDropped("theory::arith::PureUpdate::dropped", 0),
-  d_pureUpdateConflicts("theory::arith::PureUpdate::conflicts", 0),
-  d_foundConflicts("theory::arith::PureUpdate::foundConflicts", 0),
-  d_attemptPureUpdatesTimer("theory::arith::PureUpdate::timer"),
-  d_processSignalsTime("theory::arith::PureUpdate::process::timer"),
-  d_constructionTimer("theory::arith::PureUpdate::construction::timer")
-{
-  StatisticsRegistry::registerStat(&d_pureUpdateFoundUnsat);
-  StatisticsRegistry::registerStat(&d_pureUpdateFoundSat);
-  StatisticsRegistry::registerStat(&d_pureUpdateMissed);
-  StatisticsRegistry::registerStat(&d_pureUpdates);
-  StatisticsRegistry::registerStat(&d_pureUpdateDropped);
-  StatisticsRegistry::registerStat(&d_pureUpdateConflicts);
-
-  StatisticsRegistry::registerStat(&d_foundConflicts);
-
-  StatisticsRegistry::registerStat(&d_attemptPureUpdatesTimer);
-  StatisticsRegistry::registerStat(&d_processSignalsTime);
-  StatisticsRegistry::registerStat(&d_constructionTimer);
-}
-
-PureUpdateSimplexDecisionProcedure::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_pureUpdateFoundUnsat);
-  StatisticsRegistry::unregisterStat(&d_pureUpdateFoundSat);
-  StatisticsRegistry::unregisterStat(&d_pureUpdateMissed);
-  StatisticsRegistry::unregisterStat(&d_pureUpdates);
-  StatisticsRegistry::unregisterStat(&d_pureUpdateDropped);
-  StatisticsRegistry::unregisterStat(&d_pureUpdateConflicts);
-
-  StatisticsRegistry::unregisterStat(&d_foundConflicts);
-
-  StatisticsRegistry::unregisterStat(&d_attemptPureUpdatesTimer);
-  StatisticsRegistry::unregisterStat(&d_processSignalsTime);
-  StatisticsRegistry::unregisterStat(&d_constructionTimer);
-}
-
-bool PureUpdateSimplexDecisionProcedure::attemptPureUpdates(){
-  TimerStat::CodeTimer codeTimer(d_statistics.d_attemptPureUpdatesTimer);
-
-  Assert(!d_errorSet.focusEmpty());
-  Assert(d_errorSet.noSignals());
-
-  d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_constructionTimer);
-
-  UpdateInfo proposal;
-  int boundImprovements = 0;
-  int dropped = 0;
-  int computations = 0;
-
-  for( Tableau::RowIterator ri = d_tableau.basicRowIterator(d_focusErrorVar); !ri.atEnd(); ++ri){
-    const Tableau::Entry& e = *ri;
-
-    ArithVar curr = e.getColVar();
-    if(curr == d_focusErrorVar){ continue; }
-
-    int dir = e.getCoefficient().sgn();
-    Assert(dir != 0);
-
-    bool worthwhile  = false;
-
-    if( (dir > 0 && d_variables.cmpAssignmentUpperBound(curr) < 0) ||
-        (dir < 0 && d_variables.cmpAssignmentLowerBound(curr) > 0) ){
-
-      ++computations;
-      proposal = UpdateInfo(curr, dir);
-      d_linEq.computeSafeUpdate(proposal, &LinearEqualityModule::noPreference);
-
-      Assert(proposal.errorsChange() <= 0);
-      Assert(proposal.focusDirection() >= 0);
-
-      worthwhile = proposal.errorsChange() < 0 ||
-        (proposal.focusDirection() > 0 &&
-         d_variables.atBoundCounts(curr).isZero() &&
-         !proposal.describesPivot());
-
-      Debug("pu::refined")
-        << "pure update proposal "
-        << curr << " "
-        << worthwhile << " "
-        << proposal
-        << endl;
-    }
-    if(worthwhile){
-      Debug("pu") << d_variables.getAssignment(d_focusErrorVar) << endl;
-
-      BoundCounts before = d_variables.atBoundCounts(curr);
-      DeltaRational newAssignment =
-        d_variables.getAssignment(curr) + proposal.nonbasicDelta();
-      d_linEq.updateTracked(curr, newAssignment);
-      BoundCounts after = d_variables.atBoundCounts(curr);
-
-      ++d_statistics.d_pureUpdates;
-      ++boundImprovements;
-      Debug("pu") << boundImprovements  << ": " << curr
-                  << " before: " << before
-                  << " after: " << after
-                  << e.getCoefficient()
-                  << d_variables.getAssignment(d_focusErrorVar) << endl;
-
-      uint32_t prevSize = d_errorSet.errorSize();
-      Assert(d_errorSet.moreSignals());
-      if(Debug.isOn("pu")){  d_errorSet.debugPrint(Debug("pu")); }
-      while(d_errorSet.moreSignals()){
-        ArithVar updated = d_errorSet.topSignal();
-        bool wasInError = d_errorSet.inError(updated);
-        d_errorSet.popSignal();
-        if(updated == curr){ continue; }
-        Assert(d_tableau.isBasic(updated));
-        if(!d_linEq.basicIsTracked(updated)){continue;}
-
-
-        Assert(d_linEq.basicIsTracked(updated));
-        Assert(wasInError || d_variables.assignmentIsConsistent(updated));
-
-        if(!d_variables.assignmentIsConsistent(updated)
-           && checkBasicForConflict(updated)){
-          Assert(!d_conflictVariables.isMember(updated) );
-          Debug("pu")
-            << "It worked? "
-            << d_statistics.d_pureUpdateConflicts.getData()
-            << " " << curr
-            << " "  << checkBasicForConflict(updated) << endl;
-          reportConflict(updated);
-          ++(d_statistics.d_foundConflicts);
-          ++(d_statistics.d_pureUpdateConflicts);
-        }
-      }
-      if(d_conflictVariables.empty()){
-        if(Debug.isOn("pu")){  d_errorSet.debugPrint(Debug("pu")); }
-        uint32_t currSize = d_errorSet.errorSize();
-        Assert(currSize <= prevSize);
-        if(currSize < prevSize){
-          dropped+= prevSize - currSize;
-          if(currSize == 0){
-            break;
-          }
-        }
-      }else{
-        break;
-      }
-    }
-  }
-
-  tearDownInfeasiblityFunction(d_statistics.d_constructionTimer, d_focusErrorVar);
-  d_focusErrorVar = ARITHVAR_SENTINEL;
-
-  (d_statistics.d_pureUpdateDropped) += dropped;
-
-  Assert(d_errorSet.noSignals());
-  return !d_conflictVariables.empty();
-}
-
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/arith/pure_update_simplex.h b/src/theory/arith/pure_update_simplex.h
deleted file mode 100644
index 50b751d7b..000000000
--- a/src/theory/arith/pure_update_simplex.h
+++ /dev/null
@@ -1,118 +0,0 @@
-/*********************                                                        */
-/*! \file simplex.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): kshitij, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief This is an implementation of the Simplex Module for the Simplex for DPLL(T)
- ** decision procedure.
- **
- ** 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 heuristic 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 heuristics, 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
- **/
-
-
-#include "cvc4_private.h"
-
-#pragma once
-
-#include "theory/arith/simplex.h"
-#include "util/dense_map.h"
-#include "util/statistics_registry.h"
-#include <stdint.h>
-#include "theory/arith/arithvar.h"
-#include "theory/arith/delta_rational.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class PureUpdateSimplexDecisionProcedure : public SimplexDecisionProcedure{
-public:
-  PureUpdateSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
-
-  Result::Sat findModel(bool exactResult);
-
-private:
-  ArithVar d_focusErrorVar;
-
-  bool attemptPureUpdates();
-
-  /**
-   * This is the main simplex for DPLL(T) loop.
-   * It runs for at most maxIterations.
-   *
-   * Returns true iff it has found a conflict.
-   * d_conflictVariable will be set and the conflict for this row is reported.
-   */
-  bool searchForFeasibleSolution(uint32_t maxIterations);
-
-  bool processSignals(){
-    TimerStat &timer = d_statistics.d_processSignalsTime;
-    IntStat& conflictStat  = d_statistics.d_foundConflicts;
-    return standardProcessSignals(timer, conflictStat);
-  }
-
-  /** These fields are designed to be accessible to TheoryArith methods. */
-  class Statistics {
-  public:
-    IntStat d_pureUpdateFoundUnsat;
-    IntStat d_pureUpdateFoundSat;
-    IntStat d_pureUpdateMissed;
-    IntStat d_pureUpdates;
-    IntStat d_pureUpdateDropped;
-    IntStat d_pureUpdateConflicts;
-
-    IntStat d_foundConflicts;
-
-    TimerStat d_attemptPureUpdatesTimer;
-    TimerStat d_processSignalsTime;
-    
-    TimerStat d_constructionTimer;
-
-    Statistics();
-    ~Statistics();
-  } d_statistics;
-};/* class PureUpdateSimplexDecisionProcedure */
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
diff --git a/src/theory/arith/simplex-converge.cpp b/src/theory/arith/simplex-converge.cpp
deleted file mode 100644
index decce3882..000000000
--- a/src/theory/arith/simplex-converge.cpp
+++ /dev/null
@@ -1,1674 +0,0 @@
-/*********************                                                        */
-/*! \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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-#include "theory/arith/simplex.h"
-#include "theory/arith/options.h"
-
-using namespace std;
-
-using namespace CVC4;
-using namespace CVC4::kind;
-
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
-
-static const bool CHECK_AFTER_PIVOT = true;
-
-SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel, ArithVarMalloc& malloc, ConstraintDatabase& cd) :
-  d_conflictVariable(ARITHVAR_SENTINEL),
-  d_linEq(linEq),
-  d_partialModel(d_linEq.getPartialModel()),
-  d_tableau(d_linEq.getTableau()),
-  d_queue(d_partialModel, d_tableau),
-  d_numVariables(0),
-  d_conflictChannel(conflictChannel),
-  d_pivotsInRound(),
-  d_DELTA_ZERO(0,0),
-  d_arithVarMalloc(malloc),
-  d_constraintDatabase(cd),
-  d_optRow(ARITHVAR_SENTINEL),
-  d_negOptConstant(d_DELTA_ZERO)
-{
-  switch(ArithHeuristicPivotRule rule = options::arithHeuristicPivotRule()) {
-  case MINIMUM:
-    d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
-    break;
-  case BREAK_TIES:
-    d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES);
-    break;
-  case MAXIMUM:
-    d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM);
-    break;
-  default:
-    Unhandled(rule);
-  }
-
-  srand(62047);
-}
-
-SimplexDecisionProcedure::Statistics::Statistics():
-  d_statUpdateConflicts("theory::arith::UpdateConflicts", 0),
-  d_findConflictOnTheQueueTime("theory::arith::findConflictOnTheQueueTime"),
-  d_attemptBeforeDiffSearch("theory::arith::qi::BeforeDiffSearch::attempt",0),
-  d_successBeforeDiffSearch("theory::arith::qi::BeforeDiffSearch::success",0),
-  d_attemptAfterDiffSearch("theory::arith::qi::AfterDiffSearch::attempt",0),
-  d_successAfterDiffSearch("theory::arith::qi::AfterDiffSearch::success",0),
-  d_attemptDuringDiffSearch("theory::arith::qi::DuringDiffSearch::attempt",0),
-  d_successDuringDiffSearch("theory::arith::qi::DuringDiffSearch::success",0),
-  d_attemptDuringVarOrderSearch("theory::arith::qi::DuringVarOrderSearch::attempt",0),
-  d_successDuringVarOrderSearch("theory::arith::qi::DuringVarOrderSearch::success",0),
-  d_attemptAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::attempt",0),
-  d_successAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::success",0),
-  d_weakeningAttempts("theory::arith::weakening::attempts",0),
-  d_weakeningSuccesses("theory::arith::weakening::success",0),
-  d_weakenings("theory::arith::weakening::total",0),
-  d_weakenTime("theory::arith::weakening::time"),
-  d_simplexConflicts("theory::arith::simplexConflicts",0),
-  // primal
-  d_primalTimer("theory::arith::primal::overall::timer"),
-  d_internalTimer("theory::arith::primal::internal::timer"),
-  d_primalCalls("theory::arith::primal::calls",0),
-  d_primalSatCalls("theory::arith::primal::calls::sat",0),
-  d_primalUnsatCalls("theory::arith::primal::calls::unsat",0),
-  d_primalPivots("theory::arith::primal::pivots",0),
-  d_primalImprovingPivots("theory::arith::primal::pivots::improving",0),
-  d_primalThresholdReachedPivot("theory::arith::primal::thresholds",0),
-  d_primalThresholdReachedPivot_dropped("theory::arith::primal::thresholds::dropped",0),
-  d_primalReachedMaxPivots("theory::arith::primal::maxpivots",0),
-  d_primalReachedMaxPivots_contractMadeProgress("theory::arith::primal::maxpivots::contract",0),
-  d_primalReachedMaxPivots_checkForConflictWorked("theory::arith::primal::maxpivots::checkworked",0),
-  d_primalGlobalMinimum("theory::arith::primal::minimum",0),
-  d_primalGlobalMinimum_rowConflictWorked("theory::arith::primal::minimum::checkworked",0),
-  d_primalGlobalMinimum_firstHalfWasSat("theory::arith::primal::minimum::firsthalf::sat",0),
-  d_primalGlobalMinimum_firstHalfWasUnsat("theory::arith::primal::minimum::firsthalf::unsat",0),
-  d_primalGlobalMinimum_contractMadeProgress("theory::arith::primal::minimum::progress",0),
-  d_unboundedFound("theory::arith::primal::unbounded",0),
-  d_unboundedFound_drive("theory::arith::primal::unbounded::drive",0),
-  d_unboundedFound_dropped("theory::arith::primal::unbounded::dropped",0)
-{
-  StatisticsRegistry::registerStat(&d_statUpdateConflicts);
-
-  StatisticsRegistry::registerStat(&d_findConflictOnTheQueueTime);
-
-  StatisticsRegistry::registerStat(&d_attemptBeforeDiffSearch);
-  StatisticsRegistry::registerStat(&d_successBeforeDiffSearch);
-  StatisticsRegistry::registerStat(&d_attemptAfterDiffSearch);
-  StatisticsRegistry::registerStat(&d_successAfterDiffSearch);
-  StatisticsRegistry::registerStat(&d_attemptDuringDiffSearch);
-  StatisticsRegistry::registerStat(&d_successDuringDiffSearch);
-  StatisticsRegistry::registerStat(&d_attemptDuringVarOrderSearch);
-  StatisticsRegistry::registerStat(&d_successDuringVarOrderSearch);
-  StatisticsRegistry::registerStat(&d_attemptAfterVarOrderSearch);
-  StatisticsRegistry::registerStat(&d_successAfterVarOrderSearch);
-
-  StatisticsRegistry::registerStat(&d_weakeningAttempts);
-  StatisticsRegistry::registerStat(&d_weakeningSuccesses);
-  StatisticsRegistry::registerStat(&d_weakenings);
-  StatisticsRegistry::registerStat(&d_weakenTime);
-
-  StatisticsRegistry::registerStat(&d_simplexConflicts);
-
-  //primal  
-  StatisticsRegistry::registerStat(&d_primalTimer);
-  StatisticsRegistry::registerStat(&d_internalTimer);
-
-  StatisticsRegistry::registerStat(&d_primalCalls);
-  StatisticsRegistry::registerStat(&d_primalSatCalls);
-  StatisticsRegistry::registerStat(&d_primalUnsatCalls);
-
-  StatisticsRegistry::registerStat(&d_primalPivots);
-  StatisticsRegistry::registerStat(&d_primalImprovingPivots);
-
-  StatisticsRegistry::registerStat(&d_primalThresholdReachedPivot);
-  StatisticsRegistry::registerStat(&d_primalThresholdReachedPivot_dropped);
-    
-  StatisticsRegistry::registerStat(&d_primalReachedMaxPivots);
-  StatisticsRegistry::registerStat(&d_primalReachedMaxPivots_contractMadeProgress);
-  StatisticsRegistry::registerStat(&d_primalReachedMaxPivots_checkForConflictWorked);
-
-    
-  StatisticsRegistry::registerStat(&d_primalGlobalMinimum);
-  StatisticsRegistry::registerStat(&d_primalGlobalMinimum_rowConflictWorked);
-  StatisticsRegistry::registerStat(&d_primalGlobalMinimum_firstHalfWasSat);
-  StatisticsRegistry::registerStat(&d_primalGlobalMinimum_firstHalfWasUnsat);
-  StatisticsRegistry::registerStat(&d_primalGlobalMinimum_contractMadeProgress);
-
-  
-  StatisticsRegistry::registerStat(&d_unboundedFound);
-  StatisticsRegistry::registerStat(&d_unboundedFound_drive);
-  StatisticsRegistry::registerStat(&d_unboundedFound_dropped);
-
-}
-
-SimplexDecisionProcedure::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_statUpdateConflicts);
-
-  StatisticsRegistry::unregisterStat(&d_findConflictOnTheQueueTime);
-
-  StatisticsRegistry::unregisterStat(&d_attemptBeforeDiffSearch);
-  StatisticsRegistry::unregisterStat(&d_successBeforeDiffSearch);
-  StatisticsRegistry::unregisterStat(&d_attemptAfterDiffSearch);
-  StatisticsRegistry::unregisterStat(&d_successAfterDiffSearch);
-  StatisticsRegistry::unregisterStat(&d_attemptDuringDiffSearch);
-  StatisticsRegistry::unregisterStat(&d_successDuringDiffSearch);
-  StatisticsRegistry::unregisterStat(&d_attemptDuringVarOrderSearch);
-  StatisticsRegistry::unregisterStat(&d_successDuringVarOrderSearch);
-  StatisticsRegistry::unregisterStat(&d_attemptAfterVarOrderSearch);
-  StatisticsRegistry::unregisterStat(&d_successAfterVarOrderSearch);
-
-  StatisticsRegistry::unregisterStat(&d_weakeningAttempts);
-  StatisticsRegistry::unregisterStat(&d_weakeningSuccesses);
-  StatisticsRegistry::unregisterStat(&d_weakenings);
-  StatisticsRegistry::unregisterStat(&d_weakenTime);
-
-  StatisticsRegistry::unregisterStat(&d_simplexConflicts);
-
-  //primal
-  StatisticsRegistry::unregisterStat(&d_primalTimer);
-  StatisticsRegistry::unregisterStat(&d_internalTimer);
-
-  StatisticsRegistry::unregisterStat(&d_primalCalls);
-  StatisticsRegistry::unregisterStat(&d_primalSatCalls);
-  StatisticsRegistry::unregisterStat(&d_primalUnsatCalls);
-
-  StatisticsRegistry::unregisterStat(&d_primalPivots);
-  StatisticsRegistry::unregisterStat(&d_primalImprovingPivots);
-
-  StatisticsRegistry::unregisterStat(&d_primalThresholdReachedPivot);
-  StatisticsRegistry::unregisterStat(&d_primalThresholdReachedPivot_dropped);
-    
-  StatisticsRegistry::unregisterStat(&d_primalReachedMaxPivots);
-  StatisticsRegistry::unregisterStat(&d_primalReachedMaxPivots_contractMadeProgress);
-  StatisticsRegistry::unregisterStat(&d_primalReachedMaxPivots_checkForConflictWorked);
-
-    
-  StatisticsRegistry::unregisterStat(&d_primalGlobalMinimum);
-  StatisticsRegistry::unregisterStat(&d_primalGlobalMinimum_rowConflictWorked);
-  StatisticsRegistry::unregisterStat(&d_primalGlobalMinimum_firstHalfWasSat);
-  StatisticsRegistry::unregisterStat(&d_primalGlobalMinimum_firstHalfWasUnsat);
-  StatisticsRegistry::unregisterStat(&d_primalGlobalMinimum_contractMadeProgress);
-
-  StatisticsRegistry::unregisterStat(&d_unboundedFound);
-  StatisticsRegistry::unregisterStat(&d_unboundedFound_drive);
-  StatisticsRegistry::unregisterStat(&d_unboundedFound_dropped);
-}
-
-
-
-
-ArithVar SimplexDecisionProcedure::minVarOrder(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){
-  Assert(x != ARITHVAR_SENTINEL);
-  Assert(y != ARITHVAR_SENTINEL);
-  // Assert(!simp.d_tableau.isBasic(x));
-  // Assert(!simp.d_tableau.isBasic(y));
-  if(x <= y){
-    return x;
-  } else {
-    return y;
-  }
-}
-
-ArithVar SimplexDecisionProcedure::minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){
-  Assert(x != ARITHVAR_SENTINEL);
-  Assert(y != ARITHVAR_SENTINEL);
-  Assert(!simp.d_tableau.isBasic(x));
-  Assert(!simp.d_tableau.isBasic(y));
-  uint32_t xLen = simp.d_tableau.getColLength(x);
-  uint32_t yLen = simp.d_tableau.getColLength(y);
-  if( xLen > yLen){
-     return y;
-  } else if( xLen== yLen ){
-    return minVarOrder(simp,x,y);
-  }else{
-    return x;
-  }
-}
-
-ArithVar SimplexDecisionProcedure::minRowLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){
-  Assert(x != ARITHVAR_SENTINEL);
-  Assert(y != ARITHVAR_SENTINEL);
-  Assert(simp.d_tableau.isBasic(x));
-  Assert(simp.d_tableau.isBasic(y));
-  uint32_t xLen = simp.d_tableau.getRowLength(simp.d_tableau.basicToRowIndex(x));
-  uint32_t yLen = simp.d_tableau.getRowLength(simp.d_tableau.basicToRowIndex(y));
-  if( xLen > yLen){
-     return y;
-  } else if( xLen == yLen ){
-    return minVarOrder(simp,x,y);
-  }else{
-    return x;
-  }
-}
-ArithVar SimplexDecisionProcedure::minBoundAndRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){
-  Assert(x != ARITHVAR_SENTINEL);
-  Assert(y != ARITHVAR_SENTINEL);
-  Assert(!simp.d_tableau.isBasic(x));
-  Assert(!simp.d_tableau.isBasic(y));
-  if(simp.d_partialModel.hasEitherBound(x) && !simp.d_partialModel.hasEitherBound(y)){
-    return y;
-  }else if(!simp.d_partialModel.hasEitherBound(x) && simp.d_partialModel.hasEitherBound(y)){
-    return x;
-  }else {
-    return minColLength(simp, x, y);
-  }
-}
-
-template <bool above>
-ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, SimplexDecisionProcedure::PreferenceFunction pref){
-  ArithVar slack = ARITHVAR_SENTINEL;
-
-  for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd();  ++iter){
-    const Tableau::Entry& entry = *iter;
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == x_i) continue;
-
-    const Rational& a_ij = entry.getCoefficient();
-    int sgn = a_ij.sgn();
-    if(isAcceptableSlack<above>(sgn, nonbasic)){
-      //If one of the above conditions is met, we have found an acceptable
-      //nonbasic variable to pivot x_i with.  We can now choose which one we
-      //prefer the most.
-      slack = (slack == ARITHVAR_SENTINEL) ? nonbasic : pref(*this, slack, nonbasic);
-    }
-  }
-
-  return slack;
-}
-
-Node betterConflict(TNode x, TNode y){
-  if(x.isNull()) return y;
-  else if(y.isNull()) return x;
-  else if(x.getNumChildren() <= y.getNumChildren()) return x;
-  else return y;
-}
-
-bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
-  TimerStat::CodeTimer codeTimer(d_statistics.d_findConflictOnTheQueueTime);
-  Assert(d_successes.empty());
-
-  switch(type){
-  case BeforeDiffSearch:     ++(d_statistics.d_attemptBeforeDiffSearch); break;
-  case DuringDiffSearch:     ++(d_statistics.d_attemptDuringDiffSearch); break;
-  case AfterDiffSearch:      ++(d_statistics.d_attemptAfterDiffSearch); break;
-  case DuringVarOrderSearch: ++(d_statistics.d_attemptDuringVarOrderSearch); break;
-  case AfterVarOrderSearch:  ++(d_statistics.d_attemptAfterVarOrderSearch); break;
-  }
-
-  ArithPriorityQueue::const_iterator i = d_queue.begin();
-  ArithPriorityQueue::const_iterator end = d_queue.end();
-  for(; i != end; ++i){
-    ArithVar x_i = *i;
-
-    if(x_i != d_conflictVariable && d_tableau.isBasic(x_i) && !d_successes.isMember(x_i)){
-      Node possibleConflict = checkBasicForConflict(x_i);
-      if(!possibleConflict.isNull()){
-        d_successes.add(x_i);
-        reportConflict(possibleConflict);
-      }
-    }
-  }
-  if(!d_successes.empty()){
-    switch(type){
-    case BeforeDiffSearch:     ++(d_statistics.d_successBeforeDiffSearch); break;
-    case DuringDiffSearch:     ++(d_statistics.d_successDuringDiffSearch); break;
-    case AfterDiffSearch:      ++(d_statistics.d_successAfterDiffSearch); break;
-    case DuringVarOrderSearch: ++(d_statistics.d_successDuringVarOrderSearch); break;
-    case AfterVarOrderSearch:  ++(d_statistics.d_successAfterVarOrderSearch); break;
-    }
-    d_successes.purge();
-    return true;
-  }else{
-    return false;
-  }
-}
-
-Result::Sat SimplexDecisionProcedure::dualFindModel(bool exactResult){
-  Assert(d_conflictVariable == ARITHVAR_SENTINEL);
-  Assert(d_queue.inCollectionMode());
-
-  if(d_queue.empty()){
-    return Result::SAT;
-  }
-  static CVC4_THREADLOCAL(unsigned int) instance = 0;
-  instance = instance + 1;
-  Debug("arith::findModel") << "begin findModel()" << instance << endl;
-
-  d_queue.transitionToDifferenceMode();
-
-  Result::Sat result = Result::SAT_UNKNOWN;
-
-  if(d_queue.empty()){
-    result = Result::SAT;
-  }else if(d_queue.size() > 1){
-    if(findConflictOnTheQueue(BeforeDiffSearch)){
-      result = Result::UNSAT;
-    }
-  }
-  static const bool verbose = false;
-  exactResult |= options::arithStandardCheckVarOrderPivots() < 0;
-  const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : options::arithStandardCheckVarOrderPivots();
-
-  uint32_t checkPeriod = options::arithSimplexCheckPeriod();
-  if(result == Result::SAT_UNKNOWN){
-    uint32_t numDifferencePivots = options::arithHeuristicPivots() < 0 ?
-      d_numVariables + 1 : options::arithHeuristicPivots();
-    // The signed to unsigned conversion is safe.
-    uint32_t pivotsRemaining = numDifferencePivots;
-    while(!d_queue.empty() &&
-          result != Result::UNSAT &&
-          pivotsRemaining > 0){
-      uint32_t pivotsToDo = min(checkPeriod, pivotsRemaining);
-      pivotsRemaining -= pivotsToDo;
-      if(searchForFeasibleSolution(pivotsToDo)){
-        result = Result::UNSAT;
-      }//Once every CHECK_PERIOD examine the entire queue for conflicts
-      if(result != Result::UNSAT){
-        if(findConflictOnTheQueue(DuringDiffSearch)) { result = Result::UNSAT; }
-      }else{
-        findConflictOnTheQueue(AfterDiffSearch); // already unsat
-      }
-    }
-
-    if(verbose && numDifferencePivots > 0){
-      if(result ==  Result::UNSAT){
-        Message() << "diff order found unsat" << endl;
-      }else if(d_queue.empty()){
-        Message() << "diff order found model" << endl;
-      }else{
-        Message() << "diff order missed" << endl;
-      }
-    }
-  }
-
-  if(!d_queue.empty() && result != Result::UNSAT){
-    if(exactResult){
-      d_queue.transitionToVariableOrderMode();
-
-      while(!d_queue.empty() && result != Result::UNSAT){
-        if(searchForFeasibleSolution(checkPeriod)){
-          result = Result::UNSAT;
-        }
-
-        //Once every CHECK_PERIOD examine the entire queue for conflicts
-        if(result != Result::UNSAT){
-          if(findConflictOnTheQueue(DuringVarOrderSearch)){
-            result = Result::UNSAT;
-          }
-        } else{
-          findConflictOnTheQueue(AfterVarOrderSearch);
-        }
-      }
-      if(verbose){
-        if(result ==  Result::UNSAT){
-          Message() << "bland found unsat" << endl;
-        }else if(d_queue.empty()){
-          Message() << "bland found model" << endl;
-        }else{
-          Message() << "bland order missed" << endl;
-        }
-      }
-    }else{
-      d_queue.transitionToVariableOrderMode();
-
-      if(searchForFeasibleSolution(inexactResultsVarOrderPivots)){
-        result = Result::UNSAT;
-        findConflictOnTheQueue(AfterVarOrderSearch); // already unsat
-      }else{
-        if(findConflictOnTheQueue(AfterVarOrderSearch)) { result = Result::UNSAT; }
-      }
-
-      if(verbose){
-        if(result ==  Result::UNSAT){
-          Message() << "restricted var order found unsat" << endl;
-        }else if(d_queue.empty()){
-          Message() << "restricted var order found model" << endl;
-        }else{
-          Message() << "restricted var order missed" << endl;
-        }
-      }
-    }
-  }
-
-  if(result == Result::SAT_UNKNOWN && d_queue.empty()){
-    result = Result::SAT;
-  }
-
-
-
-  d_pivotsInRound.purge();
-  // ensure that the conflict variable is still in the queue.
-  if(d_conflictVariable != ARITHVAR_SENTINEL){
-    d_queue.enqueueIfInconsistent(d_conflictVariable);
-  }
-  d_conflictVariable = ARITHVAR_SENTINEL;
-
-  d_queue.transitionToCollectionMode();
-  Assert(d_queue.inCollectionMode());
-  Debug("arith::findModel") << "end findModel() " << instance << " " << result <<  endl;
-  return result;
-
-
-  // Assert(foundConflict || d_queue.empty());
-
-  // // Curiously the invariant that we always do a full check
-  // // means that the assignment we can always empty these queues.
-  // d_queue.clear();
-  // d_pivotsInRound.purge();
-  // d_conflictVariable = ARITHVAR_SENTINEL;
-
-  // Assert(!d_queue.inCollectionMode());
-  // d_queue.transitionToCollectionMode();
-
-
-  // Assert(d_queue.inCollectionMode());
-
-  // Debug("arith::findModel") << "end findModel() " << instance << endl;
-
-  // return foundConflict;
-}
-
-
-
-Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
-
-  Assert(d_tableau.isBasic(basic));
-  const DeltaRational& beta = d_partialModel.getAssignment(basic);
-
-  if(d_partialModel.strictlyLessThanLowerBound(basic, beta)){
-    ArithVar x_j = selectSlackUpperBound(basic);
-    if(x_j == ARITHVAR_SENTINEL ){
-      return generateConflictBelowLowerBound(basic);
-    }
-  }else if(d_partialModel.strictlyGreaterThanUpperBound(basic, beta)){
-    ArithVar x_j = selectSlackLowerBound(basic);
-    if(x_j == ARITHVAR_SENTINEL ){
-      return generateConflictAboveUpperBound(basic);
-    }
-  }
-  return Node::null();
-}
-
-//corresponds to Check() in dM06
-//template <SimplexDecisionProcedure::PreferenceFunction pf>
-bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
-  Debug("arith") << "searchForFeasibleSolution" << endl;
-  Assert(remainingIterations > 0);
-
-  while(remainingIterations > 0){
-    if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
-
-    ArithVar x_i = d_queue.dequeueInconsistentBasicVariable();
-    Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
-    if(x_i == ARITHVAR_SENTINEL){
-      Debug("arith_update") << "No inconsistent variables" << endl;
-      return false; //sat
-    }
-
-    --remainingIterations;
-
-    bool useVarOrderPivot = d_pivotsInRound.count(x_i) >=  options::arithPivotThreshold();
-    if(!useVarOrderPivot){
-      d_pivotsInRound.add(x_i);
-    }
-
-
-    Debug("playground") << "pivots in rounds: " <<  d_pivotsInRound.count(x_i)
-                        << " use " << useVarOrderPivot
-                        << " threshold " << options::arithPivotThreshold()
-                        << endl;
-
-    PreferenceFunction pf = useVarOrderPivot ? minVarOrder : minBoundAndRowCount;
-
-    DeltaRational beta_i = d_partialModel.getAssignment(x_i);
-    ArithVar x_j = ARITHVAR_SENTINEL;
-
-    if(d_partialModel.strictlyLessThanLowerBound(x_i, beta_i)){
-      x_j = selectSlackUpperBound(x_i, pf);
-      if(x_j == ARITHVAR_SENTINEL ){
-        ++(d_statistics.d_statUpdateConflicts);
-        Node conflict = generateConflictBelowLowerBound(x_i); //unsat
-        d_conflictVariable = x_i;
-        reportConflict(conflict);
-        return true;
-      }
-      DeltaRational l_i = d_partialModel.getLowerBound(x_i);
-      d_linEq.pivotAndUpdate(x_i, x_j, l_i);
-
-    }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, beta_i)){
-      x_j = selectSlackLowerBound(x_i, pf);
-      if(x_j == ARITHVAR_SENTINEL ){
-        ++(d_statistics.d_statUpdateConflicts);
-        Node conflict = generateConflictAboveUpperBound(x_i); //unsat
-
-        d_conflictVariable = x_i;
-        reportConflict(conflict);
-        return true;
-      }
-      DeltaRational u_i = d_partialModel.getUpperBound(x_i);
-      d_linEq.pivotAndUpdate(x_i, x_j, u_i);
-    }
-    Assert(x_j != ARITHVAR_SENTINEL);
-
-    //Check to see if we already have a conflict with x_j to prevent wasteful work
-    if(CHECK_AFTER_PIVOT){
-      Node possibleConflict = checkBasicForConflict(x_j);
-      if(!possibleConflict.isNull()){
-        d_conflictVariable = x_j;
-        reportConflict(possibleConflict);
-        return true; // unsat
-      }
-    }
-  }
-  Assert(remainingIterations == 0);
-
-  return false;
-}
-
-
-
-Constraint SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){
-
-  int sgn = coeff.sgn();
-  bool ub = aboveUpper?(sgn < 0) : (sgn > 0);
-
-  Constraint c = ub ?
-    d_partialModel.getUpperBoundConstraint(v) :
-    d_partialModel.getLowerBoundConstraint(v);
-
-// #warning "revisit"
-//   Node exp = ub ?
-//     d_partialModel.explainUpperBound(v) :
-//     d_partialModel.explainLowerBound(v);
-
-  bool weakened;
-  do{
-    const DeltaRational& bound = c->getValue();
-
-    weakened = false;
-
-    Constraint weaker = ub?
-      c->getStrictlyWeakerUpperBound(true, true):
-      c->getStrictlyWeakerLowerBound(true, true);
-
-    // Node weaker = ub?
-    //   d_propManager.strictlyWeakerAssertedUpperBound(v, bound):
-    //   d_propManager.strictlyWeakerAssertedLowerBound(v, bound);
-
-    if(weaker != NullConstraint){
-    //if(!weaker.isNull()){
-      const DeltaRational& weakerBound = weaker->getValue();
-      //DeltaRational weakerBound = asDeltaRational(weaker);
-
-      DeltaRational diff = aboveUpper ? bound - weakerBound : weakerBound - bound;
-      //if var == basic,
-      //  if aboveUpper, weakerBound > bound, multiply by -1
-      //  if !aboveUpper, weakerBound < bound, multiply by -1
-      diff = diff * coeff;
-      if(surplus > diff){
-        ++d_statistics.d_weakenings;
-        weakened = true;
-        anyWeakening = true;
-        surplus = surplus - diff;
-
-        Debug("weak") << "found:" << endl;
-        if(v == basic){
-          Debug("weak") << "  basic: ";
-        }
-        Debug("weak") << "  " << surplus << " "<< diff  << endl
-                      << "  " << bound << c << endl
-                      << "  " << weakerBound << weaker << endl;
-
-        Assert(diff > d_DELTA_ZERO);
-        c = weaker;
-      }
-    }
-  }while(weakened);
-
-  return c;
-}
-
-Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar){
-  TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
-
-  const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
-  DeltaRational surplus;
-  if(aboveUpper){
-    Assert(d_partialModel.hasUpperBound(basicVar));
-    Assert(assignment > d_partialModel.getUpperBound(basicVar));
-    surplus = assignment - d_partialModel.getUpperBound(basicVar);
-  }else{
-    Assert(d_partialModel.hasLowerBound(basicVar));
-    Assert(assignment < d_partialModel.getLowerBound(basicVar));
-    surplus = d_partialModel.getLowerBound(basicVar) - assignment;
-  }
-
-  NodeBuilder<> conflict(kind::AND);
-  bool anyWeakenings = false;
-  for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){
-    const Tableau::Entry& entry = *i;
-    ArithVar v = entry.getColVar();
-    const Rational& coeff = entry.getCoefficient();
-    bool weakening = false;
-    Constraint c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar);
-    Debug("weak") << "weak : " << weakening << " "
-                  << c->assertedToTheTheory() << " "
-                  << d_partialModel.getAssignment(v) << " "
-                  << c << endl
-                  << c->explainForConflict() << endl;
-    anyWeakenings = anyWeakenings || weakening;
-
-    Debug("weak") << "weak : " << c->explainForConflict() << endl;
-    c->explainForConflict(conflict);
-  }
-  ++d_statistics.d_weakeningAttempts;
-  if(anyWeakenings){
-    ++d_statistics.d_weakeningSuccesses;
-  }
-  return conflict;
-}
-
-
-Node SimplexDecisionProcedure::generateConflictAboveUpperBound(ArithVar conflictVar){
-  return weakenConflict(true, conflictVar);
-}
-
-Node SimplexDecisionProcedure::generateConflictBelowLowerBound(ArithVar conflictVar){
-  return weakenConflict(false, conflictVar);
-}
-
-
-// responses 
-//   unbounded below(arithvar)
-//   reached threshold
-//   reached maxpivots
-//   reached GlobalMinimumd
-//   
-SimplexDecisionProcedure::PrimalResponse SimplexDecisionProcedure::primal(uint32_t maxIterations)
-{
-  Assert(d_optRow != ARITHVAR_SENTINEL);
-
-  for(uint32_t iteration = 0; iteration < maxIterations; iteration++){
-    if(belowThreshold()){
-      return ReachedThresholdValue;
-    }
-
-    PrimalResponse res = primalCheck();
-    switch(res){
-    case GlobalMinimum:
-    case FoundUnboundedVariable:
-      return res;
-    case NoProgressOnLeaving:
-      ++d_statistics.d_primalPivots;
-      ++d_pivotsSinceOptProgress;
-      ++d_pivotsSinceLastCheck;
-      ++d_pivotsSinceErrorProgress;
-
-      d_linEq.pivotAndUpdate(d_primalCarry.d_entering, d_primalCarry.d_leaving, d_partialModel.getAssignment(d_primalCarry.d_entering));
-
-      if(Debug.isOn("primal::tableau")){
-	d_linEq.debugCheckTableau();
-      }
-      if(Debug.isOn("primal::consistent")){ Assert(d_linEq.debugEntireLinEqIsConsistent("MakeProgressOnLeaving")); }
-
-      break;
-    case MakeProgressOnLeaving:
-      {
-	++d_statistics.d_primalPivots;
-	++d_statistics.d_primalImprovingPivots;
-
-	d_pivotsSinceOptProgress = 0;
-	++d_pivotsSinceErrorProgress;
-	++d_pivotsSinceLastCheck;
-
-	d_linEq.pivotAndUpdate(d_primalCarry.d_entering, d_primalCarry.d_leaving, d_primalCarry.d_nextEnteringValue);
-
-	static int helpful = 0;
-	static int hurtful = 0;
-	static int penguin = 0;
-	if(d_currentErrorVariables.isKey(d_primalCarry.d_entering)){
-	  cout << "entering is error " << d_primalCarry.d_entering;
-	  if(d_currentErrorVariables[d_primalCarry.d_entering].errorIsLeqZero(d_partialModel)){
-	    cout << " now below threshold (" << (++helpful) << ") " << d_pivotsSinceErrorProgress << endl;
-	  }else{
-	    cout << "ouch (" << (++hurtful) << ")"<< d_pivotsSinceErrorProgress << endl;
-	  }
-	}else if(d_currentErrorVariables.isKey(d_primalCarry.d_leaving)){
-	  cout << "leaving is error " << d_primalCarry.d_leaving;
-	  if(d_currentErrorVariables[d_primalCarry.d_leaving].errorIsLeqZero(d_partialModel)){
-	    cout << " now below threshold(" << (++helpful) << ")" << d_pivotsSinceErrorProgress << endl;
-	  }else{
-	    cout << "ouch (" << (++hurtful) << ")" << d_pivotsSinceErrorProgress<< endl;
-	  }
-	}else{
-	  cout << " penguin (" << (++penguin) << ")" << d_pivotsSinceErrorProgress<< endl;
-	}
-
-	if(Debug.isOn("primal::tableau")){
-	  d_linEq.debugCheckTableau();
-	}
-	if(Debug.isOn("primal::consistent")){ Assert(d_linEq.debugEntireLinEqIsConsistent("MakeProgressOnLeaving")); }
-      }
-      break;
-    default:
-      Unreachable();
-    }
-  }
-  return UsedMaxPivots;
-}
-
-
-/**
- * Error set
- * ErrorVariable |-> {ErrorVariable, InputVariable, InputConstraint}
- */
-
-/**
- * Returns SAT if it was able to satisfy all of the constraints in the error set
- * Returns UNSAT if it was able to able to find an error 
- */
-Result::Sat SimplexDecisionProcedure::primalConverge(int depth){
-  d_pivotsSinceLastCheck = 0;
-
-  while(!d_currentErrorVariables.empty()){
-    PrimalResponse res = primal(MAX_ITERATIONS - d_pivotsSinceLastCheck);
-
-    switch(res){
-    case FoundUnboundedVariable:
-
-      // Drive the variable to at least 0
-      // TODO This variable should be driven to a value that makes all of the error functions including it 0
-      // It'll or another unbounded will be selected in the next round anyways so ignore for now.
-      ++d_statistics.d_unboundedFound;
-      if( !belowThreshold() ){
-	driveOptToZero(d_primalCarry.d_unbounded);
-	d_linEq.debugCheckTableau();
-	if(Debug.isOn("primal::consistent")){ Assert(d_linEq.debugEntireLinEqIsConsistent("primalConverge")); }
-
-	++d_statistics.d_unboundedFound_drive;
-      }
-      Assert(belowThreshold());
-      {      
-	uint32_t dropped = contractErrorVariables(true);
-	Debug("primal::converge") << "primalConverge -> FoundUnboundedVariable -> dropped " << dropped  << " to " << d_currentErrorVariables.size() << endl;
-	d_statistics.d_unboundedFound_dropped += dropped;
-      }
-      break;
-    case ReachedThresholdValue:
-      ++d_statistics.d_primalThresholdReachedPivot;
-
-      Assert(belowThreshold());
-      {
-	uint32_t dropped = contractErrorVariables(true);
-	Debug("primal::converge") << "primalConverge -> ReachedThresholdValue -> dropped " << dropped  << " to " << d_currentErrorVariables.size() << endl;
-	d_statistics.d_primalThresholdReachedPivot_dropped += dropped;
-      }
-      break;
-    case UsedMaxPivots:
-      {
-	d_pivotsSinceLastCheck = 0;
-	++d_statistics.d_primalReachedMaxPivots;
-
-	// periodically attempt to do the following : 
-	//   contract the error variable
-	//   check for a conflict on an error variable
-	uint32_t dropped = contractErrorVariables(false);
-	
-	if( checkForRowConflicts() ){ // try to periodically look for a row 
-	  Debug("primal::converge") << "primalConverge -> UsedMaxPivots -> unsat " << endl;
-
-	  ++d_statistics.d_primalReachedMaxPivots_checkForConflictWorked;
-	  return Result::UNSAT; // row conflicts are minimal so stop.
-	}
-
-	if(dropped > 0){
-	  Debug("primal::converge") << "primalConverge -> UsedMaxPivots -> dropped " << dropped  << " to " << d_currentErrorVariables.size() << endl;
-	  ++d_statistics.d_primalReachedMaxPivots_contractMadeProgress;
-	}else{
-	  Debug("primal::converge") << "primalConverge -> UsedMaxPivots -> nothing " << endl;
-	}
-      }
-      break;
-    case GlobalMinimum:
-      ++d_statistics.d_primalGlobalMinimum;
-
-      // If the minimum is positive, this is unsat.
-      // However, the optimization row is not necessarily a minimal conflict
-      if(!belowThreshold()){
-
-	if(d_currentErrorVariables.size() == 1){
-	  // The optimization function is exactly the same as the last remaining variable
-	  // The conflict for the row is the same as the conflict for the optimization function.
-	  bool foundConflict = checkForRowConflicts();
-	  Assert(foundConflict);
-	  Debug("primal::converge") << "primalConverge -> GlobalMinimum -> one variable" << endl;
-
-	  return Result::UNSAT;
-	}else{
-	  // There are at least 2 error variables.
-	  // Look for a minimal conflict
-
-
-	  if(checkForRowConflicts() ){
-	    Debug("primal::converge") << "primalConverge -> GlobalMinimum -> postitive -> rowconflict " << endl;
-		  
-	    ++d_statistics.d_primalGlobalMinimum_rowConflictWorked;
-	    return Result::UNSAT;
-	  }
-
-	  uint32_t dropped = contractErrorVariables(false);
-	  
-	  Debug("primal::converge") << "primalConverge -> GlobalMinimum -> postitive -> dropped " << dropped  << " to " << d_currentErrorVariables.size() << endl;
-	  if(dropped > 0){
-	    ++d_statistics.d_primalGlobalMinimum_contractMadeProgress;
-	  }
-
-	  ErrorMap half;
-	  d_currentErrorVariables.splitInto(half);
-
-	  Debug("primal::converge") << "primalConverge -> GlobalMinimum -> recursion " << depth << endl;
-
-
-	  reconstructOptimizationFunction();
-	  Result::Sat resultOnRemaining = primalConverge(depth + 1);
-
-	  if(resultOnRemaining == Result::UNSAT){
-	    Debug("primal::converge") << "primalConverge -> GlobalMinimum -> recursion " << depth << " was unsat " << endl;
-	    ++d_statistics.d_primalGlobalMinimum_firstHalfWasUnsat;
-	    restoreErrorVariables(half);
-	    return Result::UNSAT;
-	  }else{
-	    ++d_statistics.d_primalGlobalMinimum_firstHalfWasSat;
-	    Debug("primal::converge") << "primalConverge -> GlobalMinimum -> recursion " << depth << " was sat " << endl;
-
-	    Assert(resultOnRemaining == Result::SAT);
-	    Assert(d_currentErrorVariables.empty());
-	    d_currentErrorVariables.addAll(half);
-	    reconstructOptimizationFunction();
-	    return primalConverge(depth + 1);
-	  }
-	}
-
-      }else{
-
-	// if the optimum is <= 0
-	// drop all of the satisfied variables and continue;
-	uint32_t dropped = contractErrorVariables(true);
-	Debug("primal::converge") << "primalConverge -> GlobalMinimum -> negative -> dropped "<< dropped  << " to " << d_currentErrorVariables.size() << endl;
-
-	++d_statistics.d_primalGlobalMinimum_contractMadeProgress;
-      }
-      break;
-    default:
-      Unreachable();
-    }
-   }
-
-   return Result::SAT;
-}
-
-
-Result::Sat SimplexDecisionProcedure::primalFindModel(){
-  Assert(d_primalCarry.isClear());
-
-  // Reduce the queue to only contain violations
-  reduceQueue();
-
-  if(d_queue.empty()){
-    return Result::SAT;
-  }
-  TimerStat::CodeTimer codeTimer(d_statistics.d_primalTimer);
-  
-  ++d_statistics.d_primalCalls;
-
-  Debug("primalFindModel") << "primalFindModel() begin" << endl;
-
-  const int PAUSE_RATE = 100;
-  if(Debug.isOn("primal::pause") && d_statistics.d_primalCalls.getData() % PAUSE_RATE  == 0){
-    Debug("primal::pause") << "waiting for input: ";
-    std::string dummy;
-    std::getline(std::cin, dummy);
-  }
-
-  // TODO restore the tableau by ejecting variables
-  //  Tableau copy(d_tableau);
-
-  Result::Sat answer;
-  {
-    TimerStat::CodeTimer codeTimer(d_statistics.d_internalTimer);
-
-    // This is needed because of the fiddling with the partial model
-    //context::Context::ScopedPush speculativePush(satContext);
-
-    constructErrorVariables();
-    constructOptimizationFunction();
-    if(Debug.isOn("primal::tableau")){ d_linEq.debugCheckTableau(); }
-    if(Debug.isOn("primal::consistent")){ d_linEq.debugEntireLinEqIsConsistent("primalFindModel 1"); }
-    answer = primalConverge(0);
-  }
-  removeOptimizationFunction();
-
-
-  // exit
-  uint32_t nc = d_tableau.getNumColumns();
-  //d_tableau = copy;
-  while(d_tableau.getNumColumns() < nc){
-    d_tableau.increaseSize();
-  }
-  restoreErrorVariables(d_currentErrorVariables);
-
-  reduceQueue();
-
-  if(Debug.isOn("primal::tableau")){ d_linEq.debugCheckTableau(); }
-
-  if(Debug.isOn("primal::consistent")){ d_linEq.debugEntireLinEqIsConsistent("primalFindModel2"); }
-  Debug("primalFindModel") << "primalFindModel() end " << answer << endl;
-
-  // The set of variables in conflict with their bounds will still be a subset of the
-  // variables that are in conflict with their bounds in the beginning.
-  // The basic variables are the same because of the copy.
-  // Thus it is safe to not try to not recompute the queue of violating variables
-
-  if(answer == Result::UNSAT){
-    // This needs to be done in a different context level than the push
-    ++d_statistics.d_primalUnsatCalls;
-  }else{
-    ++d_statistics.d_primalSatCalls;
-  }
-  
-  d_primalCarry.clear();
-
-  return answer;
-}
-
-/** Clears the ErrorMap and relase the resources associated with it.
- * There are a couple of error maps around
- */
-void SimplexDecisionProcedure::restoreErrorVariables(SimplexDecisionProcedure::ErrorMap& es){
-  while(!es.empty()){
-    ArithVar e = es.back();
-
-    reassertErrorConstraint(e, es, false, false);
-    es.pop_back();
-  }
-}
-
-void SimplexDecisionProcedure::constructErrorVariables(){
-  Assert(d_currentErrorVariables.empty());
-  Assert(!d_queue.empty());
-
-  for(ArithPriorityQueue::const_iterator iter = d_queue.begin(), end = d_queue.end(); iter != end; ++iter){
-    ArithVar input = *iter;
-
-    Assert(d_tableau.isBasic(input));
-    Assert(!d_partialModel.assignmentIsConsistent(input));
-
-    Assert(!d_currentErrorVariables.isKey(input));
-
-    bool ub = d_partialModel.strictlyGreaterThanUpperBound(input, d_partialModel.getAssignment(input));
-
-    Constraint original =  ub ? d_partialModel.getUpperBoundConstraint(input)
-      :  d_partialModel.getLowerBoundConstraint(input);
-
-    d_currentErrorVariables.set(input, ErrorInfo(input, ub, original));
-
-    if(ub){
-      d_partialModel.forceRelaxUpperBound(input);
-    }else{
-      d_partialModel.forceRelaxLowerBound(input);
-    }
-    Debug("primal") << "adding error variable (" << input << ", " << ", " << original <<") ";
-    Debug("primal") << "ub "<< ub << " " <<  d_partialModel.getAssignment(input)  << " " <<  original->getValue() <<")" << endl;
-    d_currentErrorVariables.set(input, ErrorInfo(input, ub, original));
-
-    // Constraint boundIsValue = d_constraintDatabase.getConstraint(bound, Equality, original->getValue());
-    // boundIsValue->setPsuedoConstraint();
-
-    // d_partialModel.setAssignment(bound, boundIsValue->getValue());
-    // d_partialModel.setUpperBoundConstraint(boundIsValue);
-    // d_partialModel.setLowerBoundConstraint(boundIsValue);
-
-    // // if ub
-    // // then  error = x - boundIsValue
-    // // else  error = boundIsValue - x
-
-    // ArithVar error = requestVariable();
-
-    // DeltaRational diff = ub ?
-    //   d_partialModel.getAssignment(input) - boundIsValue->getValue() :
-    //   boundIsValue->getValue() - d_partialModel.getAssignment(input);
-
-    // d_partialModel.setAssignment(error, diff);
-
-    // vector<Rational> coeffs;
-    // vector<ArithVar> variables;
-    // variables.push_back(input);
-    // coeffs.push_back(ub ? Rational(1) : Rational(-1));
-    // variables.push_back(bound);
-    // coeffs.push_back(ub ? Rational(-1) : Rational(1));
-
-    // d_tableau.addRow(error, coeffs, variables);
-
-
-  }
-
-  if(Debug.isOn("primal::tableau")){ d_linEq.debugCheckTableau(); }
-  if(Debug.isOn("primal::consistent")){  d_linEq.debugEntireLinEqIsConsistent("constructErrorVariables");}
-  Assert(!d_currentErrorVariables.empty());
-}
-
-
-
-/** Returns true if it has found a row conflict for any of the error variables. */
-bool SimplexDecisionProcedure::checkForRowConflicts(){
-  vector<ArithVar> inConflict;
-  for(ErrorMap::const_iterator iter = d_currentErrorVariables.begin(), end = d_currentErrorVariables.end(); iter != end; ++iter){
-    ArithVar error = *iter;
-    const ErrorInfo& info = d_currentErrorVariables[error];
-    if(d_tableau.isBasic(error) && !info.errorIsLeqZero(d_partialModel)){
-
-      ArithVar x_j = info.isUpperbound() ?
-	selectSlackLowerBound(error) :
-	selectSlackUpperBound(error);
-
-      if(x_j == ARITHVAR_SENTINEL ){
-	inConflict.push_back(error);
-      }
-    }
-  }
-
-  if(!inConflict.empty()){
-    while(!inConflict.empty()){
-      ArithVar error = inConflict.back();
-      inConflict.pop_back();
-
-      reassertErrorConstraint(error, d_currentErrorVariables, false, true);
-
-      Node conflict =  d_currentErrorVariables[error].isUpperbound() ?
-	generateConflictAboveUpperBound(error) :
-	generateConflictBelowLowerBound(error);
-      Assert(!conflict.isNull());
-
-      d_currentErrorVariables.remove(error);
-      
-      reportConflict(conflict);
-    }
-    reconstructOptimizationFunction();
-    return true;
-  }else{
-    return false;
-  }
-}
-
-void SimplexDecisionProcedure::reassertErrorConstraint(ArithVar e, SimplexDecisionProcedure::ErrorMap& es, bool definitelyTrue, bool definitelyFalse){
-  Assert(es.isKey(e));
-  const ErrorInfo& info = es.get(e);
-  Constraint original = info.getConstraint();
-
-  if(info.isUpperbound()){
-    d_partialModel.setUpperBoundConstraint(original);
-  }else if(original->isLowerBound()){
-    d_partialModel.setLowerBoundConstraint(original);
-  }
-
-  Assert(!definitelyTrue || d_partialModel.assignmentIsConsistent(e));
-  Assert(!definitelyFalse || !d_partialModel.assignmentIsConsistent(e));
-}
-
-uint32_t SimplexDecisionProcedure::contractErrorVariables(bool guaranteedSuccess){
-  uint32_t entrySize = d_currentErrorVariables.size();
-  Debug("primal::contract") << "contractErrorVariables() begin : " << d_currentErrorVariables.size() << endl;
-
-  std::vector<ArithVar> toRemove;
-  for(ErrorMap::const_iterator iter = d_currentErrorVariables.begin(), end = d_currentErrorVariables.end(); iter != end; ++iter){
-    ArithVar e = *iter;
-    if(d_currentErrorVariables[e].errorIsLeqZero(d_partialModel)){
-      toRemove.push_back(e);
-    }
-  }
-
-  Assert(!guaranteedSuccess || !toRemove.empty());
-
-  if(!toRemove.empty()){
-    while(!toRemove.empty()){
-      ArithVar e = toRemove.back();
-      toRemove.pop_back();
-      reassertErrorConstraint(e, d_currentErrorVariables, true, false);
-      d_currentErrorVariables.remove(e);
-    }
-
-    reconstructOptimizationFunction();
-  }    
-
-  Debug("primal::contract") << "contractErrorVariables() end : " << d_currentErrorVariables.size() << endl;
-  
-  uint32_t exitSize = d_currentErrorVariables.size();
-
-  Assert(exitSize <= entrySize);
-  Assert(!guaranteedSuccess|| exitSize < entrySize);
-  return entrySize - exitSize;
-}
-
-void SimplexDecisionProcedure::removeOptimizationFunction(){
-  Assert(d_optRow != ARITHVAR_SENTINEL);
-  Assert(d_tableau.isBasic(d_optRow));
-  
-  d_tableau.removeBasicRow(d_optRow);
-  releaseVariable(d_optRow);
-
-  d_optRow = ARITHVAR_SENTINEL;
-  d_negOptConstant = d_DELTA_ZERO;
-
-  Assert(d_optRow == ARITHVAR_SENTINEL);
-}
-
-void SimplexDecisionProcedure::constructOptimizationFunction(){
-  Assert(d_optRow == ARITHVAR_SENTINEL);
-  Assert(d_negOptConstant == d_DELTA_ZERO);
-  
-  d_optRow = requestVariable();
-
-
-  std::vector<Rational> coeffs;
-  std::vector<ArithVar> variables;
-  for(ErrorMap::const_iterator iter = d_currentErrorVariables.begin(), end = d_currentErrorVariables.end(); iter != end; ++iter){
-    ArithVar e = *iter;
-
-    if(d_currentErrorVariables[e].isUpperbound()){
-      coeffs.push_back(Rational(1)); 
-      variables.push_back(e);
-      d_negOptConstant = d_negOptConstant + (d_currentErrorVariables[e].getConstraint()->getValue());
-    }else{
-      coeffs.push_back(Rational(-1));
-      variables.push_back(e);
-      d_negOptConstant = d_negOptConstant - (d_currentErrorVariables[e].getConstraint()->getValue());
-    }
-  }
-  d_tableau.addRow(d_optRow, coeffs, variables);
-
-  DeltaRational newAssignment = d_linEq.computeRowValue(d_optRow, false);
-  d_partialModel.setAssignment(d_optRow, newAssignment);
-
-  if(Debug.isOn("primal::tableau")){ d_linEq.debugCheckTableau(); }
-
-
-  if(Debug.isOn("primal::consistent")){
-    d_linEq.debugEntireLinEqIsConsistent("constructOptimizationFunction");
-  }
-
-  d_pivotsSinceOptProgress = 0;
-  d_pivotsSinceErrorProgress = 0;
-
-  Assert(d_optRow != ARITHVAR_SENTINEL);
-}
-
-void SimplexDecisionProcedure::reconstructOptimizationFunction(){
-  removeOptimizationFunction();
-  constructOptimizationFunction();
-}
-
-
-
-/* TODO:
- * Very naive implementation. Recomputes everything every time.
- * Currently looks for the variable that can decrease the optimization function the most.
- * 
- */
-SimplexDecisionProcedure::PrimalResponse SimplexDecisionProcedure::primalCheck()
-{
-  Debug("primal") << "primalCheck() begin" << endl;
-
-  ArithVar leaving = ARITHVAR_SENTINEL;
-  ArithVar entering =  ARITHVAR_SENTINEL;
-  DeltaRational leavingShift = d_DELTA_ZERO; // The amount the leaving variable can change by without making the tableau inconsistent
-  DeltaRational leavingDelta = d_DELTA_ZERO; // The amount the optimization function changes by selecting leaving
-  
-  Assert(d_improvementCandidates.empty());
-
-  for( Tableau::RowIterator ri = d_tableau.basicRowIterator(d_optRow); !ri.atEnd(); ++ri){
-    const Tableau::Entry& e = *ri;
-
-    ArithVar curr = e.getColVar();
-    if(curr == d_optRow){ continue; }
-
-
-    int sgn = e.getCoefficient().sgn();
-    Assert(sgn != 0);
-    if( (sgn < 0 && d_partialModel.strictlyBelowUpperBound(curr)) ||
-	(sgn > 0 && d_partialModel.strictlyAboveLowerBound(curr)) ){
-
-      d_improvementCandidates.push_back(&e);
-    }
-  }
-
-  if(d_improvementCandidates.empty()){
-    Debug("primal") << "primalCheck() end : global" << endl;
-    return GlobalMinimum; // No variable in the optimization function can be improved
-  }
-  
-  DeltaRational minimumShift;
-  DeltaRational currShift;
-  for(EntryVector::const_iterator ci = d_improvementCandidates.begin(), end_ci = d_improvementCandidates.end(); ci != end_ci; ++ci){
-    const Tableau::Entry& e = *(*ci);
-    ArithVar curr = e.getColVar();
-
-    ArithVar currEntering;
-    bool progress;
-    
-    minimumShift = (leaving == ARITHVAR_SENTINEL ) ? leavingDelta/(e.getCoefficient().abs()) : d_DELTA_ZERO;
-    int sgn = e.getCoefficient().sgn();
-    computeShift(curr, sgn < 0, progress, currEntering, currShift, minimumShift);
-
-    if(currEntering == ARITHVAR_SENTINEL){
-      d_improvementCandidates.clear();
-
-      Debug("primal") << "primalCheck() end : unbounded" << endl;
-      d_primalCarry.d_unbounded = curr;
-      return FoundUnboundedVariable;
-    }else if(progress) {
-      leaving = curr;
-      leavingShift = currShift;
-      leavingDelta = currShift * e.getCoefficient();
-      entering = currEntering;
-
-      Assert(leavingDelta < d_DELTA_ZERO);
-
-      const int RECHECK_PERIOD = 10;
-      if(d_pivotsSinceErrorProgress % RECHECK_PERIOD != 0){
-	// we can make progress, stop
-	break;
-      }
-    }
-  }
-
-  if(leaving == ARITHVAR_SENTINEL){
-    cout << "Nothing can make progress " << endl;
-
-    const uint32_t THRESHOLD = 20;
-    if(d_pivotsSinceOptProgress <= THRESHOLD){
-
-      int index = rand() % d_improvementCandidates.size();
-      leaving =  (*d_improvementCandidates[index]).getColVar();
-      entering = selectFirstValid(leaving, (*d_improvementCandidates[index]).getCoefficient().sgn() < 0);
-    }else{ // Bland's rule
-      bool increasing;
-      for(EntryVector::const_iterator ci = d_improvementCandidates.begin(), end_ci = d_improvementCandidates.end(); ci != end_ci; ++ci){
-	const Tableau::Entry& e = *(*ci);
-	ArithVar curr = e.getColVar();
-	leaving = (leaving == ARITHVAR_SENTINEL) ? curr : minVarOrder(*this, curr, leaving);
-	if(leaving == curr){
-	  increasing = (e.getCoefficient().sgn() < 0);
-	}
-      }
-      
-      entering = selectMinimumValid(leaving, increasing);
-    }
-    Assert(leaving != ARITHVAR_SENTINEL);
-    Assert(entering != ARITHVAR_SENTINEL);
-
-    d_primalCarry.d_leaving = leaving;
-    d_primalCarry.d_entering = entering;
-
-    d_primalCarry.d_nextEnteringValue = d_partialModel.getAssignment(entering);
-
-    Debug("primal") << "primalCheck() end : no progress made " <<  leaving << " to " << entering << " (" << d_pivotsSinceOptProgress << ")"<< endl;
-    d_improvementCandidates.clear();
-    return NoProgressOnLeaving;
-  }else{
-    const Tableau::Entry& enterLeavingEntry = d_tableau.findEntry(d_tableau.basicToRowIndex(entering), leaving);
-    Assert(!enterLeavingEntry.blank());
-
-    d_primalCarry.d_leaving = leaving;
-    d_primalCarry.d_entering = entering;
-    d_primalCarry.d_nextEnteringValue = d_partialModel.getAssignment(entering)
-      + leavingShift * enterLeavingEntry.getCoefficient();
-
-    Debug("primal") << "primalCheck() end : progress" << endl
-		    << leaving << " to " << entering << " ~ "
-		    << d_partialModel.getAssignment(leaving) << " ~ "  << leavingShift
-		    << " ~ " << enterLeavingEntry.getCoefficient()
-		    << " ~ " << d_primalCarry.d_nextEnteringValue << endl;
-
-    d_improvementCandidates.clear();
-    return MakeProgressOnLeaving;
-  }
-
-  //   anyProgress = true;
-
-  //     DeltaRational currDelta = currShift * e.getCoefficient();
-
-  //     int cmp = currDelta.cmp(leavingDelta);
-      
-  //     // Cases:
-  //     // 1) No candidate yet, 
-  //     // 2) there is a candidate with a strictly better update, or
-  //     // 3) there is a candidate with the same update value that has a smaller value in the variable ordering.
-  //     //
-  //     // Case 3 covers Bland's rule.
-  //     if(entering == ARITHVAR_SENTINEL || cmp < 0){
-  // 	leaving = curr;
-  //     }else if( cmp == 0 ){
-  // 	leaving = minVarOrder(*this, curr, leaving);
-  //     }
-
-  //     if(leaving == curr){
-  // 	leavingShift = currShift;
-  // 	leavingDelta = currDelta;
-  // 	entering = currEntering;
-  //     }
-  //   }
-  // }
-
-  // if(leaving == ARITHVAR_SENTINEL){
-  //   Debug("primal") << "primalCheck() end : global" << endl;
-  //   return GlobalMinimum; // No variable in the optimization function can be improved
-  // }else{
-  //   const Tableau::Entry& enterLeavingEntry = d_tableau.findEntry(d_tableau.basicToRowIndex(entering), leaving);
-  //   Assert(!enterLeavingEntry.blank());
-
-  //   d_primalCarry.d_leaving = leaving;
-  //   d_primalCarry.d_entering = entering;
-  //   d_primalCarry.d_nextEnteringValue = d_partialModel.getAssignment(entering)
-  //     + leavingShift * enterLeavingEntry.getCoefficient();
-
-  //   Debug("primal") << "primalCheck() end : progress" << endl
-  // 		    << leaving << " to " << entering << " ~ "
-  // 		    << d_partialModel.getAssignment(leaving) << " ~ "  << leavingShift
-  // 		    << " ~ " << enterLeavingEntry.getCoefficient()
-  // 		    << " ~ " << d_primalCarry.d_nextEnteringValue << endl;
-  //   return MakeProgressOnLeaving;
-  // }
-}
-
-ArithVar SimplexDecisionProcedure::selectMinimumValid(ArithVar v, bool increasing){
-  ArithVar minimum = ARITHVAR_SENTINEL;
-  for(Tableau::ColIterator colIter = d_tableau.colIterator(v);!colIter.atEnd(); ++colIter){
-    const Tableau::Entry& e = *colIter;
-    ArithVar basic = d_tableau.rowIndexToBasic(e.getRowIndex());
-    if(basic == d_optRow) continue;
-
-    
-    int esgn = e.getCoefficient().sgn();
-    bool basicInc = (increasing  == (esgn > 0));
-
-    if(!(basicInc ? d_partialModel.strictlyBelowUpperBound(basic) :
-	 d_partialModel.strictlyAboveLowerBound(basic))){
-      if(minimum == ARITHVAR_SENTINEL){
-	minimum = basic;
-      }else{
-	minimum = minVarOrder(*this, basic, minimum);
-      }
-    }
-  }
-  return minimum;
-}
-
-ArithVar SimplexDecisionProcedure::selectFirstValid(ArithVar v, bool increasing){
-  ArithVar minimum = ARITHVAR_SENTINEL;
-
-  for(Tableau::ColIterator colIter = d_tableau.colIterator(v);!colIter.atEnd(); ++colIter){
-    const Tableau::Entry& e = *colIter;
-    ArithVar basic = d_tableau.rowIndexToBasic(e.getRowIndex());
-    if(basic == d_optRow) continue;
-
-    int esgn = e.getCoefficient().sgn();
-    bool basicInc = (increasing  == (esgn > 0));
-
-    if(!(basicInc ? d_partialModel.strictlyBelowUpperBound(basic) :
-	 d_partialModel.strictlyAboveLowerBound(basic))){
-      if(minimum == ARITHVAR_SENTINEL){
-	minimum = basic;
-      }else{
-	minimum = minRowLength(*this, basic, minimum);
-      }
-    }
-  }
-  return minimum;
-}
-
-
-
-void SimplexDecisionProcedure::computeShift(ArithVar leaving, bool increasing, bool& progress, ArithVar& entering, DeltaRational& shift, const DeltaRational& minimumShift){
-  Assert(increasing ? (minimumShift >= d_DELTA_ZERO) : (minimumShift <= d_DELTA_ZERO) );
-
-  static int instance = 0;
-  Debug("primal") << "computeshift " << ++instance  << " " << leaving << endl;
-
-  // The selection for the leaving variable
-  entering = ARITHVAR_SENTINEL;
-
-  // no progress is initially made
-  progress = false;
-
-  bool bounded = false;
-
-  if(increasing ? d_partialModel.hasUpperBound(leaving) : d_partialModel.hasLowerBound(leaving)){
-    const DeltaRational& assignment = d_partialModel.getAssignment(leaving);
-
-    bounded = true;
-
-    DeltaRational diff = increasing ? d_partialModel.getUpperBound(leaving) - assignment : d_partialModel.getLowerBound(leaving) - assignment;
-    Assert(increasing ? diff.sgn() >=0 : diff.sgn() <= 0);
-    if((increasing) ? (diff < minimumShift) : ( diff > minimumShift)){
-      Assert(!progress);
-      entering = leaving; // My my my, what an ugly hack
-      return; // no progress is possible stop
-    }
-  }
-
-  // shift has a meaningful value once entering has a meaningful value
-  // if increasing,
-  // then  shift > minimumShift >= 0
-  // else  shift < minimumShift <= 0
-  //
-  // Maintain the following invariant:
-  //
-  // if increasing,
-  //    if e_ij > 0, diff >= shift > minimumShift >= 0
-  //    if e_ij < 0, diff >= shift > minimumShift >= 0
-  // if !increasing,
-  //    if e_ij > 0, diff <= shift < minimumShift <= 0
-  //    if e_ij < 0, diff <= shift < minimumShift <= 0
-  // if increasing == (e_ij > 0), diff = (d_partialModel.getUpperBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient()
-  // if increasing != (e_ij > 0), diff = (d_partialModel.getLowerBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient()
-
-  for(Tableau::ColIterator colIter = d_tableau.colIterator(leaving);!colIter.atEnd(); ++colIter){
-    const Tableau::Entry& e = *colIter;
-    
-    ArithVar basic = d_tableau.rowIndexToBasic(e.getRowIndex());
-    if(basic == d_optRow) continue;
-
-    int esgn = e.getCoefficient().sgn();
-    bool basicInc = (increasing  == (esgn > 0));
-    // If both are true, increasing the variable entering increases the basic variable
-    // If both are false, the entering variable is decreasing, but the coefficient is negative and the basic variable is increasing
-    // If exactly one is false, the basic variable is decreasing.
-
-    Debug("primal::shift") << basic << " " << d_partialModel.hasUpperBound(basic) << " "
-			   << d_partialModel.hasLowerBound(basic) << " "
-			   << e.getCoefficient() << endl;
-
-    if( (basicInc && d_partialModel.hasUpperBound(basic))||
-	(!basicInc && d_partialModel.hasLowerBound(basic))){
-
-      if(!(basicInc ? d_partialModel.strictlyBelowUpperBound(basic) :
-	   d_partialModel.strictlyAboveLowerBound(basic))){
-	// diff == 0, as diff > minimumShift >= 0 or diff < minimumShift <= 0
-	Assert(!progress);
-	entering = basic;
-	return;
-      }else{
-	DeltaRational diff = basicInc ?
-	  (d_partialModel.getUpperBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient() :
-	  (d_partialModel.getLowerBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient();
-
-	if( entering == ARITHVAR_SENTINEL ){
-	  if(increasing ? (diff <= minimumShift) : (diff >= minimumShift)){
-	    Assert(!progress);
-	    entering = basic;
-	    return;
-	  }else{
-	    Assert(increasing ? (diff > minimumShift) : (diff < minimumShift));
-	    shift = diff;
-	    entering = basic;
-	    bounded = true;
-	  }
-	}else{
-	  if( increasing ? (diff < shift) : diff > shift){
-	    // a new min for increasing
-	    // a new max for decreasing
-
-	    if(increasing ? (diff <= minimumShift) : (diff >= minimumShift)){
-	      Assert(!progress);
-	      entering = basic;
-	      return;
-	    }else{
-	      Assert(increasing ? (diff > minimumShift) : (diff < minimumShift));
-	      shift = diff;
-	      entering = basic;
-	    }
-	  }
-	}
-      }
-    }
-  }
-  
-  if(!bounded){
-    // A totally unbounded variable
-    Assert(entering == ARITHVAR_SENTINEL);
-    progress = true;
-    return;
-  }else if(entering == ARITHVAR_SENTINEL){
-    // We have a variable that is bounded only by its maximum
-    for(Tableau::ColIterator colIter = d_tableau.colIterator(leaving);!colIter.atEnd(); ++colIter){
-      const Tableau::Entry& e = *colIter;
-    
-      ArithVar basic = d_tableau.rowIndexToBasic(e.getRowIndex());
-      if(basic == d_optRow){
-	continue;
-      } else{
-	entering = basic;
-	break;
-      }
-    }
-    Assert(entering != ARITHVAR_SENTINEL);
-    
-    Assert(increasing ? d_partialModel.hasUpperBound(leaving) : d_partialModel.hasLowerBound(leaving));
-
-    const DeltaRational& assignment = d_partialModel.getAssignment(leaving);
-    DeltaRational diff = increasing ? d_partialModel.getUpperBound(leaving) - assignment : d_partialModel.getLowerBound(leaving) - assignment;
-    
-    shift = diff;
-
-    Assert(increasing ? shift.sgn() >=0 : shift.sgn() <= 0);
-    Assert(increasing ? shift > minimumShift : shift < minimumShift);
-
-    progress = true;
-    return;
-  }else{
-    Assert(bounded);
-    progress = true;
-
-    if((increasing ? d_partialModel.hasUpperBound(leaving) : d_partialModel.hasLowerBound(leaving) )){
-      Assert(entering != ARITHVAR_SENTINEL);
-      const DeltaRational& assignment = d_partialModel.getAssignment(leaving);
-      DeltaRational diff = increasing ? d_partialModel.getUpperBound(leaving) - assignment : d_partialModel.getLowerBound(leaving) - assignment;
-      if((increasing) ? (diff < shift) : ( diff > shift)){
-	shift = diff;
-      }
-    }
-
-    Assert(increasing ? shift.sgn() >=0 : shift.sgn() <= 0);
-    Assert(increasing ? shift > minimumShift : shift < minimumShift);
-    return;
-  }
-  
-  
-	// if(! bounded ||
-	//    (increasing && diff < shift) || // a new min for increasing
-	//    (!increasing && diff > shift)){ // a new max for decreasing
-	//   bounded = true;
-	//   shift = diff;
-	//   entering = basic;
-	// }
-      // }
-
-      // if(notAtTheBound && !blandMode){
-      // 	DeltaRational diff = basicInc ?
-      // 	  (d_partialModel.getUpperBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient() :
-      // 	  (d_partialModel.getLowerBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient();
-
-      // 	if(! bounded ||
-      // 	   (increasing && diff < shift) || // a new min for increasing
-      // 	   (!increasing && diff > shift)){ // a new max for decreasing
-      // 	  bounded = true;
-      // 	  shift = diff;
-      // 	  entering = basic;
-      // 	}
-      // }else if (!notAtTheBound) { // basic is already exactly at the bound
-      // 	if(!blandMode){ // Enter into using Bland's rule
-      // 	  blandMode = true;
-      // 	  bounded = true;
-      // 	  shift = d_DELTA_ZERO;
-      // 	  entering = basic;
-      // 	}else{
-      // 	  entering = minVarOrder(*this, entering, basic); // Bland's rule.
-      // 	}
-      // }
-     // else this basic variable cannot be violated by increasing/decreasing entering
-  
-
-   
-
-  // if(!blandMode && (increasing ? d_partialModel.hasUpperBound(leaving) : d_partialModel.hasLowerBound(leaving) )){
-  //   Assert(entering != ARITHVAR_SENTINEL);
-  //   bounded = true;
-  //   DeltaRational diff = increasing ? d_partialModel.getUpperBound(leaving) - assignment : d_partialModel.getLowerBound(leaving) - assignment;
-  //   if((increasing) ? (diff < shift) : ( diff > shift)){
-  //     shift = diff;
-  //   }
-  // }
-
-  // Assert(increasing ? shift.sgn() >=0 : shift.sgn() <= 0);
-
-  // return shift;
-}
-
-
-/**
- * Given an variable on the optimization row that can be used to decrease the value of the optimization function
- * arbitrarily and an optimization function that is strictly positive in the current model,
- * driveOptToZero updates the value of unbounded s.t. the value of d_opt is exactly 0.
- */
-void SimplexDecisionProcedure::driveOptToZero(ArithVar unbounded){
-  Assert(!belowThreshold());
-
-  const Tableau::Entry& e = d_tableau.findEntry(d_tableau.basicToRowIndex(d_optRow), unbounded);
-  Assert(!e.blank());
-
-  DeltaRational theta = (d_negOptConstant-d_partialModel.getAssignment(d_optRow))/ (e.getCoefficient());
-  Assert((e.getCoefficient().sgn() > 0) ? (theta.sgn() < 0) : (theta.sgn() > 0));
-
-  DeltaRational newAssignment = d_partialModel.getAssignment(unbounded) + theta;
-  d_linEq.update(unbounded, newAssignment);
-
-  if(Debug.isOn("primal::consistent")){ Assert(d_linEq.debugEntireLinEqIsConsistent("driveOptToZero")); }
-
-  Assert(belowThreshold());
-}
diff --git a/src/theory/arith/simplex-converge.h b/src/theory/arith/simplex-converge.h
deleted file mode 100644
index dac3a9b49..000000000
--- a/src/theory/arith/simplex-converge.h
+++ /dev/null
@@ -1,531 +0,0 @@
-/*********************                                                        */
-/*! \file simplex.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 is an implementation of the Simplex Module for the Simplex for DPLL(T) decision procedure.
- **
- ** 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 heuristic 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 heuristics, 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
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__SIMPLEX_H
-#define __CVC4__THEORY__ARITH__SIMPLEX_H
-
-#include "theory/arith/arithvar.h"
-#include "theory/arith/arith_priority_queue.h"
-#include "theory/arith/delta_rational.h"
-#include "theory/arith/matrix.h"
-#include "theory/arith/partial_model.h"
-#include "theory/arith/linear_equality.h"
-
-#include "context/cdlist.h"
-
-#include "util/dense_map.h"
-#include "options/options.h"
-#include "util/stats.h"
-#include "util/result.h"
-
-#include <queue>
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class SimplexDecisionProcedure {
-private:
-  ArithVar d_conflictVariable;
-  DenseSet d_successes;
-
-  /** 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;
-
-  /** Number of variables in the system. This is used for tuning heuristics. */
-  ArithVar d_numVariables;
-
-  /** This is the call back channel for Simplex to report conflicts. */
-  NodeCallBack& d_conflictChannel;
-
-  /** Maps a variable to how many times they have been used as a pivot in the simplex search. */
-  DenseMultiset d_pivotsInRound;
-
-  /** Stores to the DeltaRational constant 0. */
-  DeltaRational d_DELTA_ZERO;
-
-  //TODO make an option
-  const static uint32_t MAX_ITERATIONS = 20;
-
-
-  /** Used for requesting d_opt, bound and error variables for primal.*/
-  ArithVarMalloc& d_arithVarMalloc;
-
-  /** Used for constructing temporary variables, bound and error variables for primal.*/
-  ConstraintDatabase& d_constraintDatabase;
-
-public:
-  SimplexDecisionProcedure(LinearEqualityModule& linEq,
-			   NodeCallBack& conflictChannel,
-			   ArithVarMalloc& variables,
-			   ConstraintDatabase& constraintDatabase);
-
-  /**
-   * 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);
-  }
-
-  /**
-   * 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.
-   *
-   * If all of the variables can be made consistent with their bounds
-   * SAT is returned. Otherwise UNSAT is returned, and at least 1 conflict
-   * was reported on the conflictCallback passed to the Module.
-   *
-   * Tableau pivoting is performed so variables may switch from being basic to
-   * nonbasic and vice versa.
-   *
-   * Corresponds to the "check()" procedure in [Cav06].
-   */
-  Result::Sat dualFindModel(bool exactResult);
-
-
-  /**
-   * Tries to update the assignments of the variables s.t. all of the assignments
-   * are consistent with their bounds.
-   *
-   * This is a REALLY heavy hammer consider calling dualFindModel(false) first.
-   *
-   * !!!!!!!!!!!!!IMPORTANT!!!!!!!!!!!!!!
-   * This procedure needs to temporarily relax contraints to contruct a satisfiable system.
-   * To do this, it is going to do a sat push.
-   */
-  Result::Sat primalFindModel();
-
-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.
-   *
-   * Both ArithVar must be non-basic in d_tableau.
-   */
-  typedef ArithVar (*PreferenceFunction)(const SimplexDecisionProcedure&, ArithVar, ArithVar);
-
-  /**
-   * minVarOrder is a PreferenceFunction for selecting the smaller of the 2 ArithVars.
-   * This PreferenceFunction is used during the VarOrder stage of
-   * findModel.
-   */
-  static ArithVar minVarOrder(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
-
-  /**
-   * minRowCount is a PreferenceFunction for selecting the variable with the smaller
-   * row count in the tableau.
-   *
-   * This is a heuristic rule and should not be used
-   * during the VarOrder stage of findModel.
-   */
-  static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
-  static ArithVar minRowLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
-
-  /**
-   * minBoundAndRowCount is a PreferenceFunction for preferring a variable
-   * without an asserted bound over variables with an asserted bound.
-   * If both have bounds or both do not have bounds,
-   * the rule falls back to minRowCount(...).
-   *
-   * This is a heuristic rule and should not be used
-   * during the VarOrder stage of findModel.
-   */
-  static ArithVar minBoundAndRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
-
-
-  /**
-   * This is the main simplex for DPLL(T) loop.
-   * It runs for at most maxIterations.
-   *
-   * Returns true iff it has found a conflict.
-   * d_conflictVariable will be set and the conflict for this row is reported.
-   */
-  bool searchForFeasibleSolution(uint32_t maxIterations);
-
-  enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch, AfterVarOrderSearch};
-
-  bool findConflictOnTheQueue(SearchPeriod period);
-
-
-  /**
-   * 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 ARITHVAR_SENTINEL if none exists.
-   *
-   * More formally one of the following conditions must be satisfied:
-   * -  lowerBound && a_ij < 0 && assignment(x_j) < upperbound(x_j)
-   * -  lowerBound && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
-   * - !lowerBound && a_ij > 0 && assignment(x_j) < upperbound(x_j)
-   * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
-   *
-   */
-  template <bool lowerBound>  ArithVar selectSlack(ArithVar x_i, PreferenceFunction pf);
-  ArithVar selectSlackLowerBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) {
-    return selectSlack<true>(x_i, pf);
-  }
-  ArithVar selectSlackUpperBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) {
-    return selectSlack<false>(x_i, pf);
-  }
-  /**
-   * 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 generateConflictAboveUpperBound(ArithVar conflictVar);
-  Node generateConflictBelowLowerBound(ArithVar conflictVar);
-
-public:
-  void increaseMax() {d_numVariables++;}
-
-
-  void clearQueue() {
-    d_queue.clear();
-  }
-
-
-  bool debugIsInCollectionQueue(ArithVar var) const{
-    Assert(d_queue.inCollectionMode());
-    return d_queue.collectionModeContains(var);
-  }
-
-  void reduceQueue(){
-    d_queue.reduce();
-  }
-
-  ArithPriorityQueue::const_iterator queueBegin() const{
-    return d_queue.begin();
-  }
-
-  ArithPriorityQueue::const_iterator queueEnd() const{
-    return d_queue.end();
-  }
-
-private:
-
-  /** Reports a conflict to on the output channel. */
-  void reportConflict(Node conflict){
-    d_conflictChannel(conflict);
-    ++(d_statistics.d_simplexConflicts);
-  }
-
-  template <bool above>
-  inline bool isAcceptableSlack(int sgn, ArithVar nonbasic){
-    return
-      ( above && sgn < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
-      ( above && sgn > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)) ||
-      (!above && sgn > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
-      (!above && sgn < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic));
-  }
-
-  /**
-   * Checks a basic variable, b, to see if it is in conflict.
-   * If a conflict is discovered a node summarizing the conflict is returned.
-   * Otherwise, Node::null() is returned.
-   */
-  Node checkBasicForConflict(ArithVar b);
-
-  Node weakenConflict(bool aboveUpper, ArithVar basicVar);
-  Constraint weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic);
-
-  /** Gets a fresh variable from TheoryArith. */
-  ArithVar requestVariable(){
-    return d_arithVarMalloc.request();
-  }
-
-  /** Releases a requested variable from TheoryArith.*/
-  void releaseVariable(ArithVar v){
-    d_arithVarMalloc.release(v);
-  }
-
-
-  /** An error info keeps the information associated with the construction of an ErrorVariable. */
-  class ErrorInfo {
-  private:
-    /** The variable for which the error variable was constructed.*/
-    ArithVar d_variable;
-
-    // If false -> lowerbound
-    bool d_upperbound;
-    
-    /** The violated constraint this was constructed to try to satisfy.*/
-    Constraint d_violated;
-    
-  public:
-    ErrorInfo(ArithVar error, bool ub, const Constraint original)
-      : d_variable(error), d_upperbound(ub), d_violated(original) {}
-
-    ErrorInfo() :
-    d_variable(ARITHVAR_SENTINEL), d_upperbound(false), d_violated(NullConstraint){}
-
-    inline ArithVar getVariable() const {
-      return d_variable;
-    }
-
-    inline bool isUpperbound() const {
-      return d_upperbound;
-    }
-
-    inline bool errorIsLeqZero(const ArithPartialModel& d_pm) const{
-      return isUpperbound() ?
-	(d_pm.getAssignment(d_variable) <= d_violated->getValue()) :
-	(d_pm.getAssignment(d_variable) >= d_violated->getValue());
-    }
-
-    inline Constraint getConstraint() const {
-      return d_violated;
-    }
-
-    inline DeltaRational getErrorAmount(const ArithPartialModel& d_pm) const {
-      return isUpperbound() ?
-	(d_pm.getAssignment(d_variable) - d_violated->getValue()) :
-	(d_violated->getValue() - d_pm.getAssignment(d_variable));
-    }
-  };
-
-  typedef DenseMap<ErrorInfo> ErrorMap;
-
-  /** A map from the error variables to the associated ErrorInfo.*/
-  ErrorMap d_currentErrorVariables;
-
-  /** The optimization function is implicitly defined as
-   * f_i  = d_optRow - d_negOptConstant
-   *
-   * d_optRow is a basic variable in the tableau.
-   * The tableau maintains that it is equal to the sum of -1^{!ub} * the error variables in
-   * d_currentErrorVariables.
-   *
-   * d_negOptConstant is explicitly the negation of the sum of the bounds that were violated
-   *
-   * assignment(f_i) <= 0 iff assignment(d_optRow) <= d_negOptConstant
-   */
-  /** The variable for the variable part of the optimization function.*/
-  ArithVar d_optRow; 
-
-  /** The constant part of the optimization function.*/
-  DeltaRational d_negOptConstant;
-
-  inline bool belowThreshold() const {
-    return d_partialModel.getAssignment(d_optRow) <= d_negOptConstant;
-  }
-
-  /**
-   * A PrimalResponse represents the state that the primal simplex solver is in.
-   */
-  enum PrimalResponse {
-    // The optimization can decrease arbitrarily on some variable in the function
-    FoundUnboundedVariable,
-
-    // The optimization function has reached a threshold value and is checking back in
-    ReachedThresholdValue,
-
-    // Simplex has used up its pivot bound and is checking back in with its caller
-    UsedMaxPivots,
-
-    //Simplex can make progress on the pair of entering and leaving variables
-    MakeProgressOnLeaving,
-
-    //Simplex is not at a minimum but no leaving variable can be changed to help
-    NoProgressOnLeaving,
-
-    // Simplex has reached a minimum for its optimization function
-    GlobalMinimum
-  };
-
-  /**
-   * These fields are for sticking information for passing information back with the PrimalRespones.
-   * These fields should be ignored as unsafe/unknown unless you have a PrimalResponse that states
-   * the field makes sense.
-   */
-  struct PrimalPassBack {
-  public:
-    /**
-     * A variable s.t. its value can be increased/decreased arbitrarily to change the optimization function
-     * arbitrarily low.
-     */
-    ArithVar d_unbounded;
-    
-    /** The leaving variable selection for primal simplex. */
-    ArithVar d_leaving;
-
-    /** The entering variable selection for primal simplex. */
-    ArithVar d_entering;
-
-    /** The new value for the leaving variable value for primal simplex.*/
-    DeltaRational d_nextEnteringValue;
-
-    PrimalPassBack() { clear(); }
-    void clear(){
-      d_unbounded = (d_leaving = (d_entering = ARITHVAR_SENTINEL));
-      d_nextEnteringValue = DeltaRational();
-    }
-
-    bool isClear() const {
-      return d_unbounded == ARITHVAR_SENTINEL &&
-	d_leaving == ARITHVAR_SENTINEL &&
-	d_entering == ARITHVAR_SENTINEL &&
-	d_nextEnteringValue.sgn() == 0;
-    }
-  } d_primalCarry;
-
-  uint32_t d_pivotsSinceErrorProgress;
-  uint32_t d_pivotsSinceOptProgress;
-  uint32_t d_pivotsSinceLastCheck;
-
-  typedef std::vector< const Tableau::Entry* > EntryVector;
-  EntryVector d_improvementCandidates;
-
-  PrimalResponse primal(uint32_t maxIterations);
-  PrimalResponse primalCheck();
-  Result::Sat primalConverge(int depth);
-  void driveOptToZero(ArithVar unbounded);
-  uint32_t contractErrorVariables(bool guaranteedSuccess);
-  bool checkForRowConflicts();
-  void restoreErrorVariables(ErrorMap& es);
-  void constructErrorVariables();
-  void constructOptimizationFunction();
-  void removeOptimizationFunction();
-  void reconstructOptimizationFunction();
-  ArithVar selectMinimumValid(ArithVar v, bool increasing);
-  ArithVar selectFirstValid(ArithVar v, bool increasing);
-
-  void reassertErrorConstraint(ArithVar e, ErrorMap& es, bool definitelyTrue, bool definitelyFalse);
-  void computeShift(ArithVar leaving, bool increasing, bool& progress, ArithVar& entering, DeltaRational& shift, const DeltaRational& minimumShift);
-
-  /** These fields are designed to be accessible to TheoryArith methods. */
-  class Statistics {
-  public:
-    IntStat d_statUpdateConflicts;
-
-    TimerStat d_findConflictOnTheQueueTime;
-
-    IntStat d_attemptBeforeDiffSearch, d_successBeforeDiffSearch;
-    IntStat d_attemptAfterDiffSearch, d_successAfterDiffSearch;
-    IntStat d_attemptDuringDiffSearch, d_successDuringDiffSearch;
-    IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch;
-    IntStat d_attemptAfterVarOrderSearch, d_successAfterVarOrderSearch;
-
-    IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings;
-    TimerStat d_weakenTime;
-
-
-    IntStat d_simplexConflicts;
-
-    // Primal stuffs
-    TimerStat d_primalTimer;
-    TimerStat d_internalTimer;
-
-    IntStat d_primalCalls;
-    IntStat d_primalSatCalls;
-    IntStat d_primalUnsatCalls;
-
-    IntStat d_primalPivots;
-    IntStat d_primalImprovingPivots;
-
-    IntStat d_primalThresholdReachedPivot;
-    IntStat d_primalThresholdReachedPivot_dropped;
-    
-    IntStat d_primalReachedMaxPivots;
-    IntStat d_primalReachedMaxPivots_contractMadeProgress;
-    IntStat d_primalReachedMaxPivots_checkForConflictWorked;
-
-    
-    IntStat d_primalGlobalMinimum;
-    IntStat d_primalGlobalMinimum_rowConflictWorked;
-    IntStat d_primalGlobalMinimum_firstHalfWasSat;
-    IntStat d_primalGlobalMinimum_firstHalfWasUnsat;
-    IntStat d_primalGlobalMinimum_contractMadeProgress;
-
-
-    IntStat d_unboundedFound;
-    IntStat d_unboundedFound_drive;
-    IntStat d_unboundedFound_dropped;
-
-
-    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/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index d0595321c..6095727a3 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -286,7 +286,6 @@ UpdateInfo SumOfInfeasibilitiesSPD::selectUpdate(LinearEqualityModule::UpdatePre
     ArithVar curr = cand.d_nb;
     const Rational& coeff = *cand.d_coeff;
 
-#warning "Who is using computeSafeUpdate?"
     LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc = selectLeavingFunction(curr);
     UpdateInfo currProposal = d_linEq.speculativeUpdate(curr, coeff, leavingPrefFunc);
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 7eae2606c..e4b19a683 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -96,7 +96,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_currentPropagationList(),
   d_learnedBounds(c),
   d_partialModel(c, DeltaComputeCallback(*this)),
-  d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(&d_rowTracking, &d_tableau)),
+  d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)),
   d_tableau(),
   d_linEq(d_partialModel, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)),
   d_diosolver(c),
@@ -107,7 +107,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_conflicts(c),
   d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseConflict(*this)),
   d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
-  d_pureUpdate(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
   d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
   d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
   d_DELTA_ZERO(0),
@@ -2882,6 +2881,11 @@ void TheoryArithPrivate::dumpUpdatedBoundsToRows(){
   d_updatedBounds.purge();
 }
 
+const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
+  return d_rowTracking[ridx];
+}
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index e522bb8c8..b97ab3468 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -58,7 +58,6 @@
 #include "theory/arith/dual_simplex.h"
 #include "theory/arith/fc_simplex.h"
 #include "theory/arith/soi_simplex.h"
-#include "theory/arith/pure_update_simplex.h"
 
 #include "theory/arith/constraint.h"
 
@@ -316,7 +315,6 @@ private:
 
   /** This implements the Simplex decision procedure. */
   DualSimplexDecisionProcedure d_dualSimplex;
-  PureUpdateSimplexDecisionProcedure d_pureUpdate;
   FCSimplexDecisionProcedure d_fcSimplex;
   SumOfInfeasibilitiesSPD d_soiSimplex;
 
@@ -430,6 +428,10 @@ public:
    */
   ArithVar requestArithVar(TNode x, bool slack);
 
+public:
+  const BoundsInfo& boundsInfo(ArithVar basic) const;
+
+
 private:
   /** Initial (not context dependent) sets up for a variable.*/
   void setupBasicValue(ArithVar x);