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, 32 insertions, 0 deletions

diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index fdc3bee3b..682d13720 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -118,6 +118,38 @@ public:
     return *(this);
   }
 
+  bool isIntegral() const {
+    if(getInfinitesimalPart().sgn() == 0){
+      return getNoninfinitesimalPart().isIntegral();
+    }else{
+      return false;
+    }
+  }
+
+  Integer floor() const {
+    if(getNoninfinitesimalPart().isIntegral()){
+      if(getInfinitesimalPart().sgn() >= 0){
+        return getNoninfinitesimalPart().getNumerator();
+      }else{
+        return getNoninfinitesimalPart().getNumerator() - Integer(1);
+      }
+    }else{
+      return getNoninfinitesimalPart().floor();
+    }
+  }
+
+  Integer ceiling() const {
+    if(getNoninfinitesimalPart().isIntegral()){
+      if(getInfinitesimalPart().sgn() <= 0){
+        return getNoninfinitesimalPart().getNumerator();
+      }else{
+        return getNoninfinitesimalPart().getNumerator() + Integer(1);
+      }
+    }else{
+      return getNoninfinitesimalPart().ceiling();
+    }
+  }
+
   std::string toString() const;
 
 };