This commit merges in branches/arithmetic/internalbb up to revision 2831. This is a significant refactoring of code.

- r2820
-- Refactors Simplex so that it does significantly fewer functions.
--  Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model.
-- Some of the code for propagation has moved to TheoryArith.
-r2826
-- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound().
- r2827
-- Adds isZero() to Rational. Adds cmp to DeltaRational.
- r2831
-- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp.
-- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases.

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