summaryrefslogtreecommitdiff
path: root/src/theory/arith/linear_equality.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/linear_equality.cpp')
-rw-r--r--src/theory/arith/linear_equality.cpp187
1 files changed, 159 insertions, 28 deletions
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 2aeee696e..bd252bf49 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -55,6 +55,10 @@ LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, Bou
d_basicVariableUpdates(f),
d_increasing(1),
d_decreasing(-1),
+ d_upperBoundDifference(),
+ d_lowerBoundDifference(),
+ d_one(1),
+ d_negOne(-1),
d_btracking(boundsTracking),
d_areTracking(false),
d_trackCallback(this)
@@ -505,40 +509,117 @@ void LinearEqualityModule::propagateBasicFromRow(ConstraintP c){
RowIndex ridx = d_tableau.basicToRowIndex(basic);
ConstraintCPVec bounds;
- propagateRow(bounds, ridx, upperBound, c);
- c->impliedBy(bounds);
+ RationalVectorP coeffs = NULLPROOF(new RationalVector());
+ propagateRow(bounds, ridx, upperBound, c, coeffs);
+ c->impliedByFarkas(bounds, coeffs, false);
+ c->tryToPropagate();
+
+ if(coeffs != RationalVectorPSentinel) { delete coeffs; }
}
-void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bool rowUp, ConstraintP c){
+/* An explanation of the farkas coefficients.
+ *
+ * We are proving c using the other variables on the row.
+ * The proof is in terms of the other constraints and the negation of c, ~c.
+ *
+ * A row has the form:
+ * sum a_i * x_i = 0
+ * or
+ * sx + sum r y + sum q z = 0
+ * where r > 0 and q < 0.
+ *
+ * If rowUp, we are proving c
+ * g = sum r u_y + sum q l_z
+ * and c is entailed by -sx <= g
+ * If !rowUp, we are proving c
+ * g = sum r l_y + sum q u_z
+ * and c is entailed by -sx >= g
+ *
+ * | s | c | ~c | u_i | l_i
+ * if rowUp | s > 0 | x >= -g/s | x < -g/s | a_i > 0 | a_i < 0
+ * if rowUp | s < 0 | x <= -g/s | x > -g/s | a_i > 0 | a_i < 0
+ * if !rowUp | s > 0 | x <= -g/s | x > -g/s | a_i < 0 | a_i > 0
+ * if !rowUp | s < 0 | x >= -g/s | x < -g/s | a_i < 0 | a_i > 0
+ *
+ *
+ * Thus we treat !rowUp as multiplying the row by -1 and rowUp as 1
+ * for the entire row.
+ */
+void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bool rowUp, ConstraintP c, RationalVectorP farkas){
Assert(!c->assertedToTheTheory());
Assert(c->canBePropagated());
Assert(!c->hasProof());
+ if(farkas != RationalVectorPSentinel){
+ Assert(farkas->empty());
+ farkas->push_back(Rational(0));
+ }
+
ArithVar v = c->getVariable();
- Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
- << v <<") start" << endl;
+ Debug("arith::propagateRow") << "LinearEqualityModule::propagateRow("
+ << ridx << ", " << rowUp << ", " << v << ") start" << endl;
+
+ const Rational& multiple = rowUp ? d_one : d_negOne;
+ Debug("arith::propagateRow") << "multiple: " << multiple << endl;
+
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);
- ConstraintCP bound = selectUb
- ? d_variables.getUpperBoundConstraint(nonbasic)
- : d_variables.getLowerBoundConstraint(nonbasic);
- Assert(bound != NullConstraint);
- Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
- into.push_back(bound);
+ Assert( nonbasic != v ||
+ ( rowUp && a_ij.sgn() > 0 && c->isLowerBound()) ||
+ ( rowUp && a_ij.sgn() < 0 && c->isUpperBound()) ||
+ (!rowUp && a_ij.sgn() > 0 && c->isUpperBound()) ||
+ (!rowUp && a_ij.sgn() < 0 && c->isLowerBound())
+ );
+
+ if(Debug.isOn("arith::propagateRow")){
+ if(nonbasic == v){
+ Debug("arith::propagateRow") << "(target) "
+ << rowUp << " "
+ << a_ij.sgn() << " "
+ << c->isLowerBound() << " "
+ << c->isUpperBound() << endl;
+
+ Debug("arith::propagateRow") << "(target) ";
+ }
+ Debug("arith::propagateRow") << "propagateRow " << a_ij << " * " << nonbasic ;
+ }
+
+ if(nonbasic == v){
+ if(farkas != RationalVectorPSentinel){
+ Assert(farkas->front().isZero());
+ Rational multAij = multiple * a_ij;
+ Debug("arith::propagateRow") << "("<<multAij<<") ";
+ farkas->front() = multAij;
+ }
+
+ Debug("arith::propagateRow") << c << endl;
+ }else{
+
+ ConstraintCP bound = selectUb
+ ? d_variables.getUpperBoundConstraint(nonbasic)
+ : d_variables.getLowerBoundConstraint(nonbasic);
+
+ if(farkas != RationalVectorPSentinel){
+ Rational multAij = multiple * a_ij;
+ Debug("arith::propagateRow") << "("<<multAij<<") ";
+ farkas->push_back(multAij);
+ }
+ Assert(bound != NullConstraint);
+ Debug("arith::propagateRow") << bound << endl;
+ into.push_back(bound);
+ }
}
- Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
- << v << ") done" << endl;
+ Debug("arith::propagateRow") << "LinearEqualityModule::propagateRow("
+ << ridx << ", " << rowUp << ", " << v << ") done" << endl;
+
}
ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic) const {
@@ -574,13 +655,13 @@ ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRatio
anyWeakening = true;
surplus = surplus - diff;
- Debug("weak") << "found:" << endl;
+ Debug("arith::weak") << "found:" << endl;
if(v == basic){
- Debug("weak") << " basic: ";
+ Debug("arith::weak") << " basic: ";
}
- Debug("weak") << " " << surplus << " "<< diff << endl
- << " " << bound << c << endl
- << " " << weakerBound << weaker << endl;
+ Debug("arith::weak") << " " << surplus << " "<< diff << endl
+ << " " << bound << c << endl
+ << " " << weakerBound << weaker << endl;
Assert(diff.sgn() > 0);
c = weaker;
@@ -591,9 +672,48 @@ ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRatio
return c;
}
-void LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, RaiseConflict& rc) const {
+/* An explanation of the farkas coefficients.
+ *
+ * We are proving a conflict on the basic variable x_b.
+ * If aboveUpper, then the conflict is with the constraint c : x_b <= u_b.
+ * If !aboveUpper, then the conflict is with the constraint c : x_b >= l_b.
+ *
+ * A row has the form:
+ * -x_b sum a_i * x_i = 0
+ * or
+ * -x_b + sum r y + sum q z = 0,
+ * x_b = sum r y + sum q z
+ * where r > 0 and q < 0.
+ *
+ *
+ * If !aboveUp, we are proving ~c: x_b < l_b
+ * g = sum r u_y + sum q l_z
+ * x_b <= g < l_b
+ * and ~c is entailed by x_b <= g
+ *
+ * If aboveUp, we are proving ~c : x_b > u_b
+ * g = sum r l_y + sum q u_z
+ * x_b >= g > u_b
+ * and ~c is entailed by x_b >= g
+ *
+ *
+ * | s | c | ~c | u_i | l_i
+ * if !aboveUp | s > 0 | x >= -g/s | x < -g/s | a_i > 0 | a_i < 0
+ * if !aboveUp | s < 0 | x <= -g/s | x > -g/s | a_i > 0 | a_i < 0
+ * if aboveUp | s > 0 | x <= -g/s | x > -g/s | a_i < 0 | a_i > 0
+ * if aboveUp | s < 0 | x >= -g/s | x < -g/s | a_i < 0 | a_i > 0
+ *
+ * Thus we treat aboveUp as multiplying the row by -1 and !aboveUp as 1
+ * for the entire row.
+ */
+ConstraintCP LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, FarkasConflictBuilder& fcs) const {
+ Assert(!fcs.underConstruction());
TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
+ Debug("arith::weak") << "LinearEqualityModule::minimallyWeakConflict("
+ << aboveUpper <<", "<< basicVar << ", ...) start" << endl;
+
+ const Rational& adjustSgn = aboveUpper ? d_negOne : d_one;
const DeltaRational& assignment = d_variables.getAssignment(basicVar);
DeltaRational surplus;
if(aboveUpper){
@@ -605,7 +725,7 @@ void LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basic
Assert(assignment < d_variables.getLowerBound(basicVar));
surplus = d_variables.getLowerBound(basicVar) - assignment;
}
-
+
bool anyWeakenings = false;
for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){
const Tableau::Entry& entry = *i;
@@ -613,18 +733,29 @@ void LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basic
const Rational& coeff = entry.getCoefficient();
bool weakening = false;
ConstraintP c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar);
- Debug("weak") << "weak : " << weakening << " "
- << c->assertedToTheTheory() << " "
- << d_variables.getAssignment(v) << " "
- << c << endl;
+ Debug("arith::weak") << "weak : " << weakening << " "
+ << c->assertedToTheTheory() << " "
+ << d_variables.getAssignment(v) << " "
+ << c << endl;
anyWeakenings = anyWeakenings || weakening;
- rc.addConstraint(c);
+ fcs.addConstraint(c, coeff, adjustSgn);
+ if(basicVar == v){
+ Assert(! c->negationHasProof() );
+ fcs.makeLastConsequent();
+ }
}
+ Assert(fcs.consequentIsSet());
+
+ ConstraintCP conflicted = fcs.commitConflict();
+
++d_statistics.d_weakeningAttempts;
if(anyWeakenings){
++d_statistics.d_weakeningSuccesses;
}
+ Debug("arith::weak") << "LinearEqualityModule::minimallyWeakConflict("
+ << aboveUpper <<", "<< basicVar << ", ...) done" << endl;
+ return conflicted;
}
ArithVar LinearEqualityModule::minVarOrder(ArithVar x, ArithVar y) const {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback