diff options
author | Tim King <taking@cs.nyu.edu> | 2018-01-07 16:46:16 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-07 16:46:16 -0800 |
commit | 20957db27201d594a83e0e5abe77875ed4932faf (patch) | |
tree | 47c665493a2a26d9ad50d2f53de310a7ce8193e0 /src/util | |
parent | 8497910df4d1c254b26f09c3dc5ee6191c970b12 (diff) |
Removes RationalFromDoubleException. Replaces this with an explicit M… (#1476)
* Removes RationalFromDoubleException. Replaces this with an explicit Maybe<Rational> datatype. Makes Maybe<T> CVC4_PUBLIC. Updates the users of Rational::fromDouble(). Miscellaneous cleanup of ApproxSimplex.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/maybe.h | 35 | ||||
-rw-r--r-- | src/util/rational.i | 2 | ||||
-rw-r--r-- | src/util/rational_cln_imp.cpp | 20 | ||||
-rw-r--r-- | src/util/rational_cln_imp.h | 8 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.cpp | 16 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.h | 8 |
6 files changed, 32 insertions, 57 deletions
diff --git a/src/util/maybe.h b/src/util/maybe.h index b2c8b9797..f27f320ae 100644 --- a/src/util/maybe.h +++ b/src/util/maybe.h @@ -22,9 +22,10 @@ ** Nothing using a value of T ** - High level of assurance that a value is not used before it is set. **/ -#include "cvc4_private.h" +#include "cvc4_public.h" -#pragma once +#ifndef __CVC4__UTIL__MAYBE_H +#define __CVC4__UTIL__MAYBE_H #include <ostream> @@ -33,12 +34,9 @@ namespace CVC4 { template <class T> -class Maybe { -private: - bool d_just; - T d_value; - -public: +class CVC4_PUBLIC Maybe +{ + public: Maybe() : d_just(false), d_value(){} Maybe(const T& val): d_just(true), d_value(val){} @@ -50,6 +48,7 @@ public: inline bool nothing() const { return !d_just; } inline bool just() const { return d_just; } + explicit operator bool() const noexcept { return just(); } void clear() { if(just()){ @@ -58,16 +57,18 @@ public: } } - T& value() { - Assert(just(), "Maybe::value() requires the maybe to be set."); - return d_value; - } - const T& constValue() const { - Assert(just(), "Maybe::constValue() requires the maybe to be set."); + const T& value() const + { + if (nothing()) + { + throw Exception("Maybe::value() requires the maybe to be set."); + } return d_value; } - operator const T&() const { return constValue(); } + private: + bool d_just; + T d_value; }; template <class T> @@ -77,10 +78,12 @@ inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){ out << "Nothing"; }else{ out << "Just "; - out << m.constValue(); + out << m.value(); } out << "}"; return out; } }/* CVC4 namespace */ + +#endif /* __CVC4__UTIL__MAYBE_H */ diff --git a/src/util/rational.i b/src/util/rational.i index a9e3e23f8..a65c78327 100644 --- a/src/util/rational.i +++ b/src/util/rational.i @@ -2,8 +2,6 @@ #include "util/rational.h" %} -%ignore CVC4::RationalFromDoubleException::RationalFromDoubleException(double); - %ignore CVC4::Rational::Rational(int); %ignore CVC4::Rational::Rational(unsigned int); %ignore CVC4::Rational::Rational(int, int); diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 09e3c8168..6250cbccd 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -84,29 +84,21 @@ int Rational::absCmp(const Rational& q) const{ } } -Rational Rational::fromDouble(double d) throw(RationalFromDoubleException){ +Maybe<Rational> Rational::fromDouble(double d) +{ 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); + return Maybe<Rational>(); }catch(cln::floating_point_nan_exception& fpne){ - throw RationalFromDoubleException(d); + return Maybe<Rational>(); }catch(cln::floating_point_overflow_exception& fpoe){ - throw RationalFromDoubleException(d); + return Maybe<Rational>(); } -} - -RationalFromDoubleException::RationalFromDoubleException(double d) throw() - : Exception() -{ - std::stringstream ss; - ss << "RationalFromDoubleException("; - ss << d; - ss << ")"; - setMessage(ss.str()); + Unreachable(); } } /* namespace CVC4 */ diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index bdfff9875..0b09bf1fd 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -35,14 +35,10 @@ #include "base/exception.h" #include "util/integer.h" +#include "util/maybe.h" 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, @@ -201,7 +197,7 @@ public: } /** Return an exact rational for a double d. */ - static Rational fromDouble(double d) throw(RationalFromDoubleException); + static Maybe<Rational> fromDouble(double d); /** * Get a double representation of this Rational, which is diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index 527222f7a..40c9c35f3 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -87,25 +87,15 @@ int Rational::absCmp(const Rational& q) const{ /** Return an exact rational for a double d. */ -Rational Rational::fromDouble(double d) throw(RationalFromDoubleException){ +Maybe<Rational> Rational::fromDouble(double d) +{ using namespace std; if(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()); + return Maybe<Rational>(); } } /* namespace CVC4 */ diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 70146561d..7c17ead15 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -32,14 +32,10 @@ #include "base/exception.h" #include "util/integer.h" +#include "util/maybe.h" 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, @@ -192,7 +188,7 @@ public: return Integer(d_value.get_den()); } - static Rational fromDouble(double d) throw(RationalFromDoubleException); + static Maybe<Rational> fromDouble(double d); /** * Get a double representation of this Rational, which is |