floatingpoint.h: Split in preparation to cleanly separate symFPU glue code. (#5478)

8 files changed, 858 insertions, 749 deletions

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 462c9090d..94ded3777 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -8,6 +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.h.in floatingpoint.h)
 configure_file(rational.h.in rational.h)
 configure_file(integer.h.in integer.h)
@@ -26,6 +27,8 @@ libcvc4_add_sources(
   divisible.cpp
   divisible.h
   floatingpoint.cpp
+  floatingpoint_size.cpp
+  floatingpoint_size.h
   gmp_util.h
   hash.h
   iand.h
@@ -44,6 +47,7 @@ libcvc4_add_sources(
   result.h
   regexp.cpp
   regexp.h
+  roundingmode.h
   safe_print.cpp
   safe_print.h
   sampler.cpp
@@ -58,6 +62,7 @@ libcvc4_add_sources(
   statistics_registry.h
   string.cpp
   string.h
+  symfpu_literal.cpp
   tuple.h
   unsafe_interrupt_exception.h
   utility.cpp
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index cfb0120fb..ae6197791 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -64,427 +64,8 @@ CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
 }
 #endif
 
-#ifndef CVC4_USE_SYMFPU
-#define PRECONDITION(X) Assert((X))
-#endif
-
 namespace CVC4 {
 
-FloatingPointSize::FloatingPointSize(uint32_t exp_size, uint32_t sig_size)
-    : d_exp_size(exp_size), d_sig_size(sig_size)
-{
-  PrettyCheckArgument(validExponentSize(exp_size),
-                      exp_size,
-                      "Invalid exponent size : %d",
-                      exp_size);
-  PrettyCheckArgument(validSignificandSize(sig_size),
-                      sig_size,
-                      "Invalid significand size : %d",
-                      sig_size);
-}
-
-FloatingPointSize::FloatingPointSize(const FloatingPointSize& old)
-    : d_exp_size(old.d_exp_size), d_sig_size(old.d_sig_size)
-{
-  PrettyCheckArgument(validExponentSize(d_exp_size),
-                      d_exp_size,
-                      "Invalid exponent size : %d",
-                      d_exp_size);
-  PrettyCheckArgument(validSignificandSize(d_sig_size),
-                      d_sig_size,
-                      "Invalid significand size : %d",
-                      d_sig_size);
-}
-
-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(this->getWidth()));
-}
-template <bool isSigned>
-CVC4Prop wrappedBitVector<isSigned>::isAllZeros() const
-{
-  return (*this == wrappedBitVector<isSigned>::zero(this->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 this->BitVector::leftShift(op);
-}
-
-template <>
-wrappedBitVector<true> wrappedBitVector<true>::operator>>(
-    const wrappedBitVector<true> &op) const
-{
-  return this->BitVector::arithRightShift(op);
-}
-
-template <>
-wrappedBitVector<false> wrappedBitVector<false>::operator>>(
-    const wrappedBitVector<false> &op) const
-{
-  return this->BitVector::logicalRightShift(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
-    const wrappedBitVector<isSigned> &op) const
-{
-  return this->BitVector::operator|(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
-    const wrappedBitVector<isSigned> &op) const
-{
-  return this->BitVector::operator&(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
-    const wrappedBitVector<isSigned> &op) const
-{
-  return this->BitVector::operator+(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
-    const wrappedBitVector<isSigned> &op) const
-{
-  return this->BitVector::operator-(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
-    const wrappedBitVector<isSigned> &op) const
-{
-  return this->BitVector::operator*(op);
-}
-
-template <>
-wrappedBitVector<false> wrappedBitVector<false>::operator/(
-    const wrappedBitVector<false> &op) const
-{
-  return this->BitVector::unsignedDivTotal(op);
-}
-
-template <>
-wrappedBitVector<false> wrappedBitVector<false>::operator%(
-    const wrappedBitVector<false> &op) const
-{
-  return this->BitVector::unsignedRemTotal(op);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
-{
-  return this->BitVector::operator-();
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void)const
-{
-  return this->BitVector::operator~();
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
-{
-  return *this + wrappedBitVector<isSigned>::one(this->getWidth());
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
-{
-  return *this - wrappedBitVector<isSigned>::one(this->getWidth());
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
-    const wrappedBitVector<isSigned> &op) const
-{
-  return this->BitVector::arithRightShift(BitVector(this->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 this->increment();
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
-{
-  return this->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 this->BitVector::operator==(op);
-}
-
-template <>
-CVC4Prop wrappedBitVector<true>::operator<=(
-    const wrappedBitVector<true>& op) const
-{
-  return this->signedLessThanEq(op);
-}
-
-template <>
-CVC4Prop wrappedBitVector<true>::operator>=(
-    const wrappedBitVector<true>& op) const
-{
-  return !(this->signedLessThan(op));
-}
-
-template <>
-CVC4Prop wrappedBitVector<true>::operator<(
-    const wrappedBitVector<true>& op) const
-{
-  return this->signedLessThan(op);
-}
-
-template <>
-CVC4Prop wrappedBitVector<true>::operator>(
-    const wrappedBitVector<true>& op) const
-{
-  return !(this->signedLessThanEq(op));
-}
-
-template <>
-CVC4Prop wrappedBitVector<false>::operator<=(
-    const wrappedBitVector<false>& op) const
-{
-  return this->unsignedLessThanEq(op);
-}
-
-template <>
-CVC4Prop wrappedBitVector<false>::operator>=(
-    const wrappedBitVector<false>& op) const
-{
-  return !(this->unsignedLessThan(op));
-}
-
-template <>
-CVC4Prop wrappedBitVector<false>::operator<(
-    const wrappedBitVector<false>& op) const
-{
-  return this->unsignedLessThan(op);
-}
-
-template <>
-CVC4Prop wrappedBitVector<false>::operator>(
-    const wrappedBitVector<false>& op) const
-{
-  return !(this->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 this->BitVector::signExtend(extension);
-  }
-  else
-  {
-    return this->BitVector::zeroExtend(extension);
-  }
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
-    CVC4BitWidth reduction) const
-{
-  PRECONDITION(this->getWidth() > reduction);
-
-  return this->extract((this->getWidth() - 1) - reduction, 0);
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::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 <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
-    const wrappedBitVector<isSigned> &op) const
-{
-  PRECONDITION(this->getWidth() <= op.getWidth());
-  return this->extend(op.getWidth() - this->getWidth());
-}
-
-template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
-    const wrappedBitVector<isSigned> &op) const
-{
-  return this->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
-{
-  PRECONDITION(upper >= lower);
-  return this->BitVector::extract(upper, lower);
-}
-
-// Explicit instantiation
-template class wrappedBitVector<true>;
-template class wrappedBitVector<false>;
-
-traits::rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; };
-traits::rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; };
-traits::rm traits::RTP(void) { return ::CVC4::roundTowardPositive; };
-traits::rm traits::RTN(void) { return ::CVC4::roundTowardNegative; };
-traits::rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
-// 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;
-}
-}
-
 #ifndef CVC4_USE_SYMFPU
 void FloatingPointLiteral::unfinished(void) const
 {
diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in
index 7e430ad87..bcf792c56 100644
--- a/src/util/floatingpoint.h.in
+++ b/src/util/floatingpoint.h.in
@@ -20,10 +20,11 @@
 #ifndef CVC4__FLOATINGPOINT_H
 #define CVC4__FLOATINGPOINT_H
 
-#include <fenv.h>
-
 #include "util/bitvector.h"
+#include "util/floatingpoint_size.h"
 #include "util/rational.h"
+#include "util/roundingmode.h"
+#include "util/symfpu_literal.h"
 
 // clang-format off
 #if @CVC4_USE_SYMFPU@
@@ -31,340 +32,13 @@
 #include <symfpu/core/unpackedFloat.h>
 #endif /* @CVC4_USE_SYMFPU@ */
 
-namespace CVC4 {
-// Inline these!
-inline bool CVC4_PUBLIC validExponentSize(uint32_t e) { return e >= 2; }
-inline bool CVC4_PUBLIC validSignificandSize(uint32_t s) { return s >= 2; }
-
-/* -------------------------------------------------------------------------- */
-
-/**
- * Floating point sorts are parameterised by two constants > 1 giving the
- * width (in bits) of the exponent and significand (including the hidden bit).
- * So, IEEE-754 single precision, a.k.a. float, is described as 8 24.
- */
-class CVC4_PUBLIC FloatingPointSize
-{
- public:
-  /** Constructors. */
-  FloatingPointSize(uint32_t exp_size, uint32_t sig_size);
-  FloatingPointSize(const FloatingPointSize& old);
-
-  /** Operator overload for equality comparison. */
-  bool operator==(const FloatingPointSize& fps) const
-  {
-    return (d_exp_size == fps.d_exp_size) && (d_sig_size == fps.d_sig_size);
-  }
-
-  /** Implement the interface that symfpu uses for floating-point formats. */
-
-  /** Get the exponent bit-width of this floating-point format. */
-  inline uint32_t exponentWidth(void) const { return this->d_exp_size; }
-  /** Get the significand bit-width of this floating-point format. */
-  inline uint32_t significandWidth(void) const { return this->d_sig_size; }
-  /**
-   * Get the bit-width of the packed representation of this floating-point
-   * format (= exponent + significand bit-width, convenience wrapper).
-   */
-  inline uint32_t packedWidth(void) const
-  {
-    return this->exponentWidth() + this->significandWidth();
-  }
-  /**
-   * Get the exponent bit-width of the packed representation of this
-   * floating-point format (= exponent bit-width).
-   */
-  inline uint32_t packedExponentWidth(void) const
-  {
-    return this->exponentWidth();
-  }
-  /**
-   * Get the significand bit-width of the packed representation of this
-   * floating-point format (= significand bit-width - 1).
-   */
-  inline uint32_t packedSignificandWidth(void) const
-  {
-    return this->significandWidth() - 1;
-  }
-
- private:
-  /** Exponent bit-width. */
-  uint32_t d_exp_size;
-  /** Significand bit-width. */
-  uint32_t d_sig_size;
-
-}; /* class FloatingPointSize */
-
-/**
- * Hash function for floating point formats.
- */
-struct CVC4_PUBLIC FloatingPointSizeHashFunction
-{
-  static inline size_t ROLL(size_t X, size_t N)
-  {
-    return (((X) << (N)) | ((X) >> (8 * sizeof((X)) - (N))));
-  }
-
-  inline size_t operator()(const FloatingPointSize& t) const
-  {
-    return size_t(ROLL(t.exponentWidth(), 4 * sizeof(uint32_t))
-                  | t.significandWidth());
-  }
-}; /* struct FloatingPointSizeHashFunction */
-
 /* -------------------------------------------------------------------------- */
 
-/**
- * A concrete instance of the rounding mode sort
- */
-enum CVC4_PUBLIC RoundingMode
-{
-  roundNearestTiesToEven = FE_TONEAREST,
-  roundTowardPositive = FE_UPWARD,
-  roundTowardNegative = FE_DOWNWARD,
-  roundTowardZero = FE_TOWARDZERO,
-  // Initializes this to the diagonalization of the 4 other values.
-  roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2)
-                            | ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8))
-}; /* enum RoundingMode */
-
-/**
- * Hash function for rounding mode values.
- */
-struct CVC4_PUBLIC RoundingModeHashFunction
-{
-  inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); }
-}; /* struct RoundingModeHashFunction */
+namespace CVC4 {
 
 /* -------------------------------------------------------------------------- */
 
 /**
- * This is a symfpu literal "back-end".  It allows the library to be used as
- * an arbitrary precision floating-point implementation.  This is effectively
- * the glue between symfpu's notion of "signed bit-vector" and CVC4's
- * BitVector.
- */
-namespace symfpuLiteral {
-
-/**
- * Forward declaration of wrapper so that traits can be defined early and so
- * used in the implementation of wrappedBitVector.
- */
-template <bool T>
-class wrappedBitVector;
-
-using CVC4BitWidth = uint32_t;
-using CVC4Prop = bool;
-using CVC4RM = ::CVC4::RoundingMode;
-using CVC4FPSize = ::CVC4::FloatingPointSize;
-using CVC4UnsignedBitVector = wrappedBitVector<false>;
-using CVC4SignedBitVector = wrappedBitVector<true>;
-
-/**
- * This is the template parameter for symfpu's templates.
- */
-class traits
-{
- public:
-  /** The six key types that symfpu uses. */
-  using bwt = CVC4BitWidth;           // bit-width type
-  using prop = CVC4Prop;              // boolean type
-  using rm = CVC4RM;                  // rounding-mode type
-  using fpt = CVC4FPSize;             // floating-point format type
-  using ubv = CVC4UnsignedBitVector;  // unsigned bit-vector type
-  using sbv = CVC4SignedBitVector;    // signed bit-vector type
-
-  /** Give concrete instances of each rounding mode, mainly for comparisons. */
-  static rm RNE(void);
-  static rm RNA(void);
-  static rm RTP(void);
-  static rm RTN(void);
-  static rm RTZ(void);
-
-  /** The sympfu properties. */
-  static void precondition(const prop& p);
-  static void postcondition(const prop& p);
-  static void invariant(const prop& p);
-};
-
-/**
- * Type function for mapping between types.
- */
-template <bool T>
-struct signedToLiteralType;
-
-template <>
-struct signedToLiteralType<true>
-{
-  using literalType = int32_t;
-};
-template <>
-struct signedToLiteralType<false>
-{
-  using literalType = uint32_t;
-};
-
-/**
- * This extends the interface for CVC4::BitVector for compatibility with symFPU.
- * The template parameter distinguishes signed and unsigned bit-vectors, a
- * distinction symfpu uses.
- */
-template <bool isSigned>
-class wrappedBitVector : public BitVector
-{
- protected:
-  using literalType = typename signedToLiteralType<isSigned>::literalType;
-  friend wrappedBitVector<!isSigned>;  // To allow conversion between types
-
-// clang-format off
-#if @CVC4_USE_SYMFPU@
-  // clang-format on
-  friend ::symfpu::ite<CVC4Prop, wrappedBitVector<isSigned> >;  // For ITE
-#endif /* @CVC4_USE_SYMFPU@ */
-
- public:
-  /** Constructors. */
-  wrappedBitVector(const CVC4BitWidth w, const uint32_t v) : BitVector(w, v) {}
-  wrappedBitVector(const CVC4Prop& p) : BitVector(1, p ? 1U : 0U) {}
-  wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {}
-  wrappedBitVector(const BitVector& old) : BitVector(old) {}
-
-  /** Get the bit-width of this wrapped bit-vector. */
-  CVC4BitWidth getWidth(void) const { return getSize(); }
-
-  /** Create a zero value of given bit-width 'w'. */
-  static wrappedBitVector<isSigned> one(const CVC4BitWidth& w);
-  /** Create a one value of given bit-width 'w'. */
-  static wrappedBitVector<isSigned> zero(const CVC4BitWidth& w);
-  /** Create a ones value (all bits 1) of given bit-width 'w'. */
-  static wrappedBitVector<isSigned> allOnes(const CVC4BitWidth& w);
-  /** Create a maximum signed/unsigned value of given bit-width 'w'. */
-  static wrappedBitVector<isSigned> maxValue(const CVC4BitWidth& w);
-  /** Create a minimum signed/unsigned value of given bit-width 'w'. */
-  static wrappedBitVector<isSigned> minValue(const CVC4BitWidth& w);
-
-  /** Return true if this a bit-vector representing a ones value. */
-  CVC4Prop isAllOnes() const;
-  /** Return true if this a bit-vector representing a zero value. */
-  CVC4Prop isAllZeros() const;
-
-  /** Left shift. */
-  wrappedBitVector<isSigned> operator<<(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Logical (unsigned) and arithmetic (signed) right shift. */
-  wrappedBitVector<isSigned> operator>>(
-      const wrappedBitVector<isSigned>& op) const;
-
-  /**
-   * Inherited but ...
-   * *sigh* if we use the inherited version then it will return a
-   * CVC4::BitVector which can be converted back to a
-   * wrappedBitVector<isSigned> but isn't done automatically when working
-   * out types for templates instantiation.  ITE is a particular
-   * problem as expressions and constants no longer derive the
-   * same type.  There aren't any good solutions in C++, we could
-   * use CRTP but Liana wouldn't appreciate that, so the following
-   * pointless wrapping functions are needed.
-   */
-
-  /** Bit-wise or. */
-  wrappedBitVector<isSigned> operator|(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-wise and. */
-  wrappedBitVector<isSigned> operator&(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector addition. */
-  wrappedBitVector<isSigned> operator+(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector subtraction. */
-  wrappedBitVector<isSigned> operator-(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector multiplication. */
-  wrappedBitVector<isSigned> operator*(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector signed/unsigned division. */
-  wrappedBitVector<isSigned> operator/(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector signed/unsigned remainder. */
-  wrappedBitVector<isSigned> operator%(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector negation. */
-  wrappedBitVector<isSigned> operator-(void) const;
-  /** Bit-wise not. */
-  wrappedBitVector<isSigned> operator~(void) const;
-
-  /** Bit-vector increment. */
-  wrappedBitVector<isSigned> increment() const;
-  /** Bit-vector decrement. */
-  wrappedBitVector<isSigned> decrement() const;
-  /**
-   * Bit-vector logical/arithmetic right shift where 'op' extended to the
-   * bit-width of this wrapped bit-vector.
-   */
-  wrappedBitVector<isSigned> signExtendRightShift(
-      const wrappedBitVector<isSigned>& op) const;
-
-  /**
-   * Modular operations.
-   * Note: No overflow checking so these are the same as other operations.
-   */
-  wrappedBitVector<isSigned> modularLeftShift(
-      const wrappedBitVector<isSigned>& op) const;
-  wrappedBitVector<isSigned> modularRightShift(
-      const wrappedBitVector<isSigned>& op) const;
-  wrappedBitVector<isSigned> modularIncrement() const;
-  wrappedBitVector<isSigned> modularDecrement() const;
-  wrappedBitVector<isSigned> modularAdd(
-      const wrappedBitVector<isSigned>& op) const;
-  wrappedBitVector<isSigned> modularNegate() const;
-
-  /** Bit-vector equality. */
-  CVC4Prop operator==(const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector signed/unsigned less or equal than. */
-  CVC4Prop operator<=(const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector sign/unsigned greater or equal than. */
-  CVC4Prop operator>=(const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector signed/unsigned less than. */
-  CVC4Prop operator<(const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector sign/unsigned greater or equal than. */
-  CVC4Prop operator>(const wrappedBitVector<isSigned>& op) const;
-
-  /** Convert this bit-vector to a signed bit-vector. */
-  wrappedBitVector<true> toSigned(void) const;
-  /** Convert this bit-vector to an unsigned bit-vector. */
-  wrappedBitVector<false> toUnsigned(void) const;
-
-  /** Bit-vector signed/unsigned (zero) extension. */
-  wrappedBitVector<isSigned> extend(CVC4BitWidth extension) const;
-  /**
-   * Create a "contracted" bit-vector by cutting off the 'reduction' number of
-   * most significant bits, i.e., by extracting the (bit-width - reduction)
-   * least significant bits.
-   */
-  wrappedBitVector<isSigned> contract(CVC4BitWidth reduction) const;
-  /**
-   * Create a "resized" bit-vector of given size bei either extending (if new
-   * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
-   */
-  wrappedBitVector<isSigned> resize(CVC4BitWidth newSize) const;
-  /**
-   * Create an extension of this bit-vector that matches the bit-width of the
-   * given bit-vector.
-   * Note: The size of the given bit-vector may not be larger than the size of
-   * this bit-vector.
-   */
-  wrappedBitVector<isSigned> matchWidth(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector concatenation. */
-  wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
-
-  /** Inclusive of end points, thus if the same, extracts just one bit. */
-  wrappedBitVector<isSigned> extract(CVC4BitWidth upper,
-                                     CVC4BitWidth lower) const;
-};
-}  // namespace symfpuLiteral
-
-/**
  * A concrete floating point value.
  */
 // clang-format off
diff --git a/src/util/floatingpoint_size.cpp b/src/util/floatingpoint_size.cpp
new file mode 100644
index 000000000..e068eb69a
--- /dev/null
+++ b/src/util/floatingpoint_size.cpp
@@ -0,0 +1,34 @@
+/*********************                                                        */
+/*! \file floatingpoint_size.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Martin Brain
+ ** 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 The class representing a floating-point format.
+ **/
+#include "util/floatingpoint_size.h"
+
+#include "base/check.h"
+
+namespace CVC4 {
+
+FloatingPointSize::FloatingPointSize(uint32_t exp_size, uint32_t sig_size)
+    : d_exp_size(exp_size), d_sig_size(sig_size)
+{
+  Assert(validExponentSize(exp_size));
+  Assert(validSignificandSize(sig_size));
+}
+
+FloatingPointSize::FloatingPointSize(const FloatingPointSize& old)
+    : d_exp_size(old.d_exp_size), d_sig_size(old.d_sig_size)
+{
+  Assert(validExponentSize(d_exp_size));
+  Assert(validSignificandSize(d_sig_size));
+}
+
+}  // namespace CVC4
diff --git a/src/util/floatingpoint_size.h b/src/util/floatingpoint_size.h
new file mode 100644
index 000000000..20684ca42
--- /dev/null
+++ b/src/util/floatingpoint_size.h
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \file floatingpoint_size.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Martin Brain, Tim King
+ ** 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 The class representing a floating-point format.
+ **/
+#include "cvc4_public.h"
+
+#ifndef CVC4__FLOATINGPOINT_SIZE_H
+#define CVC4__FLOATINGPOINT_SIZE_H
+
+namespace CVC4 {
+
+// Inline these!
+inline bool CVC4_PUBLIC validExponentSize(uint32_t e) { return e >= 2; }
+inline bool CVC4_PUBLIC validSignificandSize(uint32_t s) { return s >= 2; }
+
+/**
+ * Floating point sorts are parameterised by two constants > 1 giving the
+ * width (in bits) of the exponent and significand (including the hidden bit).
+ * So, IEEE-754 single precision, a.k.a. float, is described as 8 24.
+ */
+class CVC4_PUBLIC FloatingPointSize
+{
+ public:
+  /** Constructors. */
+  FloatingPointSize(uint32_t exp_size, uint32_t sig_size);
+  FloatingPointSize(const FloatingPointSize& old);
+
+  /** Operator overload for equality comparison. */
+  bool operator==(const FloatingPointSize& fps) const
+  {
+    return (d_exp_size == fps.d_exp_size) && (d_sig_size == fps.d_sig_size);
+  }
+
+  /** Implement the interface that symfpu uses for floating-point formats. */
+
+  /** Get the exponent bit-width of this floating-point format. */
+  inline uint32_t exponentWidth(void) const { return d_exp_size; }
+  /** Get the significand bit-width of this floating-point format. */
+  inline uint32_t significandWidth(void) const { return d_sig_size; }
+  /**
+   * Get the bit-width of the packed representation of this floating-point
+   * format (= exponent + significand bit-width, convenience wrapper).
+   */
+  inline uint32_t packedWidth(void) const
+  {
+    return exponentWidth() + significandWidth();
+  }
+  /**
+   * Get the exponent bit-width of the packed representation of this
+   * floating-point format (= exponent bit-width).
+   */
+  inline uint32_t packedExponentWidth(void) const { return exponentWidth(); }
+  /**
+   * Get the significand bit-width of the packed representation of this
+   * floating-point format (= significand bit-width - 1).
+   */
+  inline uint32_t packedSignificandWidth(void) const
+  {
+    return significandWidth() - 1;
+  }
+
+ private:
+  /** Exponent bit-width. */
+  uint32_t d_exp_size;
+  /** Significand bit-width. */
+  uint32_t d_sig_size;
+
+}; /* class FloatingPointSize */
+
+/**
+ * Hash function for floating point formats.
+ */
+struct CVC4_PUBLIC FloatingPointSizeHashFunction
+{
+  static inline size_t ROLL(size_t X, size_t N)
+  {
+    return (((X) << (N)) | ((X) >> (8 * sizeof((X)) - (N))));
+  }
+
+  inline size_t operator()(const FloatingPointSize& t) const
+  {
+    return size_t(ROLL(t.exponentWidth(), 4 * sizeof(uint32_t))
+                  | t.significandWidth());
+  }
+}; /* struct FloatingPointSizeHashFunction */
+}  // namespace CVC4
+
+#endif
diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h
new file mode 100644
index 000000000..181755a60
--- /dev/null
+++ b/src/util/roundingmode.h
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file roundingmode.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Martin Brain, Tim King
+ ** 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 The definition of rounding mode values.
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+#include "cvc4_public.h"
+
+#ifndef CVC4__ROUNDINGMODE_H
+#define CVC4__ROUNDINGMODE_H
+
+#include <fenv.h>
+
+namespace CVC4 {
+
+/**
+ * A concrete instance of the rounding mode sort
+ */
+enum CVC4_PUBLIC RoundingMode
+{
+  roundNearestTiesToEven = FE_TONEAREST,
+  roundTowardPositive = FE_UPWARD,
+  roundTowardNegative = FE_DOWNWARD,
+  roundTowardZero = FE_TOWARDZERO,
+  // Initializes this to the diagonalization of the 4 other values.
+  roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2)
+                            | ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8))
+}; /* enum RoundingMode */
+
+/**
+ * Hash function for rounding mode values.
+ */
+struct CVC4_PUBLIC RoundingModeHashFunction
+{
+  inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); }
+}; /* struct RoundingModeHashFunction */
+
+}  // namespace CVC4
+
+#endif
diff --git a/src/util/symfpu_literal.cpp b/src/util/symfpu_literal.cpp
new file mode 100644
index 000000000..a547daccd
--- /dev/null
+++ b/src/util/symfpu_literal.cpp
@@ -0,0 +1,409 @@
+/*********************                                                        */
+/*! \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 {
+
+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(this->getWidth()));
+}
+template <bool isSigned>
+CVC4Prop wrappedBitVector<isSigned>::isAllZeros() const
+{
+  return (*this == wrappedBitVector<isSigned>::zero(this->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 this->BitVector::leftShift(op);
+}
+
+template <>
+wrappedBitVector<true> wrappedBitVector<true>::operator>>(
+    const wrappedBitVector<true>& op) const
+{
+  return this->BitVector::arithRightShift(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator>>(
+    const wrappedBitVector<false>& op) const
+{
+  return this->BitVector::logicalRightShift(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
+    const wrappedBitVector<isSigned>& op) const
+{
+  return this->BitVector::operator|(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
+    const wrappedBitVector<isSigned>& op) const
+{
+  return this->BitVector::operator&(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
+    const wrappedBitVector<isSigned>& op) const
+{
+  return this->BitVector::operator+(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
+    const wrappedBitVector<isSigned>& op) const
+{
+  return this->BitVector::operator-(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
+    const wrappedBitVector<isSigned>& op) const
+{
+  return this->BitVector::operator*(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator/(
+    const wrappedBitVector<false>& op) const
+{
+  return this->BitVector::unsignedDivTotal(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator%(
+    const wrappedBitVector<false>& op) const
+{
+  return this->BitVector::unsignedRemTotal(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
+{
+  return this->BitVector::operator-();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void) const
+{
+  return this->BitVector::operator~();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
+{
+  return *this + wrappedBitVector<isSigned>::one(this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
+{
+  return *this - wrappedBitVector<isSigned>::one(this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
+    const wrappedBitVector<isSigned>& op) const
+{
+  return this->BitVector::arithRightShift(BitVector(this->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 this->increment();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
+{
+  return this->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 this->BitVector::operator==(op);
+}
+
+template <>
+CVC4Prop wrappedBitVector<true>::operator<=(
+    const wrappedBitVector<true>& op) const
+{
+  return this->signedLessThanEq(op);
+}
+
+template <>
+CVC4Prop wrappedBitVector<true>::operator>=(
+    const wrappedBitVector<true>& op) const
+{
+  return !(this->signedLessThan(op));
+}
+
+template <>
+CVC4Prop wrappedBitVector<true>::operator<(
+    const wrappedBitVector<true>& op) const
+{
+  return this->signedLessThan(op);
+}
+
+template <>
+CVC4Prop wrappedBitVector<true>::operator>(
+    const wrappedBitVector<true>& op) const
+{
+  return !(this->signedLessThanEq(op));
+}
+
+template <>
+CVC4Prop wrappedBitVector<false>::operator<=(
+    const wrappedBitVector<false>& op) const
+{
+  return this->unsignedLessThanEq(op);
+}
+
+template <>
+CVC4Prop wrappedBitVector<false>::operator>=(
+    const wrappedBitVector<false>& op) const
+{
+  return !(this->unsignedLessThan(op));
+}
+
+template <>
+CVC4Prop wrappedBitVector<false>::operator<(
+    const wrappedBitVector<false>& op) const
+{
+  return this->unsignedLessThan(op);
+}
+
+template <>
+CVC4Prop wrappedBitVector<false>::operator>(
+    const wrappedBitVector<false>& op) const
+{
+  return !(this->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 this->BitVector::signExtend(extension);
+  }
+  else
+  {
+    return this->BitVector::zeroExtend(extension);
+  }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
+    CVC4BitWidth reduction) const
+{
+  Assert(this->getWidth() > reduction);
+
+  return this->extract((this->getWidth() - 1) - reduction, 0);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::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 <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
+    const wrappedBitVector<isSigned>& op) const
+{
+  Assert(this->getWidth() <= op.getWidth());
+  return this->extend(op.getWidth() - this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
+    const wrappedBitVector<isSigned>& op) const
+{
+  return this->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 this->BitVector::extract(upper, lower);
+}
+
+// Explicit instantiation
+template class wrappedBitVector<true>;
+template class wrappedBitVector<false>;
+
+traits::rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; };
+traits::rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; };
+traits::rm traits::RTP(void) { return ::CVC4::roundTowardPositive; };
+traits::rm traits::RTN(void) { return ::CVC4::roundTowardNegative; };
+traits::rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
+// 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
new file mode 100644
index 000000000..e0cd95d52
--- /dev/null
+++ b/src/util/symfpu_literal.h.in
@@ -0,0 +1,259 @@
+/*********************                                                        */
+/*! \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.
+ **/
+#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 <symfpu/core/unpackedFloat.h>
+#endif /* @CVC4_USE_SYMFPU@ */
+
+namespace CVC4 {
+
+class FloatingPointSize;
+
+/**
+ * This is a symfpu literal "back-end".  It allows the library to be used as
+ * an arbitrary precision floating-point implementation.  This is effectively
+ * the glue between symfpu's notion of "signed bit-vector" and CVC4's
+ * BitVector.
+ */
+namespace symfpuLiteral {
+
+/**
+ * Forward declaration of wrapper so that traits can be defined early and so
+ * used in the implementation of wrappedBitVector.
+ */
+template <bool T>
+class wrappedBitVector;
+
+using CVC4BitWidth = uint32_t;
+using CVC4Prop = bool;
+using CVC4RM = ::CVC4::RoundingMode;
+using CVC4FPSize = ::CVC4::FloatingPointSize;
+using CVC4UnsignedBitVector = wrappedBitVector<false>;
+using CVC4SignedBitVector = wrappedBitVector<true>;
+
+/**
+ * This is the template parameter for symfpu's templates.
+ */
+class traits
+{
+ public:
+  /** The six key types that symfpu uses. */
+  using bwt = CVC4BitWidth;           // bit-width type
+  using prop = CVC4Prop;              // boolean type
+  using rm = CVC4RM;                  // rounding-mode type
+  using fpt = CVC4FPSize;             // floating-point format type
+  using ubv = CVC4UnsignedBitVector;  // unsigned bit-vector type
+  using sbv = CVC4SignedBitVector;    // signed bit-vector type
+
+  /** Give concrete instances of each rounding mode, mainly for comparisons. */
+  static rm RNE(void);
+  static rm RNA(void);
+  static rm RTP(void);
+  static rm RTN(void);
+  static rm RTZ(void);
+
+  /** The sympfu properties. */
+  static void precondition(const prop& p);
+  static void postcondition(const prop& p);
+  static void invariant(const prop& p);
+};
+
+/**
+ * Type function for mapping between types.
+ */
+template <bool T>
+struct signedToLiteralType;
+
+template <>
+struct signedToLiteralType<true>
+{
+  using literalType = int32_t;
+};
+template <>
+struct signedToLiteralType<false>
+{
+  using literalType = uint32_t;
+};
+
+/**
+ * This extends the interface for CVC4::BitVector for compatibility with symFPU.
+ * The template parameter distinguishes signed and unsigned bit-vectors, a
+ * distinction symfpu uses.
+ */
+template <bool isSigned>
+class wrappedBitVector : public BitVector
+{
+ protected:
+  using literalType = typename signedToLiteralType<isSigned>::literalType;
+  friend wrappedBitVector<!isSigned>;  // To allow conversion between types
+
+// clang-format off
+#if @CVC4_USE_SYMFPU@
+  // clang-format on
+  friend ::symfpu::ite<CVC4Prop, wrappedBitVector<isSigned> >;  // For ITE
+#endif /* @CVC4_USE_SYMFPU@ */
+
+ public:
+  /** Constructors. */
+  wrappedBitVector(const CVC4BitWidth w, const uint32_t v) : BitVector(w, v) {}
+  wrappedBitVector(const CVC4Prop& p) : BitVector(1, p ? 1U : 0U) {}
+  wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {}
+  wrappedBitVector(const BitVector& old) : BitVector(old) {}
+
+  /** Get the bit-width of this wrapped bit-vector. */
+  CVC4BitWidth getWidth(void) const { return getSize(); }
+
+  /** Create a zero value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> one(const CVC4BitWidth& w);
+  /** Create a one value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> zero(const CVC4BitWidth& w);
+  /** Create a ones value (all bits 1) of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> allOnes(const CVC4BitWidth& w);
+  /** Create a maximum signed/unsigned value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> maxValue(const CVC4BitWidth& w);
+  /** Create a minimum signed/unsigned value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> minValue(const CVC4BitWidth& w);
+
+  /** Return true if this a bit-vector representing a ones value. */
+  CVC4Prop isAllOnes() const;
+  /** Return true if this a bit-vector representing a zero value. */
+  CVC4Prop isAllZeros() const;
+
+  /** Left shift. */
+  wrappedBitVector<isSigned> operator<<(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Logical (unsigned) and arithmetic (signed) right shift. */
+  wrappedBitVector<isSigned> operator>>(
+      const wrappedBitVector<isSigned>& op) const;
+
+  /**
+   * Inherited but ...
+   * *sigh* if we use the inherited version then it will return a
+   * CVC4::BitVector which can be converted back to a
+   * wrappedBitVector<isSigned> but isn't done automatically when working
+   * out types for templates instantiation.  ITE is a particular
+   * problem as expressions and constants no longer derive the
+   * same type.  There aren't any good solutions in C++, we could
+   * use CRTP but Liana wouldn't appreciate that, so the following
+   * pointless wrapping functions are needed.
+   */
+
+  /** Bit-wise or. */
+  wrappedBitVector<isSigned> operator|(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-wise and. */
+  wrappedBitVector<isSigned> operator&(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector addition. */
+  wrappedBitVector<isSigned> operator+(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector subtraction. */
+  wrappedBitVector<isSigned> operator-(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector multiplication. */
+  wrappedBitVector<isSigned> operator*(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned division. */
+  wrappedBitVector<isSigned> operator/(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned remainder. */
+  wrappedBitVector<isSigned> operator%(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector negation. */
+  wrappedBitVector<isSigned> operator-(void) const;
+  /** Bit-wise not. */
+  wrappedBitVector<isSigned> operator~(void) const;
+
+  /** Bit-vector increment. */
+  wrappedBitVector<isSigned> increment() const;
+  /** Bit-vector decrement. */
+  wrappedBitVector<isSigned> decrement() const;
+  /**
+   * Bit-vector logical/arithmetic right shift where 'op' extended to the
+   * bit-width of this wrapped bit-vector.
+   */
+  wrappedBitVector<isSigned> signExtendRightShift(
+      const wrappedBitVector<isSigned>& op) const;
+
+  /**
+   * Modular operations.
+   * Note: No overflow checking so these are the same as other operations.
+   */
+  wrappedBitVector<isSigned> modularLeftShift(
+      const wrappedBitVector<isSigned>& op) const;
+  wrappedBitVector<isSigned> modularRightShift(
+      const wrappedBitVector<isSigned>& op) const;
+  wrappedBitVector<isSigned> modularIncrement() const;
+  wrappedBitVector<isSigned> modularDecrement() const;
+  wrappedBitVector<isSigned> modularAdd(
+      const wrappedBitVector<isSigned>& op) const;
+  wrappedBitVector<isSigned> modularNegate() const;
+
+  /** Bit-vector equality. */
+  CVC4Prop operator==(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned less or equal than. */
+  CVC4Prop operator<=(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector sign/unsigned greater or equal than. */
+  CVC4Prop operator>=(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned less than. */
+  CVC4Prop operator<(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector sign/unsigned greater or equal than. */
+  CVC4Prop operator>(const wrappedBitVector<isSigned>& op) const;
+
+  /** Convert this bit-vector to a signed bit-vector. */
+  wrappedBitVector<true> toSigned(void) const;
+  /** Convert this bit-vector to an unsigned bit-vector. */
+  wrappedBitVector<false> toUnsigned(void) const;
+
+  /** Bit-vector signed/unsigned (zero) extension. */
+  wrappedBitVector<isSigned> extend(CVC4BitWidth extension) const;
+  /**
+   * Create a "contracted" bit-vector by cutting off the 'reduction' number of
+   * most significant bits, i.e., by extracting the (bit-width - reduction)
+   * least significant bits.
+   */
+  wrappedBitVector<isSigned> contract(CVC4BitWidth reduction) const;
+  /**
+   * Create a "resized" bit-vector of given size bei either extending (if new
+   * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
+   */
+  wrappedBitVector<isSigned> resize(CVC4BitWidth newSize) const;
+  /**
+   * Create an extension of this bit-vector that matches the bit-width of the
+   * given bit-vector.
+   * Note: The size of the given bit-vector may not be larger than the size of
+   * this bit-vector.
+   */
+  wrappedBitVector<isSigned> matchWidth(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector concatenation. */
+  wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
+
+  /** Inclusive of end points, thus if the same, extracts just one bit. */
+  wrappedBitVector<isSigned> extract(CVC4BitWidth upper,
+                                     CVC4BitWidth lower) const;
+};
+}  // namespace symfpuLiteral
+}
+
+#endif