#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 */
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,