Removing throw specifiers from TypeEnumeratorBase's operator* and isFinished. (#1176)

The throw specifier has been moved to a comment.f

This allows for fixing several CIDs on FloatingPointEnumerator: 1457254, 1457258, 1457260, 1457269, 1457270, 1457274, and 1457275.

This also has miscellaneous formatting, documentation and const labeling improvements.

2 files changed, 93 insertions, 90 deletions

diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h
index 265199694..0ae6462bc 100644
--- a/src/theory/fp/type_enumerator.h
+++ b/src/theory/fp/type_enumerator.h
@@ -19,110 +19,112 @@
 #ifndef __CVC4__THEORY__FP__TYPE_ENUMERATOR_H
 #define __CVC4__THEORY__FP__TYPE_ENUMERATOR_H
 
-#include "util/floatingpoint.h"
-#include "util/bitvector.h"
-#include "theory/type_enumerator.h"
-#include "expr/type_node.h"
 #include "expr/kind.h"
+#include "expr/type_node.h"
+#include "theory/type_enumerator.h"
+#include "util/bitvector.h"
+#include "util/floatingpoint.h"
 
 namespace CVC4 {
 namespace theory {
 namespace fp {
 
-class FloatingPointEnumerator : public TypeEnumeratorBase<FloatingPointEnumerator> {
-
-  unsigned e;
-  unsigned s;
-  BitVector state;
-  bool enumerationComplete;
-
-protected :
-
-  FloatingPoint createFP (void) const {
-    // Rotate the LSB into the sign so that NaN is the last value
-    BitVector value = state.logicalRightShift(1) | state.leftShift(state.getSize() - 1);
-    
-    return FloatingPoint(e, s, value);
-  }
-
-
-public:
-
-  FloatingPointEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
-    TypeEnumeratorBase<FloatingPointEnumerator>(type),
-      e(type.getFloatingPointExponentSize()),
-      s(type.getFloatingPointSignificandSize()),
-      state(e + s, 0U),
-      enumerationComplete(false) 
-    {}
-
-
-  Node operator*() throw(NoMoreValuesException) {
-    if (enumerationComplete) {
+class FloatingPointEnumerator
+    : public TypeEnumeratorBase<FloatingPointEnumerator> {
+ public:
+  FloatingPointEnumerator(TypeNode type,
+                          TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<FloatingPointEnumerator>(type),
+        d_e(type.getFloatingPointExponentSize()),
+        d_s(type.getFloatingPointSignificandSize()),
+        d_state(d_e + d_s, 0U),
+        d_enumerationComplete(false) {}
+
+  /** Throws NoMoreValuesException if the enumeration is complete. */
+  Node operator*() override {
+    if (d_enumerationComplete) {
       throw NoMoreValuesException(getType());
     }
     return NodeManager::currentNM()->mkConst(createFP());
   }
 
-  FloatingPointEnumerator& operator++() throw() {
-    FloatingPoint current(createFP());
-
+  FloatingPointEnumerator& operator++() {
+    const FloatingPoint current(createFP());
     if (current.isNaN()) {
-      enumerationComplete = true;
+      d_enumerationComplete = true;
     } else {
-      state = state + BitVector(state.getSize(), 1U);
+      d_state = d_state + BitVector(d_state.getSize(), 1U);
     }
-
     return *this;
   }
 
-  bool isFinished() throw() {
-    return enumerationComplete;
-  }
-
-};/* FloatingPointEnumerator */
-
-class RoundingModeEnumerator : public TypeEnumeratorBase<RoundingModeEnumerator> {
-
-  RoundingMode rm;
-  bool enumerationComplete;
-
-public:
+  bool isFinished() override { return d_enumerationComplete; }
 
-  RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
-    TypeEnumeratorBase<RoundingModeEnumerator>(type),
-      rm(roundNearestTiesToEven),
-      enumerationComplete(false)
-    {}
+ protected:
+  FloatingPoint createFP(void) const {
+    // Rotate the LSB into the sign so that NaN is the last value
+    const BitVector value =
+        d_state.logicalRightShift(1) | d_state.leftShift(d_state.getSize() - 1);
 
+    return FloatingPoint(d_e, d_s, value);
+  }
 
-  Node operator*() throw(NoMoreValuesException) {
-    if (enumerationComplete) {
+ private:
+  const unsigned d_e;
+  const unsigned d_s;
+  BitVector d_state;
+  bool d_enumerationComplete;
+}; /* FloatingPointEnumerator */
+
+class RoundingModeEnumerator
+    : public TypeEnumeratorBase<RoundingModeEnumerator> {
+ public:
+  RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
+      : TypeEnumeratorBase<RoundingModeEnumerator>(type),
+        d_rm(roundNearestTiesToEven),
+        d_enumerationComplete(false) {}
+
+  /** Throws NoMoreValuesException if the enumeration is complete. */
+  Node operator*() override {
+    if (d_enumerationComplete) {
       throw NoMoreValuesException(getType());
     }
-    return NodeManager::currentNM()->mkConst(rm);
+    return NodeManager::currentNM()->mkConst(d_rm);
   }
 
-  RoundingModeEnumerator& operator++() throw() {
-    switch (rm) {
-    case roundNearestTiesToEven : rm = roundTowardPositive; break;
-    case roundTowardPositive : rm = roundTowardNegative; break;
-    case roundTowardNegative : rm = roundTowardZero; break;
-    case roundTowardZero : rm = roundNearestTiesToAway; break;
-    case roundNearestTiesToAway : enumerationComplete = true; break;
-    default : Unreachable("Unknown rounding mode?"); break;
+  RoundingModeEnumerator& operator++() {
+    switch (d_rm) {
+      case roundNearestTiesToEven:
+        d_rm = roundTowardPositive;
+        break;
+      case roundTowardPositive:
+        d_rm = roundTowardNegative;
+        break;
+      case roundTowardNegative:
+        d_rm = roundTowardZero;
+        break;
+      case roundTowardZero:
+        d_rm = roundNearestTiesToAway;
+        break;
+      case roundNearestTiesToAway:
+        d_enumerationComplete = true;
+        break;
+      default:
+        Unreachable("Unknown rounding mode?");
+        break;
     }
     return *this;
   }
 
-  bool isFinished() throw() {
-    return enumerationComplete;
-  }
+  bool isFinished() override { return d_enumerationComplete; }
 
-};/* RoundingModeEnumerator */
+ private:
+  RoundingMode d_rm;
+  bool d_enumerationComplete;
+}; /* RoundingModeEnumerator */
 
-}/* CVC4::theory::fp namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace fp
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* __CVC4__THEORY__FP__TYPE_ENUMERATOR_H */
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index 197363c1f..f8d24f4eb 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -28,39 +28,40 @@ namespace CVC4 {
 namespace theory {
 
 class NoMoreValuesException : public Exception {
-public:
+ public:
   NoMoreValuesException(TypeNode n) throw() :
     Exception("No more values for type `" + n.toString() + "'") {
   }
 };/* class NoMoreValuesException */
 
 class TypeEnumeratorInterface {
-  TypeNode d_type;
-
-public:
-
-  TypeEnumeratorInterface(TypeNode type) :
-    d_type(type) {
-  }
+ public:
+  TypeEnumeratorInterface(TypeNode type) : d_type(type) {}
 
   virtual ~TypeEnumeratorInterface() {}
 
   /** Is this enumerator out of constants to enumerate? */
-  virtual bool isFinished() throw() = 0;
+  virtual bool isFinished() = 0;
 
-  /** Get the current constant of this type (throws if no such constant exists) */
+  /**
+   * Get the current constant of this type.
+   *
+   * @throws NoMoreValuesException if no such constant exists.
+   */
   virtual Node operator*() = 0;
 
-  /** Increment the pointer to the next available constant */
+  /** Increment the pointer to the next available constant. */
   virtual TypeEnumeratorInterface& operator++() = 0;
 
-  /** Clone this enumerator */
+  /** Clone this enumerator. */
   virtual TypeEnumeratorInterface* clone() const = 0;
 
-  /** Get the type from which we're enumerating constants */
-  TypeNode getType() const throw() { return d_type; }
+  /** Get the type from which we're enumerating constants. */
+  TypeNode getType() const { return d_type; }
 
-};/* class TypeEnumeratorInterface */
+ private:
+  const TypeNode d_type;
+}; /* class TypeEnumeratorInterface */
 
 // AJR: This class stores particular information that is relevant to type enumeration.
 //      For finite model finding, we set d_fixed_usort=true,