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;
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){
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){
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){
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){
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.
BoundInfoMap& d_btracking;
bool d_areTracking;
-#warning "Remove legacy code"
- template <bool upperBound>
- void propagateNonbasics(ArithVar basic, Constraint c);
-
public:
- void propagateNonbasicsLowerBound(ArithVar basic, Constraint c){
- propagateNonbasics<false>(basic, c);
- }
- void propagateNonbasicsUpperBound(ArithVar basic, Constraint c){
- propagateNonbasics<true>(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.
*/
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
* 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<true>(x_i, &LinearEqualityModule::noPreference);
- }
- ArithVar _anySlackUpperBound(ArithVar x_i) const {
- return selectSlack<false>(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 {
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);
}
}
- // 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()){
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))){
}
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")){
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){
projects / cvc5.git / commitdiff