Remove throw qualifiers in type enumerators

This addresses Coverity issues:

- 1172154
- 1172156
- 1172157
- 1172158
- 1172159
- 1379612
- 1379612
- 1421430
- 1172166
- 1172144
- 1362709
- 1362696
- 1172145
- 1172147
- 1172148
- 1379610
- 1362772
- 1362676
- 1362704
- 1362749
- 1362876
- 1362843
- 1362837
- 1362881
- 1172223
- 1172155

diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 0208fe52d6a2b4e4bb6e6ebde59ec37dbbf4a659..25a8ca3f280d60c39138b7b4842d22ae68de953b 100644 (file)
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -41,7 +41,7 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
 
 public:
 
-  ArrayEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
+  ArrayEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
     TypeEnumeratorBase<ArrayEnumerator>(type),
     d_tep(tep),
     d_index(type.getArrayIndexType(), tep),
@@ -87,7 +87,7 @@ public:
     }
   }
 
-  Node operator*() throw(NoMoreValuesException) {
+  Node operator*() {
     if (d_finished) {
       throw NoMoreValuesException(getType());
     }
@@ -101,7 +101,7 @@ public:
     return n;
   }
 
-  ArrayEnumerator& operator++() throw() {
+  ArrayEnumerator& operator++() {
     Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl;
 
     if (d_finished) {

diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h
index 3949d15d50d37e7e39ccf644387c70d3772589d1..e91f47317ab35b381053baf261d05fe8174d9a4f 100644 (file)
--- a/src/theory/booleans/type_enumerator.h
+++ b/src/theory/booleans/type_enumerator.h
@@ -39,7 +39,7 @@ public:
            type.getConst<TypeConstant>() == BOOLEAN_TYPE);
   }
 
-  Node operator*() throw(NoMoreValuesException) {
+  Node operator*() {
     switch(d_value) {
     case FALSE:
       return NodeManager::currentNM()->mkConst(false);

diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 3840bb3b160040fc24f9c389b7b54035c86ee78f..6ee540004e71ba6896bacf31b5ca2854f9b7563c 100644 (file)
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -35,7 +35,7 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortE
   Integer d_fixed_bound;
 public:
 
-  UninterpretedSortEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
+  UninterpretedSortEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
     TypeEnumeratorBase<UninterpretedSortEnumerator>(type),
     d_count(0) {
     Assert(type.getKind() == kind::SORT_TYPE);
@@ -53,7 +53,7 @@ public:
     }
   }
 
-  Node operator*() throw(NoMoreValuesException) {
+  Node operator*() {
     if(isFinished()) {
       throw NoMoreValuesException(getType());
     }

diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 39f1e87f6000cd1df47482d5031776524971a2f7..3c984def8b8cf51d656506086d117b4ef845c6f4 100644 (file)
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -35,13 +35,13 @@ class BitVectorEnumerator : public TypeEnumeratorBase<BitVectorEnumerator> {
 
 public:
 
-  BitVectorEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
+  BitVectorEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
     TypeEnumeratorBase<BitVectorEnumerator>(type),
     d_size(type.getBitVectorSize()),
     d_bits(0) {
   }
 
-  Node operator*() throw(NoMoreValuesException) {
+  Node operator*() {
     if(d_bits != d_bits.modByPow2(d_size)) {
       throw NoMoreValuesException(getType());
     }

diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 83c93829958903aa19eafd4434cf255fb6a36e1a..5889090aa8305b2c5417f5fb088cd7d495341a5a 100644 (file)
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -81,7 +81,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
   void init();
 public:
 
-  DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
+  DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) :
     TypeEnumeratorBase<DatatypesEnumerator>(type),
     d_tep(tep),
     d_datatype(DatatypeType(type.toType()).getDatatype()),
@@ -89,7 +89,7 @@ public:
     d_child_enum = false;
     init();
   }
-  DatatypesEnumerator(TypeNode type, bool childEnum, TypeEnumeratorProperties * tep = NULL) throw() :
+  DatatypesEnumerator(TypeNode type, bool childEnum, TypeEnumeratorProperties * tep = NULL) :
     TypeEnumeratorBase<DatatypesEnumerator>(type),
     d_tep(tep),
     d_datatype(DatatypeType(type.toType()).getDatatype()),
@@ -97,7 +97,7 @@ public:
     d_child_enum = childEnum;
     init();
   }
-  DatatypesEnumerator(const DatatypesEnumerator& de) throw() :
+  DatatypesEnumerator(const DatatypesEnumerator& de) :
     TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
     d_tep(de.d_tep),
     d_datatype(de.d_datatype),
@@ -130,7 +130,7 @@ public:
   virtual ~DatatypesEnumerator() throw() {
   }
 
-  Node operator*() throw(NoMoreValuesException) {
+  Node operator*() {
     Debug("dt-enum-debug") << ": get term " << this << std::endl;
     if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) {
       return getCurrentTerm( d_ctor );
@@ -139,7 +139,7 @@ public:
     }
   }
 
-  DatatypesEnumerator& operator++() throw() {
+  DatatypesEnumerator& operator++() {
     Debug("dt-enum-debug") << ": increment " << this << std::endl;
     unsigned prevSize = d_size_limit;
     while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) {

diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h
index 1fe3d79f68d99a806af6c371bde30b33ba27cca3..22dc903ab566ed507d8eb22cf08208bd19ea7559 100644 (file)
--- a/src/theory/strings/type_enumerator.h
+++ b/src/theory/strings/type_enumerator.h
@@ -50,7 +50,7 @@ public:
   Node operator*() throw() {
     return d_curr;
   }
-  StringEnumerator& operator++() throw() {
+  StringEnumerator& operator++() {
   bool changed = false;
   do{
     for(unsigned i=0; i<d_data.size(); ++i) {
@@ -99,7 +99,7 @@ public:
     return d_curr;
   }
 
-  StringEnumeratorLength& operator++() throw() {
+  StringEnumeratorLength& operator++() {
     bool changed = false;
     for(unsigned i=0; i<d_data.size(); ++i) {
       if( d_data[i] + 1 < d_cardinality ) {

diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index bcd7e695fb77f831e49b09cb8a52924fced46f60..258bf6a3a17dc54ee194842674ef57d4664a89c4 100644 (file)
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -49,10 +49,10 @@ public:
   virtual bool isFinished() throw() = 0;
 
   /** Get the current constant of this type (throws if no such constant exists) */
-  virtual Node operator*() throw(NoMoreValuesException) = 0;
+  virtual Node operator*() = 0;
 
   /** Increment the pointer to the next available constant */
-  virtual TypeEnumeratorInterface& operator++() throw() = 0;
+  virtual TypeEnumeratorInterface& operator++() = 0;
 
   /** Clone this enumerator */
   virtual TypeEnumeratorInterface* clone() const = 0;