summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/rational_cln_imp.cpp54
-rw-r--r--src/util/rational_cln_imp.h19
-rw-r--r--src/util/rational_gmp_imp.cpp51
-rw-r--r--src/util/rational_gmp_imp.h20
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 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback