diff options
| -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"); |