Commenting out throw specifiers for DeltaRationExceptions. These functions can be...

diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index fba7fdaf658aa1afa10e91dd147777f44d943f49..7a94674d62c5af0c0413f5afdfd7fe20acb071b7 100644 (file)
--- 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 7a1c18ea22f78ea29563a116dc718ef165d05399..5e4b2c3a81353f4df93c4a2664dff2e0b29fa90a 100644 (file)
--- 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 f05f475959e1020adb82f46fa0779d11ea71ca35..6a4456844bd01657aca9f22df67ea1fee79b8529 100644 (file)
--- 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 912bae5e69d56eec70ba105d28bfe6e4fe4c6d2a..459bb41d9c05f4f22e42d5b79314409f87c5ab19 100644 (file)
--- 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);