diff options
author | Tim King <taking@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
commit | 9098391fe334d829ec4101f190b8f1fa21c30752 (patch) | |
tree | b134fc1fe1c767a50013e1449330ca6a7ee18a3d /src/theory/arith/linear_equality.cpp | |
parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) |
FCSimplex branch merge
Diffstat (limited to 'src/theory/arith/linear_equality.cpp')
-rw-r--r-- | src/theory/arith/linear_equality.cpp | 1326 |
1 files changed, 1262 insertions, 64 deletions
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 7229eba95..42d8b41f8 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -16,6 +16,7 @@ #include "theory/arith/linear_equality.h" +#include "theory/arith/constraint.h" using namespace std; @@ -23,109 +24,283 @@ namespace CVC4 { namespace theory { namespace arith { -/* Explicitly instatiate this function. */ +/* Explicitly instatiate these functions. */ template void LinearEqualityModule::propagateNonbasics<true>(ArithVar basic, Constraint c); template void LinearEqualityModule::propagateNonbasics<false>(ArithVar basic, Constraint c); +template ArithVar LinearEqualityModule::selectSlack<true>(ArithVar x_i, VarPreferenceFunction pf) const; +template ArithVar LinearEqualityModule::selectSlack<false>(ArithVar x_i, VarPreferenceFunction pf) const; + +// template bool LinearEqualityModule::preferNonDegenerate<true>(const UpdateInfo& a, const UpdateInfo& b) const; +// template bool LinearEqualityModule::preferNonDegenerate<false>(const UpdateInfo& a, const UpdateInfo& b) const; + +// template bool LinearEqualityModule::preferErrorsFixed<true>(const UpdateInfo& a, const UpdateInfo& b) const; +// template bool LinearEqualityModule::preferErrorsFixed<false>(const UpdateInfo& a, const UpdateInfo& b) const; + +template bool LinearEqualityModule::preferWitness<true>(const UpdateInfo& a, const UpdateInfo& b) const; +template bool LinearEqualityModule::preferWitness<false>(const UpdateInfo& a, const UpdateInfo& b) const; + + +void Border::output(std::ostream& out) const{ + out << "{Border" + << ", " << d_bound->getVariable() + << ", " << d_bound->getValue() + << ", " << d_diff + << ", " << d_areFixing + << ", " << d_upperbound; + if(ownBorder()){ + out << ", ownBorder"; + }else{ + out << ", " << d_entry->getCoefficient(); + } + out << ", " << d_bound + << "}"; +} + +LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundCountingVector& boundTracking, BasicVarModelUpdateCallBack f): + d_variables(vars), + d_tableau(t), + d_basicVariableUpdates(f), + d_increasing(1), + d_decreasing(-1), + d_relevantErrorBuffer(), + d_boundTracking(boundTracking), + d_areTracking(false), + d_trackCallback(this) +{} + LinearEqualityModule::Statistics::Statistics(): d_statPivots("theory::arith::pivots",0), d_statUpdates("theory::arith::updates",0), - d_pivotTime("theory::arith::pivotTime") + d_pivotTime("theory::arith::pivotTime"), + d_adjTime("theory::arith::adjTime"), + d_weakeningAttempts("theory::arith::weakening::attempts",0), + d_weakeningSuccesses("theory::arith::weakening::success",0), + d_weakenings("theory::arith::weakening::total",0), + d_weakenTime("theory::arith::weakening::time") { StatisticsRegistry::registerStat(&d_statPivots); StatisticsRegistry::registerStat(&d_statUpdates); StatisticsRegistry::registerStat(&d_pivotTime); + StatisticsRegistry::registerStat(&d_adjTime); + + StatisticsRegistry::registerStat(&d_weakeningAttempts); + StatisticsRegistry::registerStat(&d_weakeningSuccesses); + StatisticsRegistry::registerStat(&d_weakenings); + StatisticsRegistry::registerStat(&d_weakenTime); } LinearEqualityModule::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_statPivots); StatisticsRegistry::unregisterStat(&d_statUpdates); StatisticsRegistry::unregisterStat(&d_pivotTime); + StatisticsRegistry::unregisterStat(&d_adjTime); + + + StatisticsRegistry::unregisterStat(&d_weakeningAttempts); + StatisticsRegistry::unregisterStat(&d_weakeningSuccesses); + StatisticsRegistry::unregisterStat(&d_weakenings); + StatisticsRegistry::unregisterStat(&d_weakenTime); +} +void LinearEqualityModule::includeBoundCountChange(ArithVar nb, BoundCounts prev){ + if(d_tableau.isBasic(nb)){ + return; + } + Assert(!d_tableau.isBasic(nb)); + Assert(!d_areTracking); + + BoundCounts curr = d_variables.boundCounts(nb); + + Assert(prev != curr); + Tableau::ColIterator basicIter = d_tableau.colIterator(nb); + for(; !basicIter.atEnd(); ++basicIter){ + const Tableau::Entry& entry = *basicIter; + Assert(entry.getColVar() == nb); + int a_ijSgn = entry.getCoefficient().sgn(); + + ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex()); + + BoundCounts& counts = d_boundTracking.get(basic); + Debug("includeBoundCountChange") << basic << " " << counts << " to " ; + counts -= prev.multiplyBySgn(a_ijSgn); + counts += curr.multiplyBySgn(a_ijSgn); + Debug("includeBoundCountChange") << counts << " " << a_ijSgn << std::endl; + } + d_boundTracking.set(nb, curr); +} + +void LinearEqualityModule::updateMany(const DenseMap<DeltaRational>& many){ + for(DenseMap<DeltaRational>::const_iterator i = many.begin(), i_end = many.end(); i != i_end; ++i){ + ArithVar nb = *i; + Assert(!d_tableau.isBasic(nb)); + const DeltaRational& newValue = many[nb]; + if(newValue != d_variables.getAssignment(nb)){ + Trace("arith::updateMany") + << "updateMany:" << nb << " " + << d_variables.getAssignment(nb) << " to "<< newValue << endl; + update(nb, newValue); + } + } } -void LinearEqualityModule::update(ArithVar x_i, const DeltaRational& v){ + +void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){ + DenseSet needsToBeAdded; + for(DenseSet::const_iterator i = newBasis.begin(), i_end = newBasis.end(); i != i_end; ++i){ + ArithVar b = *i; + if(!d_tableau.isBasic(b)){ + needsToBeAdded.add(b); + } + } + + while(!needsToBeAdded.empty()){ + ArithVar toRemove = ARITHVAR_SENTINEL; + ArithVar toAdd = ARITHVAR_SENTINEL; + DenseSet::const_iterator i = needsToBeAdded.begin(), i_end = needsToBeAdded.end(); + for(; toAdd == ARITHVAR_SENTINEL && i != i_end; ++i){ + ArithVar v = *i; + + Tableau::ColIterator colIter = d_tableau.colIterator(v); + for(; !colIter.atEnd(); ++colIter){ + const Tableau::Entry& entry = *colIter; + Assert(entry.getColVar() == v); + ArithVar b = d_tableau.rowIndexToBasic(entry.getRowIndex()); + if(!newBasis.isMember(b)){ + toAdd = v; + if(toRemove == ARITHVAR_SENTINEL || + d_tableau.basicRowLength(toRemove) > d_tableau.basicRowLength(b)){ + toRemove = b; + } + } + } + } + Assert(toRemove != ARITHVAR_SENTINEL); + Assert(toAdd != ARITHVAR_SENTINEL); + + Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl; + d_tableau.pivot(toRemove, toAdd, d_trackCallback); + d_basicVariableUpdates(toAdd); + + Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl; + needsToBeAdded.remove(toAdd); + } +} + +void LinearEqualityModule::updateUntracked(ArithVar x_i, const DeltaRational& v){ Assert(!d_tableau.isBasic(x_i)); - DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i); + Assert(!d_areTracking); + const DeltaRational& assignment_x_i = d_variables.getAssignment(x_i); ++(d_statistics.d_statUpdates); + Debug("arith") <<"update " << x_i << ": " << assignment_x_i << "|-> " << v << endl; DeltaRational diff = v - assignment_x_i; - //Assert(matchingSets(d_tableau, x_i)); - Tableau::ColIterator basicIter = d_tableau.colIterator(x_i); - for(; !basicIter.atEnd(); ++basicIter){ - const Tableau::Entry& entry = *basicIter; + Tableau::ColIterator colIter = d_tableau.colIterator(x_i); + for(; !colIter.atEnd(); ++colIter){ + const Tableau::Entry& entry = *colIter; Assert(entry.getColVar() == x_i); ArithVar x_j = d_tableau.rowIndexToBasic(entry.getRowIndex()); - //ReducedRowVector& row_j = d_tableau.lookup(x_j); - - //const Rational& a_ji = row_j.lookup(x_i); const Rational& a_ji = entry.getCoefficient(); - const DeltaRational& assignment = d_partialModel.getAssignment(x_j); + const DeltaRational& assignment = d_variables.getAssignment(x_j); DeltaRational nAssignment = assignment+(diff * a_ji); - d_partialModel.setAssignment(x_j, nAssignment); + d_variables.setAssignment(x_j, nAssignment); d_basicVariableUpdates(x_j); } - d_partialModel.setAssignment(x_i, v); + d_variables.setAssignment(x_i, v); + + if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } +} + +void LinearEqualityModule::updateTracked(ArithVar x_i, const DeltaRational& v){ + TimerStat::CodeTimer codeTimer(d_statistics.d_adjTime); + + Assert(!d_tableau.isBasic(x_i)); + Assert(d_areTracking); + + ++(d_statistics.d_statUpdates); + + DeltaRational diff = v - d_variables.getAssignment(x_i); + Debug("arith") <<"update " << x_i << ": " + << d_variables.getAssignment(x_i) << "|-> " << v << endl; + + + BoundCounts before = d_variables.boundCounts(x_i); + d_variables.setAssignment(x_i, v); + BoundCounts after = d_variables.boundCounts(x_i); + + bool anyChange = before != after; + + Tableau::ColIterator colIter = d_tableau.colIterator(x_i); + for(; !colIter.atEnd(); ++colIter){ + const Tableau::Entry& entry = *colIter; + Assert(entry.getColVar() == x_i); - //double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_i)); + ArithVar x_j = d_tableau.rowIndexToBasic(entry.getRowIndex()); + const Rational& a_ji = entry.getCoefficient(); + + const DeltaRational& assignment = d_variables.getAssignment(x_j); + DeltaRational nAssignment = assignment+(diff * a_ji); + Debug("update") << x_j << " " << a_ji << assignment << " -> " << nAssignment << endl; + d_variables.setAssignment(x_j, nAssignment); + + if(anyChange && basicIsTracked(x_j)){ + BoundCounts& next_bc_k = d_boundTracking.get(x_j); + next_bc_k.addInChange(a_ji.sgn(), before, after); + } + + d_basicVariableUpdates(x_j); + } - //(d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference); if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } } -void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v){ +void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& x_i_value){ Assert(x_i != x_j); TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime); + static int instance = 0; + + if(Debug.isOn("arith::tracking::pre")){ + ++instance; + Debug("arith::tracking") << "pre update #" << instance << endl; + debugCheckTracking(); + } + if(Debug.isOn("arith::simplex:row")){ debugPivot(x_i, x_j); } RowIndex ridx = d_tableau.basicToRowIndex(x_i); const Tableau::Entry& entry_ij = d_tableau.findEntry(ridx, x_j); Assert(!entry_ij.blank()); - const Rational& a_ij = entry_ij.getCoefficient(); + const DeltaRational& betaX_i = d_variables.getAssignment(x_i); + DeltaRational theta = (x_i_value - betaX_i)/a_ij; + DeltaRational x_j_value = d_variables.getAssignment(x_j) + theta; + updateTracked(x_j, x_j_value); - const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i); - - Rational inv_aij = a_ij.inverse(); - DeltaRational theta = (v - betaX_i)*inv_aij; - - d_partialModel.setAssignment(x_i, v); - - - DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta; - d_partialModel.setAssignment(x_j, tmp); - - - //Assert(matchingSets(d_tableau, x_j)); - for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){ - const Tableau::Entry& entry = *iter; - Assert(entry.getColVar() == x_j); - RowIndex currRow = entry.getRowIndex(); - if(ridx != currRow ){ - ArithVar x_k = d_tableau.rowIndexToBasic(currRow); - const Rational& a_kj = entry.getCoefficient(); - DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); - d_partialModel.setAssignment(x_k, nextAssignment); - - d_basicVariableUpdates(x_k); - } + if(Debug.isOn("arith::tracking::mid")){ + Debug("arith::tracking") << "postupdate prepivot #" << instance << endl; + debugCheckTracking(); } // Pivots ++(d_statistics.d_statPivots); - d_tableau.pivot(x_i, x_j); + d_tableau.pivot(x_i, x_j, d_trackCallback); + + if(Debug.isOn("arith::tracking::post")){ + Debug("arith::tracking") << "postpivot #" << instance << endl; + debugCheckTracking(); + } d_basicVariableUpdates(x_j); @@ -134,6 +309,51 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const Delt } } +uint32_t LinearEqualityModule::updateProduct(const UpdateInfo& inf) const { + uint32_t colLen = d_tableau.getColLength(inf.nonbasic()); + if(inf.describesPivot()){ + Assert(inf.leaving() != inf.nonbasic()); + return colLen + d_tableau.basicRowLength(inf.leaving()); + }else{ + return colLen; + } +} + +void LinearEqualityModule::debugCheckTracking(){ + Tableau::BasicIterator basicIter = d_tableau.beginBasic(), + endIter = d_tableau.endBasic(); + for(; basicIter != endIter; ++basicIter){ + ArithVar basic = *basicIter; + Debug("arith::tracking") << "arith::tracking row basic: " << basic << endl; + + for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd() && Debug.isOn("arith::tracking"); ++iter){ + const Tableau::Entry& entry = *iter; + + ArithVar var = entry.getColVar(); + const Rational& coeff = entry.getCoefficient(); + DeltaRational beta = d_variables.getAssignment(var); + Debug("arith::tracking") << var << " " << d_variables.boundCounts(var) + << " " << beta << coeff; + if(d_variables.hasLowerBound(var)){ + Debug("arith::tracking") << "(lb " << d_variables.getLowerBound(var) << ")"; + } + if(d_variables.hasUpperBound(var)){ + Debug("arith::tracking") << "(up " << d_variables.getUpperBound(var) << ")"; + } + Debug("arith::tracking") << endl; + } + Debug("arith::tracking") << "end row"<< endl; + + if(basicIsTracked(basic)){ + BoundCounts computed = computeBoundCounts(basic); + Debug("arith::tracking") + << "computed " << computed + << " tracking " << d_boundTracking[basic] << endl; + Assert(computed == d_boundTracking[basic]); + + } + } +} void LinearEqualityModule::debugPivot(ArithVar x_i, ArithVar x_j){ Debug("arith::pivot") << "debugPivot("<< x_i <<"|->"<< x_j << ")" << endl; @@ -143,13 +363,13 @@ void LinearEqualityModule::debugPivot(ArithVar x_i, ArithVar x_j){ ArithVar var = entry.getColVar(); const Rational& coeff = entry.getCoefficient(); - DeltaRational beta = d_partialModel.getAssignment(var); + DeltaRational beta = d_variables.getAssignment(var); Debug("arith::pivot") << var << beta << coeff; - if(d_partialModel.hasLowerBound(var)){ - Debug("arith::pivot") << "(lb " << d_partialModel.getLowerBound(var) << ")"; + if(d_variables.hasLowerBound(var)){ + Debug("arith::pivot") << "(lb " << d_variables.getLowerBound(var) << ")"; } - if(d_partialModel.hasUpperBound(var)){ - Debug("arith::pivot") << "(up " << d_partialModel.getUpperBound(var) << ")"; + if(d_variables.hasUpperBound(var)){ + Debug("arith::pivot") << "(up " << d_variables.getUpperBound(var) << ")"; } Debug("arith::pivot") << endl; } @@ -177,11 +397,11 @@ void LinearEqualityModule::debugCheckTableau(){ if(basic == nonbasic) continue; const Rational& coeff = entry.getCoefficient(); - DeltaRational beta = d_partialModel.getAssignment(nonbasic); + DeltaRational beta = d_variables.getAssignment(nonbasic); Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl; sum = sum + (beta*coeff); } - DeltaRational shouldBe = d_partialModel.getAssignment(basic); + DeltaRational shouldBe = d_variables.getAssignment(basic); Debug("paranoid:check_tableau") << "ending row" << sum << "," << shouldBe << endl; @@ -193,8 +413,8 @@ bool LinearEqualityModule::debugEntireLinEqIsConsistent(const string& s){ for(ArithVar var = 0, end = d_tableau.getNumColumns(); var != end; ++var){ // for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ //ArithVar var = d_arithvarNodeMap.asArithVar(*i); - if(!d_partialModel.assignmentIsConsistent(var)){ - d_partialModel.printModel(var); + if(!d_variables.assignmentIsConsistent(var)){ + d_variables.printModel(var); Warning() << s << ":" << "Assignment is not consistent for " << var ; if(d_tableau.isBasic(var)){ Warning() << " (basic)"; @@ -217,8 +437,8 @@ DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound bool ub = upperBound ? (sgn > 0) : (sgn < 0); const DeltaRational& bound = ub ? - d_partialModel.getUpperBound(nonbasic): - d_partialModel.getLowerBound(nonbasic); + d_variables.getUpperBound(nonbasic): + d_variables.getLowerBound(nonbasic); DeltaRational diff = bound * coeff; sum = sum + diff; @@ -239,7 +459,7 @@ DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){ if(nonbasic == x) continue; const Rational& coeff = entry.getCoefficient(); - const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); + const DeltaRational& assignment = d_variables.getAssignment(nonbasic, useSafe); sum = sum + (assignment * coeff); } return sum; @@ -253,13 +473,13 @@ bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){ if(var == basic) continue; int sgn = entry.getCoefficient().sgn(); if(upperBound){ - if( (sgn < 0 && !d_partialModel.hasLowerBound(var)) || - (sgn > 0 && !d_partialModel.hasUpperBound(var))){ + if( (sgn < 0 && !d_variables.hasLowerBound(var)) || + (sgn > 0 && !d_variables.hasUpperBound(var))){ return false; } }else{ - if( (sgn < 0 && !d_partialModel.hasUpperBound(var)) || - (sgn > 0 && !d_partialModel.hasLowerBound(var))){ + if( (sgn < 0 && !d_variables.hasUpperBound(var)) || + (sgn > 0 && !d_variables.hasLowerBound(var))){ return false; } } @@ -272,6 +492,8 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ Assert(d_tableau.isBasic(basic)); Assert(c->getVariable() == basic); Assert(!c->assertedToTheTheory()); + Assert(!upperBound || c->isUpperBound()); // upperbound implies c is an upperbound + Assert(upperBound || c->isLowerBound()); // !upperbound implies c is a lowerbound //Assert(c->canBePropagated()); Assert(!c->hasProof()); @@ -293,17 +515,17 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ Constraint bound = NullConstraint; if(upperBound){ if(sgn < 0){ - bound = d_partialModel.getLowerBoundConstraint(nonbasic); + bound = d_variables.getLowerBoundConstraint(nonbasic); }else{ Assert(sgn > 0); - bound = d_partialModel.getUpperBoundConstraint(nonbasic); + bound = d_variables.getUpperBoundConstraint(nonbasic); } }else{ if(sgn < 0){ - bound = d_partialModel.getUpperBoundConstraint(nonbasic); + bound = d_variables.getUpperBoundConstraint(nonbasic); }else{ Assert(sgn > 0); - bound = d_partialModel.getLowerBoundConstraint(nonbasic); + bound = d_variables.getLowerBoundConstraint(nonbasic); } } Assert(bound != NullConstraint); @@ -315,6 +537,982 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ << basic << ") done" << endl; } +Constraint LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic) const { + + int sgn = coeff.sgn(); + bool ub = aboveUpper?(sgn < 0) : (sgn > 0); + + Constraint c = ub ? + d_variables.getUpperBoundConstraint(v) : + d_variables.getLowerBoundConstraint(v); + + bool weakened; + do{ + const DeltaRational& bound = c->getValue(); + + weakened = false; + + Constraint weaker = ub? + c->getStrictlyWeakerUpperBound(true, true): + c->getStrictlyWeakerLowerBound(true, true); + + if(weaker != NullConstraint){ + const DeltaRational& weakerBound = weaker->getValue(); + + DeltaRational diff = aboveUpper ? bound - weakerBound : weakerBound - bound; + //if var == basic, + // if aboveUpper, weakerBound > bound, multiply by -1 + // if !aboveUpper, weakerBound < bound, multiply by -1 + diff = diff * coeff; + if(surplus > diff){ + ++d_statistics.d_weakenings; + weakened = true; + anyWeakening = true; + surplus = surplus - diff; + + Debug("weak") << "found:" << endl; + if(v == basic){ + Debug("weak") << " basic: "; + } + Debug("weak") << " " << surplus << " "<< diff << endl + << " " << bound << c << endl + << " " << weakerBound << weaker << endl; + + Assert(diff.sgn() > 0); + c = weaker; + } + } + }while(weakened); + + return c; +} + +Node LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basicVar) const { + TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime); + + const DeltaRational& assignment = d_variables.getAssignment(basicVar); + DeltaRational surplus; + if(aboveUpper){ + Assert(d_variables.hasUpperBound(basicVar)); + Assert(assignment > d_variables.getUpperBound(basicVar)); + surplus = assignment - d_variables.getUpperBound(basicVar); + }else{ + Assert(d_variables.hasLowerBound(basicVar)); + Assert(assignment < d_variables.getLowerBound(basicVar)); + surplus = d_variables.getLowerBound(basicVar) - assignment; + } + + NodeBuilder<> conflict(kind::AND); + bool anyWeakenings = false; + for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){ + const Tableau::Entry& entry = *i; + ArithVar v = entry.getColVar(); + const Rational& coeff = entry.getCoefficient(); + bool weakening = false; + Constraint c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar); + Debug("weak") << "weak : " << weakening << " " + << c->assertedToTheTheory() << " " + << d_variables.getAssignment(v) << " " + << c << endl + << c->explainForConflict() << endl; + anyWeakenings = anyWeakenings || weakening; + + Debug("weak") << "weak : " << c->explainForConflict() << endl; + c->explainForConflict(conflict); + } + ++d_statistics.d_weakeningAttempts; + if(anyWeakenings){ + ++d_statistics.d_weakeningSuccesses; + } + return conflict; +} + +ArithVar LinearEqualityModule::minVarOrder(ArithVar x, ArithVar y) const { + Assert(x != ARITHVAR_SENTINEL); + Assert(y != ARITHVAR_SENTINEL); + if(x <= y){ + return x; + } else { + return y; + } +} + +ArithVar LinearEqualityModule::minColLength(ArithVar x, ArithVar y) const { + Assert(x != ARITHVAR_SENTINEL); + Assert(y != ARITHVAR_SENTINEL); + Assert(!d_tableau.isBasic(x)); + Assert(!d_tableau.isBasic(y)); + uint32_t xLen = d_tableau.getColLength(x); + uint32_t yLen = d_tableau.getColLength(y); + if( xLen > yLen){ + return y; + } else if( xLen== yLen ){ + return minVarOrder(x,y); + }else{ + return x; + } +} + +ArithVar LinearEqualityModule::minRowLength(ArithVar x, ArithVar y) const { + Assert(x != ARITHVAR_SENTINEL); + Assert(y != ARITHVAR_SENTINEL); + Assert(d_tableau.isBasic(x)); + Assert(d_tableau.isBasic(y)); + uint32_t xLen = d_tableau.basicRowLength(x); + uint32_t yLen = d_tableau.basicRowLength(y); + if( xLen > yLen){ + return y; + } else if( xLen== yLen ){ + return minVarOrder(x,y); + }else{ + return x; + } +} + +ArithVar LinearEqualityModule::minBoundAndColLength(ArithVar x, ArithVar y) const{ + Assert(x != ARITHVAR_SENTINEL); + Assert(y != ARITHVAR_SENTINEL); + Assert(!d_tableau.isBasic(x)); + Assert(!d_tableau.isBasic(y)); + if(d_variables.hasEitherBound(x) && !d_variables.hasEitherBound(y)){ + return y; + }else if(!d_variables.hasEitherBound(x) && d_variables.hasEitherBound(y)){ + return x; + }else { + return minColLength(x, y); + } +} + +template <bool above> +ArithVar LinearEqualityModule::selectSlack(ArithVar x_i, VarPreferenceFunction pref) const{ + ArithVar slack = ARITHVAR_SENTINEL; + + for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){ + const Tableau::Entry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); + if(nonbasic == x_i) continue; + + const Rational& a_ij = entry.getCoefficient(); + int sgn = a_ij.sgn(); + if(isAcceptableSlack<above>(sgn, 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 : (this->*pref)(slack, nonbasic); + } + } + + return slack; +} + +const Tableau::Entry* LinearEqualityModule::selectSlackEntry(ArithVar x_i, bool above) const{ + for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){ + const Tableau::Entry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); + if(nonbasic == x_i) continue; + + const Rational& a_ij = entry.getCoefficient(); + int sgn = a_ij.sgn(); + if(above && isAcceptableSlack<true>(sgn, 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. + return &entry; + }else if(!above && isAcceptableSlack<false>(sgn, nonbasic)){ + return &entry; + } + } + + return NULL; +} + +void LinearEqualityModule::startTrackingBoundCounts(){ + Assert(!d_areTracking); + d_areTracking = true; + if(Debug.isOn("arith::tracking")){ + debugCheckTracking(); + } + Assert(d_areTracking); +} + +void LinearEqualityModule::stopTrackingBoundCounts(){ + Assert(d_areTracking); + d_areTracking = false; + if(Debug.isOn("arith::tracking")){ + debugCheckTracking(); + } + Assert(!d_areTracking); +} + + +void LinearEqualityModule::trackVariable(ArithVar x_i){ + Assert(!basicIsTracked(x_i)); + BoundCounts counts(0,0); + + for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){ + const Tableau::Entry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); + if(nonbasic == x_i) continue; + + const Rational& a_ij = entry.getCoefficient(); + counts += (d_variables.oldBoundCounts(nonbasic)).multiplyBySgn(a_ij.sgn()); + } + d_boundTracking.set(x_i, counts); +} + +BoundCounts LinearEqualityModule::computeBoundCounts(ArithVar x_i) const{ + BoundCounts counts(0,0); + + for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){ + const Tableau::Entry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); + if(nonbasic == x_i) continue; + + const Rational& a_ij = entry.getCoefficient(); + counts += (d_variables.boundCounts(nonbasic)).multiplyBySgn(a_ij.sgn()); + } + + return counts; +} + +// BoundCounts LinearEqualityModule::cachingCountBounds(ArithVar x_i) const{ +// if(d_boundTracking.isKey(x_i)){ +// return d_boundTracking[x_i]; +// }else{ +// return computeBoundCounts(x_i); +// } +// } +BoundCounts LinearEqualityModule::_countBounds(ArithVar x_i) const { + Assert(d_boundTracking.isKey(x_i)); + return d_boundTracking[x_i]; +} + +// BoundCounts LinearEqualityModule::countBounds(ArithVar x_i){ +// if(d_boundTracking.isKey(x_i)){ +// return d_boundTracking[x_i]; +// }else{ +// BoundCounts bc = computeBoundCounts(x_i); +// if(d_areTracking){ +// d_boundTracking.set(x_i,bc); +// } +// return bc; +// } +// } + +bool LinearEqualityModule::basicsAtBounds(const UpdateInfo& u) const { + Assert(u.describesPivot()); + + ArithVar nonbasic = u.nonbasic(); + ArithVar basic = u.leaving(); + Assert(basicIsTracked(basic)); + int coeffSgn = u.getCoefficient().sgn(); + int nbdir = u.nonbasicDirection(); + + Constraint c = u.limiting(); + int toUB = (c->getType() == UpperBound || + c->getType() == Equality) ? 1 : 0; + int toLB = (c->getType() == LowerBound || + c->getType() == Equality) ? 1 : 0; + + + BoundCounts bcs = d_boundTracking[basic]; + // x = c*n + \sum d*m + // n = 1/c * x + -1/c * (\sum d*m) + BoundCounts nonb = bcs - d_variables.boundCounts(nonbasic).multiplyBySgn(coeffSgn); + nonb = nonb.multiplyBySgn(-coeffSgn); + nonb += BoundCounts(toLB, toUB).multiplyBySgn(coeffSgn); + + uint32_t length = d_tableau.basicRowLength(basic); + Debug("basicsAtBounds") + << "bcs " << bcs + << "nonb " << nonb + << "length " << length << endl; + + if(nbdir < 0){ + return bcs.atLowerBounds() + 1 == length; + }else{ + Assert(nbdir > 0); + return bcs.atUpperBounds() + 1 == length; + } +} + +bool LinearEqualityModule::nonbasicsAtLowerBounds(ArithVar basic) const { + Assert(basicIsTracked(basic)); + BoundCounts bcs = d_boundTracking[basic]; + uint32_t length = d_tableau.basicRowLength(basic); + + return bcs.atLowerBounds() + 1 == length; +} + +bool LinearEqualityModule::nonbasicsAtUpperBounds(ArithVar basic) const { + Assert(basicIsTracked(basic)); + BoundCounts bcs = d_boundTracking[basic]; + uint32_t length = d_tableau.basicRowLength(basic); + + return bcs.atUpperBounds() + 1 == length; +} + +void LinearEqualityModule::trackingSwap(ArithVar basic, ArithVar nb, int nbSgn) { + Assert(basicIsTracked(basic)); + + // z = a*x + \sum b*y + // x = (1/a) z + \sum (-1/a)*b*y + // basicCount(z) = bc(a*x) + bc(\sum b y) + // basicCount(x) = bc(z/a) + bc(\sum -b/a * y) + + // sgn(1/a) = sgn(a) + // bc(a*x) = bc(x).multiply(sgn(a)) + // bc(z/a) = bc(z).multiply(sgn(a)) + // bc(\sum -b/a * y) = bc(\sum b y).multiplyBySgn(-sgn(a)) + // bc(\sum b y) = basicCount(z) - bc(a*x) + // basicCount(x) = + // = bc(z).multiply(sgn(a)) + (basicCount(z) - bc(a*x)).multiplyBySgn(-sgn(a)) + + BoundCounts bc = d_boundTracking[basic]; + bc -= (d_variables.boundCounts(nb)).multiplyBySgn(nbSgn); + bc = bc.multiplyBySgn(-nbSgn); + bc += d_variables.boundCounts(basic).multiplyBySgn(nbSgn); + d_boundTracking.set(nb, bc); + d_boundTracking.remove(basic); +} + +void LinearEqualityModule::trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){ + Assert(oldSgn != currSgn); + BoundCounts nb_bc = d_variables.boundCounts(nb); + + if(!nb_bc.isZero()){ + ArithVar basic = d_tableau.rowIndexToBasic(ridx); + Assert(basicIsTracked(basic)); + + BoundCounts& basic_bc = d_boundTracking.get(basic); + basic_bc.addInSgn(nb_bc, oldSgn, currSgn); + } +} + +void LinearEqualityModule::computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction pref){ + ArithVar nb = inf.nonbasic(); + int sgn = inf.nonbasicDirection(); + Assert(sgn != 0); + Assert(!d_tableau.isBasic(nb)); + + //inf.setErrorsChange(0); + //inf.setlimiting = NullConstraint; + + + // Error variables moving in the correct direction + Assert(d_relevantErrorBuffer.empty()); + + // phases : + enum ComputeSafePhase { + NoBoundSelected, + NbsBoundSelected, + BasicBoundSelected, + DegenerateBoundSelected + } phase; + + phase = NoBoundSelected; + + static int instance = 0; + Debug("computeSafeUpdate") << "computeSafeUpdate " << (++instance) << endl; + + if(sgn > 0 && d_variables.hasUpperBound(nb)){ + Constraint ub = d_variables.getUpperBoundConstraint(nb); + inf.updatePureFocus(ub->getValue() - d_variables.getAssignment(nb), ub); + + Assert(inf.nonbasicDelta().sgn() == sgn); + Debug("computeSafeUpdate") << "computeSafeUpdate " << inf.limiting() << endl; + phase = NbsBoundSelected; + }else if(sgn < 0 && d_variables.hasLowerBound(nb)){ + Constraint lb = d_variables.getLowerBoundConstraint(nb); + inf.updatePureFocus(lb->getValue() - d_variables.getAssignment(nb), lb); + + Assert(inf.nonbasicDelta().sgn() == sgn); + + Debug("computeSafeUpdate") << "computeSafeUpdate " << inf.limiting() << endl; + phase = NbsBoundSelected; + } + + Tableau::ColIterator basicIter = d_tableau.colIterator(nb); + for(; !basicIter.atEnd(); ++basicIter){ + const Tableau::Entry& entry = *basicIter; + Assert(entry.getColVar() == nb); + + ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex()); + const Rational& a_ji = entry.getCoefficient(); + int basic_movement = sgn * a_ji.sgn(); + + Debug("computeSafeUpdate") + << "computeSafeUpdate: " + << basic << ", " + << basic_movement << ", " + << d_variables.cmpAssignmentUpperBound(basic) << ", " + << d_variables.cmpAssignmentLowerBound(basic) << ", " + << a_ji << ", " + << d_variables.getAssignment(basic) << endl; + + Constraint proposal = NullConstraint; + + if(basic_movement > 0){ + if(d_variables.cmpAssignmentLowerBound(basic) < 0){ + d_relevantErrorBuffer.push_back(&entry); + } + if(d_variables.hasUpperBound(basic) && + d_variables.cmpAssignmentUpperBound(basic) <= 0){ + proposal = d_variables.getUpperBoundConstraint(basic); + } + }else if(basic_movement < 0){ + if(d_variables.cmpAssignmentUpperBound(basic) > 0){ + d_relevantErrorBuffer.push_back(&entry); + } + if(d_variables.hasLowerBound(basic) && + d_variables.cmpAssignmentLowerBound(basic) >= 0){ + proposal = d_variables.getLowerBoundConstraint(basic); + } + } + if(proposal != NullConstraint){ + const Rational& coeff = entry.getCoefficient(); + DeltaRational diff = proposal->getValue() - d_variables.getAssignment(basic); + diff /= coeff; + int cmp = phase == NoBoundSelected ? 0 : diff.cmp(inf.nonbasicDelta()); + Assert(diff.sgn() == sgn || diff.sgn() == 0); + bool prefer = false; + switch(phase){ + case NoBoundSelected: + prefer = true; + break; + case NbsBoundSelected: + prefer = (sgn > 0 && cmp < 0 ) || (sgn < 0 && cmp > 0); + break; + case BasicBoundSelected: + prefer = + (sgn > 0 && cmp < 0 ) || + (sgn < 0 && cmp > 0) || + (cmp == 0 && basic == (this->*pref)(basic, inf.leaving())); + break; + case DegenerateBoundSelected: + prefer = cmp == 0 && basic == (this->*pref)(basic, inf.leaving()); + break; + } + if(prefer){ + inf.updatePivot(diff, coeff, proposal); + + phase = (diff.sgn() != 0) ? BasicBoundSelected : DegenerateBoundSelected; + } + } + } + + if(phase == DegenerateBoundSelected){ + inf.setErrorsChange(0); + }else{ + computedFixed(inf); + } + inf.determineFocusDirection(); + + d_relevantErrorBuffer.clear(); +} + +void LinearEqualityModule::computedFixed(UpdateInfo& proposal){ + Assert(proposal.nonbasicDirection() != 0); + Assert(!d_tableau.isBasic(proposal.nonbasic())); + + //bool unconstrained = (proposal.d_limiting == NullConstraint); + + Assert(!proposal.unbounded() || !d_relevantErrorBuffer.empty()); + + Assert(proposal.unbounded() || + proposal.nonbasicDelta().sgn() == proposal.nonbasicDirection()); + + // proposal.d_value is the max + + UpdateInfo max; + int dropped = 0; + //Constraint maxFix = NullConstraint; + //DeltaRational maxAmount; + + EntryPointerVector::const_iterator i = d_relevantErrorBuffer.begin(); + EntryPointerVector::const_iterator i_end = d_relevantErrorBuffer.end(); + for(; i != i_end; ++i){ + const Tableau::Entry& entry = *(*i); + Assert(entry.getColVar() == proposal.nonbasic()); + + ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex()); + const Rational& a_ji = entry.getCoefficient(); + int basic_movement = proposal.nonbasicDirection() * a_ji.sgn(); + + DeltaRational theta; + DeltaRational proposedValue; + if(!proposal.unbounded()){ + theta = proposal.nonbasicDelta() * a_ji; + proposedValue = theta + d_variables.getAssignment(basic); + } + + Constraint fixed = NullConstraint; + + if(basic_movement < 0){ + Assert(d_variables.cmpAssignmentUpperBound(basic) > 0); + + if(proposal.unbounded() || d_variables.cmpToUpperBound(basic, proposedValue) <= 0){ + --dropped; + fixed = d_variables.getUpperBoundConstraint(basic); + } + }else if(basic_movement > 0){ + Assert(d_variables.cmpAssignmentLowerBound(basic) < 0); + + if(proposal.unbounded() || d_variables.cmpToLowerBound(basic, proposedValue) >= 0){ + --dropped; + fixed = d_variables.getLowerBoundConstraint(basic); + } + } + if(fixed != NullConstraint){ + DeltaRational amount = fixed->getValue() - d_variables.getAssignment(basic); + amount /= a_ji; + Assert(amount.sgn() == proposal.nonbasicDirection()); + + if(max.uninitialized()){ + max = UpdateInfo(proposal.nonbasic(), proposal.nonbasicDirection()); + max.updatePivot(amount, a_ji, fixed, dropped); + }else{ + int cmp = amount.cmp(max.nonbasicDelta()); + bool prefer = + (proposal.nonbasicDirection() < 0 && cmp < 0) || + (proposal.nonbasicDirection() > 0 && cmp > 0) || + (cmp == 0 && fixed->getVariable() < max.limiting()->getVariable()); + + if(prefer){ + max.updatePivot(amount, a_ji, fixed, dropped); + }else{ + max.setErrorsChange(dropped); + } + } + } + } + Assert(dropped < 0 || !proposal.unbounded()); + + if(dropped < 0){ + proposal = max; + }else{ + Assert(dropped == 0); + Assert(proposal.nonbasicDelta().sgn() != 0); + Assert(proposal.nonbasicDirection() != 0); + proposal.setErrorsChange(0); + } + Assert(proposal.errorsChange() == dropped); +} + +ArithVar LinearEqualityModule::minBy(const ArithVarVec& vec, VarPreferenceFunction pf) const{ + if(vec.empty()) { + return ARITHVAR_SENTINEL; + }else { + ArithVar sel = vec.front(); + ArithVarVec::const_iterator i = vec.begin() + 1; + ArithVarVec::const_iterator i_end = vec.end(); + for(; i != i_end; ++i){ + sel = (this->*pf)(sel, *i); + } + return sel; + } +} + +bool LinearEqualityModule::accumulateBorder(const Tableau::Entry& entry, bool ub){ + ArithVar currBasic = d_tableau.rowIndexToBasic(entry.getRowIndex()); + + Assert(basicIsTracked(currBasic)); + + Constraint bound = ub ? + d_variables.getUpperBoundConstraint(currBasic): + d_variables.getLowerBoundConstraint(currBasic); + + if(bound == NullConstraint){ return false; } + Assert(bound != NullConstraint); + + const Rational& coeff = entry.getCoefficient(); + + const DeltaRational& assignment = d_variables.getAssignment(currBasic); + DeltaRational toBound = bound->getValue() - assignment; + DeltaRational nbDiff = toBound/coeff; + + // if ub + // if toUB >= 0 + // then ub >= currBasic + // if sgn > 0, + // then diff >= 0, so nb must increase for G + // else diff <= 0, so nb must decrease for G + // else ub < currBasic + // if sgn > 0, + // then diff < 0, so nb must decrease for G + // else diff > 0, so nb must increase for G + + int diffSgn = nbDiff.sgn(); + + if(diffSgn != 0 && willBeInConflictAfterPivot(entry, nbDiff, ub)){ + return true; + }else{ + bool areFixing = ub ? (toBound.sgn() < 0 ) : (toBound.sgn() > 0); + Border border(bound, nbDiff, areFixing, &entry, ub); + bool increasing = + (diffSgn > 0) || + (diffSgn == 0 && ((coeff.sgn() > 0) == ub)); + + // assume diffSgn == 0 + // if coeff > 0, + // if ub, inc + // else, dec + // else coeff < 0 + // if ub, dec + // else, inc + + if(increasing){ + Debug("handleBorders") << "push back increasing " << border << endl; + d_increasing.push_back(border); + }else{ + Debug("handleBorders") << "push back decreasing " << border << endl; + d_decreasing.push_back(border); + } + return false; + } +} + +bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entry, const DeltaRational& nbDiff, bool bToUB) const{ + int nbSgn = nbDiff.sgn(); + Assert(nbSgn != 0); + + if(nbSgn > 0){ + if(d_upperBoundDifference.nothing() || nbDiff <= d_upperBoundDifference){ + return false; + } + }else{ + if(d_lowerBoundDifference.nothing() || nbDiff >= d_lowerBoundDifference){ + return false; + } + } + + // Assume past this point, nb will be in error if this pivot is done + ArithVar nb = entry.getColVar(); + ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex()); + Assert(basicIsTracked(basic)); + int coeffSgn = entry.getCoefficient().sgn(); + + + // if bToUB, then basic is going to be set to its upperbound + // if not bToUB, then basic is going to be set to its lowerbound + + // Different steps of solving for this: + // 1) y = a * x + \sum b * z + // 2) -a * x = -y + \sum b * z + // 3) x = (-1/a) * ( -y + \sum b * z) + + Assert(basicIsTracked(basic)); + BoundCounts bc = d_boundTracking[basic]; + + // 1) y = a * x + \sum b * z + // Get bc(\sum b * z) + BoundCounts sumOnly = bc - d_variables.boundCounts(nb).multiplyBySgn(coeffSgn); + + // y's bounds in the proposed model + int yWillBeAtUb = (bToUB || d_variables.boundsAreEqual(basic)) ? 1 : 0; + int yWillBeAtLb = (!bToUB || d_variables.boundsAreEqual(basic)) ? 1 : 0; + BoundCounts ysBounds(yWillBeAtLb, yWillBeAtUb); + + // 2) -a * x = -y + \sum b * z + // Get bc(-y + \sum b * z) + BoundCounts withNegY = sumOnly + ysBounds.multiplyBySgn(-1); + + // 3) x = (-1/a) * ( -y + \sum b * z) + // Get bc((-1/a) * ( -y + \sum b * z)) + BoundCounts xsBoundsAfterPivot = withNegY.multiplyBySgn(-coeffSgn); + + uint32_t length = d_tableau.basicRowLength(basic); + if(nbSgn > 0){ + // Only check for the upper bound being violated + return xsBoundsAfterPivot.atLowerBounds() + 1 == length; + }else{ + // Only check for the lower bound being violated + return xsBoundsAfterPivot.atUpperBounds() + 1 == length; + } +} + +UpdateInfo LinearEqualityModule::mkConflictUpdate(const Tableau::Entry& entry, bool ub) const{ + ArithVar currBasic = d_tableau.rowIndexToBasic(entry.getRowIndex()); + ArithVar nb = entry.getColVar(); + + Constraint bound = ub ? + d_variables.getUpperBoundConstraint(currBasic): + d_variables.getLowerBoundConstraint(currBasic); + + + const Rational& coeff = entry.getCoefficient(); + const DeltaRational& assignment = d_variables.getAssignment(currBasic); + DeltaRational toBound = bound->getValue() - assignment; + DeltaRational nbDiff = toBound/coeff; + + return UpdateInfo::conflict(nb, nbDiff, coeff, bound); +} + +UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational& focusCoeff, UpdatePreferenceFunction pref){ + Assert(d_increasing.empty()); + Assert(d_decreasing.empty()); + Assert(d_lowerBoundDifference.nothing()); + Assert(d_upperBoundDifference.nothing()); + + int focusCoeffSgn = focusCoeff.sgn(); + + static int instance = 0; + ++instance; + Debug("speculativeUpdate") << "speculativeUpdate " << instance << endl; + Debug("speculativeUpdate") << "nb " << nb << endl; + Debug("speculativeUpdate") << "focusCoeff " << focusCoeff << endl; + + if(d_variables.hasUpperBound(nb)){ + Constraint ub = d_variables.getUpperBoundConstraint(nb); + d_upperBoundDifference = ub->getValue() - d_variables.getAssignment(nb); + Border border(ub, d_upperBoundDifference, false, NULL, true); + Debug("handleBorders") << "push back increasing " << border << endl; + d_increasing.push_back(border); + } + if(d_variables.hasLowerBound(nb)){ + Constraint lb = d_variables.getLowerBoundConstraint(nb); + d_lowerBoundDifference = lb->getValue() - d_variables.getAssignment(nb); + Border border(lb, d_lowerBoundDifference, false, NULL, false); + Debug("handleBorders") << "push back decreasing " << border << endl; + d_decreasing.push_back(border); + } + + Tableau::ColIterator colIter = d_tableau.colIterator(nb); + for(; !colIter.atEnd(); ++colIter){ + const Tableau::Entry& entry = *colIter; + Assert(entry.getColVar() == nb); + + if(accumulateBorder(entry, true)){ + clearSpeculative(); + return mkConflictUpdate(entry, true); + } + if(accumulateBorder(entry, false)){ + clearSpeculative(); + return mkConflictUpdate(entry, false); + } + } + + UpdateInfo selected; + BorderHeap& withSgn = focusCoeffSgn > 0 ? d_increasing : d_decreasing; + BorderHeap& againstSgn = focusCoeffSgn > 0 ? d_decreasing : d_increasing; + + handleBorders(selected, nb, focusCoeff, withSgn, 0, pref); + int m = 1 - selected.errorsChangeSafe(0); + handleBorders(selected, nb, focusCoeff, againstSgn, m, pref); + + clearSpeculative(); + return selected; +} + +void LinearEqualityModule::clearSpeculative(){ + // clear everything away + d_increasing.clear(); + d_decreasing.clear(); + d_lowerBoundDifference.clear(); + d_upperBoundDifference.clear(); +} + +void LinearEqualityModule::handleBorders(UpdateInfo& selected, ArithVar nb, const Rational& focusCoeff, BorderHeap& heap, int minimumFixes, UpdatePreferenceFunction pref){ + Assert(minimumFixes >= 0); + + // The values popped off of the heap + // should be popped with the values closest to 0 + // being first and larger in absolute value last + + + int fixesRemaining = heap.possibleFixes(); + + Debug("handleBorders") + << "handleBorders " + << "nb " << nb + << "fc " << focusCoeff + << "h.e " << heap.empty() + << "h.dir " << heap.direction() + << "h.rem " << fixesRemaining + << "h.0s " << heap.numZeroes() + << "min " << minimumFixes + << endl; + + if(heap.empty()){ + // if the heap is empty, return + return; + } + + bool zeroesWillDominate = fixesRemaining - heap.numZeroes() < minimumFixes; + + // can the number of fixes ever exceed the minimum? + // no more than the number of possible fixes can be fixed in total + // nothing can be fixed before the zeroes are taken care of + if(minimumFixes > 0 && zeroesWillDominate){ + return; + } + + + int negErrorChange = 0; + int nbDir = heap.direction(); + + // points at the beginning of the heap + if(zeroesWillDominate){ + heap.dropNonZeroes(); + } + heap.make_heap(); + + + // pretend like the previous block had a value of zero. + // The block that actually has a value of 0 must handle this. + const DeltaRational zero(0); + const DeltaRational* prevBlockValue = &zero; + + /** The coefficient changes as the value crosses border. */ + Rational effectiveCoefficient = focusCoeff; + + /* Keeps track of the change to the value of the focus function.*/ + DeltaRational totalFocusChange(0); + + const int focusCoeffSgn = focusCoeff.sgn(); + + while(heap.more() && + (fixesRemaining + negErrorChange > minimumFixes || + (fixesRemaining + negErrorChange == minimumFixes && + effectiveCoefficient.sgn() == focusCoeffSgn))){ + // There are more elements && + // we can either fix at least 1 more variable in the error function + // or we can improve the error function + + + int brokenInBlock = 0; + BorderVec::const_iterator endBlock = heap.end(); + + pop_block(heap, brokenInBlock, fixesRemaining, negErrorChange); + + // if endVec == beginVec, block starts there + // other wise, block starts at endVec + BorderVec::const_iterator startBlock + = heap.more() ? heap.end() : heap.begin(); + + const DeltaRational& blockValue = (*startBlock).d_diff; + + // if decreasing + // blockValue < prevBlockValue + // diff.sgn() = -1 + DeltaRational diff = blockValue - (*prevBlockValue); + DeltaRational blockChangeToFocus = diff * effectiveCoefficient; + totalFocusChange += blockChangeToFocus; + + Debug("handleBorders") + << "blockValue " << (blockValue) + << "diff " << diff + << "blockChangeToFocus " << totalFocusChange + << "blockChangeToFocus " << totalFocusChange + << "negErrorChange " << negErrorChange + << "brokenInBlock " << brokenInBlock + << "fixesRemaining " << fixesRemaining + << endl; + + int currFocusChangeSgn = totalFocusChange.sgn(); + for(BorderVec::const_iterator i = startBlock; i != endBlock; ++i){ + const Border& b = *i; + + Debug("handleBorders") << b << endl; + + bool makesImprovement = negErrorChange > 0 || + (negErrorChange == 0 && currFocusChangeSgn > 0); + + if(!makesImprovement){ + if(b.ownBorder() || minimumFixes > 0){ + continue; + } + } + + UpdateInfo proposal(nb, nbDir); + if(b.ownBorder()){ + proposal.witnessedUpdate(b.d_diff, b.d_bound, -negErrorChange, currFocusChangeSgn); + }else{ + proposal.update(b.d_diff, b.getCoefficient(), b.d_bound, -negErrorChange, currFocusChangeSgn); + } + + if(selected.unbounded() || (this->*pref)(selected, proposal)){ + selected = proposal; + } + } + + effectiveCoefficient += updateCoefficient(startBlock, endBlock); + prevBlockValue = &blockValue; + negErrorChange -= brokenInBlock; + } +} + +Rational LinearEqualityModule::updateCoefficient(BorderVec::const_iterator startBlock, BorderVec::const_iterator endBlock){ + //update coefficient + Rational changeToCoefficient(0); + for(BorderVec::const_iterator i = startBlock; i != endBlock; ++i){ + const Border& curr = *i; + if(curr.ownBorder()){// breaking its own bound + if(curr.d_upperbound){ + changeToCoefficient -= 1; + }else{ + changeToCoefficient += 1; + } + }else{ + const Rational& coeff = curr.d_entry->getCoefficient(); + if(curr.d_areFixing){ + if(curr.d_upperbound){// fixing an upper bound + changeToCoefficient += coeff; + }else{// fixing a lower bound + changeToCoefficient -= coeff; + } + }else{ + if(curr.d_upperbound){// breaking an upper bound + changeToCoefficient -= coeff; + }else{ + // breaking a lower bound + changeToCoefficient += coeff; + } + } + } + } + return changeToCoefficient; +} + +void LinearEqualityModule::pop_block(BorderHeap& heap, int& brokenInBlock, int& fixesRemaining, int& negErrorChange){ + Assert(heap.more()); + + if(heap.top().d_areFixing){ + fixesRemaining--; + negErrorChange++; + }else{ + brokenInBlock++; + } + heap.pop_heap(); + const DeltaRational& blockValue = (*heap.end()).d_diff; + + while(heap.more()){ + const Border& top = heap.top(); + if(blockValue == top.d_diff){ + // belongs to the block + if(top.d_areFixing){ + fixesRemaining--; + negErrorChange++; + }else{ + brokenInBlock++; + } + heap.pop_heap(); + }else{ + // does not belong to the block + Assert((heap.direction() > 0) ? + (blockValue < top.d_diff) : (blockValue > top.d_diff)); + break; + } + } +} + +void LinearEqualityModule::substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult){ + d_tableau.substitutePlusTimesConstant(to, from, mult, d_trackCallback); +} +void LinearEqualityModule::directlyAddToCoefficient(ArithVar row, ArithVar col, const Rational& mult){ + d_tableau.directlyAddToCoefficient(row, col, mult, d_trackCallback); +} + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |