From: Aina Niemetz Date: Sat, 21 Nov 2020 01:30:43 +0000 (-0800) Subject: Rename symfpu_literal.(h.in|cpp) -> floatingpoint_literal_symfpu.(h.in|cpp). (#5502) X-Git-Tag: cvc5-1.0.0~2564 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2a1e97cb8bc0ce7ab102035c3e481465fc59ec12;p=cvc5.git Rename symfpu_literal.(h.in|cpp) -> floatingpoint_literal_symfpu.(h.in|cpp). (#5502) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index aea57ef00..366e72af0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1205,7 +1205,7 @@ install(FILES ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h ${CMAKE_CURRENT_BINARY_DIR}/util/real_algebraic_number.h - ${CMAKE_CURRENT_BINARY_DIR}/util/symfpu_literal.h + ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint_literal_symfpu.h DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/util) diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index b8e6f381c..85482bf6d 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -18,7 +18,7 @@ #include "theory/theory.h" // theory.h Only needed for the leaf test #include "util/floatingpoint.h" -#include "util/symfpu_literal.h" +#include "util/floatingpoint_literal_symfpu.h" #ifdef CVC4_USE_SYMFPU #include "symfpu/core/add.h" diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index a9b0b1dca..24e485f5e 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -8,7 +8,7 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## -configure_file(symfpu_literal.h.in symfpu_literal.h) +configure_file(floatingpoint_literal_symfpu.h.in floatingpoint_literal_symfpu.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) @@ -62,7 +62,7 @@ libcvc4_add_sources( statistics_registry.h string.cpp string.h - symfpu_literal.cpp + floatingpoint_literal_symfpu.cpp tuple.h unsafe_interrupt_exception.h utility.cpp diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index 4e4b076f0..c5ec4d0c6 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -23,8 +23,8 @@ #include #include "base/check.h" +#include "util/floatingpoint_literal_symfpu.h" #include "util/integer.h" -#include "util/symfpu_literal.h" #ifdef CVC4_USE_SYMFPU #include "symfpu/core/add.h" diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp new file mode 100644 index 000000000..fb5c0b7b5 --- /dev/null +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -0,0 +1,428 @@ +/********************* */ +/*! \file floatingpoint_literal_symfpu.cpp + ** \verbatim + ** Top contributors (to current version): + ** Martin Brain, Aina Niemetz + ** 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. + **/ +#include "util/floatingpoint_literal_symfpu.h" + +#include "base/check.h" + +namespace CVC4 { + +#ifndef CVC4_USE_SYMFPU +void FloatingPointLiteral::unfinished(void) const +{ + Unimplemented() << "Floating-point literals not yet implemented."; +} + +bool FloatingPointLiteral::operator==(const FloatingPointLiteral& other) const +{ + unfinished(); + return false; +} + +size_t FloatingPointLiteral::hash(void) const +{ + unfinished(); + return 23; +} +#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(this->getWidth())); +} +template +CVC4Prop wrappedBitVector::isAllZeros() const +{ + return (*this == wrappedBitVector::zero(this->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 this->BitVector::leftShift(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator>>( + const wrappedBitVector& op) const +{ + return this->BitVector::arithRightShift(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator>>( + const wrappedBitVector& op) const +{ + return this->BitVector::logicalRightShift(op); +} + +template +wrappedBitVector wrappedBitVector::operator|( + const wrappedBitVector& op) const +{ + return this->BitVector::operator|(op); +} + +template +wrappedBitVector wrappedBitVector::operator&( + const wrappedBitVector& op) const +{ + return this->BitVector::operator&(op); +} + +template +wrappedBitVector wrappedBitVector::operator+( + const wrappedBitVector& op) const +{ + return this->BitVector::operator+(op); +} + +template +wrappedBitVector wrappedBitVector::operator-( + const wrappedBitVector& op) const +{ + return this->BitVector::operator-(op); +} + +template +wrappedBitVector wrappedBitVector::operator*( + const wrappedBitVector& op) const +{ + return this->BitVector::operator*(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator/( + const wrappedBitVector& op) const +{ + return this->BitVector::unsignedDivTotal(op); +} + +template <> +wrappedBitVector wrappedBitVector::operator%( + const wrappedBitVector& op) const +{ + return this->BitVector::unsignedRemTotal(op); +} + +template +wrappedBitVector wrappedBitVector::operator-(void) const +{ + return this->BitVector::operator-(); +} + +template +wrappedBitVector wrappedBitVector::operator~(void) const +{ + return this->BitVector::operator~(); +} + +template +wrappedBitVector wrappedBitVector::increment() const +{ + return *this + wrappedBitVector::one(this->getWidth()); +} + +template +wrappedBitVector wrappedBitVector::decrement() const +{ + return *this - wrappedBitVector::one(this->getWidth()); +} + +template +wrappedBitVector wrappedBitVector::signExtendRightShift( + const wrappedBitVector& op) const +{ + return this->BitVector::arithRightShift(BitVector(this->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 this->increment(); +} + +template +wrappedBitVector wrappedBitVector::modularDecrement() const +{ + return this->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 this->BitVector::operator==(op); +} + +template <> +CVC4Prop wrappedBitVector::operator<=( + const wrappedBitVector& op) const +{ + return this->signedLessThanEq(op); +} + +template <> +CVC4Prop wrappedBitVector::operator>=( + const wrappedBitVector& op) const +{ + return !(this->signedLessThan(op)); +} + +template <> +CVC4Prop wrappedBitVector::operator<( + const wrappedBitVector& op) const +{ + return this->signedLessThan(op); +} + +template <> +CVC4Prop wrappedBitVector::operator>( + const wrappedBitVector& op) const +{ + return !(this->signedLessThanEq(op)); +} + +template <> +CVC4Prop wrappedBitVector::operator<=( + const wrappedBitVector& op) const +{ + return this->unsignedLessThanEq(op); +} + +template <> +CVC4Prop wrappedBitVector::operator>=( + const wrappedBitVector& op) const +{ + return !(this->unsignedLessThan(op)); +} + +template <> +CVC4Prop wrappedBitVector::operator<( + const wrappedBitVector& op) const +{ + return this->unsignedLessThan(op); +} + +template <> +CVC4Prop wrappedBitVector::operator>( + const wrappedBitVector& op) const +{ + return !(this->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 this->BitVector::signExtend(extension); + } + else + { + return this->BitVector::zeroExtend(extension); + } +} + +template +wrappedBitVector wrappedBitVector::contract( + CVC4BitWidth reduction) const +{ + Assert(this->getWidth() > reduction); + + return this->extract((this->getWidth() - 1) - reduction, 0); +} + +template +wrappedBitVector wrappedBitVector::resize( + CVC4BitWidth newSize) const +{ + CVC4BitWidth width = this->getWidth(); + + if (newSize > width) + { + return this->extend(newSize - width); + } + else if (newSize < width) + { + return this->contract(width - newSize); + } + else + { + return *this; + } +} + +template +wrappedBitVector wrappedBitVector::matchWidth( + const wrappedBitVector& op) const +{ + Assert(this->getWidth() <= op.getWidth()); + return this->extend(op.getWidth() - this->getWidth()); +} + +template +wrappedBitVector wrappedBitVector::append( + const wrappedBitVector& op) const +{ + return this->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 this->BitVector::extract(upper, lower); +} + +// Explicit instantiation +template class wrappedBitVector; +template class wrappedBitVector; + +traits::rm traits::RNE(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_EVEN; }; +traits::rm traits::RNA(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_AWAY; }; +traits::rm traits::RTP(void) { return ::CVC4::ROUND_TOWARD_POSITIVE; }; +traits::rm traits::RTN(void) { return ::CVC4::ROUND_TOWARD_NEGATIVE; }; +traits::rm traits::RTZ(void) { return ::CVC4::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 CVC4 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 +#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 +class wrappedBitVector; + +using CVC4BitWidth = uint32_t; +using CVC4Prop = bool; +using CVC4RM = ::CVC4::RoundingMode; +using CVC4FPSize = ::CVC4::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 CVC4::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 + * CVC4::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 +using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat; +#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 diff --git a/src/util/symfpu_literal.cpp b/src/util/symfpu_literal.cpp deleted file mode 100644 index b916d62f9..000000000 --- a/src/util/symfpu_literal.cpp +++ /dev/null @@ -1,428 +0,0 @@ -/********************* */ -/*! \file symfpu_literal.cpp - ** \verbatim - ** Top contributors (to current version): - ** Martin Brain, Aina Niemetz - ** 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. - **/ -#include "util/symfpu_literal.h" - -#include "base/check.h" - -namespace CVC4 { - -#ifndef CVC4_USE_SYMFPU -void FloatingPointLiteral::unfinished(void) const -{ - Unimplemented() << "Floating-point literals not yet implemented."; -} - -bool FloatingPointLiteral::operator==(const FloatingPointLiteral& other) const -{ - unfinished(); - return false; -} - -size_t FloatingPointLiteral::hash(void) const -{ - unfinished(); - return 23; -} -#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(this->getWidth())); -} -template -CVC4Prop wrappedBitVector::isAllZeros() const -{ - return (*this == wrappedBitVector::zero(this->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 this->BitVector::leftShift(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator>>( - const wrappedBitVector& op) const -{ - return this->BitVector::arithRightShift(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator>>( - const wrappedBitVector& op) const -{ - return this->BitVector::logicalRightShift(op); -} - -template -wrappedBitVector wrappedBitVector::operator|( - const wrappedBitVector& op) const -{ - return this->BitVector::operator|(op); -} - -template -wrappedBitVector wrappedBitVector::operator&( - const wrappedBitVector& op) const -{ - return this->BitVector::operator&(op); -} - -template -wrappedBitVector wrappedBitVector::operator+( - const wrappedBitVector& op) const -{ - return this->BitVector::operator+(op); -} - -template -wrappedBitVector wrappedBitVector::operator-( - const wrappedBitVector& op) const -{ - return this->BitVector::operator-(op); -} - -template -wrappedBitVector wrappedBitVector::operator*( - const wrappedBitVector& op) const -{ - return this->BitVector::operator*(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator/( - const wrappedBitVector& op) const -{ - return this->BitVector::unsignedDivTotal(op); -} - -template <> -wrappedBitVector wrappedBitVector::operator%( - const wrappedBitVector& op) const -{ - return this->BitVector::unsignedRemTotal(op); -} - -template -wrappedBitVector wrappedBitVector::operator-(void) const -{ - return this->BitVector::operator-(); -} - -template -wrappedBitVector wrappedBitVector::operator~(void) const -{ - return this->BitVector::operator~(); -} - -template -wrappedBitVector wrappedBitVector::increment() const -{ - return *this + wrappedBitVector::one(this->getWidth()); -} - -template -wrappedBitVector wrappedBitVector::decrement() const -{ - return *this - wrappedBitVector::one(this->getWidth()); -} - -template -wrappedBitVector wrappedBitVector::signExtendRightShift( - const wrappedBitVector& op) const -{ - return this->BitVector::arithRightShift(BitVector(this->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 this->increment(); -} - -template -wrappedBitVector wrappedBitVector::modularDecrement() const -{ - return this->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 this->BitVector::operator==(op); -} - -template <> -CVC4Prop wrappedBitVector::operator<=( - const wrappedBitVector& op) const -{ - return this->signedLessThanEq(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>=( - const wrappedBitVector& op) const -{ - return !(this->signedLessThan(op)); -} - -template <> -CVC4Prop wrappedBitVector::operator<( - const wrappedBitVector& op) const -{ - return this->signedLessThan(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>( - const wrappedBitVector& op) const -{ - return !(this->signedLessThanEq(op)); -} - -template <> -CVC4Prop wrappedBitVector::operator<=( - const wrappedBitVector& op) const -{ - return this->unsignedLessThanEq(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>=( - const wrappedBitVector& op) const -{ - return !(this->unsignedLessThan(op)); -} - -template <> -CVC4Prop wrappedBitVector::operator<( - const wrappedBitVector& op) const -{ - return this->unsignedLessThan(op); -} - -template <> -CVC4Prop wrappedBitVector::operator>( - const wrappedBitVector& op) const -{ - return !(this->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 this->BitVector::signExtend(extension); - } - else - { - return this->BitVector::zeroExtend(extension); - } -} - -template -wrappedBitVector wrappedBitVector::contract( - CVC4BitWidth reduction) const -{ - Assert(this->getWidth() > reduction); - - return this->extract((this->getWidth() - 1) - reduction, 0); -} - -template -wrappedBitVector wrappedBitVector::resize( - CVC4BitWidth newSize) const -{ - CVC4BitWidth width = this->getWidth(); - - if (newSize > width) - { - return this->extend(newSize - width); - } - else if (newSize < width) - { - return this->contract(width - newSize); - } - else - { - return *this; - } -} - -template -wrappedBitVector wrappedBitVector::matchWidth( - const wrappedBitVector& op) const -{ - Assert(this->getWidth() <= op.getWidth()); - return this->extend(op.getWidth() - this->getWidth()); -} - -template -wrappedBitVector wrappedBitVector::append( - const wrappedBitVector& op) const -{ - return this->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 this->BitVector::extract(upper, lower); -} - -// Explicit instantiation -template class wrappedBitVector; -template class wrappedBitVector; - -traits::rm traits::RNE(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_EVEN; }; -traits::rm traits::RNA(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_AWAY; }; -traits::rm traits::RTP(void) { return ::CVC4::ROUND_TOWARD_POSITIVE; }; -traits::rm traits::RTN(void) { return ::CVC4::ROUND_TOWARD_NEGATIVE; }; -traits::rm traits::RTZ(void) { return ::CVC4::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 CVC4 diff --git a/src/util/symfpu_literal.h.in b/src/util/symfpu_literal.h.in deleted file mode 100644 index e477bb0c1..000000000 --- a/src/util/symfpu_literal.h.in +++ /dev/null @@ -1,327 +0,0 @@ -/********************* */ -/*! \file symfpu_literal.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__SYMFPULITERAL__SYMFPU_LITERAL_H -#define CVC4__SYMFPULITERAL__SYMFPU_LITERAL_H - -#include "util/bitvector.h" -#include "util/roundingmode.h" - -// clang-format off -#if @CVC4_USE_SYMFPU@ -// clang-format on -#include -#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 -class wrappedBitVector; - -using CVC4BitWidth = uint32_t; -using CVC4Prop = bool; -using CVC4RM = ::CVC4::RoundingMode; -using CVC4FPSize = ::CVC4::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 CVC4::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 - * CVC4::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 -using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat; -#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