Removing throw specifiers for TypeRules. (#1501)

8 files changed, 97 insertions, 95 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();
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();
   }
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 7de38b6af..405748324 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -26,7 +26,7 @@ namespace boolean {
 class BooleanTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     TypeNode booleanType = nodeManager->booleanType();
     if( check ) {
       TNode::iterator child_it = n.begin();
@@ -47,7 +47,7 @@ public:
 class IteTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     TypeNode thenType = n[1].getType(check);
     TypeNode elseType = n[2].getType(check);
     TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType);
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.
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 2ea7e9b72..16600e006 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -27,7 +27,7 @@ namespace quantifiers {
 
 struct QuantifierForallTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Debug("typecheck-q") << "type check for fa " << n << std::endl;
     Assert(n.getKind() == kind::FORALL && n.getNumChildren()>0 );
     if( check ){
@@ -47,7 +47,7 @@ struct QuantifierForallTypeRule {
 
 struct QuantifierExistsTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Debug("typecheck-q") << "type check for ex " << n << std::endl;
     Assert(n.getKind() == kind::EXISTS && n.getNumChildren()>0 );
     if( check ){
@@ -67,7 +67,7 @@ struct QuantifierExistsTypeRule {
 
 struct QuantifierBoundVarListTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Assert(n.getKind() == kind::BOUND_VAR_LIST );
     if( check ){
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
@@ -82,7 +82,7 @@ struct QuantifierBoundVarListTypeRule {
 
 struct QuantifierInstPatternTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Assert(n.getKind() == kind::INST_PATTERN );
     if( check ){
       TypeNode tn = n[0].getType(check);
@@ -97,7 +97,7 @@ struct QuantifierInstPatternTypeRule {
 
 struct QuantifierInstNoPatternTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Assert(n.getKind() == kind::INST_NO_PATTERN );
     return nodeManager->instPatternType();
   }
@@ -105,7 +105,7 @@ struct QuantifierInstNoPatternTypeRule {
 
 struct QuantifierInstAttributeTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Assert(n.getKind() == kind::INST_ATTRIBUTE );
     return nodeManager->instPatternType();
   }
@@ -113,7 +113,7 @@ struct QuantifierInstAttributeTypeRule {
 
 struct QuantifierInstPatternListTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Assert(n.getKind() == kind::INST_PATTERN_LIST );
     if( check ){
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
@@ -128,7 +128,7 @@ struct QuantifierInstPatternListTypeRule {
 
 struct QuantifierInstClosureTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Assert(n.getKind() == kind::INST_CLOSURE );
     if( check ){
       TypeNode tn = n[0].getType(check);
@@ -155,7 +155,7 @@ public:
    */
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Debug("typecheck-r") << "type check for rr " << n << std::endl;
     Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 );
     if( check ){
@@ -181,7 +181,7 @@ class RRRewriteTypeRule {
 public:
 
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Assert(n.getKind() == kind::RR_REWRITE );
     if( check ){
       if( n[0].getType(check)!=n[1].getType(check) ){
@@ -203,7 +203,7 @@ class RRRedDedTypeRule {
 public:
 
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
+  {
     Assert(n.getKind() == kind::RR_REDUCTION ||
            n.getKind() == kind::RR_DEDUCTION );
     if( check ){
diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h
index d060b44e9..0e0373586 100644
--- a/src/theory/sep/theory_sep_type_rules.h
+++ b/src/theory/sep/theory_sep_type_rules.h
@@ -26,7 +26,7 @@ namespace sep {
 class SepEmpTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::SEP_EMP);
     return nodeManager->booleanType();
   }
@@ -34,7 +34,7 @@ public:
 
 struct SepPtoTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::SEP_PTO);
     if( check ) {
       TypeNode refType = n[0].getType(check);
@@ -46,7 +46,7 @@ struct SepPtoTypeRule {
 
 struct SepStarTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     TypeNode btype = nodeManager->booleanType();
     Assert(n.getKind() == kind::SEP_STAR);
     if( check ){
@@ -63,7 +63,7 @@ struct SepStarTypeRule {
 
 struct SepWandTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     TypeNode btype = nodeManager->booleanType();
     Assert(n.getKind() == kind::SEP_WAND);
     if( check ){
@@ -80,7 +80,7 @@ struct SepWandTypeRule {
 
 struct SepLabelTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     TypeNode btype = nodeManager->booleanType();
     Assert(n.getKind() == kind::SEP_LABEL);
     if( check ){
@@ -99,7 +99,7 @@ struct SepLabelTypeRule {
 
 struct SepNilTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::SEP_NIL);
     Assert(check);
     TypeNode type = n.getType();
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 23b185230..dcac963b0 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -37,8 +37,7 @@ public:
    */
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check)
-    throw (TypeCheckingExceptionPrivate) {
-
+  {
     // TODO: implement me!
     Unimplemented();
 
@@ -48,7 +47,7 @@ public:
 
 struct SetsBinaryOperatorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::UNION ||
            n.getKind() == kind::INTERSECTION ||
            n.getKind() == kind::SETMINUS);
@@ -87,7 +86,7 @@ struct SetsBinaryOperatorTypeRule {
 
 struct SubsetTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::SUBSET);
     TypeNode setType = n[0].getType(check);
     if( check ) {
@@ -107,7 +106,7 @@ struct SubsetTypeRule {
 
 struct MemberTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::MEMBER);
     TypeNode setType = n[1].getType(check);
     if( check ) {
@@ -146,7 +145,7 @@ struct MemberTypeRule {
 
 struct SingletonTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::SINGLETON);
     return nodeManager->mkSetType(n[0].getType(check));
   }
@@ -159,7 +158,7 @@ struct SingletonTypeRule {
 
 struct EmptySetTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::EMPTYSET);
     EmptySet emptySet = n.getConst<EmptySet>();
     Type setType = emptySet.getType();
@@ -169,7 +168,7 @@ struct EmptySetTypeRule {
 
 struct CardTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::CARD);
     TypeNode setType = n[0].getType(check);
     if( check ) {
@@ -188,7 +187,7 @@ struct CardTypeRule {
 
 struct ComplementTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::COMPLEMENT);
     TypeNode setType = n[0].getType(check);
     if( check ) {
@@ -207,7 +206,7 @@ struct ComplementTypeRule {
 
 struct UniverseSetTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::UNIVERSE_SET);
     // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation
     Assert(check);
@@ -221,7 +220,7 @@ struct UniverseSetTypeRule {
 
 struct InsertTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::INSERT);
     size_t numChildren = n.getNumChildren();
     Assert( numChildren >= 2 );
@@ -249,7 +248,7 @@ struct InsertTypeRule {
 
 struct RelBinaryOperatorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::PRODUCT ||
            n.getKind() == kind::JOIN);
 
@@ -295,7 +294,7 @@ struct RelBinaryOperatorTypeRule {
 
 struct RelTransposeTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::TRANSPOSE);
     TypeNode setType = n[0].getType(check);
     if(check && (!setType.isSet() || !setType.getSetElementType().isTuple())) {
@@ -313,7 +312,7 @@ struct RelTransposeTypeRule {
 
 struct RelTransClosureTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::TCLOSURE);
     TypeNode setType = n[0].getType(check);
     if(check) {
@@ -339,7 +338,7 @@ struct RelTransClosureTypeRule {
 
 struct JoinImageTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::JOIN_IMAGE);
 
     TypeNode firstRelType = n[0].getType(check);
@@ -386,7 +385,7 @@ struct JoinImageTypeRule {
 
 struct RelIdenTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     Assert(n.getKind() == kind::IDEN);
     TypeNode setType = n[0].getType(check);
     if(check) {
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index b02257d38..176398776 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -27,7 +27,7 @@ namespace strings {
 class StringConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     return nodeManager->stringType();
   }
 };
@@ -35,7 +35,7 @@ public:
 class StringConcatTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ){
       TNode::iterator it = n.begin();
       TNode::iterator it_end = n.end();
@@ -58,7 +58,7 @@ public:
 class StringLengthTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
@@ -72,7 +72,7 @@ public:
 class StringSubstrTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
@@ -94,7 +94,7 @@ public:
 class StringContainTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
@@ -112,7 +112,7 @@ public:
 class StringCharAtTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
@@ -130,7 +130,7 @@ public:
 class StringIndexOfTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
@@ -152,7 +152,7 @@ public:
 class StringReplaceTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
@@ -174,7 +174,7 @@ public:
 class StringPrefixOfTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
@@ -192,7 +192,7 @@ public:
 class StringSuffixOfTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
@@ -210,7 +210,7 @@ public:
 class StringIntToStrTypeRule {
 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()) {
@@ -224,7 +224,7 @@ public:
 class StringStrToIntTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
@@ -238,7 +238,7 @@ public:
 class RegExpConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     return nodeManager->regExpType();
   }
 };
@@ -246,7 +246,7 @@ public:
 class RegExpConcatTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TNode::iterator it = n.begin();
       TNode::iterator it_end = n.end();
@@ -269,7 +269,7 @@ public:
 class RegExpUnionTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TNode::iterator it = n.begin();
       TNode::iterator it_end = n.end();
@@ -287,7 +287,7 @@ public:
 class RegExpInterTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TNode::iterator it = n.begin();
       TNode::iterator it_end = n.end();
@@ -305,7 +305,7 @@ public:
 class RegExpStarTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isRegExp()) {
@@ -319,7 +319,7 @@ public:
 class RegExpPlusTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isRegExp()) {
@@ -333,7 +333,7 @@ public:
 class RegExpOptTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isRegExp()) {
@@ -347,7 +347,7 @@ public:
 class RegExpRangeTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TNode::iterator it = n.begin();
       unsigned char ch[2];
@@ -380,7 +380,7 @@ public:
 class RegExpLoopTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TNode::iterator it = n.begin();
       TNode::iterator it_end = n.end();
@@ -416,7 +416,7 @@ public:
 class StringToRegExpTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
@@ -433,7 +433,7 @@ public:
 class StringInRegExpTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate, AssertionException) {
+  {
     if( check ) {
       TNode::iterator it = n.begin();
       TypeNode t = (*it).getType(check);
@@ -453,8 +453,7 @@ public:
 class EmptyRegExpTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
-
+  {
     Assert(n.getKind() == kind::REGEXP_EMPTY);
     return nodeManager->regExpType();
   }
@@ -463,8 +462,7 @@ public:
 class SigmaRegExpTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw (TypeCheckingExceptionPrivate, AssertionException) {
-
+  {
     Assert(n.getKind() == kind::REGEXP_SIGMA);
     return nodeManager->regExpType();
   }
@@ -473,7 +471,7 @@ public:
 class RegExpRVTypeRule {
 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()) {