diff options
Diffstat (limited to 'src/util/floatingpoint.h.in')
| -rw-r--r-- | src/util/floatingpoint.h.in | 334 |
1 files changed, 4 insertions, 330 deletions
diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in index 7e430ad87..bcf792c56 100644 --- a/src/util/floatingpoint.h.in +++ b/src/util/floatingpoint.h.in @@ -20,10 +20,11 @@ #ifndef CVC4__FLOATINGPOINT_H #define CVC4__FLOATINGPOINT_H -#include <fenv.h> - #include "util/bitvector.h" +#include "util/floatingpoint_size.h" #include "util/rational.h" +#include "util/roundingmode.h" +#include "util/symfpu_literal.h" // clang-format off #if @CVC4_USE_SYMFPU@ @@ -31,340 +32,13 @@ #include <symfpu/core/unpackedFloat.h> #endif /* @CVC4_USE_SYMFPU@ */ -namespace CVC4 { -// Inline these! -inline bool CVC4_PUBLIC validExponentSize(uint32_t e) { return e >= 2; } -inline bool CVC4_PUBLIC validSignificandSize(uint32_t s) { return s >= 2; } - -/* -------------------------------------------------------------------------- */ - -/** - * Floating point sorts are parameterised by two constants > 1 giving the - * width (in bits) of the exponent and significand (including the hidden bit). - * So, IEEE-754 single precision, a.k.a. float, is described as 8 24. - */ -class CVC4_PUBLIC FloatingPointSize -{ - public: - /** Constructors. */ - FloatingPointSize(uint32_t exp_size, uint32_t sig_size); - FloatingPointSize(const FloatingPointSize& old); - - /** Operator overload for equality comparison. */ - bool operator==(const FloatingPointSize& fps) const - { - return (d_exp_size == fps.d_exp_size) && (d_sig_size == fps.d_sig_size); - } - - /** Implement the interface that symfpu uses for floating-point formats. */ - - /** Get the exponent bit-width of this floating-point format. */ - inline uint32_t exponentWidth(void) const { return this->d_exp_size; } - /** Get the significand bit-width of this floating-point format. */ - inline uint32_t significandWidth(void) const { return this->d_sig_size; } - /** - * Get the bit-width of the packed representation of this floating-point - * format (= exponent + significand bit-width, convenience wrapper). - */ - inline uint32_t packedWidth(void) const - { - return this->exponentWidth() + this->significandWidth(); - } - /** - * Get the exponent bit-width of the packed representation of this - * floating-point format (= exponent bit-width). - */ - inline uint32_t packedExponentWidth(void) const - { - return this->exponentWidth(); - } - /** - * Get the significand bit-width of the packed representation of this - * floating-point format (= significand bit-width - 1). - */ - inline uint32_t packedSignificandWidth(void) const - { - return this->significandWidth() - 1; - } - - private: - /** Exponent bit-width. */ - uint32_t d_exp_size; - /** Significand bit-width. */ - uint32_t d_sig_size; - -}; /* class FloatingPointSize */ - -/** - * Hash function for floating point formats. - */ -struct CVC4_PUBLIC FloatingPointSizeHashFunction -{ - static inline size_t ROLL(size_t X, size_t N) - { - return (((X) << (N)) | ((X) >> (8 * sizeof((X)) - (N)))); - } - - inline size_t operator()(const FloatingPointSize& t) const - { - return size_t(ROLL(t.exponentWidth(), 4 * sizeof(uint32_t)) - | t.significandWidth()); - } -}; /* struct FloatingPointSizeHashFunction */ - /* -------------------------------------------------------------------------- */ -/** - * A concrete instance of the rounding mode sort - */ -enum CVC4_PUBLIC RoundingMode -{ - roundNearestTiesToEven = FE_TONEAREST, - roundTowardPositive = FE_UPWARD, - roundTowardNegative = FE_DOWNWARD, - roundTowardZero = FE_TOWARDZERO, - // Initializes this to the diagonalization of the 4 other values. - roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) - | ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8)) -}; /* enum RoundingMode */ - -/** - * Hash function for rounding mode values. - */ -struct CVC4_PUBLIC RoundingModeHashFunction -{ - inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); } -}; /* struct RoundingModeHashFunction */ +namespace CVC4 { /* -------------------------------------------------------------------------- */ /** - * This is a symfpu literal "back-end". It allows the library to be used as - * an arbitrary precision floating-point implementation. This is effectively - * the glue between symfpu's notion of "signed bit-vector" and CVC4's - * BitVector. - */ -namespace symfpuLiteral { - -/** - * Forward declaration of wrapper so that traits can be defined early and so - * used in the implementation of wrappedBitVector. - */ -template <bool T> -class wrappedBitVector; - -using CVC4BitWidth = uint32_t; -using CVC4Prop = bool; -using CVC4RM = ::CVC4::RoundingMode; -using CVC4FPSize = ::CVC4::FloatingPointSize; -using CVC4UnsignedBitVector = wrappedBitVector<false>; -using CVC4SignedBitVector = wrappedBitVector<true>; - -/** - * This is the template parameter for symfpu's templates. - */ -class traits -{ - public: - /** The six key types that symfpu uses. */ - using bwt = CVC4BitWidth; // bit-width type - using prop = CVC4Prop; // boolean type - using rm = CVC4RM; // rounding-mode type - using fpt = CVC4FPSize; // floating-point format type - using ubv = CVC4UnsignedBitVector; // unsigned bit-vector type - using sbv = CVC4SignedBitVector; // signed bit-vector type - - /** Give concrete instances of each rounding mode, mainly for comparisons. */ - static rm RNE(void); - static rm RNA(void); - static rm RTP(void); - static rm RTN(void); - static rm RTZ(void); - - /** The sympfu properties. */ - static void precondition(const prop& p); - static void postcondition(const prop& p); - static void invariant(const prop& p); -}; - -/** - * Type function for mapping between types. - */ -template <bool T> -struct signedToLiteralType; - -template <> -struct signedToLiteralType<true> -{ - using literalType = int32_t; -}; -template <> -struct signedToLiteralType<false> -{ - using literalType = uint32_t; -}; - -/** - * This extends the interface for CVC4::BitVector for compatibility with symFPU. - * The template parameter distinguishes signed and unsigned bit-vectors, a - * distinction symfpu uses. - */ -template <bool isSigned> -class wrappedBitVector : public BitVector -{ - protected: - using literalType = typename signedToLiteralType<isSigned>::literalType; - friend wrappedBitVector<!isSigned>; // To allow conversion between types - -// clang-format off -#if @CVC4_USE_SYMFPU@ - // clang-format on - friend ::symfpu::ite<CVC4Prop, wrappedBitVector<isSigned> >; // For ITE -#endif /* @CVC4_USE_SYMFPU@ */ - - public: - /** Constructors. */ - wrappedBitVector(const CVC4BitWidth w, const uint32_t v) : BitVector(w, v) {} - wrappedBitVector(const CVC4Prop& p) : BitVector(1, p ? 1U : 0U) {} - wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {} - wrappedBitVector(const BitVector& old) : BitVector(old) {} - - /** Get the bit-width of this wrapped bit-vector. */ - CVC4BitWidth getWidth(void) const { return getSize(); } - - /** Create a zero value of given bit-width 'w'. */ - static wrappedBitVector<isSigned> one(const CVC4BitWidth& w); - /** Create a one value of given bit-width 'w'. */ - static wrappedBitVector<isSigned> zero(const CVC4BitWidth& w); - /** Create a ones value (all bits 1) of given bit-width 'w'. */ - static wrappedBitVector<isSigned> allOnes(const CVC4BitWidth& w); - /** Create a maximum signed/unsigned value of given bit-width 'w'. */ - static wrappedBitVector<isSigned> maxValue(const CVC4BitWidth& w); - /** Create a minimum signed/unsigned value of given bit-width 'w'. */ - static wrappedBitVector<isSigned> minValue(const CVC4BitWidth& w); - - /** Return true if this a bit-vector representing a ones value. */ - CVC4Prop isAllOnes() const; - /** Return true if this a bit-vector representing a zero value. */ - CVC4Prop isAllZeros() const; - - /** Left shift. */ - wrappedBitVector<isSigned> operator<<( - const wrappedBitVector<isSigned>& op) const; - /** Logical (unsigned) and arithmetic (signed) right shift. */ - wrappedBitVector<isSigned> operator>>( - const wrappedBitVector<isSigned>& op) const; - - /** - * Inherited but ... - * *sigh* if we use the inherited version then it will return a - * CVC4::BitVector which can be converted back to a - * wrappedBitVector<isSigned> but isn't done automatically when working - * out types for templates instantiation. ITE is a particular - * problem as expressions and constants no longer derive the - * same type. There aren't any good solutions in C++, we could - * use CRTP but Liana wouldn't appreciate that, so the following - * pointless wrapping functions are needed. - */ - - /** Bit-wise or. */ - wrappedBitVector<isSigned> operator|( - const wrappedBitVector<isSigned>& op) const; - /** Bit-wise and. */ - wrappedBitVector<isSigned> operator&( - const wrappedBitVector<isSigned>& op) const; - /** Bit-vector addition. */ - wrappedBitVector<isSigned> operator+( - const wrappedBitVector<isSigned>& op) const; - /** Bit-vector subtraction. */ - wrappedBitVector<isSigned> operator-( - const wrappedBitVector<isSigned>& op) const; - /** Bit-vector multiplication. */ - wrappedBitVector<isSigned> operator*( - const wrappedBitVector<isSigned>& op) const; - /** Bit-vector signed/unsigned division. */ - wrappedBitVector<isSigned> operator/( - const wrappedBitVector<isSigned>& op) const; - /** Bit-vector signed/unsigned remainder. */ - wrappedBitVector<isSigned> operator%( - const wrappedBitVector<isSigned>& op) const; - /** Bit-vector negation. */ - wrappedBitVector<isSigned> operator-(void) const; - /** Bit-wise not. */ - wrappedBitVector<isSigned> operator~(void) const; - - /** Bit-vector increment. */ - wrappedBitVector<isSigned> increment() const; - /** Bit-vector decrement. */ - wrappedBitVector<isSigned> decrement() const; - /** - * Bit-vector logical/arithmetic right shift where 'op' extended to the - * bit-width of this wrapped bit-vector. - */ - wrappedBitVector<isSigned> signExtendRightShift( - const wrappedBitVector<isSigned>& op) const; - - /** - * Modular operations. - * Note: No overflow checking so these are the same as other operations. - */ - wrappedBitVector<isSigned> modularLeftShift( - const wrappedBitVector<isSigned>& op) const; - wrappedBitVector<isSigned> modularRightShift( - const wrappedBitVector<isSigned>& op) const; - wrappedBitVector<isSigned> modularIncrement() const; - wrappedBitVector<isSigned> modularDecrement() const; - wrappedBitVector<isSigned> modularAdd( - const wrappedBitVector<isSigned>& op) const; - wrappedBitVector<isSigned> modularNegate() const; - - /** Bit-vector equality. */ - CVC4Prop operator==(const wrappedBitVector<isSigned>& op) const; - /** Bit-vector signed/unsigned less or equal than. */ - CVC4Prop operator<=(const wrappedBitVector<isSigned>& op) const; - /** Bit-vector sign/unsigned greater or equal than. */ - CVC4Prop operator>=(const wrappedBitVector<isSigned>& op) const; - /** Bit-vector signed/unsigned less than. */ - CVC4Prop operator<(const wrappedBitVector<isSigned>& op) const; - /** Bit-vector sign/unsigned greater or equal than. */ - CVC4Prop operator>(const wrappedBitVector<isSigned>& op) const; - - /** Convert this bit-vector to a signed bit-vector. */ - wrappedBitVector<true> toSigned(void) const; - /** Convert this bit-vector to an unsigned bit-vector. */ - wrappedBitVector<false> toUnsigned(void) const; - - /** Bit-vector signed/unsigned (zero) extension. */ - wrappedBitVector<isSigned> extend(CVC4BitWidth extension) const; - /** - * Create a "contracted" bit-vector by cutting off the 'reduction' number of - * most significant bits, i.e., by extracting the (bit-width - reduction) - * least significant bits. - */ - wrappedBitVector<isSigned> contract(CVC4BitWidth reduction) const; - /** - * Create a "resized" bit-vector of given size bei either extending (if new - * size is larger) or contracting (if it is smaller) this wrapped bit-vector. - */ - wrappedBitVector<isSigned> resize(CVC4BitWidth newSize) const; - /** - * Create an extension of this bit-vector that matches the bit-width of the - * given bit-vector. - * Note: The size of the given bit-vector may not be larger than the size of - * this bit-vector. - */ - wrappedBitVector<isSigned> matchWidth( - const wrappedBitVector<isSigned>& op) const; - /** Bit-vector concatenation. */ - wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const; - - /** Inclusive of end points, thus if the same, extracts just one bit. */ - wrappedBitVector<isSigned> extract(CVC4BitWidth upper, - CVC4BitWidth lower) const; -}; -} // namespace symfpuLiteral - -/** * A concrete floating point value. */ // clang-format off |