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

diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 2b29ece22..f674481de 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -17,6 +17,7 @@
 #include "cvc4autoconfig.h"
 #include "util/rational.h"
 #include <string>
+#include <sstream>
 
 #ifndef CVC4_CLN_IMP
 #  error "This source should only ever be built if CVC4_CLN_IMP is on !"
@@ -50,3 +51,56 @@ std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
   return os << q.toString();
 }
 
+
+
+/** Equivalent to calling (this->abs()).cmp(b.abs()) */
+int Rational::absCmp(const Rational& q) const{
+  const Rational& r = *this;
+  int rsgn = r.sgn();
+  int qsgn = q.sgn();
+  if(rsgn == 0){
+    return (qsgn == 0) ? 0 : -1;
+  }else if(qsgn == 0){
+    Assert(rsgn != 0);
+    return 1;
+  }else if((rsgn > 0) && (qsgn > 0)){
+    return r.cmp(q);
+  }else if((rsgn < 0) && (qsgn < 0)){
+    // if r < q < 0, q.cmp(r) = +1, (r.abs()).cmp(q.abs()) = +1
+    // if q < r < 0, q.cmp(r) = -1, (r.abs()).cmp(q.abs()) = -1
+    // if q = r < 0, q.cmp(r) =  0, (r.abs()).cmp(q.abs()) =  0
+    return q.cmp(r);
+  }else if((rsgn < 0) && (qsgn > 0)){
+    Rational rpos = -r;
+    return rpos.cmp(q);
+  }else {
+    Assert(rsgn > 0 && (qsgn < 0));
+    Rational qpos = -q;
+    return r.cmp(qpos);
+  }
+}
+
+Rational Rational::fromDouble(double d) throw(RationalFromDoubleException){
+  try{
+    cln::cl_DF fromD = d;
+    Rational q;
+    q.d_value = cln::rationalize(fromD);
+    return q;
+  }catch(cln::floating_point_underflow_exception& fpue){
+    throw RationalFromDoubleException(d);
+  }catch(cln::floating_point_nan_exception& fpne){
+    throw RationalFromDoubleException(d);
+  }catch(cln::floating_point_overflow_exception& fpoe){
+    throw RationalFromDoubleException(d);
+  }
+}
+
+RationalFromDoubleException::RationalFromDoubleException(double d) throw()
+  : Exception()
+{
+  std::stringstream ss;
+  ss << "RationalFromDoubleException(";
+  ss << d;
+  ss << ")";
+  setMessage(ss.str());
+}