diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-05 17:33:01 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-05 17:33:01 +0000 |
commit | 56edc6f7b4f9982ea5cbeec850e346ff7e4a8f00 (patch) | |
tree | 95a5028ab0cafa69cd4330b1bf58139f99d81237 /src/theory/arith/simplex.h | |
parent | 042ee6a15455d3f4193d55cbb2d3d18da3e34776 (diff) |
- Adds "PreferenceFunction" to SimplexDecisionProcedure. A PreferenceFunction allows for specifying how to choose between two nonbasic variables for which should become basic during the selectSlack(...) function. This partially addresses a point brought up by Dejan during the Code Review. (Unfortunately, function pointers are involved in the implementation. Because of this, I have had Morgan review this code before check-in.)
Diffstat (limited to 'src/theory/arith/simplex.h')
-rw-r--r-- | src/theory/arith/simplex.h | 60 |
1 files changed, 47 insertions, 13 deletions
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index b847259a0..544f49a06 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -25,7 +25,6 @@ namespace arith { class SimplexDecisionProcedure { private: - /** Stores system wide constants to avoid unnessecary reconstruction. */ const ArithConstants& d_constants; @@ -62,7 +61,6 @@ public: public: - /** * Assert*(n, orig) takes an bound n that is implied by orig. * and asserts that as a new bound if it is tighter than the current bound @@ -96,6 +94,42 @@ private: */ void pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v); +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 + * updateInconsistentVars. + */ + 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 hueristic rule and should not be used + * during the VarOrder stage of updateInconsistentVars. + */ + static ArithVar minRowCount(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 hueristic rule and should not be used + * during the VarOrder stage of updateInconsistentVars. + */ + static ArithVar minBoundAndRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); + public: /** * Tries to update the assignments of variables such that all of the @@ -114,34 +148,32 @@ public: */ Node updateInconsistentVars(); private: - template <bool limitIterations> Node searchForFeasibleSolution(uint32_t maxIterations); + template <PreferenceFunction> Node searchForFeasibleSolution(uint32_t maxIterations); enum SearchPeriod {BeforeDiffSearch, AfterDiffSearch, DuringVarOrderSearch}; Node findConflictOnTheQueue(SearchPeriod period); -private: + /** * 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 TNode::null() if none exists. - * - * If first is true, return the first ArithVar in the row to satisfy these conditions. - * If first is false, return the ArithVar with the smallest row count. + * This returns ARITHVAR_SENTINEL if none exists. * * More formally one of the following conditions must be satisfied: * - above && a_ij < 0 && assignment(x_j) < upperbound(x_j) * - above && a_ij > 0 && assignment(x_j) > lowerbound(x_j) * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j) * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j) + * */ - template <bool above> ArithVar selectSlack(ArithVar x_i, bool first); - ArithVar selectSlackBelow(ArithVar x_i, bool first) { - return selectSlack<false>(x_i, first); + template <bool above, PreferenceFunction> ArithVar selectSlack(ArithVar x_i); + template <PreferenceFunction pf> ArithVar selectSlackBelow(ArithVar x_i) { + return selectSlack<false, pf>(x_i); } - ArithVar selectSlackAbove(ArithVar x_i, bool first) { - return selectSlack<true>(x_i, first); + template <PreferenceFunction pf> ArithVar selectSlackAbove(ArithVar x_i) { + return selectSlack<true, pf>(x_i); } /** * Returns the smallest basic variable whose assignment is not consistent @@ -174,6 +206,8 @@ public: } } + +public: /** * Checks to make sure the assignment is consistent with the tableau. * This code is for debugging. |