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.

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