From: Tim King <taking@cs.nyu.edu>
Date: Fri, 3 May 2013 19:52:11 +0000 (-0400)
Subject: More misc. arithmetic cleanup. Removing unused files and functions. Also removing... 
X-Git-Tag: cvc5-1.0.0~7287^2~158
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4c20ab57d70c4812d75af037e95c371c65418333;p=cvc5.git

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.
---

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);