From 69410776fdd18f8020a5c0a1daec8bc928ab8551 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 3 May 2013 15:01:02 -0400 Subject: [PATCH] Removing arithmetic legacy code and unifying functions. --- src/theory/arith/linear_equality.cpp | 103 ++-------------------- src/theory/arith/linear_equality.h | 67 +++++++------- src/theory/arith/theory_arith_private.cpp | 41 ++++----- 3 files changed, 57 insertions(+), 154 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(ArithVar basic, Constraint c); -template void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c); template ArithVar LinearEqualityModule::selectSlack(ArithVar x_i, VarPreferenceFunction pf) const; template ArithVar LinearEqualityModule::selectSlack(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 -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 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& into, RowIndex ridx, bool rowUp, Constraint c){ @@ -589,7 +501,6 @@ void LinearEqualityModule::propagateRow(vector& into, RowIndex ridx, ArithVar v = c->getVariable(); Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" << v <<") start" << endl; - //vector bounds; Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx); for(; !iter.atEnd(); ++iter){ diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index b1f3d00d7..4d18d5c81 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -261,9 +261,6 @@ public: void forceNewBasis(const DenseSet& newBasis); -#warning "Remove legacy code." - bool hasBounds(ArithVar basic, bool upperBound); - /** * Returns a pointer to the first Tableau entry on the row ridx that does not * have an either a lower bound/upper bound for proving a bound on skip. @@ -416,17 +413,13 @@ private: BoundInfoMap& d_btracking; bool d_areTracking; -#warning "Remove legacy code" - template - void propagateNonbasics(ArithVar basic, Constraint c); - public: - void propagateNonbasicsLowerBound(ArithVar basic, Constraint c){ - propagateNonbasics(basic, c); - } - void propagateNonbasicsUpperBound(ArithVar basic, Constraint c){ - propagateNonbasics(basic, c); - } + /** + * The constraint on a basic variable b is implied by the constraints + * on its row. This is a wrapper for propagateRow(). + */ + void propagateBasicFromRow(Constraint c); + /** * Exports either the explanation of an upperbound or a lower bound * of the basic variable basic, using the non-basic variables in the row. @@ -442,13 +435,6 @@ public: */ DeltaRational computeRowValue(ArithVar x, bool useSafe) const; - inline DeltaRational computeLowerBound(ArithVar basic) const{ - return computeBound(basic, false); - } - inline DeltaRational computeUpperBound(ArithVar basic) const{ - return computeBound(basic, true); - } - /** * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure, * and 2 ArithVar variables and returns one of the ArithVar variables @@ -547,29 +533,45 @@ public: * The minimum/maximum is determined by the direction the non-basic is changing. */ bool basicsAtBounds(const UpdateInfo& u) const; + private: + + /** + * Recomputes the bound info for a row using either the information + * in the bounds queue or the current information. + * O(row length of ridx) + */ BoundsInfo computeRowBoundInfo(RowIndex ridx, bool inQueue) const; + public: + /** Debug only routine. */ BoundCounts debugBasicAtBoundCount(ArithVar x_i) const; + + /** Track the effect of the change of coefficient for bound counting. */ void trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn); + + /** Track the effect of multiplying a row by a sign for bound counting. */ void trackingMultiplyRow(RowIndex ridx, int sgn); + /** Count for how many on a row have *an* upper/lower bounds. */ BoundCounts hasBoundCount(RowIndex ri) const { Assert(d_variables.boundsQueueEmpty()); return d_btracking[ri].hasBounds(); } -#warning "Remove legacy code" + /** + * Are there any non-basics on x_i's row that are not at + * their respective lower bounds (mod sgns). + * O(1) time due to the atBound() count. + */ bool nonbasicsAtLowerBounds(ArithVar x_i) const; - bool nonbasicsAtUpperBounds(ArithVar x_i) const; -#warning "Remove legacy code" - ArithVar _anySlackLowerBound(ArithVar x_i) const { - return selectSlack(x_i, &LinearEqualityModule::noPreference); - } - ArithVar _anySlackUpperBound(ArithVar x_i) const { - return selectSlack(x_i, &LinearEqualityModule::noPreference); - } + /** + * Are there any non-basics on x_i's row that are not at + * their respective upper bounds (mod sgns). + * O(1) time due to the atBound() count. + */ + bool nonbasicsAtUpperBounds(ArithVar x_i) const; private: class TrackingCallback : public CoefficientChangeCallback { @@ -616,11 +618,12 @@ public: return minimallyWeakConflict(false, conflictVar); } + /** + * Computes the sum of the upper/lower bound of row. + * The variable skip is not included in the sum. + */ DeltaRational computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const; -private: - DeltaRational computeBound(ArithVar basic, bool upperBound) const; - public: void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult); void directlyAddToCoefficient(ArithVar row, ArithVar col, const Rational& mult); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 31b6cd032..7eae2606c 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1401,20 +1401,6 @@ Constraint TheoryArithPrivate::constraintFromFactQueue(){ } } - // Kind simpleKind = Comparison::comparisonKind(assertion); - // Assert(simpleKind != UNDEFINED_KIND); - // Assert(constraint != NullConstraint || - // simpleKind == EQUAL || - // simpleKind == DISTINCT ); - // if(simpleKind == EQUAL || simpleKind == DISTINCT){ - // Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion; - - // if(!isSetup(eq)){ - // //The previous code was equivalent to: - // setupAtom(eq); - // constraint = d_constraintDatabase.lookup(assertion); - // } - // } Assert(constraint != NullConstraint); if(constraint->negationHasProof()){ @@ -2490,9 +2476,8 @@ EqualityStatus TheoryArithPrivate::getEqualityStatus(TNode a, TNode b) { bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound){ ++d_statistics.d_boundComputations; - DeltaRational bound = upperBound ? - d_linEq.computeUpperBound(basic): - d_linEq.computeLowerBound(basic); + RowIndex ridx = d_tableau.basicToRowIndex(basic); + DeltaRational bound = d_linEq.computeRowBound(ridx, upperBound, basic); if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) || (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){ @@ -2540,13 +2525,7 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound } if(!assertedToTheTheory && canBePropagated && !hasProof ){ - if(upperBound){ - Assert(bestImplied != d_partialModel.getUpperBoundConstraint(basic)); - d_linEq.propagateNonbasicsUpperBound(basic, bestImplied); - }else{ - Assert(bestImplied != d_partialModel.getLowerBoundConstraint(basic)); - d_linEq.propagateNonbasicsLowerBound(basic, bestImplied); - } + d_linEq.propagateBasicFromRow(bestImplied); // I think this can be skipped if canBePropagated is true //d_learnedBounds.push(bestImplied); if(Debug.isOn("arith::prop")){ @@ -2570,10 +2549,20 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound void TheoryArithPrivate::propagateCandidate(ArithVar basic){ bool success = false; - if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasBounds(basic, false)){ + RowIndex ridx = d_tableau.basicToRowIndex(basic); + + bool tryLowerBound = + d_partialModel.strictlyAboveLowerBound(basic) && + d_linEq.rowLacksBound(ridx, false, basic) == NULL; + + bool tryUpperBound = + d_partialModel.strictlyBelowUpperBound(basic) && + d_linEq.rowLacksBound(ridx, true, basic) == NULL; + + if(tryLowerBound){ success |= propagateCandidateLowerBound(basic); } - if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasBounds(basic, true)){ + if(tryUpperBound){ success |= propagateCandidateUpperBound(basic); } if(success){ -- 2.30.2