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.
** 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"
## 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)
floatingpoint.h
floatingpoint_size.cpp
floatingpoint_size.h
+ floatingpoint_literal_symfpu.cpp
+ floatingpoint_literal_symfpu_traits.cpp
gmp_util.h
hash.h
iand.h
stats_utils.h
string.cpp
string.h
- floatingpoint_literal_symfpu.cpp
tuple.h
unsafe_interrupt_exception.h
utility.cpp
#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) \
{ \
#ifdef CVC4_USE_SYMFPU
,
d_symuf(symfpu::unpack<symfpuLiteral::traits>(
- symfpuLiteral::CVC4FPSize(exp_size, sig_size), bv))
+ symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv))
#endif
{
}
#ifdef CVC4_USE_SYMFPU
,
d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>(
- symfpuLiteral::CVC4FPSize(size),
- symfpuLiteral::CVC4RM(rm),
- symfpuLiteral::CVC4SignedBitVector(bv))
+ symfpuLiteral::Cvc5FPSize(size),
+ symfpuLiteral::Cvc5RM(rm),
+ symfpuLiteral::Cvc5SignedBitVector(bv))
: symfpu::convertUBVToFloat<symfpuLiteral::traits>(
- symfpuLiteral::CVC4FPSize(size),
- symfpuLiteral::CVC4RM(rm),
- symfpuLiteral::CVC4UnsignedBitVector(bv)))
+ symfpuLiteral::Cvc5FPSize(size),
+ symfpuLiteral::Cvc5RM(rm),
+ symfpuLiteral::Cvc5UnsignedBitVector(bv)))
#endif
{
}
}
#endif
-namespace symfpuLiteral {
-
-// To simplify the property macros
-typedef traits t;
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(
- const CVC4BitWidth& w)
-{
- return wrappedBitVector<isSigned>(w, 1);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(
- const CVC4BitWidth& w)
-{
- return wrappedBitVector<isSigned>(w, 0);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(
- const CVC4BitWidth& w)
-{
- return ~wrappedBitVector<isSigned>::zero(w);
-}
-
-template <bool isSigned>
-CVC4Prop wrappedBitVector<isSigned>::isAllOnes() const
-{
- return (*this == wrappedBitVector<isSigned>::allOnes(getWidth()));
-}
-template <bool isSigned>
-CVC4Prop wrappedBitVector<isSigned>::isAllZeros() const
-{
- return (*this == wrappedBitVector<isSigned>::zero(getWidth()));
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(
- const CVC4BitWidth& w)
-{
- if (isSigned)
- {
- BitVector base(w - 1, 0U);
- return wrappedBitVector<true>((~base).zeroExtend(1));
- }
- else
- {
- return wrappedBitVector<false>::allOnes(w);
- }
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(
- const CVC4BitWidth& w)
-{
- if (isSigned)
- {
- BitVector base(w, 1U);
- BitVector shiftAmount(w, w - 1);
- BitVector result(base.leftShift(shiftAmount));
- return wrappedBitVector<true>(result);
- }
- else
- {
- return wrappedBitVector<false>::zero(w);
- }
-}
-
-/*** Operators ***/
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<(
- const wrappedBitVector<isSigned>& op) const
-{
- return BitVector::leftShift(op);
-}
-
-template <>
-wrappedBitVector<true> wrappedBitVector<true>::operator>>(
- const wrappedBitVector<true>& op) const
-{
- return BitVector::arithRightShift(op);
-}
-
-template <>
-wrappedBitVector<false> wrappedBitVector<false>::operator>>(
- const wrappedBitVector<false>& op) const
-{
- return BitVector::logicalRightShift(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
- const wrappedBitVector<isSigned>& op) const
-{
- return BitVector::operator|(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
- const wrappedBitVector<isSigned>& op) const
-{
- return BitVector::operator&(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
- const wrappedBitVector<isSigned>& op) const
-{
- return BitVector::operator+(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
- const wrappedBitVector<isSigned>& op) const
-{
- return BitVector::operator-(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
- const wrappedBitVector<isSigned>& op) const
-{
- return BitVector::operator*(op);
-}
-
-template <>
-wrappedBitVector<false> wrappedBitVector<false>::operator/(
- const wrappedBitVector<false>& op) const
-{
- return BitVector::unsignedDivTotal(op);
-}
-
-template <>
-wrappedBitVector<false> wrappedBitVector<false>::operator%(
- const wrappedBitVector<false>& op) const
-{
- return BitVector::unsignedRemTotal(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
-{
- return BitVector::operator-();
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void) const
-{
- return BitVector::operator~();
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
-{
- return *this + wrappedBitVector<isSigned>::one(getWidth());
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
-{
- return *this - wrappedBitVector<isSigned>::one(getWidth());
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
- const wrappedBitVector<isSigned>& op) const
-{
- return BitVector::arithRightShift(BitVector(getWidth(), op));
-}
-
-/*** Modular opertaions ***/
-// No overflow checking so these are the same as other operations
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift(
- const wrappedBitVector<isSigned>& op) const
-{
- return *this << op;
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift(
- const wrappedBitVector<isSigned>& op) const
-{
- return *this >> op;
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const
-{
- return increment();
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
-{
- return decrement();
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd(
- const wrappedBitVector<isSigned>& op) const
-{
- return *this + op;
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
-{
- return -(*this);
-}
-
-/*** Comparisons ***/
-
-template <bool isSigned>
-CVC4Prop wrappedBitVector<isSigned>::operator==(
- const wrappedBitVector<isSigned>& op) const
-{
- return BitVector::operator==(op);
-}
-
-template <>
-CVC4Prop wrappedBitVector<true>::operator<=(
- const wrappedBitVector<true>& op) const
-{
- return signedLessThanEq(op);
-}
-
-template <>
-CVC4Prop wrappedBitVector<true>::operator>=(
- const wrappedBitVector<true>& op) const
-{
- return !(signedLessThan(op));
-}
-
-template <>
-CVC4Prop wrappedBitVector<true>::operator<(
- const wrappedBitVector<true>& op) const
-{
- return signedLessThan(op);
-}
-
-template <>
-CVC4Prop wrappedBitVector<true>::operator>(
- const wrappedBitVector<true>& op) const
-{
- return !(signedLessThanEq(op));
-}
-
-template <>
-CVC4Prop wrappedBitVector<false>::operator<=(
- const wrappedBitVector<false>& op) const
-{
- return unsignedLessThanEq(op);
-}
-
-template <>
-CVC4Prop wrappedBitVector<false>::operator>=(
- const wrappedBitVector<false>& op) const
-{
- return !(unsignedLessThan(op));
-}
-
-template <>
-CVC4Prop wrappedBitVector<false>::operator<(
- const wrappedBitVector<false>& op) const
-{
- return unsignedLessThan(op);
-}
-
-template <>
-CVC4Prop wrappedBitVector<false>::operator>(
- const wrappedBitVector<false>& op) const
-{
- return !(unsignedLessThanEq(op));
-}
-
-/*** Type conversion ***/
-// CVC4 nodes make no distinction between signed and unsigned, thus ...
-template <bool isSigned>
-wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const
-{
- return wrappedBitVector<true>(*this);
-}
-
-template <bool isSigned>
-wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const
-{
- return wrappedBitVector<false>(*this);
-}
-
-/*** Bit hacks ***/
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
- CVC4BitWidth extension) const
-{
- if (isSigned)
- {
- return BitVector::signExtend(extension);
- }
- else
- {
- return BitVector::zeroExtend(extension);
- }
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
- CVC4BitWidth reduction) const
-{
- Assert(getWidth() > reduction);
-
- return extract((getWidth() - 1) - reduction, 0);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::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 <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
- const wrappedBitVector<isSigned>& op) const
-{
- Assert(getWidth() <= op.getWidth());
- return extend(op.getWidth() - getWidth());
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
- const wrappedBitVector<isSigned>& op) const
-{
- return BitVector::concat(op);
-}
-
-// Inclusive of end points, thus if the same, extracts just one bit
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(
- CVC4BitWidth upper, CVC4BitWidth lower) const
-{
- Assert(upper >= lower);
- return BitVector::extract(upper, lower);
-}
-
-// Explicit instantiation
-template class wrappedBitVector<true>;
-template class wrappedBitVector<false>;
-
-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
#include "util/bitvector.h"
#include "util/floatingpoint_size.h"
+#include "util/floatingpoint_literal_symfpu_traits.h"
#include "util/roundingmode.h"
-// clang-format off
-#if @CVC4_USE_SYMFPU@
-// clang-format on
-#include <symfpu/core/unpackedFloat.h>
-#endif /* @CVC4_USE_SYMFPU@ */
-
/* -------------------------------------------------------------------------- */
namespace cvc5 {
-class FloatingPointSize;
-class FloatingPointLiteral;
-
-/* -------------------------------------------------------------------------- */
-
-/**
- * This is a symfpu literal "back-end". It allows the library to be used as
- * an arbitrary precision floating-point implementation. This is effectively
- * the glue between symfpu's notion of "signed bit-vector" and CVC4's
- * BitVector.
- */
-namespace symfpuLiteral {
-
-/* -------------------------------------------------------------------------- */
-
-/**
- * Forward declaration of wrapper so that traits can be defined early and so
- * used in the implementation of wrappedBitVector.
- */
-template <bool T>
-class wrappedBitVector;
-
-using CVC4BitWidth = uint32_t;
-using CVC4Prop = bool;
-using CVC4RM = ::cvc5::RoundingMode;
-using CVC4FPSize = ::cvc5::FloatingPointSize;
-using CVC4UnsignedBitVector = wrappedBitVector<false>;
-using CVC4SignedBitVector = wrappedBitVector<true>;
-
-/**
- * This is the template parameter for symfpu's templates.
- */
-class traits
-{
- public:
- /** The six key types that symfpu uses. */
- using bwt = CVC4BitWidth; // bit-width type
- using prop = CVC4Prop; // boolean type
- using rm = CVC4RM; // rounding-mode type
- using fpt = CVC4FPSize; // floating-point format type
- using ubv = CVC4UnsignedBitVector; // unsigned bit-vector type
- using sbv = CVC4SignedBitVector; // signed bit-vector type
-
- /** Give concrete instances of each rounding mode, mainly for comparisons. */
- static rm RNE(void);
- static rm RNA(void);
- static rm RTP(void);
- static rm RTN(void);
- static rm RTZ(void);
-
- /** The sympfu properties. */
- static void precondition(const prop& p);
- static void postcondition(const prop& p);
- static void invariant(const prop& p);
-};
-
-/**
- * Type function for mapping between types.
- */
-template <bool T>
-struct signedToLiteralType;
-
-template <>
-struct signedToLiteralType<true>
-{
- using literalType = int32_t;
-};
-template <>
-struct signedToLiteralType<false>
-{
- using literalType = uint32_t;
-};
-
-/**
- * This extends the interface for cvc5::BitVector for compatibility with symFPU.
- * The template parameter distinguishes signed and unsigned bit-vectors, a
- * distinction symfpu uses.
- */
-template <bool isSigned>
-class wrappedBitVector : public BitVector
-{
- protected:
- using literalType = typename signedToLiteralType<isSigned>::literalType;
- friend wrappedBitVector<!isSigned>; // To allow conversion between types
-
-// clang-format off
-#if @CVC4_USE_SYMFPU@
- // clang-format on
- friend ::symfpu::ite<CVC4Prop, wrappedBitVector<isSigned> >; // For ITE
-#endif /* @CVC4_USE_SYMFPU@ */
-
- public:
- /** Constructors. */
- wrappedBitVector(const CVC4BitWidth w, const uint32_t v) : BitVector(w, v) {}
- wrappedBitVector(const CVC4Prop& p) : BitVector(1, p ? 1U : 0U) {}
- wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {}
- wrappedBitVector(const BitVector& old) : BitVector(old) {}
-
- /** Get the bit-width of this wrapped bit-vector. */
- CVC4BitWidth getWidth(void) const { return getSize(); }
-
- /** Create a zero value of given bit-width 'w'. */
- static wrappedBitVector<isSigned> one(const CVC4BitWidth& w);
- /** Create a one value of given bit-width 'w'. */
- static wrappedBitVector<isSigned> zero(const CVC4BitWidth& w);
- /** Create a ones value (all bits 1) of given bit-width 'w'. */
- static wrappedBitVector<isSigned> allOnes(const CVC4BitWidth& w);
- /** Create a maximum signed/unsigned value of given bit-width 'w'. */
- static wrappedBitVector<isSigned> maxValue(const CVC4BitWidth& w);
- /** Create a minimum signed/unsigned value of given bit-width 'w'. */
- static wrappedBitVector<isSigned> minValue(const CVC4BitWidth& w);
-
- /** Return true if this a bit-vector representing a ones value. */
- CVC4Prop isAllOnes() const;
- /** Return true if this a bit-vector representing a zero value. */
- CVC4Prop isAllZeros() const;
-
- /** Left shift. */
- wrappedBitVector<isSigned> operator<<(
- const wrappedBitVector<isSigned>& op) const;
- /** Logical (unsigned) and arithmetic (signed) right shift. */
- wrappedBitVector<isSigned> operator>>(
- const wrappedBitVector<isSigned>& op) const;
-
- /**
- * Inherited but ...
- * *sigh* if we use the inherited version then it will return a
- * cvc5::BitVector which can be converted back to a
- * wrappedBitVector<isSigned> but isn't done automatically when working
- * out types for templates instantiation. ITE is a particular
- * problem as expressions and constants no longer derive the
- * same type. There aren't any good solutions in C++, we could
- * use CRTP but Liana wouldn't appreciate that, so the following
- * pointless wrapping functions are needed.
- */
-
- /** Bit-wise or. */
- wrappedBitVector<isSigned> operator|(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-wise and. */
- wrappedBitVector<isSigned> operator&(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector addition. */
- wrappedBitVector<isSigned> operator+(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector subtraction. */
- wrappedBitVector<isSigned> operator-(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector multiplication. */
- wrappedBitVector<isSigned> operator*(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector signed/unsigned division. */
- wrappedBitVector<isSigned> operator/(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector signed/unsigned remainder. */
- wrappedBitVector<isSigned> operator%(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector negation. */
- wrappedBitVector<isSigned> operator-(void) const;
- /** Bit-wise not. */
- wrappedBitVector<isSigned> operator~(void) const;
-
- /** Bit-vector increment. */
- wrappedBitVector<isSigned> increment() const;
- /** Bit-vector decrement. */
- wrappedBitVector<isSigned> decrement() const;
- /**
- * Bit-vector logical/arithmetic right shift where 'op' extended to the
- * bit-width of this wrapped bit-vector.
- */
- wrappedBitVector<isSigned> signExtendRightShift(
- const wrappedBitVector<isSigned>& op) const;
-
- /**
- * Modular operations.
- * Note: No overflow checking so these are the same as other operations.
- */
- wrappedBitVector<isSigned> modularLeftShift(
- const wrappedBitVector<isSigned>& op) const;
- wrappedBitVector<isSigned> modularRightShift(
- const wrappedBitVector<isSigned>& op) const;
- wrappedBitVector<isSigned> modularIncrement() const;
- wrappedBitVector<isSigned> modularDecrement() const;
- wrappedBitVector<isSigned> modularAdd(
- const wrappedBitVector<isSigned>& op) const;
- wrappedBitVector<isSigned> modularNegate() const;
-
- /** Bit-vector equality. */
- CVC4Prop operator==(const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector signed/unsigned less or equal than. */
- CVC4Prop operator<=(const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector sign/unsigned greater or equal than. */
- CVC4Prop operator>=(const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector signed/unsigned less than. */
- CVC4Prop operator<(const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector sign/unsigned greater or equal than. */
- CVC4Prop operator>(const wrappedBitVector<isSigned>& op) const;
-
- /** Convert this bit-vector to a signed bit-vector. */
- wrappedBitVector<true> toSigned(void) const;
- /** Convert this bit-vector to an unsigned bit-vector. */
- wrappedBitVector<false> toUnsigned(void) const;
-
- /** Bit-vector signed/unsigned (zero) extension. */
- wrappedBitVector<isSigned> extend(CVC4BitWidth extension) const;
-
- /**
- * Create a "contracted" bit-vector by cutting off the 'reduction' number of
- * most significant bits, i.e., by extracting the (bit-width - reduction)
- * least significant bits.
- */
- wrappedBitVector<isSigned> contract(CVC4BitWidth reduction) const;
-
- /**
- * Create a "resized" bit-vector of given size bei either extending (if new
- * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
- */
- wrappedBitVector<isSigned> resize(CVC4BitWidth newSize) const;
-
- /**
- * Create an extension of this bit-vector that matches the bit-width of the
- * given bit-vector.
- *
- * Note: The size of the given bit-vector may not be larger than the size of
- * this bit-vector.
- */
- wrappedBitVector<isSigned> matchWidth(
- const wrappedBitVector<isSigned>& op) const;
-
- /** Bit-vector concatenation. */
- wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
-
- /** Inclusive of end points, thus if the same, extracts just one bit. */
- wrappedBitVector<isSigned> extract(CVC4BitWidth upper,
- CVC4BitWidth lower) const;
-};
-
-/* -------------------------------------------------------------------------- */
-
-} // namespace symfpuLiteral
-
-/* -------------------------------------------------------------------------- */
-
// clang-format off
#if @CVC4_USE_SYMFPU@
// clang-format on
--- /dev/null
+/********************* */
+/*! \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 <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(
+ const Cvc5BitWidth& w)
+{
+ return wrappedBitVector<isSigned>(w, 1);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(
+ const Cvc5BitWidth& w)
+{
+ return wrappedBitVector<isSigned>(w, 0);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(
+ const Cvc5BitWidth& w)
+{
+ return ~wrappedBitVector<isSigned>::zero(w);
+}
+
+template <bool isSigned>
+Cvc5Prop wrappedBitVector<isSigned>::isAllOnes() const
+{
+ return (*this == wrappedBitVector<isSigned>::allOnes(getWidth()));
+}
+template <bool isSigned>
+Cvc5Prop wrappedBitVector<isSigned>::isAllZeros() const
+{
+ return (*this == wrappedBitVector<isSigned>::zero(getWidth()));
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(
+ const Cvc5BitWidth& w)
+{
+ if (isSigned)
+ {
+ BitVector base(w - 1, 0U);
+ return wrappedBitVector<true>((~base).zeroExtend(1));
+ }
+ else
+ {
+ return wrappedBitVector<false>::allOnes(w);
+ }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(
+ const Cvc5BitWidth& w)
+{
+ if (isSigned)
+ {
+ BitVector base(w, 1U);
+ BitVector shiftAmount(w, w - 1);
+ BitVector result(base.leftShift(shiftAmount));
+ return wrappedBitVector<true>(result);
+ }
+ else
+ {
+ return wrappedBitVector<false>::zero(w);
+ }
+}
+
+/*** Operators ***/
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return BitVector::leftShift(op);
+}
+
+template <>
+wrappedBitVector<true> wrappedBitVector<true>::operator>>(
+ const wrappedBitVector<true>& op) const
+{
+ return BitVector::arithRightShift(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator>>(
+ const wrappedBitVector<false>& op) const
+{
+ return BitVector::logicalRightShift(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return BitVector::operator|(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return BitVector::operator&(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return BitVector::operator+(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return BitVector::operator-(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return BitVector::operator*(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator/(
+ const wrappedBitVector<false>& op) const
+{
+ return BitVector::unsignedDivTotal(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator%(
+ const wrappedBitVector<false>& op) const
+{
+ return BitVector::unsignedRemTotal(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
+{
+ return BitVector::operator-();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void) const
+{
+ return BitVector::operator~();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
+{
+ return *this + wrappedBitVector<isSigned>::one(getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
+{
+ return *this - wrappedBitVector<isSigned>::one(getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return BitVector::arithRightShift(BitVector(getWidth(), op));
+}
+
+/*** Modular opertaions ***/
+// No overflow checking so these are the same as other operations
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return *this << op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return *this >> op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const
+{
+ return increment();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
+{
+ return decrement();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return *this + op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
+{
+ return -(*this);
+}
+
+/*** Comparisons ***/
+
+template <bool isSigned>
+Cvc5Prop wrappedBitVector<isSigned>::operator==(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return BitVector::operator==(op);
+}
+
+template <>
+Cvc5Prop wrappedBitVector<true>::operator<=(
+ const wrappedBitVector<true>& op) const
+{
+ return signedLessThanEq(op);
+}
+
+template <>
+Cvc5Prop wrappedBitVector<true>::operator>=(
+ const wrappedBitVector<true>& op) const
+{
+ return !(signedLessThan(op));
+}
+
+template <>
+Cvc5Prop wrappedBitVector<true>::operator<(
+ const wrappedBitVector<true>& op) const
+{
+ return signedLessThan(op);
+}
+
+template <>
+Cvc5Prop wrappedBitVector<true>::operator>(
+ const wrappedBitVector<true>& op) const
+{
+ return !(signedLessThanEq(op));
+}
+
+template <>
+Cvc5Prop wrappedBitVector<false>::operator<=(
+ const wrappedBitVector<false>& op) const
+{
+ return unsignedLessThanEq(op);
+}
+
+template <>
+Cvc5Prop wrappedBitVector<false>::operator>=(
+ const wrappedBitVector<false>& op) const
+{
+ return !(unsignedLessThan(op));
+}
+
+template <>
+Cvc5Prop wrappedBitVector<false>::operator<(
+ const wrappedBitVector<false>& op) const
+{
+ return unsignedLessThan(op);
+}
+
+template <>
+Cvc5Prop wrappedBitVector<false>::operator>(
+ const wrappedBitVector<false>& op) const
+{
+ return !(unsignedLessThanEq(op));
+}
+
+/*** Type conversion ***/
+
+// Node makes no distinction between signed and unsigned, thus ...
+template <bool isSigned>
+wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const
+{
+ return wrappedBitVector<true>(*this);
+}
+
+template <bool isSigned>
+wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const
+{
+ return wrappedBitVector<false>(*this);
+}
+
+/*** Bit hacks ***/
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
+ Cvc5BitWidth extension) const
+{
+ if (isSigned)
+ {
+ return BitVector::signExtend(extension);
+ }
+ else
+ {
+ return BitVector::zeroExtend(extension);
+ }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
+ Cvc5BitWidth reduction) const
+{
+ Assert(getWidth() > reduction);
+
+ return extract((getWidth() - 1) - reduction, 0);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::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 <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
+ const wrappedBitVector<isSigned>& op) const
+{
+ Assert(getWidth() <= op.getWidth());
+ return extend(op.getWidth() - getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return BitVector::concat(op);
+}
+
+// Inclusive of end points, thus if the same, extracts just one bit
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(
+ Cvc5BitWidth upper, Cvc5BitWidth lower) const
+{
+ Assert(upper >= lower);
+ return BitVector::extract(upper, lower);
+}
+
+// Explicit instantiation
+template class wrappedBitVector<true>;
+template class wrappedBitVector<false>;
+
+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
--- /dev/null
+/********************* */
+/*! \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 <symfpu/core/unpackedFloat.h>
+
+/* -------------------------------------------------------------------------- */
+
+namespace cvc5 {
+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 Cvc5BitWidth = uint32_t;
+using Cvc5Prop = bool;
+using Cvc5RM = ::cvc5::RoundingMode;
+using Cvc5FPSize = ::cvc5::FloatingPointSize;
+using Cvc5UnsignedBitVector = wrappedBitVector<false>;
+using Cvc5SignedBitVector = wrappedBitVector<true>;
+
+/**
+ * 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 <bool T>
+struct signedToLiteralType;
+
+template <>
+struct signedToLiteralType<true>
+{
+ using literalType = int32_t;
+};
+template <>
+struct signedToLiteralType<false>
+{
+ using literalType = uint32_t;
+};
+
+/**
+ * This extends the interface for cvc5::BitVector for compatibility with symFPU.
+ * The template parameter distinguishes signed and unsigned bit-vectors, a
+ * distinction symfpu uses.
+ */
+template <bool isSigned>
+class wrappedBitVector : public BitVector
+{
+ protected:
+ using literalType = typename signedToLiteralType<isSigned>::literalType;
+ friend wrappedBitVector<!isSigned>; // To allow conversion between types
+
+ friend ::symfpu::ite<Cvc5Prop, wrappedBitVector<isSigned> >; // 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<isSigned>& 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<isSigned> one(const Cvc5BitWidth& w);
+ /** Create a one value of given bit-width 'w'. */
+ static wrappedBitVector<isSigned> zero(const Cvc5BitWidth& w);
+ /** Create a ones value (all bits 1) of given bit-width 'w'. */
+ static wrappedBitVector<isSigned> allOnes(const Cvc5BitWidth& w);
+ /** Create a maximum signed/unsigned value of given bit-width 'w'. */
+ static wrappedBitVector<isSigned> maxValue(const Cvc5BitWidth& w);
+ /** Create a minimum signed/unsigned value of given bit-width 'w'. */
+ static wrappedBitVector<isSigned> 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<isSigned> operator<<(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Logical (unsigned) and arithmetic (signed) right shift. */
+ wrappedBitVector<isSigned> operator>>(
+ const wrappedBitVector<isSigned>& op) const;
+
+ /**
+ * Inherited but ...
+ * *sigh* if we use the inherited version then it will return a
+ * cvc5::BitVector which can be converted back to a
+ * wrappedBitVector<isSigned> but isn't done automatically when working
+ * out types for templates instantiation. ITE is a particular
+ * problem as expressions and constants no longer derive the
+ * same type. There aren't any good solutions in C++, we could
+ * use CRTP but Liana wouldn't appreciate that, so the following
+ * pointless wrapping functions are needed.
+ */
+
+ /** Bit-wise or. */
+ wrappedBitVector<isSigned> operator|(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-wise and. */
+ wrappedBitVector<isSigned> operator&(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector addition. */
+ wrappedBitVector<isSigned> operator+(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector subtraction. */
+ wrappedBitVector<isSigned> operator-(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector multiplication. */
+ wrappedBitVector<isSigned> operator*(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector signed/unsigned division. */
+ wrappedBitVector<isSigned> operator/(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector signed/unsigned remainder. */
+ wrappedBitVector<isSigned> operator%(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector negation. */
+ wrappedBitVector<isSigned> operator-(void) const;
+ /** Bit-wise not. */
+ wrappedBitVector<isSigned> operator~(void) const;
+
+ /** Bit-vector increment. */
+ wrappedBitVector<isSigned> increment() const;
+ /** Bit-vector decrement. */
+ wrappedBitVector<isSigned> decrement() const;
+ /**
+ * Bit-vector logical/arithmetic right shift where 'op' extended to the
+ * bit-width of this wrapped bit-vector.
+ */
+ wrappedBitVector<isSigned> signExtendRightShift(
+ const wrappedBitVector<isSigned>& op) const;
+
+ /**
+ * Modular operations.
+ * Note: No overflow checking so these are the same as other operations.
+ */
+ wrappedBitVector<isSigned> modularLeftShift(
+ const wrappedBitVector<isSigned>& op) const;
+ wrappedBitVector<isSigned> modularRightShift(
+ const wrappedBitVector<isSigned>& op) const;
+ wrappedBitVector<isSigned> modularIncrement() const;
+ wrappedBitVector<isSigned> modularDecrement() const;
+ wrappedBitVector<isSigned> modularAdd(
+ const wrappedBitVector<isSigned>& op) const;
+ wrappedBitVector<isSigned> modularNegate() const;
+
+ /** Bit-vector equality. */
+ Cvc5Prop operator==(const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector signed/unsigned less or equal than. */
+ Cvc5Prop operator<=(const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector sign/unsigned greater or equal than. */
+ Cvc5Prop operator>=(const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector signed/unsigned less than. */
+ Cvc5Prop operator<(const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector sign/unsigned greater or equal than. */
+ Cvc5Prop 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(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<isSigned> 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<isSigned> 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<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(Cvc5BitWidth upper,
+ Cvc5BitWidth lower) const;
+};
+} // namespace symfpuLiteral
+}
+
+#endif
+#endif
projects / cvc5.git / commitdiff