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);