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.h | |
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.h')
-rw-r--r-- | src/theory/arith/partial_model.h | 55 |
1 files changed, 37 insertions, 18 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index cf0fc7d4e..d9fa51d8d 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -132,33 +132,52 @@ public: const DeltaRational& getAssignment(ArithVar x) const; + bool equalsLowerBound(ArithVar x, const DeltaRational& c); + bool equalsUpperBound(ArithVar x, const DeltaRational& c); /** - * x >= l - * ? c < l + * If lowerbound > - \infty: + * return getAssignment(x).cmp(getLowerBound(x)) + * If lowerbound = - \infty: + * return 1 */ - bool belowLowerBound(ArithVar x, const DeltaRational& c, bool strict); + int cmpToLowerBound(ArithVar x, const DeltaRational& c); - /** - * x <= u - * ? c > u - */ - bool aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict); + inline bool strictlyLessThanLowerBound(ArithVar x, const DeltaRational& c){ + return cmpToLowerBound(x, c) < 0; + } + inline bool lessThanLowerBound(ArithVar x, const DeltaRational& c){ + return cmpToLowerBound(x, c) <= 0; + } - bool equalsLowerBound(ArithVar x, const DeltaRational& c); - bool equalsUpperBound(ArithVar x, const DeltaRational& c); + inline bool strictlyGreaterThanLowerBound(ArithVar x, const DeltaRational& c){ + return cmpToLowerBound(x, c) > 0; + } /** - * x <= u - * ? c < u + * If upperbound < \infty: + * return getAssignment(x).cmp(getUpperBound(x)) + * If upperbound = \infty: + * return -1 */ - bool strictlyBelowUpperBound(ArithVar x, const DeltaRational& c); + int cmpToUpperBound(ArithVar x, const DeltaRational& c); + + inline bool strictlyLessThanUpperBound(ArithVar x, const DeltaRational& c){ + return cmpToUpperBound(x, c) < 0; + } + + inline bool lessThanUpperBound(ArithVar x, const DeltaRational& c){ + return cmpToUpperBound(x, c) <= 0; + } + + inline bool strictlyGreaterThanUpperBound(ArithVar x, const DeltaRational& c){ + return cmpToUpperBound(x, c) > 0; + } + + inline bool greaterThanUpperBound(ArithVar x, const DeltaRational& c){ + return cmpToUpperBound(x, c) >= 0; + } - /** - * x <= u - * ? c < u - */ - bool strictlyAboveLowerBound(ArithVar x, const DeltaRational& c); bool strictlyBelowUpperBound(ArithVar x); bool strictlyAboveLowerBound(ArithVar x); |