This commit merges into trunk the branch branches/arithmetic/integers2 from r2650 to r2779.

- This excludes revision 2777.  This revision had some strange performance implications and was delaying the merge.
- This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts.
- The DioSolver can be disabled at command line using --disable-dio-solver.
- This includes a number of changes to the arithmetic normal form.
- The Integer class features a number of new number theoretic function.
- This commit includes a few rather loud warning. I will do my best to take care of them today.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 73f80a70d..4a126ec55 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -28,6 +28,13 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
 
+bool ArithPartialModel::boundsAreEqual(ArithVar x){
+  if(hasLowerBound(x) && hasUpperBound(x)){
+    return d_upperBound[x] == d_lowerBound[x];
+  }else{
+    return false;
+  }
+}
 
 void ArithPartialModel::zeroDifferenceDetected(ArithVar x){
   Assert(d_dm.isDifferenceSlack(x));