diff options
author | Tim King <taking@cs.nyu.edu> | 2017-10-01 22:05:49 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-01 22:05:49 -0700 |
commit | 117864affc006f81e4d58ed024ffc1744213fffd (patch) | |
tree | 268b23a3581121b28b28c7403ff29e562ddc84f4 /src/theory/fp | |
parent | 970eb62a87cefbd0449e914dcd60ac9c0580aa7f (diff) |
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.
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/type_enumerator.h | 152 |
1 files changed, 77 insertions, 75 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 */ |