From 84dacb32c728c0cc44fc704dd02a5340f1c470fd Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 23 Jan 2018 00:14:43 -0800
Subject: [PATCH] Commenting out throw specifiers for DeltaRationExceptions.
 These functions can be cleaned up later. (#1529)

---
 src/theory/arith/delta_rational.cpp       |  7 ++++---
 src/theory/arith/delta_rational.h         | 13 ++++++++-----
 src/theory/arith/theory_arith_private.cpp |  2 +-
 src/theory/arith/theory_arith_private.h   |  2 +-
 4 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index fba7fdaf6..7a94674d6 100644
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -83,8 +83,8 @@ DeltaRationalException::DeltaRationalException(const char* op,
 }
 
 DeltaRationalException::~DeltaRationalException() {}
-
-Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){
+Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const
+{
   if(isIntegral() && y.isIntegral()){
     Integer ti = floor();
     Integer yi = y.floor();
@@ -94,7 +94,8 @@ Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const thr
   }
 }
 
-Integer DeltaRational::euclidianDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException){
+Integer DeltaRational::euclidianDivideRemainder(const DeltaRational& y) const
+{
   if(isIntegral() && y.isIntegral()){
     Integer ti = floor();
     Integer yi = y.floor();
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 7a1c18ea2..5e4b2c3a8 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -116,7 +116,8 @@ public:
    * This can be done whenever this->k or a.k is 0.
    * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
    */
-  DeltaRational operator*(const DeltaRational& a) const throw(DeltaRationalException){
+  DeltaRational operator*(const DeltaRational& a) const
+  /* throw(DeltaRationalException) */ {
     if(infinitesimalIsZero()){
       return a * (this->getNoninfinitesimalPart());
     }else if(a.infinitesimalIsZero()){
@@ -153,7 +154,8 @@ public:
    * This can be done when a.k is 0 and a.c is non-zero.
    * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
    */
-  DeltaRational operator/(const DeltaRational& a) const throw(DeltaRationalException){
+  DeltaRational operator/(const DeltaRational& a) const
+  /* throw(DeltaRationalException) */ {
     if(a.infinitesimalIsZero()){
       return (*this) / a.getNoninfinitesimalPart();
     }else{
@@ -258,11 +260,12 @@ public:
   }
 
   /** Only well defined if both this and y are integral. */
-  Integer euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException);
+  Integer euclidianDivideQuotient(const DeltaRational& y) const
+      /* throw(DeltaRationalException) */;
 
   /** Only well defined if both this and y are integral. */
-  Integer euclidianDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException);
-
+  Integer euclidianDivideRemainder(const DeltaRational& y) const
+      /* throw(DeltaRationalException) */;
 
   std::string toString() const;
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index f05f47595..6a4456844 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4120,7 +4120,7 @@ void TheoryArithPrivate::propagate(Theory::Effort e) {
 }
 
 DeltaRational TheoryArithPrivate::getDeltaValue(TNode term) const
-    throw(DeltaRationalException, ModelException) {
+{
   AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN);
   Debug("arith::value") << term << std::endl;
 
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 912bae5e6..459bb41d9 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -414,7 +414,7 @@ private:
    * precondition: The linear abstraction of the nodes must be satisfiable.
    */
   DeltaRational getDeltaValue(TNode term) const
-      throw(DeltaRationalException, ModelException);
+      /* throw(DeltaRationalException, ModelException) */;
 
   Node axiomIteForTotalDivision(Node div_tot);
   Node axiomIteForTotalIntDivision(Node int_div_like);
-- 
2.30.2