diff options
author | Tim King <taking@cs.nyu.edu> | 2012-02-28 21:26:35 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-02-28 21:26:35 +0000 |
commit | eefe0b63e564320eb135eb66d6c02c9dc6e9e8de (patch) | |
tree | 14d9643427fadab3e1c064d5528fa02e46f6bef7 /src/theory/arith/partial_model.cpp | |
parent | 9450e5841a08db3a9529c25e03fc5cea16a8f1f5 (diff) |
This commit merges in branches/arithmetic/internalbb up to revision 2831. This is a significant refactoring of code.
- r2820
-- Refactors Simplex so that it does significantly fewer functions.
-- Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model.
-- Some of the code for propagation has moved to TheoryArith.
-r2826
-- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound().
- r2827
-- Adds isZero() to Rational. Adds cmp to DeltaRational.
- r2831
-- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp.
-- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases.
Diffstat (limited to 'src/theory/arith/partial_model.cpp')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 105 |
1 files changed, 62 insertions, 43 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 4a126ec55..f113c4d34 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -209,21 +209,52 @@ TNode ArithPartialModel::getUpperConstraint(ArithVar x){ return d_upperConstraint[x]; } - - -bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){ +int ArithPartialModel::cmpToLowerBound(ArithVar x, const DeltaRational& c){ if(!hasLowerBound(x)){ // l = -\intfy // ? c < -\infty |- _|_ - return false; + return 1; + }else{ + return c.cmp(d_lowerBound[x]); } - if(strict){ - return c < d_lowerBound[x]; +} + +int ArithPartialModel::cmpToUpperBound(ArithVar x, const DeltaRational& c){ + if(!hasUpperBound(x)){ + //u = \intfy + // ? c > \infty |- _|_ + return -1; }else{ - return c <= d_lowerBound[x]; + return c.cmp(d_upperBound[x]); } } +// bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){ +// if(!hasLowerBound(x)){ +// // l = -\intfy +// // ? c < -\infty |- _|_ +// return false; +// } +// if(strict){ +// return c < d_lowerBound[x]; +// }else{ +// return c <= d_lowerBound[x]; +// } +// } + +// bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){ +// if(!hasUpperBound(x)){ +// // u = \intfy +// // ? c > \infty |- _|_ +// return false; +// } +// if(strict){ +// return c > d_upperBound[x]; +// }else{ +// return c >= d_upperBound[x]; +// } +// } + bool ArithPartialModel::equalsLowerBound(ArithVar x, const DeltaRational& c){ if(!hasLowerBound(x)){ return false; @@ -239,18 +270,6 @@ bool ArithPartialModel::equalsUpperBound(ArithVar x, const DeltaRational& c){ } } -bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){ - if(!hasUpperBound(x)){ - // u = \intfy - // ? c > \infty |- _|_ - return false; - } - if(strict){ - return c > d_upperBound[x]; - }else{ - return c >= d_upperBound[x]; - } -} bool ArithPartialModel::hasEitherBound(ArithVar x){ return hasLowerBound(x) || hasUpperBound(x); } @@ -271,35 +290,35 @@ bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){ return d_lowerBound[x] < d_assignment[x]; } -/** - * x <= u - * ? c < u - */ -bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){ - Assert(inMaps(x)); - if(!hasUpperBound(x)){ // u = \infty - return true; - } - return c < d_upperBound[x]; -} - -/** - * x <= u - * ? c < u - */ -bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){ - Assert(inMaps(x)); - if(!hasLowerBound(x)){ // l = -\infty - return true; - } - return d_lowerBound[x] < c; -} +// /** +// * x <= u +// * ? c < u +// */ +// bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){ +// Assert(inMaps(x)); +// if(!hasUpperBound(x)){ // u = \infty +// return true; +// } +// return c < d_upperBound[x]; +// } + +// /** +// * x <= u +// * ? c < u +// */ +// bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){ +// Assert(inMaps(x)); +// if(!hasLowerBound(x)){ // l = -\infty +// return true; +// } +// return d_lowerBound[x] < c; +// } bool ArithPartialModel::assignmentIsConsistent(ArithVar x){ const DeltaRational& beta = getAssignment(x); //l_i <= beta(x_i) <= u_i - return !belowLowerBound(x,beta,true) && !aboveUpperBound(x,beta,true); + return cmpToLowerBound(x,beta) >= 0 && cmpToUpperBound(x,beta) <= 0; } |