diff options
author | Tim King <taking@cs.nyu.edu> | 2014-03-07 18:00:37 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2014-03-07 18:00:52 -0500 |
commit | 9ccdea06edbc72e3ecd282e9e015f6fc4b2e7173 (patch) | |
tree | cde6138cb9ab6ef0b7c15edf42e3e8cc53637002 /src/util | |
parent | 42be934ef4d4430944ae9074c7202a7d130c75bb (diff) |
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.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/rational_cln_imp.cpp | 54 | ||||
-rw-r--r-- | src/util/rational_cln_imp.h | 19 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.cpp | 51 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.h | 20 |
4 files changed, 132 insertions, 12 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()); +} 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 { diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index d496803dc..25c7dab59 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -17,6 +17,8 @@ #include "cvc4autoconfig.h" #include "util/rational.h" #include <string> +#include <sstream> +#include <cmath> #ifndef CVC4_GMP_IMP # error "This source should only ever be built if CVC4_GMP_IMP is on !" @@ -50,3 +52,52 @@ 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); + } +} + + +/** Return an exact rational for a double d. */ +Rational Rational::fromDouble(double d) throw(RationalFromDoubleException){ + if(std::isfinite(d)){ + Rational q; + mpq_set_d(q.d_value.get_mpq_t(), d); + return q; + } + + throw RationalFromDoubleException(d); +} + +RationalFromDoubleException::RationalFromDoubleException(double d) throw() + : Exception() +{ + std::stringstream ss; + ss << "RationalFromDoubleException("; + ss << d; + ss << ")"; + setMessage(ss.str()); +} diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 02ccc273c..273b3072d 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -28,6 +28,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, @@ -172,12 +177,7 @@ public: return Integer(d_value.get_den()); } - /** Return an exact rational for a double d. */ - static Rational fromDouble(double d){ - Rational q; - mpq_set_d(q.d_value.get_mpq_t(), d); - return q; - } + static Rational fromDouble(double d) throw(RationalFromDoubleException); /** * Get a double representation of this Rational, which is @@ -234,6 +234,10 @@ public: return Integer(q); } + Rational floor_frac() const { + return (*this) - Rational(floor()); + } + Rational& operator=(const Rational& x){ if(this == &x) return *this; d_value = x.d_value; @@ -326,6 +330,10 @@ public: uint32_t denLen = getDenominator().length(); return numLen + denLen; } + + /** Equivalent to calling (this->abs()).cmp(b.abs()) */ + int absCmp(const Rational& q) const; + };/* class Rational */ struct RationalHashFunction { |