From: Tim King Date: Sat, 5 Mar 2011 17:33:01 +0000 (+0000) Subject: - Adds "PreferenceFunction" to SimplexDecisionProcedure. A PreferenceFunction allows... X-Git-Tag: cvc5-1.0.0~8669 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=56edc6f7b4f9982ea5cbeec850e346ff7e4a8f00;p=cvc5.git - 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.) --- diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 68ab429ca..956a83563 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -327,14 +327,49 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR } } -template -ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, bool first){ +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::minRowCount(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_tableau.getRowCount(x) > simp.d_tableau.getRowCount(y)){ + return 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 minRowCount(simp, x, y); + } +} + +template +ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ ReducedRowVector& row_i = d_tableau.lookup(x_i); ArithVar slack = ARITHVAR_SENTINEL; - uint32_t numRows = std::numeric_limits::max(); - - bool pivotStage = !first; for(ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end(); nbi != end; ++nbi){ @@ -342,47 +377,15 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, bool first){ if(nonbasic == x_i) continue; const Rational& a_ij = (*nbi).getCoefficient(); - int cmp = a_ij.cmp(d_constants.d_ZERO); - if(above){ // beta(x_i) > u_i - if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ - if(pivotStage){ - if(d_tableau.getRowCount(nonbasic) < numRows){ - slack = nonbasic; - numRows = d_tableau.getRowCount(nonbasic); - } - }else{ - slack = nonbasic; break; - } - }else if( cmp > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ - if(pivotStage){ - if(d_tableau.getRowCount(nonbasic) < numRows){ - slack = nonbasic; - numRows = d_tableau.getRowCount(nonbasic); - } - }else{ - slack = nonbasic; break; - } - } - }else{ //beta(x_i) < l_i - if(cmp > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ - if(pivotStage){ - if(d_tableau.getRowCount(nonbasic) < numRows){ - slack = nonbasic; - numRows = d_tableau.getRowCount(nonbasic); - } - }else{ - slack = nonbasic; break; - } - }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ - if(pivotStage){ - if(d_tableau.getRowCount(nonbasic) < numRows){ - slack = nonbasic; - numRows = d_tableau.getRowCount(nonbasic); - } - }else{ - slack = nonbasic; break; - } - } + int sgn = a_ij.sgn(); + if(( 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))) { + //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); } } @@ -437,8 +440,9 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ return Node::null(); } static unsigned int instance = 0; - ++instance; + + static const uint32_t CHECK_PERIOD = 100; Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() " << instance << endl; @@ -449,14 +453,22 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ possibleConflict = findConflictOnTheQueue(BeforeDiffSearch); } if(possibleConflict.isNull()){ - possibleConflict = searchForFeasibleSolution(d_numVariables + 1); + possibleConflict = searchForFeasibleSolution(d_numVariables + 1); } if(d_queue.size() > 1 && possibleConflict.isNull()){ possibleConflict = findConflictOnTheQueue(AfterDiffSearch); } if(!d_queue.empty() && possibleConflict.isNull()){ d_queue.transitionToVariableOrderMode(); - possibleConflict = searchForFeasibleSolution(0); + + while(!d_queue.empty() && possibleConflict.isNull()){ + possibleConflict = searchForFeasibleSolution(CHECK_PERIOD); + + //Once every CHECK_PERIOD examine the entire queue for conflicts + if(possibleConflict.isNull()){ + possibleConflict = findConflictOnTheQueue(DuringVarOrderSearch); + } + } } Assert(!possibleConflict.isNull() || d_queue.empty()); @@ -483,12 +495,12 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ const DeltaRational& beta = d_partialModel.getAssignment(basic); if(d_partialModel.belowLowerBound(basic, beta, true)){ - ArithVar x_j = selectSlackBelow(basic, true); + ArithVar x_j = selectSlackBelow(basic); if(x_j == ARITHVAR_SENTINEL ){ return generateConflictBelow(basic); } }else if(d_partialModel.aboveUpperBound(basic, beta, true)){ - ArithVar x_j = selectSlackAbove(basic, true); + ArithVar x_j = selectSlackAbove(basic); if(x_j == ARITHVAR_SENTINEL ){ return generateConflictAbove(basic); } @@ -497,13 +509,12 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ } //corresponds to Check() in dM06 -template +template Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){ Debug("arith") << "updateInconsistentVars" << endl; + Assert(remainingIterations > 0); - static const uint32_t CHECK_PERIOD = 100; - - while(!limitIterations || remainingIterations > 0){ + while(remainingIterations > 0){ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } ArithVar x_i = d_queue.dequeueInconsistentBasicVariable(); @@ -519,7 +530,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera ArithVar x_j = ARITHVAR_SENTINEL; if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ - x_j = selectSlackBelow(x_i, !limitIterations); + x_j = selectSlackBelow(x_i); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictBelow(x_i); //unsat @@ -528,7 +539,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera pivotAndUpdate(x_i, x_j, l_i); }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){ - x_j = selectSlackAbove(x_i, !limitIterations); + x_j = selectSlackAbove(x_i); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictAbove(x_i); //unsat @@ -542,15 +553,8 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera if(!earlyConflict.isNull()){ return earlyConflict; } - //Once every CHECK_PERIOD examine the entire queue for conflicts - if(!limitIterations && remainingIterations % CHECK_PERIOD == 0){ - Node earlyConflict = findConflictOnTheQueue(DuringVarOrderSearch); - if(!earlyConflict.isNull()){ - return earlyConflict; - } - } } - AlwaysAssert(limitIterations && remainingIterations == 0); + Assert(remainingIterations == 0); return Node::null(); } @@ -577,16 +581,18 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ if(nonbasic == conflictVar) continue; const Rational& a_ij = (*nbi).getCoefficient(); - Assert(a_ij != d_constants.d_ZERO); - if(a_ij < d_constants.d_ZERO){ + int sgn = a_ij.sgn(); + Assert(sgn != 0); + if(sgn < 0){ bound = d_partialModel.getUpperConstraint(nonbasic); Debug("arith") << "below 0 " << nonbasic << " " << d_partialModel.getAssignment(nonbasic) << " " << bound << endl; nb << bound; }else{ + Assert(sgn > 0); bound = d_partialModel.getLowerConstraint(nonbasic); Debug("arith") << " above 0 " << nonbasic << " " << d_partialModel.getAssignment(nonbasic) @@ -618,9 +624,11 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ const Rational& a_ij = (*nbi).getCoefficient(); + int sgn = a_ij.sgn(); Assert(a_ij != d_constants.d_ZERO); + Assert(sgn != 0); - if(a_ij < d_constants.d_ZERO){ + if(sgn < 0){ TNode bound = d_partialModel.getLowerConstraint(nonbasic); Debug("arith") << "Lower "<< nonbasic << " " << d_partialModel.getAssignment(nonbasic) << " " @@ -628,6 +636,7 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ nb << bound; }else{ + Assert(sgn > 0); TNode bound = d_partialModel.getUpperConstraint(nonbasic); Debug("arith") << "Upper "<< nonbasic << " " << d_partialModel.getAssignment(nonbasic) << " " 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 Node searchForFeasibleSolution(uint32_t maxIterations); + template 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 ArithVar selectSlack(ArithVar x_i, bool first); - ArithVar selectSlackBelow(ArithVar x_i, bool first) { - return selectSlack(x_i, first); + template ArithVar selectSlack(ArithVar x_i); + template ArithVar selectSlackBelow(ArithVar x_i) { + return selectSlack(x_i); } - ArithVar selectSlackAbove(ArithVar x_i, bool first) { - return selectSlack(x_i, first); + template ArithVar selectSlackAbove(ArithVar x_i) { + return selectSlack(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.