From: Andres Notzli <andres.noetzli@gmail.com>
Date: Mon, 27 Mar 2017 09:40:45 +0000 (+0200)
Subject: Remove throw qualifiers in type enumerators
X-Git-Tag: cvc5-1.0.0~5866^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f5954a66ac3255fe140049e47a7b56a6fab459b3;p=cvc5.git

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 0208fe52d..25a8ca3f2 100644
--- 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 3949d15d5..e91f47317 100644
--- 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 3840bb3b1..6ee540004 100644
--- 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 39f1e87f6..3c984def8 100644
--- 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 83c938299..5889090aa 100644
--- 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 1fe3d79f6..22dc903ab 100644
--- 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 bcd7e695f..258bf6a3a 100644
--- 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;