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/builtin | |
parent | 7357de6df17449837e8da7defc9c8a52522c50de (diff) |
Removing throw specifiers for TypeRules. (#1501)
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 41 |
1 files changed, 23 insertions, 18 deletions
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index a6bd41a0b..56017f829 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -32,9 +32,9 @@ namespace theory { namespace builtin { class ApplyTypeRule { - public: + public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + { TNode f = n.getOperator(); TypeNode fType = f.getType(check); if( !fType.isFunction() && n.getNumChildren() > 0 ) { @@ -70,15 +70,20 @@ class ApplyTypeRule { class EqualityTypeRule { - public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { TypeNode booleanType = nodeManager->booleanType(); - if( check ) { + if (check) + { TypeNode lhsType = n[0].getType(check); TypeNode rhsType = n[1].getType(check); - - if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) { + + if (TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull()) + { std::stringstream ss; ss << "Subexpressions must have a common base type:" << std::endl; ss << "Equation: " << n << std::endl; @@ -95,7 +100,7 @@ class EqualityTypeRule { class DistinctTypeRule { -public: + public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { if( check ) { TNode::iterator child_it = n.begin(); @@ -114,7 +119,7 @@ public: };/* class DistinctTypeRule */ class SExprTypeRule { -public: + public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { std::vector<TypeNode> types; for(TNode::iterator child_it = n.begin(), child_it_end = n.end(); @@ -127,14 +132,14 @@ public: };/* class SExprTypeRule */ class UninterpretedConstantTypeRule { -public: + public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { return TypeNode::fromType(n.getConst<UninterpretedConstant>().getType()); } };/* class UninterpretedConstantTypeRule */ class AbstractValueTypeRule { -public: + public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { // An UnknownTypeException means that this node has no type. For now, // only abstract values are like this---and then, only if they are created @@ -145,7 +150,7 @@ public: };/* class AbstractValueTypeRule */ class LambdaTypeRule { -public: + public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { if( n[0].getType(check) != nodeManager->boundVarListType() ) { std::stringstream ss; @@ -162,7 +167,7 @@ public: } // computes whether a lambda is a constant value, via conversion to array representation inline static bool computeIsConst(NodeManager* nodeManager, TNode n) - throw (AssertionException) { + { Assert(n.getKind() == kind::LAMBDA); //get array representation of this function, if possible Node na = TheoryBuiltinRewriter::getArrayRepresentationForLambda( n, true ); @@ -228,7 +233,7 @@ class ChoiceTypeRule }; /* class ChoiceTypeRule */ class ChainTypeRule { -public: + public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { Assert(n.getKind() == kind::CHAIN); @@ -276,7 +281,7 @@ public: };/* class ChainTypeRule */ class ChainedOperatorTypeRule { -public: + public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { Assert(n.getKind() == kind::CHAIN_OP); return nodeManager->getType(nodeManager->operatorOf(n.getConst<Chain>().getOperator()), check); @@ -284,7 +289,7 @@ public: };/* class ChainedOperatorTypeRule */ class SortProperties { -public: + public: inline static bool isWellFounded(TypeNode type) { return true; } @@ -295,7 +300,7 @@ public: };/* class SortProperties */ class FunctionProperties { -public: + public: inline static Cardinality computeCardinality(TypeNode type) { // Don't assert this; allow other theories to use this cardinality // computation. @@ -315,7 +320,7 @@ public: };/* class FuctionProperties */ class SExprProperties { -public: + public: inline static Cardinality computeCardinality(TypeNode type) { // Don't assert this; allow other theories to use this cardinality // computation. |