diff options
Diffstat (limited to 'src/theory/arith/linear_equality.cpp')
| -rw-r--r-- | src/theory/arith/linear_equality.cpp | 208 |
1 files changed, 0 insertions, 208 deletions
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index b1dfa8705..1c32f80e4 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -55,7 +55,6 @@ LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, Bou d_basicVariableUpdates(f), d_increasing(1), d_decreasing(-1), - d_relevantErrorBuffer(), d_btracking(boundsTracking), d_areTracking(false), d_trackCallback(this) @@ -851,213 +850,6 @@ void LinearEqualityModule::trackingCoefficientChange(RowIndex ridx, ArithVar nb, row_bi.addInSgn(nb_inf, 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)); - - - // 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; |