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, 62 insertions, 43 deletions

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 4a126ec55..f113c4d34 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -209,21 +209,52 @@ TNode ArithPartialModel::getUpperConstraint(ArithVar x){
   return d_upperConstraint[x];
 }
 
-
-
-bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){
+int ArithPartialModel::cmpToLowerBound(ArithVar x, const DeltaRational& c){
   if(!hasLowerBound(x)){
     // l = -\intfy
     // ? c < -\infty |-  _|_
-    return false;
+    return 1;
+  }else{
+    return c.cmp(d_lowerBound[x]);
   }
-  if(strict){
-    return c < d_lowerBound[x];
+}
+
+int ArithPartialModel::cmpToUpperBound(ArithVar x, const DeltaRational& c){
+  if(!hasUpperBound(x)){
+    //u = \intfy
+    // ? c > \infty |-  _|_
+    return -1;
   }else{
-    return c <= d_lowerBound[x];
+    return c.cmp(d_upperBound[x]);
   }
 }
 
+// bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){
+//   if(!hasLowerBound(x)){
+//     // l = -\intfy
+//     // ? c < -\infty |-  _|_
+//     return false;
+//   }
+//   if(strict){
+//     return c < d_lowerBound[x];
+//   }else{
+//     return c <= d_lowerBound[x];
+//   }
+// }
+
+// bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
+//   if(!hasUpperBound(x)){
+//     // u = \intfy
+//     // ? c > \infty |-  _|_
+//     return false;
+//   }
+//   if(strict){
+//     return c > d_upperBound[x];
+//   }else{
+//     return c >= d_upperBound[x];
+//   }
+// }
+
 bool ArithPartialModel::equalsLowerBound(ArithVar x, const DeltaRational& c){
   if(!hasLowerBound(x)){
     return false;
@@ -239,18 +270,6 @@ bool ArithPartialModel::equalsUpperBound(ArithVar x, const DeltaRational& c){
   }
 }
 
-bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
-  if(!hasUpperBound(x)){
-    // u = \intfy
-    // ? c > \infty |-  _|_
-    return false;
-  }
-  if(strict){
-    return c > d_upperBound[x];
-  }else{
-    return c >= d_upperBound[x];
-  }
-}
 bool ArithPartialModel::hasEitherBound(ArithVar x){
   return hasLowerBound(x) || hasUpperBound(x);
 }
@@ -271,35 +290,35 @@ bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
   return  d_lowerBound[x] < d_assignment[x];
 }
 
-/**
- * x <= u
- * ? c < u
- */
-bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){
-  Assert(inMaps(x));
-  if(!hasUpperBound(x)){ // u = \infty
-    return true;
-  }
-  return c < d_upperBound[x];
-}
-
-/**
- * x <= u
- * ? c < u
- */
-bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){
-  Assert(inMaps(x));
-  if(!hasLowerBound(x)){ // l = -\infty
-    return true;
-  }
-  return  d_lowerBound[x] < c;
-}
+// /**
+//  * x <= u
+//  * ? c < u
+//  */
+// bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){
+//   Assert(inMaps(x));
+//   if(!hasUpperBound(x)){ // u = \infty
+//     return true;
+//   }
+//   return c < d_upperBound[x];
+// }
+
+// /**
+//  * x <= u
+//  * ? c < u
+//  */
+// bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){
+//   Assert(inMaps(x));
+//   if(!hasLowerBound(x)){ // l = -\infty
+//     return true;
+//   }
+//   return  d_lowerBound[x] < c;
+// }
 
 bool ArithPartialModel::assignmentIsConsistent(ArithVar x){
   const DeltaRational& beta = getAssignment(x);
 
   //l_i <= beta(x_i) <= u_i
-  return  !belowLowerBound(x,beta,true) && !aboveUpperBound(x,beta,true);
+  return  cmpToLowerBound(x,beta) >= 0 && cmpToUpperBound(x,beta) <= 0;
 }