From: Tim King Date: Tue, 30 Apr 2013 23:09:06 +0000 (-0400) Subject: Draft of the new propagation code. X-Git-Tag: cvc5-1.0.0~7287^2~163^2~2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d833d5790a38dc62d8a4714a13253253767c377e;p=cvc5.git Draft of the new propagation code. --- diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index eda3bf682..4779b1012 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -421,19 +421,42 @@ bool LinearEqualityModule::debugEntireLinEqIsConsistent(const string& s){ return result; } -DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){ +// 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.basicRowIterator(basic); !i.atEnd(); ++i){ + for(Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i){ const Tableau::Entry& entry = (*i); - ArithVar nonbasic = entry.getColVar(); - if(nonbasic == basic) continue; + ArithVar v = entry.getColVar(); + if(v == skip){ continue; } + const Rational& coeff = entry.getCoefficient(); - int sgn = coeff.sgn(); - bool ub = upperBound ? (sgn > 0) : (sgn < 0); + bool vUb = (rowUb == (coeff.sgn() > 0)); - const DeltaRational& bound = ub ? - d_variables.getUpperBound(nonbasic): - d_variables.getLowerBound(nonbasic); + const DeltaRational& bound = vUb ? + d_variables.getUpperBound(v): + d_variables.getLowerBound(v); DeltaRational diff = bound * coeff; sum = sum + diff; @@ -444,7 +467,7 @@ DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound /** * Computes the value of a basic variable using the current assignment. */ -DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){ +DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe) const{ Assert(d_tableau.isBasic(x)); DeltaRational sum(0); @@ -460,28 +483,54 @@ DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){ 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){ - for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd(); ++iter){ + 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){ const Tableau::Entry& entry = *iter; ArithVar var = entry.getColVar(); - if(var == basic) continue; + if(var == skip) { 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; - } + bool selectUb = (rowUb == (sgn > 0)); + bool hasBound = selectUb ? + d_variables.hasUpperBound(var): + d_variables.hasLowerBound(var); + if(!hasBound){ + return &entry; } } - return true; + return NULL; } + template void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ Assert(d_tableau.isBasic(basic)); @@ -532,6 +581,40 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ << basic << ") done" << endl; } +void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c){ + Assert(!c->assertedToTheTheory()); + Assert(c->canBePropagated()); + Assert(!c->hasProof()); + + 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){ + const Tableau::Entry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); + if(nonbasic == v){ continue; } + + const Rational& a_ij = entry.getCoefficient(); + + int sgn = a_ij.sgn(); + Assert(sgn != 0); + bool selectUb = rowUp ? (sgn > 0) : (sgn < 0); + Constraint bound = selectUb + ? d_variables.getUpperBoundConstraint(nonbasic) + : d_variables.getLowerBoundConstraint(nonbasic); + + Assert(bound != NullConstraint); + Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl; + bounds.push_back(bound); + } + c->impliedBy(bounds); + Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" + << v << ") done" << endl; +} + Constraint LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic) const { int sgn = coeff.sgn(); @@ -749,7 +832,8 @@ void LinearEqualityModule::trackRowIndex(RowIndex ridx){ BoundsInfo LinearEqualityModule::computeRowBoundInfo(RowIndex ridx, bool inQueue) const{ BoundsInfo bi; - for(Tableau::RowIterator iter = d_tableau.getRow(ridx).begin(); !iter.atEnd(); ++iter){ + Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx); + for(; !iter.atEnd(); ++iter){ const Tableau::Entry& entry = *iter; ArithVar v = entry.getColVar(); const Rational& a_ij = entry.getCoefficient(); diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index bc653fdad..767c09340 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -255,20 +255,24 @@ public: * Updates the assignment of the other basic variables accordingly. */ void pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v); - //void pivotAndUpdateAdj(ArithVar x_i, ArithVar x_j, const DeltaRational& v); ArithVariables& getVariables() const{ return d_variables; } Tableau& getTableau() const{ return d_tableau; } void forceNewBasis(const DenseSet& newBasis); +#warning "Remove legacy code." bool hasBounds(ArithVar basic, bool upperBound); - bool hasLowerBounds(ArithVar basic){ - return hasBounds(basic, false); - } - bool hasUpperBounds(ArithVar basic){ - return hasBounds(basic, true); - } + + /** + * 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. + * The variable skip is always excluded. Returns NULL if there is no such element. + * + * If skip == ARITHVAR_SENTINEL, this is equivalent to considering the whole row. + */ + const Tableau::Entry* rowLacksBound(RowIndex ridx, bool upperBound, ArithVar skip); + void startTrackingBoundCounts(); void stopTrackingBoundCounts(); @@ -412,10 +416,7 @@ private: BoundInfoMap& d_btracking; bool d_areTracking; - /** - * Exports either the explanation of an upperbound or a lower bound - * of the basic variable basic, using the non-basic variables in the row. - */ +#warning "Remove legacy code" template void propagateNonbasics(ArithVar basic, Constraint c); @@ -426,6 +427,11 @@ public: void propagateNonbasicsUpperBound(ArithVar basic, Constraint c){ propagateNonbasics(basic, 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. + */ + void propagateRow(RowIndex ridx, bool rowUp, Constraint c); /** * Computes the value of a basic variable using the assignments @@ -434,12 +440,12 @@ public: * - the the current assignment (useSafe=false) or * - the safe assignment (useSafe = true). */ - DeltaRational computeRowValue(ArithVar x, bool useSafe); + DeltaRational computeRowValue(ArithVar x, bool useSafe) const; - inline DeltaRational computeLowerBound(ArithVar basic){ + inline DeltaRational computeLowerBound(ArithVar basic) const{ return computeBound(basic, false); } - inline DeltaRational computeUpperBound(ArithVar basic){ + inline DeltaRational computeUpperBound(ArithVar basic) const{ return computeBound(basic, true); } @@ -542,18 +548,22 @@ public: */ bool basicsAtBounds(const UpdateInfo& u) const; private: - //BoundCounts computeBasicAtBoundCounts(ArithVar x_i) const; - //BoundCounts computeRowAtBoundCounts(RowIndex ridx) const; BoundsInfo computeRowBoundInfo(RowIndex ridx, bool inQueue) const; public: - //BoundCounts cachingCountBounds(ArithVar x_i) const; BoundCounts debugBasicAtBoundCount(ArithVar x_i) const; void trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn); void trackingMultiplyRow(RowIndex ridx, int sgn); + BoundCounts hasBoundCount(RowIndex ri) const { + Assert(d_variables.boundsQueueEmpty()); + return d_btracking[ri].hasBounds(); + } + +#warning "Remove legacy code" 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); } @@ -606,8 +616,10 @@ public: return minimallyWeakConflict(false, conflictVar); } + DeltaRational computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const; + private: - DeltaRational computeBound(ArithVar basic, bool upperBound); + DeltaRational computeBound(ArithVar basic, bool upperBound) const; public: void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult); diff --git a/src/theory/arith/options b/src/theory/arith/options index 977d6cb32..cf0782a92 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -91,4 +91,7 @@ option fancyFinal --fancy-final bool :default false :read-write option exportDioDecompositions --dio-decomps bool :default false :read-write Let skolem variables for integer divisibility constraints leak from the dio solver. +option newProp --new-prop bool :default false :read-write + Use the new row propagation system + endmodule diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index b1c8d1b64..3fae3751c 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -524,8 +524,12 @@ BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const { } } +bool ArithVariables::boundsQueueEmpty() const { + return d_boundsQueue.empty(); +} + void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){ - while(!d_boundsQueue.empty()){ + while(!boundsQueueEmpty()){ ArithVar v = d_boundsQueue.back(); BoundsInfo prev = d_boundsQueue[v]; d_boundsQueue.pop_back(); diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index f937fc241..953c8c0d3 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -403,6 +403,7 @@ public: BoundsInfo selectBoundsInfo(ArithVar v, bool old) const; + bool boundsQueueEmpty() const; void processBoundsQueue(BoundUpdateCallback& changed); void printEntireModel(std::ostream& out) const; diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 8b6ef1df6..deed7e7be 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -72,8 +72,12 @@ public: return getColumn(x).begin(); } + RowIterator ridRowIterator(RowIndex rid) const { + return getRow(rid).begin(); + } + RowIterator basicRowIterator(ArithVar basic) const { - return getRow(basicToRowIndex(basic)).begin(); + return ridRowIterator(basicToRowIndex(basic)); } const Entry& basicFindEntry(ArithVar basic, ArithVar col) const { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index c39dab3cb..5b40e03bc 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -489,9 +489,7 @@ bool TheoryArithPrivate::AssertUpper(Constraint constraint){ }else if(!lb->negationHasProof()){ Constraint negLb = lb->getNegation(); negLb->impliedBy(constraint, diseq); - //if(!negLb->canBePropagated()){ d_learnedBounds.push_back(negLb); - //}//otherwise let this be propagated/asserted later } } } @@ -1187,70 +1185,19 @@ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool slack){ Assert(!d_partialModel.hasArithVar(x)); Assert(x.getType().isReal()); // real or integer - // ArithVar varX = d_variables.size(); - // d_variables.push_back(Node(x)); - ArithVar max = d_partialModel.getNumberOfVariables(); ArithVar varX = d_partialModel.allocate(x, slack); bool reclaim = max >= d_partialModel.getNumberOfVariables();; - if(reclaim){ - // varX = d_pool.back(); - // d_pool.pop_back(); - - // d_partialModel.setAssignment(varX, d_DELTA_ZERO, d_DELTA_ZERO); - }else{ - // varX = d_numberOfVariables; - // ++d_numberOfVariables; - - // d_slackVars.push_back(true); - // d_variableTypes.push_back(ATReal); - + if(!reclaim){ d_dualSimplex.increaseMax(); d_tableau.increaseSize(); d_tableauSizeHasBeenModified = true; - - //d_partialModel.initialize(varX, d_DELTA_ZERO); } - - // ArithType type; - // if(slack){ - // //The type computation is not quite accurate for Rationals that are integral. - // //We'll use the isIntegral check from the polynomial package instead. - // Polynomial p = Polynomial::parsePolynomial(x); - // type = p.isIntegral() ? ATInteger : ATReal; - // }else{ - // type = nodeToArithType(x); - // } - // d_variableTypes[varX] = type; - // d_slackVars[varX] = slack; - d_constraintDatabase.addVariable(varX); - //d_partialModel.setArithVar(x,varX); - - // Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl; - - // if(slack){ - // //The type computation is not quite accurate for Rationals that are integral. - // //We'll use the isIntegral check from the polynomial package instead. - // Polynomial p = Polynomial::parsePolynomial(x); - // d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal); - // }else{ - // d_variableTypes.push_back(nodeToArithType(x)); - // } - - // d_slackVars.push_back(slack); - - // d_simplex.increaseMax(); - - // d_tableau.increaseSize(); - // d_tableauSizeHasBeenModified = true; - - // d_constraintDatabase.addVariable(varX); - Debug("arith::arithvar") << x << " |-> " << varX << endl; Assert(!d_partialModel.hasUpperBound(varX)); @@ -2160,7 +2107,11 @@ void TheoryArithPrivate::propagate(Theory::Effort e) { (options::arithPropagationMode() == BOUND_INFERENCE_PROP || options::arithPropagationMode() == BOTH_PROP) && hasAnyUpdates()){ - propagateCandidates(); + if(options::newProp()){ + propagateCandidatesNew(); + }else{ + propagateCandidates(); + } }else{ clearUpdates(); } @@ -2597,6 +2548,9 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound } // I think this can be skipped if canBePropagated is true //d_learnedBounds.push(bestImplied); + cout << "success " << bestImplied << endl; + d_partialModel.printModel(basic, cout); + return true; } cout << "failed " << basic << " " << bound << assertedToTheTheory << " " << @@ -2612,10 +2566,10 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound void TheoryArithPrivate::propagateCandidate(ArithVar basic){ bool success = false; - if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasLowerBounds(basic)){ + if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasBounds(basic, false)){ success |= propagateCandidateLowerBound(basic); } - if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasUpperBounds(basic)){ + if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasBounds(basic, true)){ success |= propagateCandidateUpperBound(basic); } if(success){ @@ -2626,6 +2580,8 @@ void TheoryArithPrivate::propagateCandidate(ArithVar basic){ void TheoryArithPrivate::propagateCandidates(){ TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime); + cout << "propagateCandidates begin" << endl; + Assert(d_candidateBasics.empty()); if(d_updatedBounds.empty()){ return; } @@ -2659,6 +2615,7 @@ void TheoryArithPrivate::propagateCandidates(){ Assert(d_tableau.isBasic(candidate)); propagateCandidate(candidate); } + cout << "propagateCandidates end" << endl << endl << endl; } void TheoryArithPrivate::propagateCandidatesNew(){ @@ -2675,6 +2632,207 @@ void TheoryArithPrivate::propagateCandidatesNew(){ * 4: The implied bound on x is strictly smaller/greater than the current bound. * (This is O(n) to compute.) */ + + TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime); + cout << "propagateCandidatesNew begin" << endl; + + Assert(d_qflraStatus == Result::SAT); + if(d_updatedBounds.empty()){ return; } + dumpUpdatedBoundsToRows(); + Assert(d_updatedBounds.empty()); + + if(!d_candidateRows.empty()){ + UpdateTrackingCallback utcb(&d_linEq); + d_partialModel.processBoundsQueue(utcb); + } + + while(!d_candidateRows.empty()){ + RowIndex candidate = d_candidateRows.back(); + d_candidateRows.pop_back(); + propagateCandidateRow(candidate); + } + cout << "propagateCandidatesNew end" << endl << endl << endl; +} + +bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{ + int cmp = ub ? d_partialModel.cmpAssignmentUpperBound(v) + : d_partialModel.cmpAssignmentLowerBound(v); + bool hasSlack = ub ? cmp < 0 : cmp > 0; + if(hasSlack){ + ConstraintType t = ub ? UpperBound : LowerBound; + const DeltaRational& a = d_partialModel.getAssignment(v); + + return NullConstraint != d_constraintDatabase.getBestImpliedBound(v, t, a); + }else{ + return false; + } +} + +bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){ + cout << " attemptSingleton" << ridx; + + const Tableau::Entry* ep; + ep = d_linEq.rowLacksBound(ridx, rowUp, ARITHVAR_SENTINEL); + Assert(ep != NULL); + + ArithVar v = ep->getColVar(); + const Rational& coeff = ep->getCoefficient(); + + // 0 = c * v + \sum rest + // Suppose rowUp + // - c * v = \sum rest \leq D + // if c > 0, v \geq -D/c so !vUp + // if c < 0, v \leq -D/c so vUp + // Suppose not rowUp + // - c * v = \sum rest \geq D + // if c > 0, v \leq -D/c so vUp + // if c < 0, v \geq -D/c so !vUp + bool vUp = (rowUp == ( coeff.sgn() < 0)); + + cout << " " << rowUp << " " << v << " " << coeff << " " << vUp << endl; + cout << " " << propagateMightSucceed(v, vUp) << endl; + + if(propagateMightSucceed(v, vUp)){ + DeltaRational dr = d_linEq.computeRowBound(ridx, rowUp, v); + DeltaRational bound = dr / (- coeff); + return tryToPropagate(ridx, rowUp, v, vUp, bound); + } + return false; +} + +bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){ + cout << " attemptFull" << ridx << endl; + + vector candidates; + + for(Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i){ + const Tableau::Entry& e =*i; + const Rational& c = e.getCoefficient(); + ArithVar v = e.getColVar(); + bool vUp = (rowUp == (c.sgn() < 0)); + if(propagateMightSucceed(v, vUp)){ + candidates.push_back(&e); + } + } + if(candidates.empty()){ return false; } + + const DeltaRational slack = + d_linEq.computeRowBound(ridx, rowUp, ARITHVAR_SENTINEL); + bool any = false; + vector::const_iterator i, iend; + for(i = candidates.begin(), iend = candidates.end(); i != iend; ++i){ + const Tableau::Entry* ep = *i; + const Rational& c = ep->getCoefficient(); + ArithVar v = ep->getColVar(); + + // See the comment for attemptSingleton() + bool activeUp = (rowUp == (c.sgn() > 0)); + bool vUb = (rowUp == (c.sgn() < 0)); + + const DeltaRational& activeBound = activeUp ? + d_partialModel.getUpperBound(v): + d_partialModel.getLowerBound(v); + + DeltaRational contribution = activeBound * c; + DeltaRational impliedBound = (slack - contribution)/(-c); + + bool success = tryToPropagate(ridx, rowUp, v, vUb, impliedBound); + if(success){ + cout << " success " << v << endl; + }else{ + cout << " fail " << v << endl; + } + any |= success; + } + return any; +} + +bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, bool vUb, const DeltaRational& bound){ + + bool weaker = vUb ? d_partialModel.strictlyLessThanUpperBound(v, bound): + d_partialModel.strictlyGreaterThanLowerBound(v, bound); + if(weaker){ + ConstraintType t = vUb ? UpperBound : LowerBound; + Constraint implied = d_constraintDatabase.getBestImpliedBound(v, t, bound); + if(implied != NullConstraint){ + return rowImplicationCanBeApplied(ridx, rowUp, implied); + } + } + return false; +} + +bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, Constraint implied){ + Assert(implied != NullConstraint); + ArithVar v = implied->getVariable(); + + bool assertedToTheTheory = implied->assertedToTheTheory(); + bool canBePropagated = implied->canBePropagated(); + bool hasProof = implied->hasProof(); + + Debug("arith::prop") << "arith::prop" << v + << " " << assertedToTheTheory + << " " << canBePropagated + << " " << hasProof + << endl; + + if(implied->negationHasProof()){ + Warning() << "the negation of " << implied << " : " << endl + << "has proof " << implied->getNegation() << endl + << implied->getNegation()->explainForConflict() << endl; + } + + if(!assertedToTheTheory && canBePropagated && !hasProof ){ + d_linEq.propagateRow(ridx, rowUp, implied); + return true; + } + cout << "failed " << v << " " << assertedToTheTheory << " " << + canBePropagated << " " << hasProof << " " << implied << endl; + d_partialModel.printModel(v, cout); + return false; +} + +bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){ + BoundCounts hasCount = d_linEq.hasBoundCount(ridx); + uint32_t rowLength = d_tableau.getRowLength(ridx); + + bool success = false; + static int instance = 0; + ++instance; + cout << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl; + + if(hasCount.lowerBoundCount() == rowLength){ + success |= attemptFull(ridx, false); + }else if(hasCount.lowerBoundCount() + 1 == rowLength){ + success |= attemptSingleton(ridx, false); + } + + if(hasCount.upperBoundCount() == rowLength){ + success |= attemptFull(ridx, true); + }else if(hasCount.upperBoundCount() + 1 == rowLength){ + success |= attemptSingleton(ridx, true); + } + return success; +} + +void TheoryArithPrivate::dumpUpdatedBoundsToRows(){ + Assert(d_candidateRows.empty()); + DenseSet::const_iterator i = d_updatedBounds.begin(); + DenseSet::const_iterator end = d_updatedBounds.end(); + for(; i != end; ++i){ + ArithVar var = *i; + if(d_tableau.isBasic(var)){ + RowIndex ridx = d_tableau.basicToRowIndex(var); + d_candidateRows.softAdd(ridx); + }else{ + Tableau::ColIterator basicIter = d_tableau.colIterator(var); + for(; !basicIter.atEnd(); ++basicIter){ + const Tableau::Entry& entry = *basicIter; + RowIndex ridx = entry.getRowIndex(); + d_candidateRows.softAdd(ridx); + } + } + } + d_updatedBounds.purge(); } }/* CVC4::theory::arith namespace */ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 4de562d0a..e522bb8c8 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -463,6 +463,7 @@ private: /** Tracks the basic variables where propagation might be possible. */ DenseSet d_candidateBasics; + DenseSet d_candidateRows; bool hasAnyUpdates() { return !d_updatedBounds.empty(); } void clearUpdates(); @@ -470,6 +471,16 @@ private: void revertOutOfConflict(); void propagateCandidatesNew(); + void dumpUpdatedBoundsToRows(); + bool propagateCandidateRow(RowIndex rid); + bool propagateMightSucceed(ArithVar v, bool ub) const; + /** Attempt to perform a row propagation where there is at most 1 possible variable.*/ + bool attemptSingleton(RowIndex ridx, bool rowUp); + /** Attempt to perform a row propagation where every variable is a potential candidate.*/ + bool attemptFull(RowIndex ridx, bool rowUp); + bool tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, bool vUp, const DeltaRational& bound); + bool rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, Constraint bestImplied); + void propagateCandidates(); void propagateCandidate(ArithVar basic);