Adding a smarter technique for pivoting in solutions for glpk.

9 files changed, 354 insertions, 78 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index ed14e972b..620b8a121 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -51,6 +51,8 @@ libarith_la_SOURCES = \
 	soi_simplex.cpp \
 	approx_simplex.h \
 	approx_simplex.cpp \
+	attempt_solution_simplex.h \
+	attempt_solution_simplex.cpp \
 	theory_arith.h \
 	theory_arith.cpp \
 	theory_arith_private_forward.h \
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 5777337ee..55e52fc53 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -132,6 +132,8 @@ private:
   bool d_solvedRelaxation;
   bool d_solvedMIP;
 
+  static int s_verbosity;
+
 public:
   ApproxGLPK(const ArithVariables& vars);
   ~ApproxGLPK();
@@ -152,6 +154,9 @@ private:
   Solution extractSolution(bool mip) const;
 };
 
+#warning "set back to 0"
+int ApproxGLPK::s_verbosity = 1;
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
@@ -221,8 +226,10 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& avars) :
   for(ArithVariables::var_iterator vi = d_vars.var_begin(), vi_end = d_vars.var_end(); vi != vi_end; ++vi){
     ArithVar v = *vi;
 
-    //cout << v  << " ";
-    //d_vars.printModel(v, cout);
+    if(s_verbosity >= 2){
+      Message() << v  << " ";
+      d_vars.printModel(v, Message());
+    }
 
     int type;
     double lb = 0.0;
@@ -407,77 +414,90 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const{
     int glpk_index = isSlack ? d_rowIndices[vi] : d_colIndices[vi];
 
     int status = isSlack ? glp_get_row_stat(d_prob, glpk_index) : glp_get_col_stat(d_prob, glpk_index);
-    //cout << "assignment " << vi << endl;
+    if(s_verbosity >= 2){
+      Message() << "assignment " << vi << endl;
+    }
+
+    bool useDefaultAssignment = false;
 
     switch(status){
     case GLP_BS:
       //cout << "basic" << endl;
       newBasis.add(vi);
+      useDefaultAssignment = true;
       break;
     case GLP_NL:
     case GLP_NS:
       if(!mip){
-        //cout << "non-basic lb" << endl;
+        if(s_verbosity >= 2){ Message() << "non-basic lb" << endl; }
         newValues.set(vi, d_vars.getLowerBound(vi));
-        break;
-      }// intentionally fall through otherwise
+      }else{// intentionally fall through otherwise
+        useDefaultAssignment = true;
+      }
+      break;
     case GLP_NU:
       if(!mip){
-        // cout << "non-basic ub" << endl;
+        if(s_verbosity >= 2){ Message() << "non-basic ub" << endl; }
         newValues.set(vi, d_vars.getUpperBound(vi));
-        break;
-      }// intentionally fall through otherwise
+      }else {// intentionally fall through otherwise
+        useDefaultAssignment = true;
+      }
+      break;
     default:
       {
-        // cout << "non-basic other" << endl;
+        useDefaultAssignment = true;
+      }
+      break;
+    }
+
+    if(useDefaultAssignment){
+      if(s_verbosity >= 2){ Message() << "non-basic other" << endl; }
 
-        double newAssign =
-          mip ?
-            (isSlack ? glp_mip_row_val(d_prob, glpk_index) :  glp_mip_col_val(d_prob, glpk_index))
-          : (isSlack ? glp_get_row_prim(d_prob, glpk_index) :  glp_get_col_prim(d_prob, glpk_index));
-        const DeltaRational& oldAssign = d_vars.getAssignment(vi);
+      double newAssign =
+        mip ?
+        (isSlack ? glp_mip_row_val(d_prob, glpk_index) :  glp_mip_col_val(d_prob, glpk_index))
+        : (isSlack ? glp_get_row_prim(d_prob, glpk_index) :  glp_get_col_prim(d_prob, glpk_index));
+      const DeltaRational& oldAssign = d_vars.getAssignment(vi);
 
 
-        if(d_vars.hasLowerBound(vi) &&
-           roughlyEqual(newAssign, d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA))){
-          //cout << "  to lb" << endl;
+      if(d_vars.hasLowerBound(vi) &&
+         roughlyEqual(newAssign, d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA))){
+        //cout << "  to lb" << endl;
 
-          newValues.set(vi, d_vars.getLowerBound(vi));
-        }else if(d_vars.hasUpperBound(vi) &&
-           roughlyEqual(newAssign, d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA))){
-          newValues.set(vi, d_vars.getUpperBound(vi));
-          // cout << "  to ub" << endl;
+        newValues.set(vi, d_vars.getLowerBound(vi));
+      }else if(d_vars.hasUpperBound(vi) &&
+               roughlyEqual(newAssign, d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA))){
+        newValues.set(vi, d_vars.getUpperBound(vi));
+        // cout << "  to ub" << endl;
+      }else{
+
+        double rounded = round(newAssign);
+        if(roughlyEqual(newAssign, rounded)){
+          // cout << "roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
+          newAssign = rounded;
         }else{
+          // cout << "not roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
+        }
+
+        DeltaRational proposal = estimateWithCFE(newAssign);
+
 
-          double rounded = round(newAssign);
-          if(roughlyEqual(newAssign, rounded)){
-            // cout << "roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
-            newAssign = rounded;
-          }else{
-            // cout << "not roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
-          }
-
-          DeltaRational proposal = estimateWithCFE(newAssign);
-
-
-          if(roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))){
-            // cout << "  to prev value" << newAssign << " " << oldAssign << endl;
-            proposal = d_vars.getAssignment(vi);
-          }
-
-
-          if(d_vars.strictlyLessThanLowerBound(vi, proposal)){
-            //cout << "  round to lb " << d_vars.getLowerBound(vi) << endl;
-            proposal = d_vars.getLowerBound(vi);
-          }else if(d_vars.strictlyGreaterThanUpperBound(vi, proposal)){
-            //cout << "  round to ub " << d_vars.getUpperBound(vi) << endl;
-            proposal = d_vars.getUpperBound(vi);
-          }else{
-            //cout << "  use proposal" << proposal << " " << oldAssign  << endl;
-          }
-          newValues.set(vi, proposal);
+        if(roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))){
+          // cout << "  to prev value" << newAssign << " " << oldAssign << endl;
+          proposal = d_vars.getAssignment(vi);
         }
-        break;
+
+
+        if(d_vars.strictlyLessThanLowerBound(vi, proposal)){
+          //cout << "  round to lb " << d_vars.getLowerBound(vi) << endl;
+          proposal = d_vars.getLowerBound(vi);
+        }else if(d_vars.strictlyGreaterThanUpperBound(vi, proposal)){
+          //cout << "  round to ub " << d_vars.getUpperBound(vi) << endl;
+          proposal = d_vars.getUpperBound(vi);
+        }else{
+          //cout << "  use proposal" << proposal << " " << oldAssign  << endl;
+        }
+        newValues.set(vi, proposal);
       }
     }
   }
@@ -493,8 +513,10 @@ ApproximateSimplex::ApproxResult ApproxGLPK::solveRelaxation(){
   parm.meth = GLP_PRIMAL;
   parm.pricing = GLP_PT_PSE;
   parm.it_lim = d_pivotLimit;
-  //parm.msg_lev = GLP_MSG_ALL;
   parm.msg_lev = GLP_MSG_OFF;
+  if(s_verbosity >= 1){
+    parm.msg_lev = GLP_MSG_ALL;
+  }
 
   int res = glp_simplex(d_prob, &parm);
   switch(res){
@@ -551,8 +573,10 @@ ApproximateSimplex::ApproxResult ApproxGLPK::solveMIP(){
   parm.cov_cuts = GLP_ON;
   parm.cb_func = stopAtBingoOrPivotLimit;
   parm.cb_info = &d_pivotLimit;
-  //parm.msg_lev = GLP_MSG_ALL;
   parm.msg_lev = GLP_MSG_OFF;
+  if(s_verbosity >= 1){
+    parm.msg_lev = GLP_MSG_ALL;
+  }
   int res = glp_intopt(d_prob, &parm);
 
   switch(res){
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index a2f3cde24..d4680939d 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -50,11 +50,6 @@ public:
   virtual ApproxResult solveMIP() = 0;
   virtual Solution extractMIP() const = 0;
 
-  static void applySolution(LinearEqualityModule& linEq, const Solution& sol){
-    linEq.forceNewBasis(sol.newBasis);
-    linEq.updateMany(sol.newValues);
-  }
-
   /** UTILIES FOR DEALING WITH ESTIMATES */
 
   static const double SMALL_FIXED_DELTA;
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
new file mode 100644
index 000000000..c8d5b6f68
--- /dev/null
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -0,0 +1,131 @@
+
+#include "theory/arith/attempt_solution_simplex.h"
+#include "theory/arith/options.h"
+#include "theory/arith/constraint.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+AttemptSolutionSDP::AttemptSolutionSDP(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
+  : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
+  , d_statistics()
+{ }
+
+AttemptSolutionSDP::Statistics::Statistics():
+  d_searchTime("theory::arith::attempt::searchTime"),
+  d_queueTime("theory::arith::attempt::queueTime"),
+  d_conflicts("theory::arith::attempt::conflicts", 0)
+{
+  StatisticsRegistry::registerStat(&d_searchTime);
+  StatisticsRegistry::registerStat(&d_queueTime);
+  StatisticsRegistry::registerStat(&d_conflicts);
+}
+
+AttemptSolutionSDP::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_searchTime);
+  StatisticsRegistry::unregisterStat(&d_queueTime);
+  StatisticsRegistry::unregisterStat(&d_conflicts);
+}
+
+bool AttemptSolutionSDP::matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const{
+  return nv[v] == d_variables.getAssignment(v);
+}
+
+Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol){
+  const DenseSet& newBasis = sol.newBasis;
+  const DenseMap<DeltaRational>& newValues = sol.newValues;
+
+  DenseSet needsToBeAdded;
+  for(DenseSet::const_iterator i = newBasis.begin(), i_end = newBasis.end(); i != i_end; ++i){
+    ArithVar b = *i;
+    if(!d_tableau.isBasic(b)){
+      needsToBeAdded.add(b);
+    }
+  }
+  DenseMap<DeltaRational>::const_iterator nvi = newValues.begin(), nvi_end = newValues.end();
+  for(; nvi != nvi_end; ++nvi){
+    ArithVar currentlyNb = *nvi;
+    if(!d_tableau.isBasic(currentlyNb)){
+      if(!matchesNewValue(newValues, currentlyNb)){
+        const DeltaRational& newValue = newValues[currentlyNb];
+        Trace("arith::updateMany")
+          << "updateMany:" << currentlyNb << " "
+          << d_variables.getAssignment(currentlyNb) << " to "<< newValue << endl;
+        d_linEq.update(currentlyNb, newValue);
+        Assert(d_variables.assignmentIsConsistent(currentlyNb));
+      }
+    }
+  }
+  d_errorSet.reduceToSignals();
+  d_errorSet.setSelectionRule(VAR_ORDER);
+
+  static int instance = 0;
+  ++instance;
+
+  if(processSignals()){
+    Debug("arith::findModel") << "attemptSolution("<< instance <<") early conflict" << endl;
+    return Result::UNSAT;
+  }else if(d_errorSet.errorEmpty()){
+    Debug("arith::findModel") << "attemptSolution("<< instance <<") fixed itself" << endl;
+    return Result::SAT;
+  }
+
+  while(!needsToBeAdded.empty() && !d_errorSet.errorEmpty()){
+    ArithVar toRemove = ARITHVAR_SENTINEL;
+    ArithVar toAdd = ARITHVAR_SENTINEL;
+    DenseSet::const_iterator i = needsToBeAdded.begin(), i_end = needsToBeAdded.end();
+    for(; toAdd == ARITHVAR_SENTINEL && i != i_end; ++i){
+      ArithVar v = *i;
+
+      Tableau::ColIterator colIter = d_tableau.colIterator(v);
+      for(; !colIter.atEnd(); ++colIter){
+        const Tableau::Entry& entry = *colIter;
+        Assert(entry.getColVar() == v);
+        ArithVar b = d_tableau.rowIndexToBasic(entry.getRowIndex());
+        if(!newBasis.isMember(b)){
+          toAdd = v;
+
+          bool favorBOverToRemove =
+            (toRemove == ARITHVAR_SENTINEL) ||
+            (matchesNewValue(newValues, toRemove) && !matchesNewValue(newValues, b)) ||
+            (d_tableau.basicRowLength(toRemove) > d_tableau.basicRowLength(b));
+
+          if(favorBOverToRemove){
+            toRemove = b;
+          }
+        }
+      }
+    }
+    Assert(toRemove != ARITHVAR_SENTINEL);
+    Assert(toAdd != ARITHVAR_SENTINEL);
+
+    Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
+    Message() << toRemove << " " << toAdd << endl;
+
+    d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]);
+
+    Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
+    Message() << needsToBeAdded.size() << "to go" << endl;
+    needsToBeAdded.remove(toAdd);
+
+    bool conflict = processSignals();
+    if(conflict){
+      d_errorSet.reduceToSignals();
+      return Result::UNSAT;
+    }
+  }
+
+  if(d_errorSet.errorEmpty()){
+    return Result::SAT;
+  }else{
+    d_errorSet.reduceToSignals();
+    return Result::SAT_UNKNOWN;
+  }
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h
new file mode 100644
index 000000000..5bcdc6aab
--- /dev/null
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \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 "util/statistics_registry.h"
+#include "theory/arith/simplex.h"
+#include "theory/arith/approx_simplex.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class AttemptSolutionSDP : public SimplexDecisionProcedure {
+public:
+  AttemptSolutionSDP(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
+
+  Result::Sat attempt(const ApproximateSimplex::Solution& sol);
+
+  Result::Sat findModel(bool exactResult){
+    Unreachable();
+  }
+
+private:
+  bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const;
+
+  bool processSignals(){
+    TimerStat &timer = d_statistics.d_queueTime;
+    IntStat& conflictStat  = d_statistics.d_conflicts;
+    return standardProcessSignals(timer, conflictStat);
+  }
+  /** These fields are designed to be accessible to TheoryArith methods. */
+  class Statistics {
+  public:
+    TimerStat d_searchTime;
+    TimerStat d_queueTime;
+    IntStat d_conflicts;
+
+    Statistics();
+    ~Statistics();
+  } d_statistics;
+};/* class AttemptSolutionSDP */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 1c32f80e4..5817a3629 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -68,7 +68,8 @@ LinearEqualityModule::Statistics::Statistics():
   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_weakenTime("theory::arith::weakening::time"),
+  d_forceTime("theory::arith::forcing::time")
 {
   StatisticsRegistry::registerStat(&d_statPivots);
   StatisticsRegistry::registerStat(&d_statUpdates);
@@ -80,6 +81,7 @@ LinearEqualityModule::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_weakeningSuccesses);
   StatisticsRegistry::registerStat(&d_weakenings);
   StatisticsRegistry::registerStat(&d_weakenTime);
+  StatisticsRegistry::registerStat(&d_forceTime);
 }
 
 LinearEqualityModule::Statistics::~Statistics(){
@@ -93,7 +95,9 @@ LinearEqualityModule::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_weakeningSuccesses);
   StatisticsRegistry::unregisterStat(&d_weakenings);
   StatisticsRegistry::unregisterStat(&d_weakenTime);
+  StatisticsRegistry::unregisterStat(&d_forceTime);
 }
+
 void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){
   Assert(!d_areTracking);
 
@@ -117,19 +121,30 @@ void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev
 void LinearEqualityModule::updateMany(const DenseMap<DeltaRational>& many){
   for(DenseMap<DeltaRational>::const_iterator i = many.begin(), i_end = many.end(); i != i_end; ++i){
     ArithVar nb = *i;
-    Assert(!d_tableau.isBasic(nb));
-    const DeltaRational& newValue = many[nb];
-    if(newValue != d_variables.getAssignment(nb)){
-      Trace("arith::updateMany")
-        << "updateMany:" << nb << " "
-        << d_variables.getAssignment(nb) << " to "<< newValue << endl;
-      update(nb, newValue);
+    if(!d_tableau.isBasic(nb)){
+      Assert(!d_tableau.isBasic(nb));
+      const DeltaRational& newValue = many[nb];
+      if(newValue != d_variables.getAssignment(nb)){
+        Trace("arith::updateMany")
+          << "updateMany:" << nb << " "
+          << d_variables.getAssignment(nb) << " to "<< newValue << endl;
+        update(nb, newValue);
+      }
     }
   }
 }
 
 
+
+
+void LinearEqualityModule::applySolution(const DenseSet& newBasis, const DenseMap<DeltaRational>& newValues){
+  forceNewBasis(newBasis);
+  updateMany(newValues);
+}
+
 void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){
+  TimerStat::CodeTimer codeTimer(d_statistics.d_forceTime);
+  cout << "force begin" << endl;
   DenseSet needsToBeAdded;
   for(DenseSet::const_iterator i = newBasis.begin(), i_end = newBasis.end(); i != i_end; ++i){
     ArithVar b = *i;
@@ -163,10 +178,12 @@ void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){
     Assert(toAdd != ARITHVAR_SENTINEL);
 
     Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
+    Message() << toRemove << " " << toAdd << endl;
     d_tableau.pivot(toRemove, toAdd, d_trackCallback);
     d_basicVariableUpdates(toAdd);
 
     Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
+    Message() << needsToBeAdded.size() << "to go" << endl;
     needsToBeAdded.remove(toAdd);
   }
 }
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 607ee6244..293a0ddad 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -243,11 +243,6 @@ public:
   /** Specialization of update if the module is not tracking yet (for Simplex). */
   void updateTracked(ArithVar x_i, const DeltaRational& v);
 
-  /**
-   * Updates every non-basic to reflect the assignment in many.
-   * For use with ApproximateSimplex.
-   */
-  void updateMany(const DenseMap<DeltaRational>& many);
 
   /**
    * Updates the value of a basic variable x_i to v,
@@ -259,7 +254,14 @@ public:
   ArithVariables& getVariables() const{ return d_variables; }
   Tableau& getTableau() const{ return d_tableau; }
 
+  /**
+   * Updates every non-basic to reflect the assignment in many.
+   * For use with ApproximateSimplex.
+   */
+  void updateMany(const DenseMap<DeltaRational>& many);
   void forceNewBasis(const DenseSet& newBasis);
+  void applySolution(const DenseSet& newBasis, const DenseMap<DeltaRational>& newValues);
+
 
   /**
    * Returns a pointer to the first Tableau entry on the row ridx that does not
@@ -689,6 +691,7 @@ private:
 
     IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings;
     TimerStat d_weakenTime;
+    TimerStat d_forceTime;
 
     Statistics();
     ~Statistics();
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index e4b19a683..504727c0b 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -109,6 +109,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_dualSimplex(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_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
   d_DELTA_ZERO(0),
   d_fullCheckCounter(0),
   d_cutCount(c, 0),
@@ -1590,27 +1591,30 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
           approxSolver->setPivotLimit(mipLimit);
           mipRes = approxSolver->solveMIP();
           d_errorSet.reduceToSignals();
+          Message() << "here" << endl;
           if(mipRes == ApproximateSimplex::ApproxSat){
             mipSolution = approxSolver->extractMIP();
-            ApproximateSimplex::applySolution(d_linEq, mipSolution);
+            d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution);
+            //d_linEq.applySolution(mipSolution.newBasis, mipSolution.newValues);
           }else{
-            ApproximateSimplex::applySolution(d_linEq, relaxSolution);
+            d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
+            //d_linEq.applySolution(relaxSolution.newBasis, relaxSolution.newValues);
             // if(d_qflraStatus != UNSAT){
             //   d_likelyIntegerUnsat = true;
             // }
           }
           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
-          d_qflraStatus = simplex.findModel(false);
+          if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); }
         }
         break;
       case ApproximateSimplex::ApproxUnsat:
         {
           ApproximateSimplex::Solution sol = approxSolver->extractRelaxation();
-          d_errorSet.reduceToSignals();
-          ApproximateSimplex::applySolution(d_linEq, sol);
-          options::arithStandardCheckVarOrderPivots.set(100);
 
-          d_qflraStatus = simplex.findModel(false);
+          d_qflraStatus = d_attemptSolSimplex.attempt(sol);
+          options::arithStandardCheckVarOrderPivots.set(pass2Limit);
+
+          if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); }
         }
         break;
       default:
@@ -1620,6 +1624,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
     }
 
     if(d_qflraStatus == Result::SAT_UNKNOWN){
+      Message() << "got sat unknown" << endl;
       vector<ArithVar> toCut = cutAllBounded();
       if(toCut.size() > 0){
         branchVector(toCut);
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index b97ab3468..f6fb42a9c 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -58,6 +58,7 @@
 #include "theory/arith/dual_simplex.h"
 #include "theory/arith/fc_simplex.h"
 #include "theory/arith/soi_simplex.h"
+#include "theory/arith/attempt_solution_simplex.h"
 
 #include "theory/arith/constraint.h"
 
@@ -317,6 +318,7 @@ private:
   DualSimplexDecisionProcedure d_dualSimplex;
   FCSimplexDecisionProcedure d_fcSimplex;
   SumOfInfeasibilitiesSPD d_soiSimplex;
+  AttemptSolutionSDP d_attemptSolSimplex;
 
   bool solveRealRelaxation(Theory::Effort effortLevel);