diff options
author | Tim King <taking@cs.nyu.edu> | 2011-11-29 21:11:45 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-11-29 21:11:45 +0000 |
commit | e9198d9b99c6037165362870436b45826674303f (patch) | |
tree | b5e8d01a53d38d353dae7c16351ff9206e1f96c6 /src/theory/arith/partial_model.cpp | |
parent | 8b202bab8442c927e9ac18a35c71a82444acf63b (diff) |
Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.
Diffstat (limited to 'src/theory/arith/partial_model.cpp')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index ed8f837d1..73f80a70d 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -27,19 +27,52 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; + + +void ArithPartialModel::zeroDifferenceDetected(ArithVar x){ + Assert(d_dm.isDifferenceSlack(x)); + Assert(upperBoundIsZero(x)); + Assert(lowerBoundIsZero(x)); + + Node lb = getLowerConstraint(x); + Node ub = getUpperConstraint(x); + Node reason = lb != ub ? lb.andNode(ub) : lb; + d_dm.differenceIsZero(x, reason); +} + void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){ d_deltaIsSafe = false; Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl; d_hasHadABound[x] = true; d_upperBound.set(x,r); + + if(d_dm.isDifferenceSlack(x)){ + int sgn = r.sgn(); + if(sgn < 0){ + d_dm.differenceCannotBeZero(x, getUpperConstraint(x)); + }else if(sgn == 0 && lowerBoundIsZero(x)){ + zeroDifferenceDetected(x); + } + } } void ArithPartialModel::setLowerBound(ArithVar x, const DeltaRational& r){ d_deltaIsSafe = false; + Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl; d_hasHadABound[x] = true; d_lowerBound.set(x,r); + + + if(d_dm.isDifferenceSlack(x)){ + int sgn = r.sgn(); + if(sgn > 0){ + d_dm.differenceCannotBeZero(x, getLowerConstraint(x)); + }else if(sgn == 0 && upperBoundIsZero(x)){ + zeroDifferenceDetected(x); + } + } } void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){ |