Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.

1 files changed, 13 insertions, 6 deletions

diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index da2af6c1f..b144ab419 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -38,6 +38,11 @@
 
 namespace CVC4 {
 
+class CVC4_PUBLIC RationalFromDoubleException : public Exception {
+public:
+  RationalFromDoubleException(double d) throw();
+};
+
 /**
  ** A multi-precision rational constant.
  ** This stores the rational as a pair of multi-precision integers,
@@ -189,12 +194,7 @@ public:
   }
 
   /** Return an exact rational for a double d. */
-  static Rational fromDouble(double d){
-    cln::cl_DF fromD = d;
-    Rational q;
-    q.d_value = cln::rationalize(fromD);
-    return q;
-  }
+  static Rational fromDouble(double d) throw(RationalFromDoubleException);
 
   /**
    * Get a double representation of this Rational, which is
@@ -259,6 +259,10 @@ public:
     return Integer(cln::ceiling1(d_value));
   }
 
+  Rational floor_frac() const {
+    return (*this) - Rational(floor());
+  }
+
   Rational& operator=(const Rational& x){
     if(this == &x) return *this;
     d_value = x.d_value;
@@ -349,6 +353,9 @@ public:
     return getNumerator().length() + getDenominator().length();
   }
 
+  /** Equivalent to calling (this->abs()).cmp(b.abs()) */
+  int absCmp(const Rational& q) const;
+
 };/* class Rational */
 
 struct RationalHashFunction {