diff options
Diffstat (limited to 'src/util/floatingpoint_literal_symfpu.h.in')
| -rw-r--r-- | src/util/floatingpoint_literal_symfpu.h.in | 327 |
1 files changed, 327 insertions, 0 deletions
diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in new file mode 100644 index 000000000..06a98b7ea --- /dev/null +++ b/src/util/floatingpoint_literal_symfpu.h.in @@ -0,0 +1,327 @@ +/********************* */ +/*! \file floatingpoint_literal_symfpu.h.in + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Martin Brain, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief SymFPU glue code for floating-point values. + ** + ** !!! This header is not to be included in any other headers !!! + **/ +#include "cvc4_public.h" + +#ifndef CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H +#define CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H + +#include "util/bitvector.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 CVC4 { + +class FloatingPointSize; +class FloatingPoint; + +/* -------------------------------------------------------------------------- */ + +/** + * 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 + +/* -------------------------------------------------------------------------- */ + +// clang-format off +#if @CVC4_USE_SYMFPU@ +// clang-format on +using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat<symfpuLiteral::traits>; +#endif + +class FloatingPointLiteral +{ + friend class FloatingPoint; + public: + /** Constructors. */ + FloatingPointLiteral(FloatingPoint& other); +// clang-format off +#if @CVC4_USE_SYMFPU@ +// clang-format on + FloatingPointLiteral(SymFPUUnpackedFloatLiteral symuf) : d_symuf(symuf){}; + FloatingPointLiteral(const bool sign, + const BitVector& exp, + const BitVector& sig) + : d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig)) + { + } +#else + FloatingPointLiteral(uint32_t, uint32_t, double) { unfinished(); }; +#endif + ~FloatingPointLiteral() {} + +// clang-format off +#if @CVC4_USE_SYMFPU@ +// clang-format on + /** Return wrapped floating-point literal. */ + const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; } +#else + /** Catch-all for unimplemented functions. */ + void unfinished(void) const; + /** Dummy hash function. */ + size_t hash(void) const; + /** Dummy comparison operator overload. */ + bool operator==(const FloatingPointLiteral& other) const; +#endif + + private: +// clang-format off +#if @CVC4_USE_SYMFPU@ +// clang-format on + /** The actual floating-point value, a SymFPU unpackedFloat. */ + SymFPUUnpackedFloatLiteral d_symuf; +#endif +}; + + +/* -------------------------------------------------------------------------- */ + +} + +#endif |