diff options
author | Tim King <taking@cs.nyu.edu> | 2011-04-18 16:48:52 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-04-18 16:48:52 +0000 |
commit | abe849b486ea3707fd51a612c7982554f3d6581f (patch) | |
tree | 8f3967f644f9098079c778dd60cf9feb36e1ab2b /src/theory/arith/partial_model.h | |
parent | b90081962840584bb9eeda368ea232a7d42a292b (diff) |
This commit merges the branch arithmetic/propagation-again into trunk.
- This adds code for bounds refinement, and conflict weakening.
- This adds util/boolean_simplification.h.
- This adds a propagation manager to theory of arithmetic.
- Propagation is disabled by default.
- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.
Diffstat (limited to 'src/theory/arith/partial_model.h')
-rw-r--r-- | src/theory/arith/partial_model.h | 31 |
1 files changed, 23 insertions, 8 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 2edfdebca..171c74942 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -48,8 +48,8 @@ private: context::CDVector<DeltaRational> d_upperBound; context::CDVector<DeltaRational> d_lowerBound; - context::CDVector<TNode> d_upperConstraint; - context::CDVector<TNode> d_lowerConstraint; + context::CDVector<Node> d_upperConstraint; + context::CDVector<Node> d_lowerConstraint; bool d_deltaIsSafe; Rational d_delta; @@ -68,10 +68,10 @@ public: d_hasSafeAssignment(), d_assignment(), d_safeAssignment(), - d_upperBound(c, false), - d_lowerBound(c, false), - d_upperConstraint(c,false), - d_lowerConstraint(c,false), + d_upperBound(c, true), + d_lowerBound(c, true), + d_upperConstraint(c,true), + d_lowerConstraint(c,true), d_deltaIsSafe(false), d_delta(-1,1), d_history() @@ -114,17 +114,32 @@ public: /** - * x <= l + * x >= l * ? c < l */ bool belowLowerBound(ArithVar x, const DeltaRational& c, bool strict); /** * x <= u - * ? c < u + * ? c > u */ bool aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict); + bool equalsLowerBound(ArithVar x, const DeltaRational& c); + bool equalsUpperBound(ArithVar x, const DeltaRational& c); + + /** + * x <= u + * ? c < u + */ + bool strictlyBelowUpperBound(ArithVar x, const DeltaRational& c); + + /** + * x <= u + * ? c < u + */ + bool strictlyAboveLowerBound(ArithVar x, const DeltaRational& c); + bool strictlyBelowUpperBound(ArithVar x); bool strictlyAboveLowerBound(ArithVar x); bool assignmentIsConsistent(ArithVar x); |