}
}
-template <bool above>
-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 <bool above, SimplexDecisionProcedure::PreferenceFunction pref>
+ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
ReducedRowVector& row_i = d_tableau.lookup(x_i);
ArithVar slack = ARITHVAR_SENTINEL;
- uint32_t numRows = std::numeric_limits<uint32_t>::max();
-
- bool pivotStage = !first;
for(ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end();
nbi != end; ++nbi){
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);
}
}
return Node::null();
}
static unsigned int instance = 0;
-
++instance;
+
+ static const uint32_t CHECK_PERIOD = 100;
Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() "
<< instance << endl;
possibleConflict = findConflictOnTheQueue(BeforeDiffSearch);
}
if(possibleConflict.isNull()){
- possibleConflict = searchForFeasibleSolution<true>(d_numVariables + 1);
+ possibleConflict = searchForFeasibleSolution<minRowCount>(d_numVariables + 1);
}
if(d_queue.size() > 1 && possibleConflict.isNull()){
possibleConflict = findConflictOnTheQueue(AfterDiffSearch);
}
if(!d_queue.empty() && possibleConflict.isNull()){
d_queue.transitionToVariableOrderMode();
- possibleConflict = searchForFeasibleSolution<false>(0);
+
+ while(!d_queue.empty() && possibleConflict.isNull()){
+ possibleConflict = searchForFeasibleSolution<minVarOrder>(CHECK_PERIOD);
+
+ //Once every CHECK_PERIOD examine the entire queue for conflicts
+ if(possibleConflict.isNull()){
+ possibleConflict = findConflictOnTheQueue(DuringVarOrderSearch);
+ }
+ }
}
Assert(!possibleConflict.isNull() || d_queue.empty());
const DeltaRational& beta = d_partialModel.getAssignment(basic);
if(d_partialModel.belowLowerBound(basic, beta, true)){
- ArithVar x_j = selectSlackBelow(basic, true);
+ ArithVar x_j = selectSlackBelow<minVarOrder>(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<minVarOrder>(basic);
if(x_j == ARITHVAR_SENTINEL ){
return generateConflictAbove(basic);
}
}
//corresponds to Check() in dM06
-template <bool limitIterations>
+template <SimplexDecisionProcedure::PreferenceFunction pf>
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();
ArithVar x_j = ARITHVAR_SENTINEL;
if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
- x_j = selectSlackBelow(x_i, !limitIterations);
+ x_j = selectSlackBelow<pf>(x_i);
if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
return generateConflictBelow(x_i); //unsat
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<pf>(x_i);
if(x_j == ARITHVAR_SENTINEL ){
++(d_statistics.d_statUpdateConflicts);
return generateConflictAbove(x_i); //unsat
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();
}
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)
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) << " "
nb << bound;
}else{
+ Assert(sgn > 0);
TNode bound = d_partialModel.getUpperConstraint(nonbasic);
Debug("arith") << "Upper "<< nonbasic << " "
<< d_partialModel.getAssignment(nonbasic) << " "
class SimplexDecisionProcedure {
private:
-
/** Stores system wide constants to avoid unnessecary reconstruction. */
const ArithConstants& d_constants;
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
*/
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
*/
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
}
}
+
+public:
/**
* Checks to make sure the assignment is consistent with the tableau.
* This code is for debugging.
projects / cvc5.git / commitdiff