diff options
author | Tim King <taking@cs.nyu.edu> | 2013-05-03 15:01:02 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-05-03 15:01:02 -0400 |
commit | 69410776fdd18f8020a5c0a1daec8bc928ab8551 (patch) | |
tree | 9ce2e92790a3d6085c7f5b78356ced96a518d398 /src/theory/arith/linear_equality.cpp | |
parent | a5cc122524cdcfe65a81ce3e1a93baa04e836781 (diff) |
Removing arithmetic legacy code and unifying functions.
Diffstat (limited to 'src/theory/arith/linear_equality.cpp')
-rw-r--r-- | src/theory/arith/linear_equality.cpp | 103 |
1 files changed, 7 insertions, 96 deletions
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index bde771102..b1dfa8705 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -25,8 +25,6 @@ namespace theory { namespace arith { /* 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; @@ -421,29 +419,6 @@ bool LinearEqualityModule::debugEntireLinEqIsConsistent(const string& s){ return result; } -// DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){ -// DeltaRational sum(0,0); -// for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){ -// const Tableau::Entry& entry = (*i); -// ArithVar nonbasic = entry.getColVar(); -// if(nonbasic == basic) continue; -// const Rational& coeff = entry.getCoefficient(); -// int sgn = coeff.sgn(); -// bool ub = upperBound ? (sgn > 0) : (sgn < 0); - -// const DeltaRational& bound = ub ? -// d_variables.getUpperBound(nonbasic): -// d_variables.getLowerBound(nonbasic); - -// DeltaRational diff = bound * coeff; -// sum = sum + diff; -// } -// return sum; -// } -DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound) const { - RowIndex rid = d_tableau.basicToRowIndex(basic); - return computeRowBound(rid, upperBound, basic); -} DeltaRational LinearEqualityModule::computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const { DeltaRational sum(0,0); for(Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i){ @@ -483,33 +458,6 @@ DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe) co return sum; } -// bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){ -// for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd(); ++iter){ -// const Tableau::Entry& entry = *iter; - -// ArithVar var = entry.getColVar(); -// if(var == basic) continue; -// int sgn = entry.getCoefficient().sgn(); -// if(upperBound){ -// if( (sgn < 0 && !d_variables.hasLowerBound(var)) || -// (sgn > 0 && !d_variables.hasUpperBound(var))){ -// return false; -// } -// }else{ -// if( (sgn < 0 && !d_variables.hasUpperBound(var)) || -// (sgn > 0 && !d_variables.hasLowerBound(var))){ -// return false; -// } -// } -// } -// return true; -// } - -bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){ - RowIndex ridx = d_tableau.basicToRowIndex(basic); - return rowLacksBound(ridx, upperBound, basic) == NULL; -} - const Tableau::Entry* LinearEqualityModule::rowLacksBound(RowIndex ridx, bool rowUb, ArithVar skip){ Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx); for(; !iter.atEnd(); ++iter){ @@ -530,55 +478,19 @@ const Tableau::Entry* LinearEqualityModule::rowLacksBound(RowIndex ridx, bool ro return NULL; } - -template <bool upperBound> -void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ - Assert(d_tableau.isBasic(basic)); - Assert(c->getVariable() == basic); +void LinearEqualityModule::propagateBasicFromRow(Constraint c){ + Assert(c != NullConstraint); + Assert(c->isUpperBound() || c->isLowerBound()); 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()); - Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" - << basic <<") start" << endl; + bool upperBound = c->isUpperBound(); + ArithVar basic = c->getVariable(); + RowIndex ridx = d_tableau.basicToRowIndex(basic); vector<Constraint> bounds; - - Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); - for(; !iter.atEnd(); ++iter){ - const Tableau::Entry& entry = *iter; - ArithVar nonbasic = entry.getColVar(); - if(nonbasic == basic) continue; - - const Rational& a_ij = entry.getCoefficient(); - - int sgn = a_ij.sgn(); - Assert(sgn != 0); - Constraint bound = NullConstraint; - if(upperBound){ - if(sgn < 0){ - bound = d_variables.getLowerBoundConstraint(nonbasic); - }else{ - Assert(sgn > 0); - bound = d_variables.getUpperBoundConstraint(nonbasic); - } - }else{ - if(sgn < 0){ - bound = d_variables.getUpperBoundConstraint(nonbasic); - }else{ - Assert(sgn > 0); - bound = d_variables.getLowerBoundConstraint(nonbasic); - } - } - Assert(bound != NullConstraint); - Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl; - bounds.push_back(bound); - } + propagateRow(bounds, ridx, upperBound, c); c->impliedBy(bounds); - Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" - << basic << ") done" << endl; } void LinearEqualityModule::propagateRow(vector<Constraint>& into, RowIndex ridx, bool rowUp, Constraint c){ @@ -589,7 +501,6 @@ void LinearEqualityModule::propagateRow(vector<Constraint>& into, RowIndex ridx, ArithVar v = c->getVariable(); Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" << v <<") start" << endl; - //vector<Constraint> bounds; Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx); for(; !iter.atEnd(); ++iter){ |