Partial merge of integers work; this is simple B&B and some pseudoboolean

infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.

1 files changed, 8 insertions, 3 deletions

diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index c05d47175..b97484ff1 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -192,6 +192,14 @@ public:
     }
   }
 
+  Integer floor() const {
+    return Integer(cln::floor1(d_value));
+  }
+
+  Integer ceiling() const {
+    return Integer(cln::ceiling1(d_value));
+  }
+
   Rational& operator=(const Rational& x){
     if(this == &x) return *this;
     d_value = x.d_value;
@@ -226,9 +234,6 @@ public:
     return d_value >= y.d_value;
   }
 
-
-  
-
   Rational operator+(const Rational& y) const{
     return Rational( d_value + y.d_value );
   }