diff options
author | Tim King <taking@cs.nyu.edu> | 2018-01-23 00:14:43 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-23 00:14:43 -0800 |
commit | 84dacb32c728c0cc44fc704dd02a5340f1c470fd (patch) | |
tree | 9be3960a78d3c929c86036fa0674691c6b4c3037 /src/theory/arith | |
parent | 7b12b1e8307295e68cb389eaa7692036fae6e872 (diff) |
Commenting out throw specifiers for DeltaRationExceptions. These functions can be cleaned up later. (#1529)
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/delta_rational.cpp | 7 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.h | 13 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 2 | ||||
-rw-r--r-- | 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); |