diff options
Diffstat (limited to 'src/theory/arith/simplex.h')
-rw-r--r-- | src/theory/arith/simplex.h | 15 |
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. |