From: Tim King Date: Mon, 2 Oct 2017 05:05:49 +0000 (-0700) Subject: Removing throw specifiers from TypeEnumeratorBase's operator* and isFinished. (#1176) X-Git-Tag: cvc5-1.0.0~5590 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=117864affc006f81e4d58ed024ffc1744213fffd;p=cvc5.git 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. --- 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 { - - 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(type), - e(type.getFloatingPointExponentSize()), - s(type.getFloatingPointSignificandSize()), - state(e + s, 0U), - enumerationComplete(false) - {} - - - Node operator*() throw(NoMoreValuesException) { - if (enumerationComplete) { +class FloatingPointEnumerator + : public TypeEnumeratorBase { + public: + FloatingPointEnumerator(TypeNode type, + TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase(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 { - - RoundingMode rm; - bool enumerationComplete; - -public: + bool isFinished() override { return d_enumerationComplete; } - RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : - TypeEnumeratorBase(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 { + public: + RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) + : TypeEnumeratorBase(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,