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;
/**
* 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);
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 <bool upperBound>
void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
Assert(d_tableau.isBasic(basic));
<< 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<Constraint> 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();
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();
* 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();
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 <bool upperBound>
void propagateNonbasics(ArithVar basic, Constraint c);
void propagateNonbasicsUpperBound(ArithVar basic, Constraint c){
propagateNonbasics<true>(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
* - 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);
}
*/
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<true>(x_i, &LinearEqualityModule::noPreference);
}
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);
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
}
}
+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();
BoundsInfo selectBoundsInfo(ArithVar v, bool old) const;
+ bool boundsQueueEmpty() const;
void processBoundsQueue(BoundUpdateCallback& changed);
void printEntireModel(std::ostream& out) const;
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 {
}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
}
}
}
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));
(options::arithPropagationMode() == BOUND_INFERENCE_PROP ||
options::arithPropagationMode() == BOTH_PROP)
&& hasAnyUpdates()){
- propagateCandidates();
+ if(options::newProp()){
+ propagateCandidatesNew();
+ }else{
+ propagateCandidates();
+ }
}else{
clearUpdates();
}
}
// 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 << " " <<
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){
void TheoryArithPrivate::propagateCandidates(){
TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
+ cout << "propagateCandidates begin" << endl;
+
Assert(d_candidateBasics.empty());
if(d_updatedBounds.empty()){ return; }
Assert(d_tableau.isBasic(candidate));
propagateCandidate(candidate);
}
+ cout << "propagateCandidates end" << endl << endl << endl;
}
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<const Tableau::Entry*> 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 Tableau::Entry*>::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 */
/** Tracks the basic variables where propagation might be possible. */
DenseSet d_candidateBasics;
+ DenseSet d_candidateRows;
bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
void clearUpdates();
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);
projects / cvc5.git / commitdiff