diff options
author | Tim King <taking@cs.nyu.edu> | 2018-01-10 12:57:38 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-10 12:57:38 -0800 |
commit | 82fa0b8a67d076287cc4c4105a42fcabc459fd18 (patch) | |
tree | b32f88c11a055f4c4a8f20c5d40f1ac2ba2ed742 /src/theory/arith | |
parent | 7357de6df17449837e8da7defc9c8a52522c50de (diff) |
Removing throw specifiers for TypeRules. (#1501)
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index e19573039..d783882f4 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -27,7 +27,7 @@ namespace arith { class ArithConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { Assert(n.getKind() == kind::CONST_RATIONAL); if(n.getConst<Rational>().isIntegral()){ return nodeManager->integerType(); @@ -40,7 +40,7 @@ public: class ArithOperatorTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { TypeNode integerType = nodeManager->integerType(); TypeNode realType = nodeManager->realType(); TNode::iterator child_it = n.begin(); @@ -76,7 +76,7 @@ public: class IntOperatorTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { TNode::iterator child_it = n.begin(); TNode::iterator child_it_end = n.end(); if(check) { @@ -94,7 +94,7 @@ public: class RealOperatorTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { TNode::iterator child_it = n.begin(); TNode::iterator child_it_end = n.end(); if(check) { @@ -112,7 +112,7 @@ public: class ArithPredicateTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { if( check ) { TypeNode lhsType = n[0].getType(check); if (!lhsType.isReal()) { @@ -130,7 +130,7 @@ public: class ArithUnaryPredicateTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { if( check ) { TypeNode t = n[0].getType(check); if (!t.isReal()) { @@ -144,7 +144,7 @@ public: class IntUnaryPredicateTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { if( check ) { TypeNode t = n[0].getType(check); if (!t.isInteger()) { @@ -158,7 +158,7 @@ public: class RealNullaryOperatorTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation Assert(check); TypeNode realType = n.getType(); |