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.

1 files changed, 1 insertions, 249 deletions

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