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, 13 insertions, 5 deletions

diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 7af1b86df..167e0fc22 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -151,7 +151,7 @@ public:
    * Returns the value of denominator of the Rational.
    * Note that this makes a deep copy of the denominator.
    */
-  Integer getDenominator() const{
+  Integer getDenominator() const {
     return Integer(d_value.get_den());
   }
 
@@ -165,11 +165,22 @@ public:
     return mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t());
   }
 
-
   int sgn() const {
     return mpq_sgn(d_value.get_mpq_t());
   }
 
+  Integer floor() const {
+    mpz_class q;
+    mpz_fdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
+    return Integer(q);
+  }
+
+  Integer ceiling() const {
+    mpz_class q;
+    mpz_cdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
+    return Integer(q);
+  }
+
   Rational& operator=(const Rational& x){
     if(this == &x) return *this;
     d_value = x.d_value;
@@ -204,9 +215,6 @@ public:
     return d_value >= y.d_value;
   }
 
-
-  
-
   Rational operator+(const Rational& y) const{
     return Rational( d_value + y.d_value );
   }