diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-28 12:35:35 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-28 14:35:35 -0500 |
| commit | f9173b366ff32814ce74402765310efed48d4610 (patch) | |
| tree | 3e1b87f5ca1f3168ba5576ed56f47bb4e90008fd /src/theory/fp | |
| parent | e496ca1fd9b400c4d50a34c22f2e9d630d17af3c (diff) | |
Remove throw specifiers in FP type checker (#2392)
Diffstat (limited to 'src/theory/fp')
| -rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 28 |
1 files changed, 12 insertions, 16 deletions
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 7b155aa58..94ce476bf 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -618,10 +618,9 @@ class FloatingPointToRealTotalTypeRule { class FloatingPointComponentBit { public: - inline static TypeNode computeType( - NodeManager* nodeManager, - TNode n, - bool check) throw(TypeCheckingExceptionPrivate, AssertionException) + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) { TRACE("FloatingPointComponentBit"); @@ -653,10 +652,9 @@ class FloatingPointComponentBit class FloatingPointComponentExponent { public: - inline static TypeNode computeType( - NodeManager* nodeManager, - TNode n, - bool check) throw(TypeCheckingExceptionPrivate, AssertionException) + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) { TRACE("FloatingPointComponentExponent"); @@ -701,10 +699,9 @@ class FloatingPointComponentExponent class FloatingPointComponentSignificand { public: - inline static TypeNode computeType( - NodeManager* nodeManager, - TNode n, - bool check) throw(TypeCheckingExceptionPrivate, AssertionException) + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) { TRACE("FloatingPointComponentSignificand"); @@ -745,10 +742,9 @@ class FloatingPointComponentSignificand class RoundingModeBitBlast { public: - inline static TypeNode computeType( - NodeManager* nodeManager, - TNode n, - bool check) throw(TypeCheckingExceptionPrivate, AssertionException) + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) { TRACE("RoundingModeBitBlast"); |