diff options
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: /** |