diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-29 22:01:30 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-29 22:01:30 +0000 |
commit | b1200db566d19132a3f0861eeef35f3c0aaa0a08 (patch) | |
tree | 9d7855232f833230ca5d92cb8948e5b894dff197 /src/theory/arith/partial_model.h | |
parent | 200a0b748085004595a948fdea7c73a5ab45bdcf (diff) |
This commit merges the decaying-rows branch into the main trunk.
Diffstat (limited to 'src/theory/arith/partial_model.h')
-rw-r--r-- | src/theory/arith/partial_model.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 0351abf9d..44631fdef 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -107,6 +107,9 @@ typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint; struct TheoryArithPropagatedID {}; typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated; +struct HasHadABoundID {}; +typedef expr::Attribute<HasHadABoundID, bool> HasHadABound; + }; /*namespace partial_model*/ @@ -152,11 +155,14 @@ public: + void setUpperBound(TNode x, const DeltaRational& r); void setLowerBound(TNode x, const DeltaRational& r); /* Sets an unsafe variable assignment */ void setAssignment(TNode x, const DeltaRational& r); + void setAssignment(TNode x, const DeltaRational& safe, const DeltaRational& r); + /** Must know that the bound exists before calling this! */ DeltaRational getUpperBound(TNode x) const; @@ -182,6 +188,11 @@ public: void printModel(TNode x); + bool hasBounds(TNode x); + bool hasEverHadABound(TNode var){ + return var.getAttribute(partial_model::HasHadABound()); + } + private: /** |