Removing throw specifiers from type enumerators. (#1502)

10 files changed, 175 insertions, 161 deletions

diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 4cb34ed4a..dad4ad4eb 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -32,20 +32,17 @@ namespace arith {
 class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> {
   Rational d_rat;
 
-public:
-
-  RationalEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
-    TypeEnumeratorBase<RationalEnumerator>(type),
-    d_rat(0) {
+ public:
+  RationalEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<RationalEnumerator>(type), d_rat(0)
+  {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == REAL_TYPE);
   }
 
-  Node operator*() throw() {
-    return NodeManager::currentNM()->mkConst(d_rat);
-  }
-
-  RationalEnumerator& operator++() throw() {
+  Node operator*() override { return NodeManager::currentNM()->mkConst(d_rat); }
+  RationalEnumerator& operator++() override
+  {
     // sequence is 0, then diagonal with negatives interleaved
     // ( 0, 1/1, -1/1, 2/1, -2/1, 1/2, -1/2, 3/1, -3/1, 1/3, -1/3,
     // 4/1, -4/1, 3/2, -3/2, 2/3, -2/3, 1/4, -1/4, ...)
@@ -70,29 +67,27 @@ public:
     return *this;
   }
 
-  bool isFinished() throw() {
-    return false;
-  }
-
+  bool isFinished() override { return false; }
 };/* class RationalEnumerator */
 
 class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
   Integer d_int;
 
-public:
-
-  IntegerEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
-    TypeEnumeratorBase<IntegerEnumerator>(type),
-    d_int(0) {
+ public:
+  IntegerEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<IntegerEnumerator>(type), d_int(0)
+  {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == INTEGER_TYPE);
   }
 
-  Node operator*() throw() {
+  Node operator*() override
+  {
     return NodeManager::currentNM()->mkConst(Rational(d_int));
   }
 
-  IntegerEnumerator& operator++() throw() {
+  IntegerEnumerator& operator++() override
+  {
     // sequence is 0, 1, -1, 2, -2, 3, -3, ...
     if(d_int <= 0) {
       d_int = -d_int + 1;
@@ -102,10 +97,7 @@ public:
     return *this;
   }
 
-  bool isFinished() throw() {
-    return false;
-  }
-
+  bool isFinished() override { return false; }
 };/* class IntegerEnumerator */
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 4314fad83..2202c69bc 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -39,18 +39,17 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
   bool d_finished;
   Node d_arrayConst;
 
-public:
-
-  ArrayEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
-    TypeEnumeratorBase<ArrayEnumerator>(type),
-    d_tep(tep),
-    d_index(type.getArrayIndexType(), tep),
-    d_constituentType(type.getArrayConstituentType()),
-    d_nm(NodeManager::currentNM()),
-    d_indexVec(),
-    d_constituentVec(),
-    d_finished(false),
-    d_arrayConst()
+ public:
+  ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<ArrayEnumerator>(type),
+        d_tep(tep),
+        d_index(type.getArrayIndexType(), tep),
+        d_constituentType(type.getArrayConstituentType()),
+        d_nm(NodeManager::currentNM()),
+        d_indexVec(),
+        d_constituentVec(),
+        d_finished(false),
+        d_arrayConst()
   {
     d_indexVec.push_back(*d_index);
     d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
@@ -61,16 +60,17 @@ public:
   // An array enumerator could be large, and generally you don't want to
   // go around copying these things; but a copy ctor is presently required
   // by the TypeEnumerator framework.
-  ArrayEnumerator(const ArrayEnumerator& ae) throw() :
-    TypeEnumeratorBase<ArrayEnumerator>(ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)),
-    d_tep(ae.d_tep),
-    d_index(ae.d_index),
-    d_constituentType(ae.d_constituentType),
-    d_nm(ae.d_nm),
-    d_indexVec(ae.d_indexVec),
-    d_constituentVec(),// copied below
-    d_finished(ae.d_finished),
-    d_arrayConst(ae.d_arrayConst)
+  ArrayEnumerator(const ArrayEnumerator& ae)
+      : TypeEnumeratorBase<ArrayEnumerator>(
+            ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)),
+        d_tep(ae.d_tep),
+        d_index(ae.d_index),
+        d_constituentType(ae.d_constituentType),
+        d_nm(ae.d_nm),
+        d_indexVec(ae.d_indexVec),
+        d_constituentVec(),  // copied below
+        d_finished(ae.d_finished),
+        d_arrayConst(ae.d_arrayConst)
   {
     for(std::vector<TypeEnumerator*>::const_iterator i =
           ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
@@ -87,7 +87,8 @@ public:
     }
   }
 
-  Node operator*() {
+  Node operator*() override
+  {
     if (d_finished) {
       throw NoMoreValuesException(getType());
     }
@@ -101,7 +102,8 @@ public:
     return n;
   }
 
-  ArrayEnumerator& operator++() {
+  ArrayEnumerator& operator++() override
+  {
     Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl;
 
     if (d_finished) {
@@ -144,7 +146,8 @@ public:
     return *this;
   }
 
-  bool isFinished() throw() {
+  bool isFinished() override
+  {
     Trace("array-type-enum") << "isFinished returning: " << d_finished << std::endl;
     return d_finished;
   }
diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h
index b0759cbb2..32c6bae42 100644
--- a/src/theory/booleans/type_enumerator.h
+++ b/src/theory/booleans/type_enumerator.h
@@ -30,11 +30,10 @@ namespace booleans {
 class BooleanEnumerator : public TypeEnumeratorBase<BooleanEnumerator> {
   enum { FALSE, TRUE, DONE } d_value;
 
-public:
-
-  BooleanEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
-    TypeEnumeratorBase<BooleanEnumerator>(type),
-    d_value(FALSE) {
+ public:
+  BooleanEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<BooleanEnumerator>(type), d_value(FALSE)
+  {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == BOOLEAN_TYPE);
   }
@@ -50,7 +49,8 @@ public:
     }
   }
 
-  BooleanEnumerator& operator++() throw() {
+  BooleanEnumerator& operator++() override
+  {
     // sequence is FALSE, TRUE
     if(d_value == FALSE) {
       d_value = TRUE;
@@ -60,10 +60,7 @@ public:
     return *this;
   }
 
-  bool isFinished() throw() {
-    return d_value == DONE;
-  }
-
+  bool isFinished() override { return d_value == DONE; }
 };/* class BooleanEnumerator */
 
 }/* CVC4::theory::booleans namespace */
diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp
index 6435d3b4b..6884d41d9 100644
--- a/src/theory/builtin/type_enumerator.cpp
+++ b/src/theory/builtin/type_enumerator.cpp
@@ -39,7 +39,7 @@ Node FunctionEnumerator::operator*()
   return TheoryBuiltinRewriter::getLambdaForArrayRepresentation(a, d_bvl);
 }
 
-FunctionEnumerator& FunctionEnumerator::operator++() throw()
+FunctionEnumerator& FunctionEnumerator::operator++()
 {
   ++d_arrayEnum;
   return *this;
@@ -47,4 +47,4 @@ FunctionEnumerator& FunctionEnumerator::operator++() throw()
 
 } /* CVC4::theory::builtin namespace */
 } /* CVC4::theory namespace */
-} /* CVC4 namespace */
\ No newline at end of file
+} /* CVC4 namespace */
diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index e75443140..e7258d27a 100644
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -34,11 +34,12 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortE
   Integer d_count;
   bool d_has_fixed_bound;
   Integer d_fixed_bound;
-public:
 
-  UninterpretedSortEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
-    TypeEnumeratorBase<UninterpretedSortEnumerator>(type),
-    d_count(0) {
+ public:
+  UninterpretedSortEnumerator(TypeNode type,
+                              TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<UninterpretedSortEnumerator>(type), d_count(0)
+  {
     Assert(type.getKind() == kind::SORT_TYPE);
     d_has_fixed_bound = false;
     Trace("uf-type-enum") << "UF enum " << type << ", tep = " << tep << std::endl;
@@ -54,19 +55,22 @@ public:
     }
   }
 
-  Node operator*() {
+  Node operator*() override
+  {
     if(isFinished()) {
       throw NoMoreValuesException(getType());
     }
     return NodeManager::currentNM()->mkConst(UninterpretedConstant(getType().toType(), d_count));
   }
 
-  UninterpretedSortEnumerator& operator++() throw() {
+  UninterpretedSortEnumerator& operator++() override
+  {
     d_count += 1;
     return *this;
   }
 
-  bool isFinished() throw() {
+  bool isFinished() override
+  {
     if( d_has_fixed_bound ){
       return d_count>=d_fixed_bound;
     }else{
@@ -87,9 +91,9 @@ class FunctionEnumerator : public TypeEnumeratorBase<FunctionEnumerator>
   /** Get the current term of the enumerator. */
   Node operator*() override;
   /** Increment the enumerator. */
-  FunctionEnumerator& operator++() throw() override;
+  FunctionEnumerator& operator++() override;
   /** is the enumerator finished? */
-  bool isFinished() throw() override { return d_arrayEnum.isFinished(); }
+  bool isFinished() override { return d_arrayEnum.isFinished(); }
  private:
   /** Enumerates arrays, which we convert to functions. */
   TypeEnumerator d_arrayEnum;
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 8cf4ab3d9..462d6306e 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -79,21 +79,25 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   Node getCurrentTerm( unsigned index );
 
   void init();
-public:
 
-  DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
-    TypeEnumeratorBase<DatatypesEnumerator>(type),
-    d_tep(tep),
-    d_datatype(DatatypeType(type.toType()).getDatatype()),
-    d_type(type) {
+ public:
+  DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<DatatypesEnumerator>(type),
+        d_tep(tep),
+        d_datatype(DatatypeType(type.toType()).getDatatype()),
+        d_type(type)
+  {
     d_child_enum = false;
     init();
   }
-  DatatypesEnumerator(TypeNode type, bool childEnum, TypeEnumeratorProperties * tep = NULL) :
-    TypeEnumeratorBase<DatatypesEnumerator>(type),
-    d_tep(tep),
-    d_datatype(DatatypeType(type.toType()).getDatatype()),
-    d_type(type) {
+  DatatypesEnumerator(TypeNode type,
+                      bool childEnum,
+                      TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<DatatypesEnumerator>(type),
+        d_tep(tep),
+        d_datatype(DatatypeType(type.toType()).getDatatype()),
+        d_type(type)
+  {
     d_child_enum = childEnum;
     init();
   }
@@ -127,10 +131,8 @@ public:
     d_child_enum = de.d_child_enum;
   }
 
-  virtual ~DatatypesEnumerator() throw() {
-  }
-
-  Node operator*() {
+  Node operator*() override
+  {
     Debug("dt-enum-debug") << ": get term " << this << std::endl;
     if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) {
       return getCurrentTerm( d_ctor );
@@ -139,7 +141,8 @@ public:
     }
   }
 
-  DatatypesEnumerator& operator++() {
+  DatatypesEnumerator& operator++() override
+  {
     Debug("dt-enum-debug") << ": increment " << this << std::endl;
     unsigned prevSize = d_size_limit;
     while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) {
@@ -171,7 +174,8 @@ public:
     return *this;
   }
 
-  bool isFinished() throw() {
+  bool isFinished() override
+  {
     return d_ctor >= d_has_debruijn+d_datatype.getNumConstructors();
   }
 
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index f261ac3fa..87a0485ae 100644
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -42,18 +42,17 @@ class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> {
   bool d_finished;
   Node d_setConst;
 
-public:
-
-  SetEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
-    TypeEnumeratorBase<SetEnumerator>(type),
-    d_tep(tep),
-    d_index(0),
-    d_constituentType(type.getSetElementType()),
-    d_nm(NodeManager::currentNM()),
-    d_indexVec(),
-    d_constituentVec(),
-    d_finished(false),
-    d_setConst()
+ public:
+  SetEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<SetEnumerator>(type),
+        d_tep(tep),
+        d_index(0),
+        d_constituentType(type.getSetElementType()),
+        d_nm(NodeManager::currentNM()),
+        d_indexVec(),
+        d_constituentVec(),
+        d_finished(false),
+        d_setConst()
   {
     // d_indexVec.push_back(false);
     // d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
@@ -63,16 +62,17 @@ public:
   // An set enumerator could be large, and generally you don't want to
   // go around copying these things; but a copy ctor is presently required
   // by the TypeEnumerator framework.
-  SetEnumerator(const SetEnumerator& ae) throw() :
-    TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)),
-    d_tep(ae.d_tep),
-    d_index(ae.d_index),
-    d_constituentType(ae.d_constituentType),
-    d_nm(ae.d_nm),
-    d_indexVec(ae.d_indexVec),
-    d_constituentVec(),// copied below
-    d_finished(ae.d_finished),
-    d_setConst(ae.d_setConst)
+  SetEnumerator(const SetEnumerator& ae)
+      : TypeEnumeratorBase<SetEnumerator>(
+            ae.d_nm->mkSetType(ae.d_constituentType)),
+        d_tep(ae.d_tep),
+        d_index(ae.d_index),
+        d_constituentType(ae.d_constituentType),
+        d_nm(ae.d_nm),
+        d_indexVec(ae.d_indexVec),
+        d_constituentVec(),  // copied below
+        d_finished(ae.d_finished),
+        d_setConst(ae.d_setConst)
   {
     for(std::vector<TypeEnumerator*>::const_iterator i =
           ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
@@ -89,7 +89,8 @@ public:
     }
   }
 
-  Node operator*() throw(NoMoreValuesException) {
+  Node operator*() override
+  {
     if (d_finished) {
       throw NoMoreValuesException(getType());
     }
@@ -108,7 +109,8 @@ public:
     return n;
   }
 
-  SetEnumerator& operator++() throw() {
+  SetEnumerator& operator++() override
+  {
     Trace("set-type-enum") << "operator++ called, **this = " << **this << std::endl;
 
     if (d_finished) {
@@ -169,7 +171,8 @@ public:
     return *this;
   }
 
-  bool isFinished() throw() {
+  bool isFinished() override
+  {
     Trace("set-type-enum") << "isFinished returning: " << d_finished << std::endl;
     return d_finished;
   }
diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h
index c7a36f2f5..b1904f53f 100644
--- a/src/theory/strings/type_enumerator.h
+++ b/src/theory/strings/type_enumerator.h
@@ -38,48 +38,52 @@ class StringEnumerator : public TypeEnumeratorBase<StringEnumerator> {
     //make constant from d_data
     d_curr = NodeManager::currentNM()->mkConst( ::CVC4::String( d_data ) );
   }
-public:
 
-  StringEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
-    TypeEnumeratorBase<StringEnumerator>(type) {
+ public:
+  StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<StringEnumerator>(type)
+  {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == STRING_TYPE);
     d_cardinality = 256;
     mkCurr();
   }
-  Node operator*() throw() {
-    return d_curr;
-  }
-  StringEnumerator& operator++() {
-  bool changed = false;
-  do{
-    for(unsigned i=0; i<d_data.size(); ++i) {
-      if( d_data[i] + 1 < d_cardinality ) {
-        ++d_data[i]; changed = true;
-        break;
-      } else {
-        d_data[i] = 0;
+  Node operator*() override { return d_curr; }
+  StringEnumerator& operator++() override
+  {
+    bool changed = false;
+    do
+    {
+      for (unsigned i = 0; i < d_data.size(); ++i)
+      {
+        if (d_data[i] + 1 < d_cardinality)
+        {
+          ++d_data[i];
+          changed = true;
+          break;
+        }
+        else
+        {
+          d_data[i] = 0;
+        }
       }
-    }
 
-    if(!changed) {
-      d_data.push_back( 0 );
-    }
-  }while(!changed);
+      if (!changed)
+      {
+        d_data.push_back(0);
+      }
+    } while (!changed);
 
-  mkCurr();
+    mkCurr();
     return *this;
   }
 
-  bool isFinished() throw() {
-    return d_curr.isNull();
-  }
-
+  bool isFinished() override { return d_curr.isNull(); }
 };/* class StringEnumerator */
 
 
 class StringEnumeratorLength {
-private:
+ private:
   unsigned d_cardinality;
   std::vector< unsigned > d_data;
   Node d_curr;
@@ -87,7 +91,8 @@ private:
     //make constant from d_data
     d_curr = NodeManager::currentNM()->mkConst( ::CVC4::String( d_data ) );
   }
-public:
+
+ public:
   StringEnumeratorLength(unsigned length, unsigned card = 256) : d_cardinality(card) {
     for( unsigned i=0; i<length; i++ ){
       d_data.push_back( 0 );
@@ -95,10 +100,7 @@ public:
     mkCurr();
   }
 
-  Node operator*() throw() {
-    return d_curr;
-  }
-
+  Node operator*() { return d_curr; }
   StringEnumeratorLength& operator++() {
     bool changed = false;
     for(unsigned i=0; i<d_data.size(); ++i) {
@@ -118,9 +120,7 @@ public:
     return *this;
   }
 
-  bool isFinished() throw() {
-    return d_curr.isNull();
-  }
+  bool isFinished() { return d_curr.isNull(); }
 };
 
 }/* CVC4::theory::strings namespace */
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index f90a06833..7ca4a6140 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -96,13 +96,13 @@ public:
 class TypeEnumerator {
   TypeEnumeratorInterface* d_te;
 
-  static TypeEnumeratorInterface* mkTypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep)
-    throw(AssertionException);
+  static TypeEnumeratorInterface* mkTypeEnumerator(
+      TypeNode type, TypeEnumeratorProperties* tep);
 
-public:
-
-  TypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
-    d_te(mkTypeEnumerator(type, tep)) {
+ public:
+  TypeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+      : d_te(mkTypeEnumerator(type, tep))
+  {
   }
 
   TypeEnumerator(const TypeEnumerator& te) :
@@ -117,8 +117,8 @@ public:
   }
 
   ~TypeEnumerator() { delete d_te; }
-
-  bool isFinished() throw() {
+  bool isFinished()
+  {
 // On Mac clang, there appears to be a code generation bug in an exception
 // block here.  For now, there doesn't appear a good workaround; just disable
 // assertions on that setup.
@@ -145,7 +145,8 @@ public:
 #endif /* CVC4_ASSERTIONS && !(APPLE || clang) */
     return d_te->isFinished();
   }
-  Node operator*() throw(NoMoreValuesException) {
+  Node operator*()
+  {
 // On Mac clang, there appears to be a code generation bug in an exception
 // block above (and perhaps here, too).  For now, there doesn't appear a
 // good workaround; just disable assertions on that setup.
@@ -163,11 +164,19 @@ public:
     return **d_te;
 #endif /* CVC4_ASSERTIONS && !(APPLE || clang) */
   }
-  TypeEnumerator& operator++() throw() { ++*d_te; return *this; }
-  TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; }
-
-  TypeNode getType() const throw() { return d_te->getType(); }
+  TypeEnumerator& operator++()
+  {
+    ++*d_te;
+    return *this;
+  }
+  TypeEnumerator operator++(int)
+  {
+    TypeEnumerator te = *this;
+    ++*d_te;
+    return te;
+  }
 
+  TypeNode getType() const { return d_te->getType(); }
 };/* class TypeEnumerator */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp
index a2bc8ab86..91ae3e1d6 100644
--- a/src/theory/type_enumerator_template.cpp
+++ b/src/theory/type_enumerator_template.cpp
@@ -29,7 +29,9 @@ using namespace std;
 namespace CVC4 {
 namespace theory {
 
-TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(TypeNode type, TypeEnumeratorProperties * tep) throw(AssertionException) {
+TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(
+    TypeNode type, TypeEnumeratorProperties* tep)
+{
   switch(type.getKind()) {
   case kind::TYPE_CONSTANT:
     switch(type.getConst<TypeConstant>()) {