summaryrefslogtreecommitdiff
path: root/src/theory/arith/partial_model.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/partial_model.h')
-rw-r--r--src/theory/arith/partial_model.h9
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 518d59fbd..2edfdebca 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -88,6 +88,7 @@ public:
/* Gets the last assignment to a variable that is known to be conistent. */
const DeltaRational& getSafeAssignment(ArithVar x) const;
+ const DeltaRational& getAssignment(ArithVar x, bool safe) const;
/* Reverts all variable assignments to their safe values. */
void revertAssignmentChanges();
@@ -131,7 +132,13 @@ public:
void printModel(ArithVar x);
/** returns true iff x has both a lower and upper bound. */
- bool hasBounds(ArithVar x);
+ bool hasEitherBound(ArithVar x);
+ inline bool hasLowerBound(ArithVar x){
+ return !d_lowerConstraint[x].isNull();
+ }
+ inline bool hasUpperBound(ArithVar x){
+ return !d_upperConstraint[x].isNull();
+ }
bool hasEverHadABound(ArithVar var){
return d_hasHadABound[var];
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback