diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-04 03:03:34 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-04 03:03:34 +0000 |
commit | 3d1c57e0506b2454aa815c3c1cb634d96ade1d7c (patch) | |
tree | 1805ae7dae1f9e9b04c2d344ce252a969fc4e7a8 /src/theory/arith/linear_equality.cpp | |
parent | 1433806056059339dd16ae8e431feaae23553150 (diff) |
- This fixes a problem where simplex produced the same conflict in the single check call.
- This increases the number of substitutions that ppAssert can solve on integer equations.
Diffstat (limited to 'src/theory/arith/linear_equality.cpp')
-rw-r--r-- | src/theory/arith/linear_equality.cpp | 16 |
1 files changed, 2 insertions, 14 deletions
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 964d27464..7efe349e5 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -257,7 +257,7 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ Assert(d_tableau.isBasic(basic)); Assert(c->getVariable() == basic); Assert(!c->assertedToTheTheory()); - Assert(c->canBePropagated()); + //Assert(c->canBePropagated()); Assert(!c->hasProof()); Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" @@ -279,35 +279,23 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ if(upperBound){ if(sgn < 0){ bound = d_partialModel.getLowerBoundConstraint(nonbasic); - //d_partialModel.explainLowerBound(nonbasic, output); - //bound = d_partialModel.explainLowerBound(nonbasic); }else{ Assert(sgn > 0); bound = d_partialModel.getUpperBoundConstraint(nonbasic); - //d_partialModel.explainUpperBound(nonbasic, output); - //bound = d_partialModel.explainUpperBound(nonbasic); } }else{ if(sgn < 0){ bound = d_partialModel.getUpperBoundConstraint(nonbasic); - //d_partialModel.explainUpperBound(nonbasic, output); - //bound = d_partialModel.explainUpperBound(nonbasic); }else{ Assert(sgn > 0); bound = d_partialModel.getLowerBoundConstraint(nonbasic); - //d_partialModel.explainLowerBound(nonbasic, output); - //bound = d_partialModel.explainLowerBound(nonbasic); } } Assert(bound != NullConstraint); Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl; bounds.push_back(bound); - //Assert(!bound.isNull()); - // Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound - // << endl; - // output << bound; } - c->propagate(bounds); + c->impliedBy(bounds); Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" << basic << ") done" << endl; } |