Merged the branch sparse-tableau into trunk.

1 files changed, 13 insertions, 2 deletions

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 93574b3da..91f0bccfc 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -107,7 +107,7 @@ private:
    * This is a hueristic rule and should not be used
    * during the VarOrder stage of updateInconsistentVars.
    */
-  static ArithVar minRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
+  static ArithVar minColLength(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.
@@ -201,7 +201,9 @@ public:
    * Checks to make sure the assignment is consistent with the tableau.
    * This code is for debugging.
    */
-  void checkTableau();
+  void debugCheckTableau();
+  void debugPivotSimplex(ArithVar x_i, ArithVar x_j);
+
 
   /**
    * Computes the value of a basic variable using the assignments
@@ -240,6 +242,15 @@ private:
     pushLemma(negatedConflict);
   }
 
+  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.