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.

14 files changed, 241 insertions, 361 deletions

diff --git a/src/cvc4.i b/src/cvc4.i
index 2f7205b19..bc5f5fdfe 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -174,8 +174,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception;
 %typemap(throws) CVC4::parser::ParserException = CVC4::Exception;
 
-%typemap(throws) CVC4::RationalFromDoubleException = Exception;
-
 // Generate an error if the mapping from C++ CVC4 Exception to Java CVC4 Exception doesn't exist above
 %typemap(throws) SWIGTYPE, SWIGTYPE &, SWIGTYPE *, SWIGTYPE [], SWIGTYPE [ANY] %{
 #error "exception $1_type doesn't map to Java correctly---please edit src/cvc4.i and add it"
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 78b57d3f6..07cb6aca6 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -144,55 +144,15 @@ struct CutScratchPad {
     d_explanation.clear();
   }
 };
+
 ApproximateStatistics::ApproximateStatistics()
-  // : d_relaxCalls("z::approx::relaxCalls",0)
-  // ,  d_relaxUnknowns("z::approx::relaxUnknowns",0)
-  // ,  d_relaxFeasible("z::approx::relaxFeasible",0)
-  // ,  d_relaxInfeasible("z::approx::relaxInfeasible",0)
-  // ,  d_relaxPivotsExhausted("z::approx::relaxPivotsExhausted",0)
-  // ,  d_mipCalls("z::approx::mipCalls",0)
-  // ,  d_mipUnknowns("z::approx::mipUnknowns",0)
-  // ,  d_mipBingo("z::approx::mipBingo",0)
-  // ,  d_mipClosed("z::approx::mipClosed",0)
-  // ,  d_mipBranchesExhausted("z::approx::mipBranchesExhausted",0)
-  // ,  d_mipPivotsExhausted("z::approx::mipPivotsExhausted",0)
-  // ,  d_mipExecExhausted("z::approx::mipExecExhausted",0)
-  // ,  d_gmiGen("z::approx::gmiGen",0)
-  // ,  d_gmiReplay("z::approx::gmiReplay",0)
-  // ,  d_mipGen("z::approx::mipGen",0)
-  // ,  d_mipReplay("z::approx::mipReplay",0)
   :  d_branchMaxDepth("z::approx::branchMaxDepth",0)
   ,  d_branchesMaxOnAVar("z::approx::branchesMaxOnAVar",0)
-  //,  d_branchTotal("z::approx::branchTotal",0)
-  //,  d_branchCuts("z::approx::branchCuts",0)
-
   ,  d_gaussianElimConstructTime("z::approx::gaussianElimConstruct::time")
   ,  d_gaussianElimConstruct("z::approx::gaussianElimConstruct::calls",0)
   ,  d_averageGuesses("z::approx::averageGuesses")
 {
-  // smtStatisticsRegistry()->registerStat(&d_relaxCalls);
-  // smtStatisticsRegistry()->registerStat(&d_relaxUnknowns);
-  // smtStatisticsRegistry()->registerStat(&d_relaxFeasible);
-  // smtStatisticsRegistry()->registerStat(&d_relaxInfeasible);
-  // smtStatisticsRegistry()->registerStat(&d_relaxPivotsExhausted);
-
-  // smtStatisticsRegistry()->registerStat(&d_mipCalls);
-  // smtStatisticsRegistry()->registerStat(&d_mipUnknowns);
-  // smtStatisticsRegistry()->registerStat(&d_mipBingo);
-  // smtStatisticsRegistry()->registerStat(&d_mipClosed);
-  // smtStatisticsRegistry()->registerStat(&d_mipBranchesExhausted);
-  // smtStatisticsRegistry()->registerStat(&d_mipPivotsExhausted);
-  // smtStatisticsRegistry()->registerStat(&d_mipExecExhausted);
-
-
-  // smtStatisticsRegistry()->registerStat(&d_gmiGen);
-  // smtStatisticsRegistry()->registerStat(&d_gmiReplay);
-  // smtStatisticsRegistry()->registerStat(&d_mipGen);
-  // smtStatisticsRegistry()->registerStat(&d_mipReplay);
-
   smtStatisticsRegistry()->registerStat(&d_branchMaxDepth);
-  //smtStatisticsRegistry()->registerStat(&d_branchTotal);
-  //smtStatisticsRegistry()->registerStat(&d_branchCuts);
   smtStatisticsRegistry()->registerStat(&d_branchesMaxOnAVar);
 
   smtStatisticsRegistry()->registerStat(&d_gaussianElimConstructTime);
@@ -202,29 +162,7 @@ ApproximateStatistics::ApproximateStatistics()
 }
 
 ApproximateStatistics::~ApproximateStatistics(){
-  // smtStatisticsRegistry()->unregisterStat(&d_relaxCalls);
-  // smtStatisticsRegistry()->unregisterStat(&d_relaxUnknowns);
-  // smtStatisticsRegistry()->unregisterStat(&d_relaxFeasible);
-  // smtStatisticsRegistry()->unregisterStat(&d_relaxInfeasible);
-  // smtStatisticsRegistry()->unregisterStat(&d_relaxPivotsExhausted);
-
-  // smtStatisticsRegistry()->unregisterStat(&d_mipCalls);
-  // smtStatisticsRegistry()->unregisterStat(&d_mipUnknowns);
-  // smtStatisticsRegistry()->unregisterStat(&d_mipBingo);
-  // smtStatisticsRegistry()->unregisterStat(&d_mipClosed);
-  // smtStatisticsRegistry()->unregisterStat(&d_mipBranchesExhausted);
-  // smtStatisticsRegistry()->unregisterStat(&d_mipPivotsExhausted);
-  // smtStatisticsRegistry()->unregisterStat(&d_mipExecExhausted);
-
-
-  // smtStatisticsRegistry()->unregisterStat(&d_gmiGen);
-  // smtStatisticsRegistry()->unregisterStat(&d_gmiReplay);
-  // smtStatisticsRegistry()->unregisterStat(&d_mipGen);
-  // smtStatisticsRegistry()->unregisterStat(&d_mipReplay);
-
   smtStatisticsRegistry()->unregisterStat(&d_branchMaxDepth);
-  //smtStatisticsRegistry()->unregisterStat(&d_branchTotal);
-  //smtStatisticsRegistry()->unregisterStat(&d_branchCuts);
   smtStatisticsRegistry()->unregisterStat(&d_branchesMaxOnAVar);
 
   smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstructTime);
@@ -373,11 +311,17 @@ Rational ApproximateSimplex::estimateWithCFE(const Rational& r, const Integer& K
   }
 }
 
-Rational ApproximateSimplex::estimateWithCFE(double d, const Integer& D) throw (RationalFromDoubleException){
-  return estimateWithCFE(Rational::fromDouble(d), D);
+Maybe<Rational> ApproximateSimplex::estimateWithCFE(double d, const Integer& D)
+{
+  if (Maybe<Rational> from_double = Rational::fromDouble(d))
+  {
+    return estimateWithCFE(from_double.value(), D);
+  }
+  return Maybe<Rational>();
 }
 
-Rational ApproximateSimplex::estimateWithCFE(double d) throw (RationalFromDoubleException){
+Maybe<Rational> ApproximateSimplex::estimateWithCFE(double d)
+{
   return estimateWithCFE(d, s_defaultMaxDenom);
 }
 
@@ -388,42 +332,32 @@ public:
   {}
   ~ApproxNoOp(){}
 
-  virtual LinResult solveRelaxation(){
-    return LinUnknown;
-  }
-  virtual Solution extractRelaxation() const throw (RationalFromDoubleException){
-    return Solution();
-  }
+  LinResult solveRelaxation() override { return LinUnknown; }
+  Solution extractRelaxation() const override { return Solution(); }
 
-  virtual ArithRatPairVec heuristicOptCoeffs() const{
+  ArithRatPairVec heuristicOptCoeffs() const override
+  {
     return ArithRatPairVec();
   }
 
-  virtual MipResult solveMIP(bool al){
-    return MipUnknown;
-  }
-  virtual Solution extractMIP() const throw (RationalFromDoubleException){
-    return Solution();
-  }
+  MipResult solveMIP(bool al) override { return MipUnknown; }
+  Solution extractMIP() const override { return Solution(); }
 
-  virtual void setOptCoeffs(const ArithRatPairVec& ref){}
-  virtual std::vector<const CutInfo*> getValidCuts(const std::set<const NodeLog*>& nodes){
-    return std::vector<const CutInfo*>();
-  }
+  void setOptCoeffs(const ArithRatPairVec& ref) override {}
 
-  virtual void tryCut(int nid, CutInfo& cut) throw (RationalFromDoubleException){}
+  void tryCut(int nid, CutInfo& cut) override {}
 
-  virtual std::vector<const CutInfo*> getValidCuts(const NodeLog& node) throw(RationalFromDoubleException){
+  std::vector<const CutInfo*> getValidCuts(const NodeLog& node) override
+  {
     return std::vector<const CutInfo*>();
   }
 
-  virtual ArithVar getBranchVar(const NodeLog& nl) const{
+  ArithVar getBranchVar(const NodeLog& nl) const override
+  {
     return ARITHVAR_SENTINEL;
   }
 
-  virtual double sumInfeasibilities(bool mip) const{
-    return 0.0;
-  }
+  double sumInfeasibilities(bool mip) const override { return 0.0; }
 };
 
 }/* CVC4::theory::arith namespace */
@@ -483,42 +417,36 @@ public:
   ApproxGLPK(const ArithVariables& v, TreeLog& l, ApproximateStatistics& s);
   ~ApproxGLPK();
 
-  virtual LinResult solveRelaxation();
-  virtual Solution extractRelaxation() const throw (RationalFromDoubleException){
-    return extractSolution(false);
-  }
+  LinResult solveRelaxation();
+  Solution extractRelaxation() const override { return extractSolution(false); }
 
-  virtual ArithRatPairVec heuristicOptCoeffs() const;
+  ArithRatPairVec heuristicOptCoeffs() const override;
 
-  virtual MipResult solveMIP(bool al);
-  virtual Solution extractMIP() const throw (RationalFromDoubleException){
-    return extractSolution(true);
-  }
-  virtual void setOptCoeffs(const ArithRatPairVec& ref);
-  //void getValidCuts(const NodeLog& con, std::vector<const CutInfo*>& out);
-  virtual std::vector<const CutInfo*> getValidCuts(const NodeLog& nodes) throw (RationalFromDoubleException);
-  //virtual std::vector<const NodeLog*> getBranches();
-
-  //Node downBranchLiteral(const NodeLog& con) const;
+  MipResult solveMIP(bool al) override;
+  Solution extractMIP() const override { return extractSolution(true); }
+  void setOptCoeffs(const ArithRatPairVec& ref) override;
+  std::vector<const CutInfo*> getValidCuts(const NodeLog& nodes) override;
   ArithVar getBranchVar(const NodeLog& con) const;
 
   static void printGLPKStatus(int status, std::ostream& out);
 
 
 private:
-  Solution extractSolution(bool mip) const throw (RationalFromDoubleException);
-  int guessDir(ArithVar v) const;
+ Solution extractSolution(bool mip) const;
+ int guessDir(ArithVar v) const;
 
-  // get this stuff out of here
-  void tryCut(int nid, CutInfo& cut) throw (RationalFromDoubleException);
+ // get this stuff out of here
+ void tryCut(int nid, CutInfo& cut) override;
 
-  ArithVar _getArithVar(int nid, int M, int ind) const;
-  ArithVar getArithVarFromRow(int nid, int ind) const {
-    if(ind >= 0){
-      const NodeLog& nl = d_log.getNode(nid);
-      return nl.lookupRowId(ind);
-    }
-    return ARITHVAR_SENTINEL;
+ ArithVar _getArithVar(int nid, int M, int ind) const;
+ ArithVar getArithVarFromRow(int nid, int ind) const
+ {
+   if (ind >= 0)
+   {
+     const NodeLog& nl = d_log.getNode(nid);
+     return nl.lookupRowId(ind);
+   }
+   return ARITHVAR_SENTINEL;
   }
 
   // virtual void mapRowId(int nid, int ind, ArithVar v){
@@ -1063,8 +991,8 @@ ApproxGLPK::~ApproxGLPK(){
 
 }
 
-
-ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const throw (RationalFromDoubleException){
+ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
+{
   Assert(d_solvedRelaxation);
   Assert(!mip  || d_solvedMIP);
 
@@ -1150,8 +1078,16 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const throw (
           // Message() << "not roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl;
         }
 
-        DeltaRational proposal = estimateWithCFE(newAssign);
-
+        DeltaRational proposal;
+        if (Maybe<Rational> maybe_new = estimateWithCFE(newAssign))
+        {
+          proposal = maybe_new.value();
+        }
+        else
+        {
+          // failed to estimate the old value. defaulting to the current.
+          proposal = d_vars.getAssignment(vi);
+        }
 
         if(roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))){
           // Message() << "  to prev value" << newAssign << " " << oldAssign << endl;
@@ -1705,7 +1641,8 @@ static void glpkCallback(glp_tree *tree, void *info){
   }
 }
 
-std::vector<const CutInfo*> ApproxGLPK::getValidCuts(const NodeLog& con) throw (RationalFromDoubleException){
+std::vector<const CutInfo*> ApproxGLPK::getValidCuts(const NodeLog& con)
+{
   std::vector<const CutInfo*> proven;
   int nid = con.getNodeId();
   for(NodeLog::const_iterator j = con.begin(), jend=con.end(); j!=jend; ++j){
@@ -1725,51 +1662,11 @@ std::vector<const CutInfo*> ApproxGLPK::getValidCuts(const NodeLog& con) throw (
   return proven;
 }
 
-// std::vector<const CutInfo*> ApproxGLPK::getValidCuts(const std::set<const NodeLog*>& nodes){
-//   // assume selected has been applied
-//   std::vector<const CutInfo*> proven;
-//   std::set<const NodeLog*>::const_iterator i, iend;
-//   for(i = nodes.begin(), iend=nodes.end(); i!=iend; ++i){
-//     const NodeLog* nl = *i;
-//     getValidCuts(*nl, proven);
-//   }
-
-//   return proven;
-// }
-
 ArithVar ApproxGLPK::getBranchVar(const NodeLog& con) const{
   int br_var = con.branchVariable();
   return getArithVarFromStructural(br_var);
 }
 
-// Node ApproxGLPK::downBranchLiteral(const NodeLog& con) const{
-//   int br_var = con.branchVariable();
-//   ArithVar v = getArithVarFromStructural(br_var);
-//   if(v != ARITHVAR_SENTINEL){
-//     if(d_vars.isIntegerInput(v) && d_vars.hasNode(v)){
-//       Node var = d_vars.asNode(v);
-//       double br_val = con.branchValue();
-//       Rational val = estimateWithCFE(br_val);
-//       if(!val.isIntegral()){
-//         NodeManager* nm = NodeManager::currentNM();
-//         Node ineq = nm->mkNode(kind::LEQ, var, mkRationalNode(val));
-//         return Rewriter::rewrite(ineq);
-//       }
-//     }
-//   }
-//   return Node::null();
-// }
-
-// std::vector<const NodeLog*> ApproxGLPK::getBranches(){
-//   std::vector<const NodeLog*> branches;
-//   for(TreeLog::const_iterator i = d_log.begin(), iend=d_log.end(); i!=iend;++i){
-//     const NodeLog& con = (*i).second;
-//     if(con.isBranch()){
-//       branches.push_back(&con);
-//     }
-//   }
-//   return branches;
-// }
 
 MipResult ApproxGLPK::solveMIP(bool activelyLog){
   Assert(d_solvedRelaxation);
@@ -2124,7 +2021,13 @@ bool ApproxGLPK::attemptBranchCut(int nid, const BranchCutInfo& br_cut){
   d_pad.d_cut.lhs.set(x, Rational(1));
 
   Rational& rhs = d_pad.d_cut.rhs;
-  rhs = estimateWithCFE(Rational::fromDouble(br_cut.getRhs()), Integer(1));
+  Maybe<Rational> br_cut_rhs = Rational::fromDouble(br_cut.getRhs());
+  if (!br_cut_rhs)
+  {
+    return true;
+  }
+
+  rhs = estimateWithCFE(br_cut_rhs.value(), Integer(1));
   d_pad.d_failure = !rhs.isIntegral();
   if(d_pad.d_failure) { return true; }
 
@@ -2175,8 +2078,13 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){
   DenseMap<Rational>& alpha = d_pad.d_alpha.lhs;
   Rational& b = d_pad.d_alpha.rhs;
 
-  Rational delta = estimateWithCFE(mir.delta);
-  d_pad.d_failure = (delta.sgn() <= 0);
+  Maybe<Rational> delta = estimateWithCFE(mir.delta);
+  if (!delta)
+  {
+    return true;
+  }
+
+  d_pad.d_failure = (delta.value().sgn() <= 0);
   if(d_pad.d_failure){ return true; }
 
   Debug("approx::mir") << "applyCMIRRule() " << delta << " " << mir.delta << endl;
@@ -2186,7 +2094,7 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){
   for(; iter != iend; ++iter){
     ArithVar v = *iter;
     const Rational& curr = alpha[v];
-    Rational next = curr / delta;
+    Rational next = curr / delta.value();
     if(compRanges.isKey(v)){
       b -= curr * compRanges[v];
       alpha.set(v, - next);
@@ -2194,7 +2102,7 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){
       alpha.set(v, next);
     }
   }
-  b = b / delta;
+  b = b / delta.value();
 
   Rational roundB = (b + Rational(1,2)).floor();
   d_pad.d_failure = (b - roundB).abs() < Rational(1,90);
@@ -2612,11 +2520,19 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){
     double coeff = row_sum.coeffs[i];
     ArithVar x = _getArithVar(nid, M, aux_ind);
     if(x == ARITHVAR_SENTINEL){ return true; }
-    Rational c = estimateWithCFE(coeff);
-    if(lhs.isKey(x)){
-      lhs.get(x) -= c;
-    }else{
-      lhs.set(x, -c);
+    Maybe<Rational> c = estimateWithCFE(coeff);
+    if (!c)
+    {
+      return true;
+    }
+
+    if (lhs.isKey(x))
+    {
+      lhs.get(x) -= c.value();
+    }
+    else
+    {
+      lhs.set(x, -c.value());
     }
   }
 
@@ -2636,9 +2552,13 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){
     double coeff = row_sum.coeffs[i];
     ArithVar x = _getArithVar(nid, M, aux_ind);
     Assert(x != ARITHVAR_SENTINEL);
-    Rational c = estimateWithCFE(coeff);
+    Maybe<Rational> c = estimateWithCFE(coeff);
+    if (!c)
+    {
+      return true;
+    }
     Assert(!lhs.isKey(x));
-    lhs.set(x, c);
+    lhs.set(x, c.value());
   }
 
   if(Debug.isOn("approx::mir")){
@@ -3070,8 +2990,12 @@ bool ApproxGLPK::guessCoefficientsConstructTableRow(int nid, int M, const Primit
     }
     Debug("guessCoefficientsConstructTableRow") << "match " << ind << "," << var << "("<<d_vars.asNode(var)<<")"<<endl;
 
-    Rational cfe = estimateWithCFE(coeff, D);
-    tab.set(var, cfe);
+    Maybe<Rational> cfe = estimateWithCFE(coeff, D);
+    if (!cfe)
+    {
+      return true;
+    }
+    tab.set(var, cfe.value());
     Debug("guessCoefficientsConstructTableRow") << var << " cfe " << cfe << endl;
   }
   if(!guessIsConstructable(tab)){
@@ -3173,7 +3097,8 @@ bool ApproxGLPK::constructGmiCut(){
   return false;
 }
 
-void ApproxGLPK::tryCut(int nid, CutInfo& cut) throw (RationalFromDoubleException){
+void ApproxGLPK::tryCut(int nid, CutInfo& cut)
+{
   Assert(!cut.reconstructed());
   Assert(cut.getKlass() != RowsDeletedKlass);
   bool failure = false;
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index 234fd10c0..eb95190bf 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -24,6 +24,7 @@
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
 #include "util/dense_map.h"
+#include "util/maybe.h"
 #include "util/rational.h"
 #include "util/statistics_registry.h"
 
@@ -49,26 +50,9 @@ enum MipResult {
 std::ostream& operator<<(std::ostream& out, MipResult res);
 
 class ApproximateStatistics {
-public:
-  // IntStat d_relaxCalls;
-  // IntStat d_relaxUnknowns;
-  // IntStat d_relaxFeasible;
-  // IntStat d_relaxInfeasible;
-  // IntStat d_relaxPivotsExhausted;
-
-  // IntStat d_mipCalls;
-  // IntStat d_mipUnknowns;
-  // IntStat d_mipBingo;
-  // IntStat d_mipClosed;
-  // IntStat d_mipBranchesExhausted;
-  // IntStat d_mipPivotsExhausted;
-  // IntStat d_mipExecExhausted;
-
-
-  // IntStat d_gmiGen;
-  // IntStat d_gmiReplay;
-  // IntStat d_mipGen;
-  // IntStat d_mipReplay;
+ public:
+  ApproximateStatistics();
+  ~ApproximateStatistics();
 
   IntStat d_branchMaxDepth;
   IntStat d_branchesMaxOnAVar;
@@ -76,9 +60,6 @@ public:
   TimerStat d_gaussianElimConstructTime;
   IntStat d_gaussianElimConstruct;
   AverageStat d_averageGuesses;
-
-  ApproximateStatistics();
-  ~ApproximateStatistics();
 };
 
 
@@ -89,26 +70,7 @@ class CutInfo;
 class RowsDeleted;
 
 class ApproximateSimplex{
-protected:
-  const ArithVariables& d_vars;
-  TreeLog& d_log;
-  ApproximateStatistics& d_stats;
-
-  int d_pivotLimit;
-  /* the maximum pivots allowed in a query. */
-
-  int d_branchLimit;
-  /* maximum branches allowed on a variable */
-
-  int d_maxDepth;
-  /* maxmimum branching depth allowed.*/
-
-  static Integer s_defaultMaxDenom;
-  /* Default denominator for diophatine approximation.
-  * 2^{26}*/
-
-public:
-
+ public:
   static bool enabled();
 
   /**
@@ -129,7 +91,6 @@ public:
   void setBranchingDepth(int bd);
 
   /** A result is either sat, unsat or unknown.*/
-  //enum ApproxResult {ApproxError, ApproxSat, ApproxUnsat};
   struct Solution {
     DenseSet newBasis;
     DenseMap<DeltaRational> newValues;
@@ -137,8 +98,6 @@ public:
   };
 
   virtual ArithVar getBranchVar(const NodeLog& nl) const = 0;
-  //virtual void mapRowId(int nid, int ind, ArithVar v) = 0;
-  //virtual void applyRowsDeleted(int nid, const RowsDeleted& rd) = 0;
 
   /** Sets a maximization criteria for the approximate solver.*/
   virtual void setOptCoeffs(const ArithRatPairVec& ref) = 0;
@@ -146,17 +105,15 @@ public:
   virtual ArithRatPairVec heuristicOptCoeffs() const = 0;
 
   virtual LinResult solveRelaxation() = 0;
-  virtual Solution extractRelaxation() const throw(RationalFromDoubleException) = 0;
+  virtual Solution extractRelaxation() const = 0;
 
   virtual MipResult solveMIP(bool activelyLog) = 0;
-  virtual Solution extractMIP() const throw(RationalFromDoubleException) = 0;
 
-  virtual std::vector<const CutInfo*> getValidCuts(const NodeLog& node) throw(RationalFromDoubleException) = 0;
-  //virtual std::vector<const NodeLog*> getBranches() = 0;
+  virtual Solution extractMIP() const = 0;
 
-  //virtual Node downBranchLiteral(const NodeLog& con) const = 0;
+  virtual std::vector<const CutInfo*> getValidCuts(const NodeLog& node) = 0;
 
-  virtual void tryCut(int nid, CutInfo& cut) throw(RationalFromDoubleException) = 0;
+  virtual void tryCut(int nid, CutInfo& cut) = 0;
 
   /** UTILITIES FOR DEALING WITH ESTIMATES */
 
@@ -171,8 +128,8 @@ public:
    * cuts off the estimate once the value is approximately zero.
    * This is designed for removing rounding artifacts.
    */
-  static Rational estimateWithCFE(double d) throw(RationalFromDoubleException);
-  static Rational estimateWithCFE(double d, const Integer& D) throw(RationalFromDoubleException);
+  static Maybe<Rational> estimateWithCFE(double d);
+  static Maybe<Rational> estimateWithCFE(double d, const Integer& D);
 
   /**
    * Converts a rational to a continued fraction expansion representation
@@ -185,10 +142,26 @@ public:
   static Rational cfeToRational(const std::vector<Integer>& exp);
 
   /** Estimates a rational as a continued fraction expansion.*/
-  //static Rational estimateWithCFE(const Rational& q, int depth);
   static Rational estimateWithCFE(const Rational& q, const Integer& K);
 
   virtual double sumInfeasibilities(bool mip) const = 0;
+
+ protected:
+  const ArithVariables& d_vars;
+  TreeLog& d_log;
+  ApproximateStatistics& d_stats;
+
+  /* the maximum pivots allowed in a query. */
+  int d_pivotLimit;
+
+  /* maximum branches allowed on a variable */
+  int d_branchLimit;
+
+  /* maxmimum branching depth allowed.*/
+  int d_maxDepth;
+
+  /* Default denominator for diophatine approximation, 2^{26} .*/
+  static Integer s_defaultMaxDenom;
 };/* class ApproximateSimplex */
 
 
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 9d414fcd7..c97ed9714 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -1074,11 +1074,15 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr
   Assert(nbSgn != 0);
 
   if(nbSgn > 0){
-    if(d_upperBoundDifference.nothing() || nbDiff <= d_upperBoundDifference){
+    if (d_upperBoundDifference.nothing()
+        || nbDiff <= d_upperBoundDifference.value())
+    {
       return false;
     }
   }else{
-    if(d_lowerBoundDifference.nothing() || nbDiff >= d_lowerBoundDifference){
+    if (d_lowerBoundDifference.nothing()
+        || nbDiff >= d_lowerBoundDifference.value())
+    {
       return false;
     }
   }
@@ -1162,14 +1166,14 @@ UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational&
   if(d_variables.hasUpperBound(nb)){
     ConstraintP ub = d_variables.getUpperBoundConstraint(nb);
     d_upperBoundDifference = ub->getValue() - d_variables.getAssignment(nb);
-    Border border(ub, d_upperBoundDifference, false, NULL, true);
+    Border border(ub, d_upperBoundDifference.value(), false, NULL, true);
     Debug("handleBorders") << "push back increasing " << border << endl;
     d_increasing.push_back(border);
   }
   if(d_variables.hasLowerBound(nb)){
     ConstraintP lb = d_variables.getLowerBoundConstraint(nb);
     d_lowerBoundDifference = lb->getValue() - d_variables.getAssignment(nb);
-    Border border(lb, d_lowerBoundDifference, false, NULL, false);
+    Border border(lb, d_lowerBoundDifference.value(), false, NULL, false);
     Debug("handleBorders") << "push back decreasing " << border << endl;
     d_decreasing.push_back(border);
   }
diff --git a/src/theory/arith/pseudoboolean_proc.cpp b/src/theory/arith/pseudoboolean_proc.cpp
index 230cfb7ca..1cdb90e20 100644
--- a/src/theory/arith/pseudoboolean_proc.cpp
+++ b/src/theory/arith/pseudoboolean_proc.cpp
@@ -15,10 +15,11 @@
  ** \todo document this file
  **/
 
+#include "theory/arith/pseudoboolean_proc.h"
+
 #include "base/output.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
-#include "theory/arith/pseudoboolean_proc.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -58,24 +59,30 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated){
 
   Polynomial p = Polynomial::parsePolynomial(l);
   clear();
-  if(negated){
+  if (negated)
+  {
     // (not (>= p r))
     // (< p r)
     // (> (-p) (-r))
     // (>= (-p) (-r +1))
     d_off = (-r.getConst<Rational>());
 
-    if(d_off.constValue().isIntegral()){
-      d_off = d_off.constValue() + Rational(1) ;
-    }else{
-      d_off = Rational(d_off.constValue().ceiling());
+    if (d_off.value().isIntegral())
+    {
+      d_off = d_off.value() + Rational(1);
     }
-  }else{
+    else
+    {
+      d_off = Rational(d_off.value().ceiling());
+    }
+  }
+  else
+  {
     // (>= p r)
     d_off = r.getConst<Rational>();
-    d_off = Rational(d_off.constValue().ceiling());
+    d_off = Rational(d_off.value().ceiling());
   }
-  Assert(d_off.constValue().isIntegral());
+  Assert(d_off.value().isIntegral());
 
   int adj = negated ? -1 : 1;
   for(Polynomial::iterator i=p.begin(), end=p.end(); i != end; ++i){
@@ -247,8 +254,8 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq){
     Debug("pbs::rewrites") << "failed " << std::endl;
     return;
   }
-  Assert(d_off.constValue().isIntegral());
-  Integer off = d_off.constValue().ceiling();
+  Assert(d_off.value().isIntegral());
+  Integer off = d_off.value().ceiling();
 
   // \sum pos >= \sum neg + off
 
@@ -323,4 +330,3 @@ void PseudoBooleanProcessor::clear() {
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h
index 7b487c8a3..70c9a5998 100644
--- a/src/theory/arith/simplex_update.h
+++ b/src/theory/arith/simplex_update.h
@@ -145,7 +145,7 @@ private:
    * d_nonbasicDelta is zero() or its sgn() must agree with d_nonbasicDirection.
    */
   bool debugSgnAgreement() const {
-    int deltaSgn = d_nonbasicDelta.constValue().sgn();
+    int deltaSgn = d_nonbasicDelta.value().sgn();
     return deltaSgn == 0 || deltaSgn == d_nonbasicDirection;
   }
 
@@ -228,16 +228,19 @@ public:
   inline int nonbasicDirection() const{  return d_nonbasicDirection; }
 
   /** Requires errorsChange to be set through setErrorsChange or updateProposal. */
-  inline int errorsChange() const { return d_errorsChange; }
+  inline int errorsChange() const { return d_errorsChange.value(); }
 
   /**
    * If errorsChange has been set, return errorsChange().
    * Otherwise, return def.
    */
   inline int errorsChangeSafe(int def) const {
-    if(d_errorsChange.just()){
-      return d_errorsChange;
-    }else{
+    if (d_errorsChange)
+    {
+      return d_errorsChange.value();
+    }
+    else
+    {
       return def;
     }
   }
@@ -250,7 +253,7 @@ public:
 
 
   /** Requires errorsChange to be set through setErrorsChange or updateProposal. */
-  inline int focusDirection() const{ return d_focusDirection; }
+  inline int focusDirection() const { return d_focusDirection.value(); }
 
   /** Sets the focusDirection. */
   void setFocusDirection(int fd){
@@ -265,18 +268,16 @@ public:
    * The burden for this being safe is on the user!
    */
   void determineFocusDirection(){
-    int deltaSgn = d_nonbasicDelta.constValue().sgn();
+    const int deltaSgn = d_nonbasicDelta.value().sgn();
     setFocusDirection(deltaSgn * d_nonbasicDirection);
   }
 
   /** Requires nonbasicDelta to be set through updateProposal(...). */
-  const DeltaRational& nonbasicDelta() const {
-    return d_nonbasicDelta;
-  }
+  const DeltaRational& nonbasicDelta() const { return d_nonbasicDelta.value(); }
   const Rational& getCoefficient() const {
     Assert(describesPivot());
-    Assert(d_tableauCoefficient.constValue() != NULL);
-    return *(d_tableauCoefficient.constValue());
+    Assert(d_tableauCoefficient.value() != NULL);
+    return *(d_tableauCoefficient.value());
   }
   int basicDirection() const {
     return nonbasicDirection() * (getCoefficient().sgn());
@@ -301,9 +302,7 @@ public:
     }
   }
 
-  const DeltaRational& focusChange() const {
-    return d_focusChange;
-  }
+  const DeltaRational& focusChange() const { return d_focusChange.value(); }
   void setFocusChange(const DeltaRational& fc) {
     d_focusChange = fc;
   }
@@ -329,13 +328,20 @@ private:
   WitnessImprovement computeWitness() const {
     if(d_foundConflict){
       return ConflictFound;
-    }else if(d_errorsChange.just() && d_errorsChange < 0){
+    }
+    else if (d_errorsChange.just() && d_errorsChange.value() < 0)
+    {
       return ErrorDropped;
-    }else if(d_errorsChange.nothing() || d_errorsChange == 0){
+    }
+    else if (d_errorsChange.nothing() || d_errorsChange.value() == 0)
+    {
       if(d_focusDirection.just()){
-        if(d_focusDirection > 0){
+        if (d_focusDirection.value() > 0)
+        {
           return FocusImproved;
-        }else if(d_focusDirection == 0){
+        }
+        else if (d_focusDirection.value() == 0)
+        {
           return Degenerate;
         }
       }
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 0e1dc62e1..f281bdfcc 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2228,18 +2228,12 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){
 
   d_replayedLemmas = false;
 
-  std::vector<ConstraintCPVec> res;
-  try{
-    /* use the try block for the purpose of pushing the sat context */
-    context::Context::ScopedPush speculativePush(getSatContext());
-    d_cmEnabled = false;
-    res = replayLogRec(approx, tl.getRootId(), NullConstraint, 1);
-  }catch(RationalFromDoubleException& rfde){
-    turnOffApproxFor(options::replayNumericFailurePenalty());
-  }
-
+  /* use the try block for the purpose of pushing the sat context */
+  context::Context::ScopedPush speculativePush(getSatContext());
+  d_cmEnabled = false;
+  std::vector<ConstraintCPVec> res =
+      replayLogRec(approx, tl.getRootId(), NullConstraint, 1);
 
-  
   if(res.empty()){
     ++d_statistics.d_replayAttemptFailed;
   }else{
@@ -2359,7 +2353,9 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const D
   return make_pair(newc, added);
 }
 
-std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(ApproximateSimplex* approx, const NodeLog& nl) throw(RationalFromDoubleException){
+std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(
+    ApproximateSimplex* approx, const NodeLog& nl)
+{
   Assert(nl.isBranch());
   Assert(d_lhsTmp.empty());
 
@@ -2368,8 +2364,12 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(Approxi
     if(d_partialModel.hasNode(v)){
       d_lhsTmp.set(v, Rational(1));
       double dval = nl.branchValue();
-      Rational val = ApproximateSimplex::estimateWithCFE(dval);
-      Rational fl(val.floor());
+      Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval);
+      if (!maybe_value)
+      {
+        return make_pair(NullConstraint, ARITHVAR_SENTINEL);
+      }
+      Rational fl(maybe_value.value().floor());
       pair<ConstraintP, ArithVar> p;
       p = replayGetConstraint(d_lhsTmp, kind::LEQ, fl, true);
       d_lhsTmp.purge();
@@ -2899,15 +2899,21 @@ ApproximateStatistics& TheoryArithPrivate::getApproxStats(){
   return *d_approxStats;
 }
 
-Node TheoryArithPrivate::branchToNode(ApproximateSimplex*  approx, const NodeLog& bn) const throw(RationalFromDoubleException) {
+Node TheoryArithPrivate::branchToNode(ApproximateSimplex* approx,
+                                      const NodeLog& bn) const
+{
   Assert(bn.isBranch());
   ArithVar v = approx->getBranchVar(bn);
   if(v != ARITHVAR_SENTINEL && d_partialModel.isIntegerInput(v)){
     if(d_partialModel.hasNode(v)){
       Node n = d_partialModel.asNode(v);
       double dval = bn.branchValue();
-      Rational val = ApproximateSimplex::estimateWithCFE(dval);
-      Rational fl(val.floor());
+      Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval);
+      if (!maybe_value)
+      {
+        return Node::null();
+      }
+      Rational fl(maybe_value.value().floor());
       NodeManager* nm = NodeManager::currentNM();
       Node leq = nm->mkNode(kind::LEQ, n, mkRationalNode(fl));
       Node norm = Rewriter::rewrite(leq);
@@ -2935,7 +2941,6 @@ Node TheoryArithPrivate::cutToLiteral(ApproximateSimplex* approx, const CutInfo&
 }
 
 bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
-  try{
     ++(d_statistics.d_mipReplayLemmaCalls);
     bool anythingnew = false;
 
@@ -2981,10 +2986,6 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
       }
     }
     return anythingnew;
-  }catch(RationalFromDoubleException& rfde){
-    turnOffApproxFor(options::replayNumericFailurePenalty());
-    return false;
-  }
 }
 
 void TheoryArithPrivate::turnOffApproxFor(int32_t rounds){
@@ -3047,7 +3048,6 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
   ApproximateSimplex* approx =
     ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel, tl, stats);
 
-  try{
     approx->setPivotLimit(mipLimit);
     if(!d_guessedCoeffSet){
       d_guessedCoeffs = approx->heuristicOptCoeffs();
@@ -3143,9 +3143,6 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
         break;
       }
     }
-  }catch(RationalFromDoubleException& rfde){
-    turnOffApproxFor(options::replayNumericFailurePenalty());
-  }
   delete approx;
 
   if(!Theory::fullEffort(effortLevel)){
@@ -3295,7 +3292,6 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
       TimerStat::CodeTimer codeTimer(d_statistics.d_lpTimer);
       relaxRes = approxSolver->solveRelaxation();
     }
-    try{
       Debug("solveRealRelaxation") << "solve relaxation? " << endl;
       switch(relaxRes){
       case LinFeasible:
@@ -3326,9 +3322,6 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
         ++d_statistics.d_relaxOthers;
         break;
       }
-    }catch(RationalFromDoubleException& rfde){
-      turnOffApproxFor(options::replayNumericFailurePenalty());
-    }
     delete approxSolver;
 
   }
@@ -5464,9 +5457,8 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg
   enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
   ResultState finalState = Unset;
 
-  int maxRounds = param.getSimplexRounds().just()
-    ? param.getSimplexRounds().constValue()
-    : -1;
+  const int maxRounds =
+      param.getSimplexRounds().just() ? param.getSimplexRounds().value() : -1;
 
   Maybe<DeltaRational> threshold;
   // TODO: get this from the parameters
@@ -5592,7 +5584,8 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg
     }
 
     if(threshold.just()){
-      if(d_partialModel.getAssignment(optVar) >= threshold.constValue()){
+      if (d_partialModel.getAssignment(optVar) >= threshold.value())
+      {
         finalState = ReachedThreshold;
         break;
       }
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 08b884a03..ff60e8436 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -590,8 +590,7 @@ private:
   void subsumption(std::vector<ConstraintCPVec>& confs) const;
 
   Node cutToLiteral(ApproximateSimplex*  approx, const CutInfo& cut) const;
-  Node branchToNode(ApproximateSimplex*  approx, const NodeLog& cut) const throw(RationalFromDoubleException);
-
+  Node branchToNode(ApproximateSimplex* approx, const NodeLog& cut) const;
 
   void propagateCandidates();
   void propagateCandidate(ArithVar basic);
@@ -705,7 +704,8 @@ private:
   std::vector<ConstraintCPVec> replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth);
 
   std::pair<ConstraintP, ArithVar> replayGetConstraint(const CutInfo& info);
-  std::pair<ConstraintP, ArithVar> replayGetConstraint(ApproximateSimplex* approx, const NodeLog& nl) throw(RationalFromDoubleException);
+  std::pair<ConstraintP, ArithVar> replayGetConstraint(
+      ApproximateSimplex* approx, const NodeLog& nl);
   std::pair<ConstraintP, ArithVar> replayGetConstraint(const DenseMap<Rational>& lhs, Kind k, const Rational& rhs, bool branch);
 
   void replayAssert(ConstraintP c);
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