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/arrays | |
| parent | 7357de6df17449837e8da7defc9c8a52522c50de (diff) | |
Removing throw specifiers for TypeRules. (#1501)
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 2dbc5affd..85d3683b3 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -28,7 +28,7 @@ namespace arrays { struct ArraySelectTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { Assert(n.getKind() == kind::SELECT); TypeNode arrayType = n[0].getType(check); if( check ) { @@ -46,7 +46,7 @@ struct ArraySelectTypeRule { struct ArrayStoreTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { if (n.getKind() == kind::STORE) { TypeNode arrayType = n[0].getType(check); if( check ) { @@ -75,7 +75,7 @@ struct ArrayStoreTypeRule { } inline static bool computeIsConst(NodeManager* nodeManager, TNode n) - throw (AssertionException) { + { Assert(n.getKind() == kind::STORE); NodeManagerScope nms(nodeManager); @@ -154,7 +154,7 @@ struct ArrayStoreTypeRule { struct ArrayTableFunTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { Assert(n.getKind() == kind::ARR_TABLE_FUN); TypeNode arrayType = n[0].getType(check); if( check ) { @@ -180,7 +180,7 @@ struct ArrayTableFunTypeRule { struct ArrayLambdaTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { Assert(n.getKind() == kind::ARRAY_LAMBDA); TypeNode lamType = n[0].getType(check); if( check ) { @@ -217,7 +217,7 @@ struct ArraysProperties { struct ArrayPartialSelectTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { Assert(n.getKind() == kind::PARTIAL_SELECT_0 || n.getKind() == kind::PARTIAL_SELECT_1); return nodeManager->integerType(); } |