From: Aina Niemetz Date: Thu, 1 Apr 2021 21:25:03 +0000 (-0700) Subject: FP: Factor out symfpu traits. (#6246) X-Git-Tag: cvc5-1.0.0~1987 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7fa534c85cbb6eb2863f10840b39501a21acc0b9;p=cvc5.git FP: Factor out symfpu traits. (#6246) This is in preparation for a MPFR floating-point literal implementation. We will need to have both literal kinds return a symFPU unpacked float via `getSymUF()` in order to be able to plug it into the fp_converter. For this, it makes sense to have the traits implemented and to be included separately, so that they can also be included in the MPFR implementation. --- diff --git a/src/api/checks.h b/src/api/checks.h index 175388bf4..e4505c1e6 100644 --- a/src/api/checks.h +++ b/src/api/checks.h @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Check macros for the CVC5 C++ API. + ** \brief Check macros for the cvc5 C++ API. ** - ** These macros implement guards for the CVC5 C++ API functions. + ** These macros implement guards for the cvc5 C++ API functions. **/ #include "cvc4_public.h" diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 52a811cb9..2ca6ab605 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -9,6 +9,8 @@ ## directory for licensing information. ## configure_file(floatingpoint_literal_symfpu.h.in floatingpoint_literal_symfpu.h) +configure_file(floatingpoint_literal_symfpu_traits.h.in + floatingpoint_literal_symfpu_traits.h) configure_file(rational.h.in rational.h) configure_file(integer.h.in integer.h) configure_file(real_algebraic_number.h.in real_algebraic_number.h) @@ -29,6 +31,8 @@ libcvc4_add_sources( floatingpoint.h floatingpoint_size.cpp floatingpoint_size.h + floatingpoint_literal_symfpu.cpp + floatingpoint_literal_symfpu_traits.cpp gmp_util.h hash.h iand.h @@ -69,7 +73,6 @@ libcvc4_add_sources( stats_utils.h string.cpp string.h - floatingpoint_literal_symfpu.cpp tuple.h unsafe_interrupt_exception.h utility.cpp diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index 666c3438d..011bce16d 100644 --- a/src/util/floatingpoint_literal_symfpu.cpp +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -39,9 +39,9 @@ namespace symfpu { #define CVC4_LIT_ITE_DFN(T) \ template <> \ - struct ite<::cvc5::symfpuLiteral::CVC4Prop, T> \ + struct ite<::cvc5::symfpuLiteral::Cvc5Prop, T> \ { \ - static const T& iteOp(const ::cvc5::symfpuLiteral::CVC4Prop& cond, \ + static const T& iteOp(const ::cvc5::symfpuLiteral::Cvc5Prop& cond, \ const T& l, \ const T& r) \ { \ @@ -90,7 +90,7 @@ FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size, #ifdef CVC4_USE_SYMFPU , d_symuf(symfpu::unpack( - symfpuLiteral::CVC4FPSize(exp_size, sig_size), bv)) + symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv)) #endif { } @@ -140,13 +140,13 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, #ifdef CVC4_USE_SYMFPU , d_symuf(signedBV ? symfpu::convertSBVToFloat( - symfpuLiteral::CVC4FPSize(size), - symfpuLiteral::CVC4RM(rm), - symfpuLiteral::CVC4SignedBitVector(bv)) + symfpuLiteral::Cvc5FPSize(size), + symfpuLiteral::Cvc5RM(rm), + symfpuLiteral::Cvc5SignedBitVector(bv)) : symfpu::convertUBVToFloat( - symfpuLiteral::CVC4FPSize(size), - symfpuLiteral::CVC4RM(rm), - symfpuLiteral::CVC4UnsignedBitVector(bv))) + symfpuLiteral::Cvc5FPSize(size), + symfpuLiteral::Cvc5RM(rm), + symfpuLiteral::Cvc5UnsignedBitVector(bv))) #endif { } @@ -517,393 +517,4 @@ size_t FloatingPointLiteral::hash(void) const } #endif -namespace symfpuLiteral { - -// To simplify the property macros -typedef traits t; - -template -wrappedBitVector wrappedBitVector::one( - const CVC4BitWidth& w) -{ - return wrappedBitVector(w, 1); -} - -template -wrappedBitVector wrappedBitVector::zero( - const CVC4BitWidth& w) -{ - return wrappedBitVector(w, 0); -} - -template -wrappedBitVector wrappedBitVector::allOnes( - const CVC4BitWidth& w) -{ - return ~wrappedBitVector::zero(w); -} - -template -CVC4Prop wrappedBitVector::isAllOnes() const -{ - return (*this == wrappedBitVector::allOnes(getWidth())); -} -template -CVC4Prop wrappedBitVector::isAllZeros() const -{ - return (*this == wrappedBitVector::zero(getWidth())); -} - -template -wrappedBitVector wrappedBitVector::maxValue( - const CVC4BitWidth& w) -{ - if (isSigned) - { - BitVector base(w - 1, 0U); - return wrappedBitVector((~base).zeroExtend(1)); - } - else - { - return wrappedBitVector::allOnes(w); - } -} - -template -wrappedBitVector wrappedBitVector::minValue( - const CVC4BitWidth& w) -{ - if (isSigned) - { - BitVector base(w, 1U); - BitVector shiftAmount(w, w - 1); - BitVector result(base.leftShift(shiftAmount)); - return wrappedBitVector(result); - } - else - { - return wrappedBitVector::zero(w); - } -} - -/*** Operators ***/ -template -wrappedBitVector wrappedBitVector::operator<<( - const wrappedBitVector& op) const -{ - return BitVector::leftShift(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator>>( - const wrappedBitVector& op) const -{ - return BitVector::arithRightShift(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator>>( - const wrappedBitVector& op) const -{ - return BitVector::logicalRightShift(op); -} - -template -wrappedBitVector wrappedBitVector::operator|( - const wrappedBitVector& op) const -{ - return BitVector::operator|(op); -} - -template -wrappedBitVector wrappedBitVector::operator&( - const wrappedBitVector& op) const -{ - return BitVector::operator&(op); -} - -template -wrappedBitVector wrappedBitVector::operator+( - const wrappedBitVector& op) const -{ - return BitVector::operator+(op); -} - -template -wrappedBitVector wrappedBitVector::operator-( - const wrappedBitVector& op) const -{ - return BitVector::operator-(op); -} - -template -wrappedBitVector wrappedBitVector::operator*( - const wrappedBitVector& op) const -{ - return BitVector::operator*(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator/( - const wrappedBitVector& op) const -{ - return BitVector::unsignedDivTotal(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator%( - const wrappedBitVector& op) const -{ - return BitVector::unsignedRemTotal(op); -} - -template -wrappedBitVector wrappedBitVector::operator-(void) const -{ - return BitVector::operator-(); -} - -template -wrappedBitVector wrappedBitVector::operator~(void) const -{ - return BitVector::operator~(); -} - -template -wrappedBitVector wrappedBitVector::increment() const -{ - return *this + wrappedBitVector::one(getWidth()); -} - -template -wrappedBitVector wrappedBitVector::decrement() const -{ - return *this - wrappedBitVector::one(getWidth()); -} - -template -wrappedBitVector wrappedBitVector::signExtendRightShift( - const wrappedBitVector& op) const -{ - return BitVector::arithRightShift(BitVector(getWidth(), op)); -} - -/*** Modular opertaions ***/ -// No overflow checking so these are the same as other operations -template -wrappedBitVector wrappedBitVector::modularLeftShift( - const wrappedBitVector& op) const -{ - return *this << op; -} - -template -wrappedBitVector wrappedBitVector::modularRightShift( - const wrappedBitVector& op) const -{ - return *this >> op; -} - -template -wrappedBitVector wrappedBitVector::modularIncrement() const -{ - return increment(); -} - -template -wrappedBitVector wrappedBitVector::modularDecrement() const -{ - return decrement(); -} - -template -wrappedBitVector wrappedBitVector::modularAdd( - const wrappedBitVector& op) const -{ - return *this + op; -} - -template -wrappedBitVector wrappedBitVector::modularNegate() const -{ - return -(*this); -} - -/*** Comparisons ***/ - -template -CVC4Prop wrappedBitVector::operator==( - const wrappedBitVector& op) const -{ - return BitVector::operator==(op); -} - -template <> -CVC4Prop wrappedBitVector::operator<=( - const wrappedBitVector& op) const -{ - return signedLessThanEq(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>=( - const wrappedBitVector& op) const -{ - return !(signedLessThan(op)); -} - -template <> -CVC4Prop wrappedBitVector::operator<( - const wrappedBitVector& op) const -{ - return signedLessThan(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>( - const wrappedBitVector& op) const -{ - return !(signedLessThanEq(op)); -} - -template <> -CVC4Prop wrappedBitVector::operator<=( - const wrappedBitVector& op) const -{ - return unsignedLessThanEq(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>=( - const wrappedBitVector& op) const -{ - return !(unsignedLessThan(op)); -} - -template <> -CVC4Prop wrappedBitVector::operator<( - const wrappedBitVector& op) const -{ - return unsignedLessThan(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>( - const wrappedBitVector& op) const -{ - return !(unsignedLessThanEq(op)); -} - -/*** Type conversion ***/ -// CVC4 nodes make no distinction between signed and unsigned, thus ... -template -wrappedBitVector wrappedBitVector::toSigned(void) const -{ - return wrappedBitVector(*this); -} - -template -wrappedBitVector wrappedBitVector::toUnsigned(void) const -{ - return wrappedBitVector(*this); -} - -/*** Bit hacks ***/ - -template -wrappedBitVector wrappedBitVector::extend( - CVC4BitWidth extension) const -{ - if (isSigned) - { - return BitVector::signExtend(extension); - } - else - { - return BitVector::zeroExtend(extension); - } -} - -template -wrappedBitVector wrappedBitVector::contract( - CVC4BitWidth reduction) const -{ - Assert(getWidth() > reduction); - - return extract((getWidth() - 1) - reduction, 0); -} - -template -wrappedBitVector wrappedBitVector::resize( - CVC4BitWidth newSize) const -{ - CVC4BitWidth width = getWidth(); - - if (newSize > width) - { - return extend(newSize - width); - } - else if (newSize < width) - { - return contract(width - newSize); - } - else - { - return *this; - } -} - -template -wrappedBitVector wrappedBitVector::matchWidth( - const wrappedBitVector& op) const -{ - Assert(getWidth() <= op.getWidth()); - return extend(op.getWidth() - getWidth()); -} - -template -wrappedBitVector wrappedBitVector::append( - const wrappedBitVector& op) const -{ - return BitVector::concat(op); -} - -// Inclusive of end points, thus if the same, extracts just one bit -template -wrappedBitVector wrappedBitVector::extract( - CVC4BitWidth upper, CVC4BitWidth lower) const -{ - Assert(upper >= lower); - return BitVector::extract(upper, lower); -} - -// Explicit instantiation -template class wrappedBitVector; -template class wrappedBitVector; - -traits::rm traits::RNE(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_EVEN; }; -traits::rm traits::RNA(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_AWAY; }; -traits::rm traits::RTP(void) { return ::cvc5::ROUND_TOWARD_POSITIVE; }; -traits::rm traits::RTN(void) { return ::cvc5::ROUND_TOWARD_NEGATIVE; }; -traits::rm traits::RTZ(void) { return ::cvc5::ROUND_TOWARD_ZERO; }; -// This is a literal back-end so props are actually bools -// so these can be handled in the same way as the internal assertions above - -void traits::precondition(const traits::prop& p) -{ - Assert(p); - return; -} -void traits::postcondition(const traits::prop& p) -{ - Assert(p); - return; -} -void traits::invariant(const traits::prop& p) -{ - Assert(p); - return; -} -} // namespace symfpuLiteral - } // namespace cvc5 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 -#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 -class wrappedBitVector; - -using CVC4BitWidth = uint32_t; -using CVC4Prop = bool; -using CVC4RM = ::cvc5::RoundingMode; -using CVC4FPSize = ::cvc5::FloatingPointSize; -using CVC4UnsignedBitVector = wrappedBitVector; -using CVC4SignedBitVector = wrappedBitVector; - -/** - * 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 -struct signedToLiteralType; - -template <> -struct signedToLiteralType -{ - using literalType = int32_t; -}; -template <> -struct signedToLiteralType -{ - 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 -class wrappedBitVector : public BitVector -{ - protected: - using literalType = typename signedToLiteralType::literalType; - friend wrappedBitVector; // To allow conversion between types - -// clang-format off -#if @CVC4_USE_SYMFPU@ - // clang-format on - friend ::symfpu::ite >; // 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& 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 one(const CVC4BitWidth& w); - /** Create a one value of given bit-width 'w'. */ - static wrappedBitVector zero(const CVC4BitWidth& w); - /** Create a ones value (all bits 1) of given bit-width 'w'. */ - static wrappedBitVector allOnes(const CVC4BitWidth& w); - /** Create a maximum signed/unsigned value of given bit-width 'w'. */ - static wrappedBitVector maxValue(const CVC4BitWidth& w); - /** Create a minimum signed/unsigned value of given bit-width 'w'. */ - static wrappedBitVector 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 operator<<( - const wrappedBitVector& op) const; - /** Logical (unsigned) and arithmetic (signed) right shift. */ - wrappedBitVector operator>>( - const wrappedBitVector& 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 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 operator|( - const wrappedBitVector& op) const; - /** Bit-wise and. */ - wrappedBitVector operator&( - const wrappedBitVector& op) const; - /** Bit-vector addition. */ - wrappedBitVector operator+( - const wrappedBitVector& op) const; - /** Bit-vector subtraction. */ - wrappedBitVector operator-( - const wrappedBitVector& op) const; - /** Bit-vector multiplication. */ - wrappedBitVector operator*( - const wrappedBitVector& op) const; - /** Bit-vector signed/unsigned division. */ - wrappedBitVector operator/( - const wrappedBitVector& op) const; - /** Bit-vector signed/unsigned remainder. */ - wrappedBitVector operator%( - const wrappedBitVector& op) const; - /** Bit-vector negation. */ - wrappedBitVector operator-(void) const; - /** Bit-wise not. */ - wrappedBitVector operator~(void) const; - - /** Bit-vector increment. */ - wrappedBitVector increment() const; - /** Bit-vector decrement. */ - wrappedBitVector decrement() const; - /** - * Bit-vector logical/arithmetic right shift where 'op' extended to the - * bit-width of this wrapped bit-vector. - */ - wrappedBitVector signExtendRightShift( - const wrappedBitVector& op) const; - - /** - * Modular operations. - * Note: No overflow checking so these are the same as other operations. - */ - wrappedBitVector modularLeftShift( - const wrappedBitVector& op) const; - wrappedBitVector modularRightShift( - const wrappedBitVector& op) const; - wrappedBitVector modularIncrement() const; - wrappedBitVector modularDecrement() const; - wrappedBitVector modularAdd( - const wrappedBitVector& op) const; - wrappedBitVector modularNegate() const; - - /** Bit-vector equality. */ - CVC4Prop operator==(const wrappedBitVector& op) const; - /** Bit-vector signed/unsigned less or equal than. */ - CVC4Prop operator<=(const wrappedBitVector& op) const; - /** Bit-vector sign/unsigned greater or equal than. */ - CVC4Prop operator>=(const wrappedBitVector& op) const; - /** Bit-vector signed/unsigned less than. */ - CVC4Prop operator<(const wrappedBitVector& op) const; - /** Bit-vector sign/unsigned greater or equal than. */ - CVC4Prop operator>(const wrappedBitVector& op) const; - - /** Convert this bit-vector to a signed bit-vector. */ - wrappedBitVector toSigned(void) const; - /** Convert this bit-vector to an unsigned bit-vector. */ - wrappedBitVector toUnsigned(void) const; - - /** Bit-vector signed/unsigned (zero) extension. */ - wrappedBitVector 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 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 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 matchWidth( - const wrappedBitVector& op) const; - - /** Bit-vector concatenation. */ - wrappedBitVector append(const wrappedBitVector& op) const; - - /** Inclusive of end points, thus if the same, extracts just one bit. */ - wrappedBitVector extract(CVC4BitWidth upper, - CVC4BitWidth lower) const; -}; - -/* -------------------------------------------------------------------------- */ - -} // namespace symfpuLiteral - -/* -------------------------------------------------------------------------- */ - // clang-format off #if @CVC4_USE_SYMFPU@ // clang-format on diff --git a/src/util/floatingpoint_literal_symfpu_traits.cpp b/src/util/floatingpoint_literal_symfpu_traits.cpp new file mode 100644 index 000000000..fe814317d --- /dev/null +++ b/src/util/floatingpoint_literal_symfpu_traits.cpp @@ -0,0 +1,409 @@ +/********************* */ +/*! \file floatingpoint_literal_symfpu_traits.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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. + **/ + +#if CVC4_USE_SYMFPU + +#include "util/floatingpoint_literal_symfpu_traits.h" + +#include "base/check.h" + +namespace cvc5 { +namespace symfpuLiteral { + +template +wrappedBitVector wrappedBitVector::one( + const Cvc5BitWidth& w) +{ + return wrappedBitVector(w, 1); +} + +template +wrappedBitVector wrappedBitVector::zero( + const Cvc5BitWidth& w) +{ + return wrappedBitVector(w, 0); +} + +template +wrappedBitVector wrappedBitVector::allOnes( + const Cvc5BitWidth& w) +{ + return ~wrappedBitVector::zero(w); +} + +template +Cvc5Prop wrappedBitVector::isAllOnes() const +{ + return (*this == wrappedBitVector::allOnes(getWidth())); +} +template +Cvc5Prop wrappedBitVector::isAllZeros() const +{ + return (*this == wrappedBitVector::zero(getWidth())); +} + +template +wrappedBitVector wrappedBitVector::maxValue( + const Cvc5BitWidth& w) +{ + if (isSigned) + { + BitVector base(w - 1, 0U); + return wrappedBitVector((~base).zeroExtend(1)); + } + else + { + return wrappedBitVector::allOnes(w); + } +} + +template +wrappedBitVector wrappedBitVector::minValue( + const Cvc5BitWidth& w) +{ + if (isSigned) + { + BitVector base(w, 1U); + BitVector shiftAmount(w, w - 1); + BitVector result(base.leftShift(shiftAmount)); + return wrappedBitVector(result); + } + else + { + return wrappedBitVector::zero(w); + } +} + +/*** Operators ***/ +template +wrappedBitVector wrappedBitVector::operator<<( + const wrappedBitVector& op) const +{ + return BitVector::leftShift(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator>>( + const wrappedBitVector& op) const +{ + return BitVector::arithRightShift(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator>>( + const wrappedBitVector& op) const +{ + return BitVector::logicalRightShift(op); +} + +template +wrappedBitVector wrappedBitVector::operator|( + const wrappedBitVector& op) const +{ + return BitVector::operator|(op); +} + +template +wrappedBitVector wrappedBitVector::operator&( + const wrappedBitVector& op) const +{ + return BitVector::operator&(op); +} + +template +wrappedBitVector wrappedBitVector::operator+( + const wrappedBitVector& op) const +{ + return BitVector::operator+(op); +} + +template +wrappedBitVector wrappedBitVector::operator-( + const wrappedBitVector& op) const +{ + return BitVector::operator-(op); +} + +template +wrappedBitVector wrappedBitVector::operator*( + const wrappedBitVector& op) const +{ + return BitVector::operator*(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator/( + const wrappedBitVector& op) const +{ + return BitVector::unsignedDivTotal(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator%( + const wrappedBitVector& op) const +{ + return BitVector::unsignedRemTotal(op); +} + +template +wrappedBitVector wrappedBitVector::operator-(void) const +{ + return BitVector::operator-(); +} + +template +wrappedBitVector wrappedBitVector::operator~(void) const +{ + return BitVector::operator~(); +} + +template +wrappedBitVector wrappedBitVector::increment() const +{ + return *this + wrappedBitVector::one(getWidth()); +} + +template +wrappedBitVector wrappedBitVector::decrement() const +{ + return *this - wrappedBitVector::one(getWidth()); +} + +template +wrappedBitVector wrappedBitVector::signExtendRightShift( + const wrappedBitVector& op) const +{ + return BitVector::arithRightShift(BitVector(getWidth(), op)); +} + +/*** Modular opertaions ***/ +// No overflow checking so these are the same as other operations +template +wrappedBitVector wrappedBitVector::modularLeftShift( + const wrappedBitVector& op) const +{ + return *this << op; +} + +template +wrappedBitVector wrappedBitVector::modularRightShift( + const wrappedBitVector& op) const +{ + return *this >> op; +} + +template +wrappedBitVector wrappedBitVector::modularIncrement() const +{ + return increment(); +} + +template +wrappedBitVector wrappedBitVector::modularDecrement() const +{ + return decrement(); +} + +template +wrappedBitVector wrappedBitVector::modularAdd( + const wrappedBitVector& op) const +{ + return *this + op; +} + +template +wrappedBitVector wrappedBitVector::modularNegate() const +{ + return -(*this); +} + +/*** Comparisons ***/ + +template +Cvc5Prop wrappedBitVector::operator==( + const wrappedBitVector& op) const +{ + return BitVector::operator==(op); +} + +template <> +Cvc5Prop wrappedBitVector::operator<=( + const wrappedBitVector& op) const +{ + return signedLessThanEq(op); +} + +template <> +Cvc5Prop wrappedBitVector::operator>=( + const wrappedBitVector& op) const +{ + return !(signedLessThan(op)); +} + +template <> +Cvc5Prop wrappedBitVector::operator<( + const wrappedBitVector& op) const +{ + return signedLessThan(op); +} + +template <> +Cvc5Prop wrappedBitVector::operator>( + const wrappedBitVector& op) const +{ + return !(signedLessThanEq(op)); +} + +template <> +Cvc5Prop wrappedBitVector::operator<=( + const wrappedBitVector& op) const +{ + return unsignedLessThanEq(op); +} + +template <> +Cvc5Prop wrappedBitVector::operator>=( + const wrappedBitVector& op) const +{ + return !(unsignedLessThan(op)); +} + +template <> +Cvc5Prop wrappedBitVector::operator<( + const wrappedBitVector& op) const +{ + return unsignedLessThan(op); +} + +template <> +Cvc5Prop wrappedBitVector::operator>( + const wrappedBitVector& op) const +{ + return !(unsignedLessThanEq(op)); +} + +/*** Type conversion ***/ + +// Node makes no distinction between signed and unsigned, thus ... +template +wrappedBitVector wrappedBitVector::toSigned(void) const +{ + return wrappedBitVector(*this); +} + +template +wrappedBitVector wrappedBitVector::toUnsigned(void) const +{ + return wrappedBitVector(*this); +} + +/*** Bit hacks ***/ + +template +wrappedBitVector wrappedBitVector::extend( + Cvc5BitWidth extension) const +{ + if (isSigned) + { + return BitVector::signExtend(extension); + } + else + { + return BitVector::zeroExtend(extension); + } +} + +template +wrappedBitVector wrappedBitVector::contract( + Cvc5BitWidth reduction) const +{ + Assert(getWidth() > reduction); + + return extract((getWidth() - 1) - reduction, 0); +} + +template +wrappedBitVector wrappedBitVector::resize( + Cvc5BitWidth newSize) const +{ + Cvc5BitWidth width = getWidth(); + + if (newSize > width) + { + return extend(newSize - width); + } + else if (newSize < width) + { + return contract(width - newSize); + } + else + { + return *this; + } +} + +template +wrappedBitVector wrappedBitVector::matchWidth( + const wrappedBitVector& op) const +{ + Assert(getWidth() <= op.getWidth()); + return extend(op.getWidth() - getWidth()); +} + +template +wrappedBitVector wrappedBitVector::append( + const wrappedBitVector& op) const +{ + return BitVector::concat(op); +} + +// Inclusive of end points, thus if the same, extracts just one bit +template +wrappedBitVector wrappedBitVector::extract( + Cvc5BitWidth upper, Cvc5BitWidth lower) const +{ + Assert(upper >= lower); + return BitVector::extract(upper, lower); +} + +// Explicit instantiation +template class wrappedBitVector; +template class wrappedBitVector; + +traits::rm traits::RNE(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_EVEN; }; +traits::rm traits::RNA(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_AWAY; }; +traits::rm traits::RTP(void) { return ::cvc5::ROUND_TOWARD_POSITIVE; }; +traits::rm traits::RTN(void) { return ::cvc5::ROUND_TOWARD_NEGATIVE; }; +traits::rm traits::RTZ(void) { return ::cvc5::ROUND_TOWARD_ZERO; }; +// This is a literal back-end so props are actually bools +// so these can be handled in the same way as the internal assertions above + +void traits::precondition(const traits::prop& p) +{ + Assert(p); + return; +} +void traits::postcondition(const traits::prop& p) +{ + Assert(p); + return; +} +void traits::invariant(const traits::prop& p) +{ + Assert(p); + return; +} +} // namespace symfpuLiteral +} // namespace cvc5 +#endif diff --git a/src/util/floatingpoint_literal_symfpu_traits.h.in b/src/util/floatingpoint_literal_symfpu_traits.h.in new file mode 100644 index 000000000..8bda58cfe --- /dev/null +++ b/src/util/floatingpoint_literal_symfpu_traits.h.in @@ -0,0 +1,265 @@ +/********************* */ +/*! \file floatingpoint_literal_symfpu_traits.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-2021 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 only to be included in floating-point literal headers !!! + **/ + +/** + * 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. + */ + +#include "cvc4_private.h" + +#ifndef CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H +#define CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H + +// clang-format off +#if @CVC4_USE_SYMFPU@ +// clang-format on + +#include "util/bitvector.h" +#include "util/floatingpoint_size.h" +#include "util/roundingmode.h" + +#include + +/* -------------------------------------------------------------------------- */ + +namespace cvc5 { +namespace symfpuLiteral { + +/** + * Forward declaration of wrapper so that traits can be defined early and so + * used in the implementation of wrappedBitVector. + */ +template +class wrappedBitVector; + +using Cvc5BitWidth = uint32_t; +using Cvc5Prop = bool; +using Cvc5RM = ::cvc5::RoundingMode; +using Cvc5FPSize = ::cvc5::FloatingPointSize; +using Cvc5UnsignedBitVector = wrappedBitVector; +using Cvc5SignedBitVector = wrappedBitVector; + +/** + * This is the template parameter for symfpu's templates. + */ +class traits +{ + public: + /** The six key types that symfpu uses. */ + using bwt = Cvc5BitWidth; // bit-width type + using prop = Cvc5Prop; // boolean type + using rm = Cvc5RM; // rounding-mode type + using fpt = Cvc5FPSize; // floating-point format type + using ubv = Cvc5UnsignedBitVector; // unsigned bit-vector type + using sbv = Cvc5SignedBitVector; // 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 +struct signedToLiteralType; + +template <> +struct signedToLiteralType +{ + using literalType = int32_t; +}; +template <> +struct signedToLiteralType +{ + 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 +class wrappedBitVector : public BitVector +{ + protected: + using literalType = typename signedToLiteralType::literalType; + friend wrappedBitVector; // To allow conversion between types + + friend ::symfpu::ite >; // For ITE + + public: + /** Constructors. */ + wrappedBitVector(const Cvc5BitWidth w, const uint32_t v) : BitVector(w, v) {} + wrappedBitVector(const Cvc5Prop& p) : BitVector(1, p ? 1U : 0U) {} + wrappedBitVector(const wrappedBitVector& old) : BitVector(old) {} + wrappedBitVector(const BitVector& old) : BitVector(old) {} + + /** Get the bit-width of this wrapped bit-vector. */ + Cvc5BitWidth getWidth(void) const { return getSize(); } + + /** Create a zero value of given bit-width 'w'. */ + static wrappedBitVector one(const Cvc5BitWidth& w); + /** Create a one value of given bit-width 'w'. */ + static wrappedBitVector zero(const Cvc5BitWidth& w); + /** Create a ones value (all bits 1) of given bit-width 'w'. */ + static wrappedBitVector allOnes(const Cvc5BitWidth& w); + /** Create a maximum signed/unsigned value of given bit-width 'w'. */ + static wrappedBitVector maxValue(const Cvc5BitWidth& w); + /** Create a minimum signed/unsigned value of given bit-width 'w'. */ + static wrappedBitVector minValue(const Cvc5BitWidth& w); + + /** Return true if this a bit-vector representing a ones value. */ + Cvc5Prop isAllOnes() const; + /** Return true if this a bit-vector representing a zero value. */ + Cvc5Prop isAllZeros() const; + + /** Left shift. */ + wrappedBitVector operator<<( + const wrappedBitVector& op) const; + /** Logical (unsigned) and arithmetic (signed) right shift. */ + wrappedBitVector operator>>( + const wrappedBitVector& 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 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 operator|( + const wrappedBitVector& op) const; + /** Bit-wise and. */ + wrappedBitVector operator&( + const wrappedBitVector& op) const; + /** Bit-vector addition. */ + wrappedBitVector operator+( + const wrappedBitVector& op) const; + /** Bit-vector subtraction. */ + wrappedBitVector operator-( + const wrappedBitVector& op) const; + /** Bit-vector multiplication. */ + wrappedBitVector operator*( + const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned division. */ + wrappedBitVector operator/( + const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned remainder. */ + wrappedBitVector operator%( + const wrappedBitVector& op) const; + /** Bit-vector negation. */ + wrappedBitVector operator-(void) const; + /** Bit-wise not. */ + wrappedBitVector operator~(void) const; + + /** Bit-vector increment. */ + wrappedBitVector increment() const; + /** Bit-vector decrement. */ + wrappedBitVector decrement() const; + /** + * Bit-vector logical/arithmetic right shift where 'op' extended to the + * bit-width of this wrapped bit-vector. + */ + wrappedBitVector signExtendRightShift( + const wrappedBitVector& op) const; + + /** + * Modular operations. + * Note: No overflow checking so these are the same as other operations. + */ + wrappedBitVector modularLeftShift( + const wrappedBitVector& op) const; + wrappedBitVector modularRightShift( + const wrappedBitVector& op) const; + wrappedBitVector modularIncrement() const; + wrappedBitVector modularDecrement() const; + wrappedBitVector modularAdd( + const wrappedBitVector& op) const; + wrappedBitVector modularNegate() const; + + /** Bit-vector equality. */ + Cvc5Prop operator==(const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned less or equal than. */ + Cvc5Prop operator<=(const wrappedBitVector& op) const; + /** Bit-vector sign/unsigned greater or equal than. */ + Cvc5Prop operator>=(const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned less than. */ + Cvc5Prop operator<(const wrappedBitVector& op) const; + /** Bit-vector sign/unsigned greater or equal than. */ + Cvc5Prop operator>(const wrappedBitVector& op) const; + + /** Convert this bit-vector to a signed bit-vector. */ + wrappedBitVector toSigned(void) const; + /** Convert this bit-vector to an unsigned bit-vector. */ + wrappedBitVector toUnsigned(void) const; + + /** Bit-vector signed/unsigned (zero) extension. */ + wrappedBitVector extend(Cvc5BitWidth 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 contract(Cvc5BitWidth 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 resize(Cvc5BitWidth 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 matchWidth( + const wrappedBitVector& op) const; + + /** Bit-vector concatenation. */ + wrappedBitVector append(const wrappedBitVector& op) const; + + /** Inclusive of end points, thus if the same, extracts just one bit. */ + wrappedBitVector extract(Cvc5BitWidth upper, + Cvc5BitWidth lower) const; +}; +} // namespace symfpuLiteral +} + +#endif +#endif