diff options
Diffstat (limited to 'src/util/floatingpoint_literal_symfpu.h.in')
-rw-r--r-- | src/util/floatingpoint_literal_symfpu.h.in | 250 |
1 files changed, 1 insertions, 249 deletions
diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in index c4352c080..dd58f1beb 100644 --- a/src/util/floatingpoint_literal_symfpu.h.in +++ b/src/util/floatingpoint_literal_symfpu.h.in @@ -20,261 +20,13 @@ #include "util/bitvector.h" #include "util/floatingpoint_size.h" +#include "util/floatingpoint_literal_symfpu_traits.h" #include "util/roundingmode.h" -// clang-format off -#if @CVC4_USE_SYMFPU@ -// clang-format on -#include <symfpu/core/unpackedFloat.h> -#endif /* @CVC4_USE_SYMFPU@ */ - /* -------------------------------------------------------------------------- */ namespace cvc5 { -class FloatingPointSize; -class FloatingPointLiteral; - -/* -------------------------------------------------------------------------- */ - -/** - * 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 = ::cvc5::RoundingMode; -using CVC4FPSize = ::cvc5::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 cvc5::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 - * cvc5::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 - -/* -------------------------------------------------------------------------- */ - // clang-format off #if @CVC4_USE_SYMFPU@ // clang-format on |