FP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206)

This pushes all symfpu specific parts from FloatingPoint into
FloatingPointLiteral. FloatingPoint is now generic. An additional
FloatingPointLiteral implementation using MPFR will be made configurable
similiarly to how we handle Integers with either GMP or CLN backend.

1 files changed, 87 insertions, 414 deletions

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index cebdbbb29..23b8253d8 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -26,49 +26,6 @@
 #include "util/floatingpoint_literal_symfpu.h"
 #include "util/integer.h"
 
-#ifdef CVC4_USE_SYMFPU
-#include "symfpu/core/add.h"
-#include "symfpu/core/classify.h"
-#include "symfpu/core/compare.h"
-#include "symfpu/core/convert.h"
-#include "symfpu/core/divide.h"
-#include "symfpu/core/fma.h"
-#include "symfpu/core/ite.h"
-#include "symfpu/core/multiply.h"
-#include "symfpu/core/packing.h"
-#include "symfpu/core/remainder.h"
-#include "symfpu/core/sign.h"
-#include "symfpu/core/sqrt.h"
-#include "symfpu/utils/numberOfRoundingModes.h"
-#include "symfpu/utils/properties.h"
-#endif
-
-/* -------------------------------------------------------------------------- */
-
-#ifdef CVC4_USE_SYMFPU
-namespace symfpu {
-
-#define CVC4_LIT_ITE_DFN(T)                                            \
-  template <>                                                          \
-  struct ite<::CVC4::symfpuLiteral::CVC4Prop, T>                       \
-  {                                                                    \
-    static const T& iteOp(const ::CVC4::symfpuLiteral::CVC4Prop& cond, \
-                          const T& l,                                  \
-                          const T& r)                                  \
-    {                                                                  \
-      return cond ? l : r;                                             \
-    }                                                                  \
-  }
-
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm);
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop);
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv);
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
-
-#undef CVC4_LIT_ITE_DFN
-}
-#endif
-
 /* -------------------------------------------------------------------------- */
 
 namespace CVC4 {
@@ -77,46 +34,23 @@ namespace CVC4 {
 
 uint32_t FloatingPoint::getUnpackedExponentWidth(FloatingPointSize& size)
 {
-#ifdef CVC4_USE_SYMFPU
-  return SymFPUUnpackedFloatLiteral::exponentWidth(size);
-#else
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return 2;
-#endif
+  return FloatingPointLiteral::getUnpackedExponentWidth(size);
 }
 
 uint32_t FloatingPoint::getUnpackedSignificandWidth(FloatingPointSize& size)
 {
-#ifdef CVC4_USE_SYMFPU
-  return SymFPUUnpackedFloatLiteral::significandWidth(size);
-#else
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return 2;
-#endif
+  return FloatingPointLiteral::getUnpackedSignificandWidth(size);
 }
 
 FloatingPoint::FloatingPoint(uint32_t d_exp_size,
                              uint32_t d_sig_size,
                              const BitVector& bv)
-    : d_fp_size(d_exp_size, d_sig_size),
-#ifdef CVC4_USE_SYMFPU
-      d_fpl(new FloatingPointLiteral(symfpu::unpack<symfpuLiteral::traits>(
-          symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv)))
-#else
-      d_fpl(new FloatingPointLiteral(d_exp_size, d_sig_size, 0.0))
-#endif
+    : d_fpl(new FloatingPointLiteral(d_exp_size, d_sig_size, bv))
 {
 }
 
 FloatingPoint::FloatingPoint(const FloatingPointSize& size, const BitVector& bv)
-    : d_fp_size(size),
-#ifdef CVC4_USE_SYMFPU
-      d_fpl(new FloatingPointLiteral(
-          symfpu::unpack<symfpuLiteral::traits>(size, bv)))
-#else
-      d_fpl(new FloatingPointLiteral(
-          size.exponentWidth(), size.significandWidth(), 0.0))
-#endif
+    : d_fpl(new FloatingPointLiteral(size, bv))
 {
 }
 
@@ -124,38 +58,13 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size,
                              const RoundingMode& rm,
                              const BitVector& bv,
                              bool signedBV)
-    : d_fp_size(size)
+    : d_fpl(new FloatingPointLiteral(size, rm, bv, signedBV))
 {
-#ifdef CVC4_USE_SYMFPU
-  if (signedBV)
-  {
-    d_fpl.reset(new FloatingPointLiteral(
-        symfpu::convertSBVToFloat<symfpuLiteral::traits>(
-            symfpuLiteral::CVC4FPSize(size),
-            symfpuLiteral::CVC4RM(rm),
-            symfpuLiteral::CVC4SignedBitVector(bv))));
-  }
-  else
-  {
-    d_fpl.reset(new FloatingPointLiteral(
-        symfpu::convertUBVToFloat<symfpuLiteral::traits>(
-            symfpuLiteral::CVC4FPSize(size),
-            symfpuLiteral::CVC4RM(rm),
-            symfpuLiteral::CVC4UnsignedBitVector(bv))));
-  }
-#else
-  d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0));
-#endif
 }
 
-FloatingPoint::FloatingPoint(const FloatingPointSize& fp_size,
-                             FloatingPointLiteral* fpl)
-    : d_fp_size(fp_size)
-{
-  d_fpl.reset(fpl);
-}
+FloatingPoint::FloatingPoint(FloatingPointLiteral* fpl) { d_fpl.reset(fpl); }
 
-FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size)
+FloatingPoint::FloatingPoint(const FloatingPoint& fp)
 {
   d_fpl.reset(new FloatingPointLiteral(*fp.d_fpl));
 }
@@ -163,25 +72,18 @@ FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size)
 FloatingPoint::FloatingPoint(const FloatingPointSize& size,
                              const RoundingMode& rm,
                              const Rational& r)
-    : d_fp_size(size)
 {
   Rational two(2, 1);
 
   if (r.isZero())
   {
-#ifdef CVC4_USE_SYMFPU
     // In keeping with the SMT-LIB standard
-    d_fpl.reset(new FloatingPointLiteral(
-        SymFPUUnpackedFloatLiteral::makeZero(size, false)));
-#else
-    d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0));
-#endif
+    d_fpl.reset(
+        new FloatingPointLiteral(FloatingPointLiteral::makeZero(size, false)));
   }
   else
   {
-#ifdef CVC4_USE_SYMFPU
     uint32_t negative = (r.sgn() < 0) ? 1 : 0;
-#endif
     Rational rabs(r.abs());
 
     // Compute the exponent
@@ -277,19 +179,14 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size,
     // A small subtlety... if the format has expBits the unpacked format
     // may have more to allow subnormals to be normalised.
     // Thus...
-#ifdef CVC4_USE_SYMFPU
     uint32_t extension =
-        SymFPUUnpackedFloatLiteral::exponentWidth(exactFormat) - expBits;
+        FloatingPointLiteral::getUnpackedExponentWidth(exactFormat) - expBits;
 
     FloatingPointLiteral exactFloat(
-        negative, exactExp.signExtend(extension), sig);
+        exactFormat, negative, exactExp.signExtend(extension), sig);
 
     // Then cast...
-    d_fpl.reset(new FloatingPointLiteral(symfpu::convertFloatToFloat(
-        exactFormat, size, rm, exactFloat.d_symuf)));
-#else
-    Unreachable() << "no concrete implementation of FloatingPointLiteral";
-#endif
+    d_fpl.reset(new FloatingPointLiteral(exactFloat.convert(size, rm)));
   }
 }
 
@@ -297,37 +194,27 @@ FloatingPoint::~FloatingPoint()
 {
 }
 
+const FloatingPointSize& FloatingPoint::getSize() const
+{
+  return d_fpl->getSize();
+}
+
 FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size)
 {
-#ifdef CVC4_USE_SYMFPU
   return FloatingPoint(
-      size,
-      new FloatingPointLiteral(SymFPUUnpackedFloatLiteral::makeNaN(size)));
-#else
-  return FloatingPoint(2, 2, BitVector(4U, 0U));
-#endif
+      new FloatingPointLiteral(FloatingPointLiteral::makeNaN(size)));
 }
 
 FloatingPoint FloatingPoint::makeInf(const FloatingPointSize& size, bool sign)
 {
-#ifdef CVC4_USE_SYMFPU
-  return FloatingPoint(size,
-                       new FloatingPointLiteral(
-                           SymFPUUnpackedFloatLiteral::makeInf(size, sign)));
-#else
-  return FloatingPoint(2, 2, BitVector(4U, 0U));
-#endif
+  return FloatingPoint(
+      new FloatingPointLiteral(FloatingPointLiteral::makeInf(size, sign)));
 }
 
 FloatingPoint FloatingPoint::makeZero(const FloatingPointSize& size, bool sign)
 {
-#ifdef CVC4_USE_SYMFPU
-  return FloatingPoint(size,
-                       new FloatingPointLiteral(
-                           SymFPUUnpackedFloatLiteral::makeZero(size, sign)));
-#else
-  return FloatingPoint(2, 2, BitVector(4U, 0U));
-#endif
+  return FloatingPoint(
+      new FloatingPointLiteral(FloatingPointLiteral::makeZero(size, sign)));
 }
 
 FloatingPoint FloatingPoint::makeMinSubnormal(const FloatingPointSize& size,
@@ -367,170 +254,75 @@ FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size,
   return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
 }
 
-/* Operations implemented using symfpu */
 FloatingPoint FloatingPoint::absolute(void) const
 {
-#ifdef CVC4_USE_SYMFPU
-  return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(
-          symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf)));
-#else
-  return *this;
-#endif
+  return FloatingPoint(new FloatingPointLiteral(d_fpl->absolute()));
 }
 
 FloatingPoint FloatingPoint::negate(void) const
 {
-#ifdef CVC4_USE_SYMFPU
-  return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(
-          symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf)));
-#else
-  return *this;
-#endif
+  return FloatingPoint(new FloatingPointLiteral(d_fpl->negate()));
 }
 
 FloatingPoint FloatingPoint::plus(const RoundingMode& rm,
                                   const FloatingPoint& arg) const
 {
-#ifdef CVC4_USE_SYMFPU
-  Assert(d_fp_size == arg.d_fp_size);
-  return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(symfpu::add<symfpuLiteral::traits>(
-          d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, true)));
-#else
-  return *this;
-#endif
+  return FloatingPoint(new FloatingPointLiteral(d_fpl->add(rm, *arg.d_fpl)));
 }
 
 FloatingPoint FloatingPoint::sub(const RoundingMode& rm,
                                  const FloatingPoint& arg) const
 {
-#ifdef CVC4_USE_SYMFPU
-  Assert(d_fp_size == arg.d_fp_size);
-  return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(symfpu::add<symfpuLiteral::traits>(
-          d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, false)));
-#else
-  return *this;
-#endif
+  return FloatingPoint(new FloatingPointLiteral(d_fpl->sub(rm, *arg.d_fpl)));
 }
 
 FloatingPoint FloatingPoint::mult(const RoundingMode& rm,
                                   const FloatingPoint& arg) const
 {
-#ifdef CVC4_USE_SYMFPU
-  Assert(d_fp_size == arg.d_fp_size);
-  return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(symfpu::multiply<symfpuLiteral::traits>(
-          d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf)));
-#else
-  return *this;
-#endif
+  return FloatingPoint(new FloatingPointLiteral(d_fpl->mult(rm, *arg.d_fpl)));
 }
 
 FloatingPoint FloatingPoint::fma(const RoundingMode& rm,
                                  const FloatingPoint& arg1,
                                  const FloatingPoint& arg2) const
 {
-#ifdef CVC4_USE_SYMFPU
-  Assert(d_fp_size == arg1.d_fp_size);
-  Assert(d_fp_size == arg2.d_fp_size);
   return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(
-          symfpu::fma<symfpuLiteral::traits>(d_fp_size,
-                                             rm,
-                                             d_fpl->d_symuf,
-                                             arg1.d_fpl->d_symuf,
-                                             arg2.d_fpl->d_symuf)));
-#else
-  return *this;
-#endif
+      new FloatingPointLiteral(d_fpl->fma(rm, *arg1.d_fpl, *arg2.d_fpl)));
 }
 
 FloatingPoint FloatingPoint::div(const RoundingMode& rm,
                                  const FloatingPoint& arg) const
 {
-#ifdef CVC4_USE_SYMFPU
-  Assert(d_fp_size == arg.d_fp_size);
-  return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(symfpu::divide<symfpuLiteral::traits>(
-          d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf)));
-#else
-  return *this;
-#endif
+  return FloatingPoint(new FloatingPointLiteral(d_fpl->div(rm, *arg.d_fpl)));
 }
 
 FloatingPoint FloatingPoint::sqrt(const RoundingMode& rm) const
 {
-#ifdef CVC4_USE_SYMFPU
-  return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(
-          symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_fpl->d_symuf)));
-#else
-  return *this;
-#endif
+  return FloatingPoint(new FloatingPointLiteral(d_fpl->sqrt(rm)));
 }
 
 FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const
 {
-#ifdef CVC4_USE_SYMFPU
-  return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(symfpu::roundToIntegral<symfpuLiteral::traits>(
-          d_fp_size, rm, d_fpl->d_symuf)));
-#else
-  return *this;
-#endif
+  return FloatingPoint(new FloatingPointLiteral(d_fpl->rti(rm)));
 }
 
 FloatingPoint FloatingPoint::rem(const FloatingPoint& arg) const
 {
-#ifdef CVC4_USE_SYMFPU
-  Assert(d_fp_size == arg.d_fp_size);
-  return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(symfpu::remainder<symfpuLiteral::traits>(
-          d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf)));
-#else
-  return *this;
-#endif
+  return FloatingPoint(new FloatingPointLiteral(d_fpl->rem(*arg.d_fpl)));
 }
 
 FloatingPoint FloatingPoint::maxTotal(const FloatingPoint& arg,
                                       bool zeroCaseLeft) const
 {
-#ifdef CVC4_USE_SYMFPU
-  Assert(d_fp_size == arg.d_fp_size);
   return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(symfpu::max<symfpuLiteral::traits>(
-          d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft)));
-#else
-  return *this;
-#endif
+      new FloatingPointLiteral(d_fpl->maxTotal(*arg.d_fpl, zeroCaseLeft)));
 }
 
 FloatingPoint FloatingPoint::minTotal(const FloatingPoint& arg,
                                       bool zeroCaseLeft) const
 {
-#ifdef CVC4_USE_SYMFPU
-  Assert(d_fp_size == arg.d_fp_size);
   return FloatingPoint(
-      d_fp_size,
-      new FloatingPointLiteral(symfpu::min<symfpuLiteral::traits>(
-          d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft)));
-#else
-  return *this;
-#endif
+      new FloatingPointLiteral(d_fpl->minTotal(*arg.d_fpl, zeroCaseLeft)));
 }
 
 FloatingPoint::PartialFloatingPoint FloatingPoint::max(
@@ -549,141 +341,46 @@ FloatingPoint::PartialFloatingPoint FloatingPoint::min(
 
 bool FloatingPoint::operator==(const FloatingPoint& fp) const
 {
-#ifdef CVC4_USE_SYMFPU
-  return ((d_fp_size == fp.d_fp_size)
-          && symfpu::smtlibEqual<symfpuLiteral::traits>(
-              d_fp_size, d_fpl->d_symuf, fp.d_fpl->d_symuf));
-#else
-  return ((d_fp_size == fp.d_fp_size));
-#endif
+  return *d_fpl == *fp.d_fpl;
 }
 
-bool FloatingPoint::operator<=(const FloatingPoint& arg) const
+bool FloatingPoint::operator<=(const FloatingPoint& fp) const
 {
-#ifdef CVC4_USE_SYMFPU
-  Assert(d_fp_size == arg.d_fp_size);
-  return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
-      d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf);
-#else
-  return false;
-#endif
+  return *d_fpl <= *fp.d_fpl;
 }
 
-bool FloatingPoint::operator<(const FloatingPoint& arg) const
+bool FloatingPoint::operator<(const FloatingPoint& fp) const
 {
-#ifdef CVC4_USE_SYMFPU
-  Assert(d_fp_size == arg.d_fp_size);
-  return symfpu::lessThan<symfpuLiteral::traits>(
-      d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf);
-#else
-  return false;
-#endif
+  return *d_fpl < *fp.d_fpl;
 }
 
-BitVector FloatingPoint::getExponent() const
-{
-#ifdef CVC4_USE_SYMFPU
-  return d_fpl->d_symuf.exponent;
-#else
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return BitVector();
-#endif
-}
+BitVector FloatingPoint::getExponent() const { return d_fpl->getExponent(); }
 
 BitVector FloatingPoint::getSignificand() const
 {
-#ifdef CVC4_USE_SYMFPU
-  return d_fpl->d_symuf.significand;
-#else
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return BitVector();
-#endif
+  return d_fpl->getSignificand();
 }
 
-bool FloatingPoint::getSign() const
-{
-#ifdef CVC4_USE_SYMFPU
-  return d_fpl->d_symuf.sign;
-#else
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return false;
-#endif
-}
+bool FloatingPoint::getSign() const { return d_fpl->getSign(); }
 
-bool FloatingPoint::isNormal(void) const
-{
-#ifdef CVC4_USE_SYMFPU
-  return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
-  return false;
-#endif
-}
+bool FloatingPoint::isNormal(void) const { return d_fpl->isNormal(); }
 
-bool FloatingPoint::isSubnormal(void) const
-{
-#ifdef CVC4_USE_SYMFPU
-  return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
-  return false;
-#endif
-}
+bool FloatingPoint::isSubnormal(void) const { return d_fpl->isSubnormal(); }
 
-bool FloatingPoint::isZero(void) const
-{
-#ifdef CVC4_USE_SYMFPU
-  return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
-  return false;
-#endif
-}
+bool FloatingPoint::isZero(void) const { return d_fpl->isZero(); }
 
-bool FloatingPoint::isInfinite(void) const
-{
-#ifdef CVC4_USE_SYMFPU
-  return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
-  return false;
-#endif
-}
+bool FloatingPoint::isInfinite(void) const { return d_fpl->isInfinite(); }
 
-bool FloatingPoint::isNaN(void) const
-{
-#ifdef CVC4_USE_SYMFPU
-  return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
-  return false;
-#endif
-}
+bool FloatingPoint::isNaN(void) const { return d_fpl->isNaN(); }
 
-bool FloatingPoint::isNegative(void) const
-{
-#ifdef CVC4_USE_SYMFPU
-  return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
-  return false;
-#endif
-}
+bool FloatingPoint::isNegative(void) const { return d_fpl->isNegative(); }
 
-bool FloatingPoint::isPositive(void) const
-{
-#ifdef CVC4_USE_SYMFPU
-  return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf);
-#else
-  return false;
-#endif
-}
+bool FloatingPoint::isPositive(void) const { return d_fpl->isPositive(); }
 
 FloatingPoint FloatingPoint::convert(const FloatingPointSize& target,
                                      const RoundingMode& rm) const
 {
-#ifdef CVC4_USE_SYMFPU
-  return FloatingPoint(target,
-                       new FloatingPointLiteral(
-                           symfpu::convertFloatToFloat<symfpuLiteral::traits>(
-                               d_fp_size, target, rm, d_fpl->d_symuf)));
-#else
-  return *this;
-#endif
+  return FloatingPoint(new FloatingPointLiteral(d_fpl->convert(target, rm)));
 }
 
 BitVector FloatingPoint::convertToBVTotal(BitVectorSize width,
@@ -691,16 +388,11 @@ BitVector FloatingPoint::convertToBVTotal(BitVectorSize width,
                                           bool signedBV,
                                           BitVector undefinedCase) const
 {
-#ifdef CVC4_USE_SYMFPU
-    if (signedBV)
-      return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
-          d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase);
-    else
-      return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
-          d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase);
-#else
-  return undefinedCase;
-#endif
+  if (signedBV)
+  {
+    return d_fpl->convertToSBVTotal(width, rm, undefinedCase);
+  }
+  return d_fpl->convertToUBVTotal(width, rm, undefinedCase);
 }
 
 Rational FloatingPoint::convertToRationalTotal(Rational undefinedCase) const
@@ -730,59 +422,40 @@ FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const
   {
     return PartialRational(Rational(0U, 1U), true);
   }
-  else
-  {
-#ifdef CVC4_USE_SYMFPU
-    Integer sign((d_fpl->d_symuf.getSign()) ? -1 : 1);
-    Integer exp(
-        d_fpl->d_symuf.getExponent().toSignedInteger()
-        - (Integer(d_fp_size.significandWidth()
-                   - 1)));  // -1 as forcibly normalised into the [1,2) range
-    Integer significand(d_fpl->d_symuf.getSignificand().toInteger());
-#else
-      Integer sign(0);
-      Integer exp(0);
-      Integer significand(0);
-#endif
-      Integer signedSignificand(sign * significand);
-
-      // We only have multiplyByPow(uint32_t) so we can't convert all numbers.
-      // As we convert Integer -> unsigned int -> uint32_t we need that
-      // unsigned int is not smaller than uint32_t
-      static_assert(sizeof(unsigned int) >= sizeof(uint32_t),
-		    "Conversion float -> real could loose data");
+  Integer sign((d_fpl->getSign()) ? -1 : 1);
+  Integer exp(
+      d_fpl->getExponent().toSignedInteger()
+      - (Integer(d_fpl->getSize().significandWidth()
+                 - 1)));  // -1 as forcibly normalised into the [1,2) range
+  Integer significand(d_fpl->getSignificand().toInteger());
+  Integer signedSignificand(sign * significand);
+
+  // We only have multiplyByPow(uint32_t) so we can't convert all numbers.
+  // As we convert Integer -> unsigned int -> uint32_t we need that
+  // unsigned int is not smaller than uint32_t
+  static_assert(sizeof(unsigned int) >= sizeof(uint32_t),
+                "Conversion float -> real could loose data");
 #ifdef CVC4_ASSERTIONS
-      // Note that multipling by 2^n requires n bits of space (worst case)
-      // so, in effect, these tests limit us to cases where the resultant
-      // number requires up to 2^32 bits = 512 megabyte to represent.
-      Integer shiftLimit(std::numeric_limits<uint32_t>::max());
+  // Note that multipling by 2^n requires n bits of space (worst case)
+  // so, in effect, these tests limit us to cases where the resultant
+  // number requires up to 2^32 bits = 512 megabyte to represent.
+  Integer shiftLimit(std::numeric_limits<uint32_t>::max());
 #endif
 
-      if (!(exp.strictlyNegative())) {
-	Assert(exp <= shiftLimit);
-	Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt()));
-	return PartialRational(Rational(r), true);
-      } else {
-	Integer one(1U);
-	Assert((-exp) <= shiftLimit);
-	Integer q(one.multiplyByPow2((-exp).toUnsignedInt()));
-	Rational r(signedSignificand, q);
-	return PartialRational(r, true);
-      }
+  if (!(exp.strictlyNegative()))
+  {
+    Assert(exp <= shiftLimit);
+    Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt()));
+    return PartialRational(Rational(r), true);
   }
-
-    Unreachable() << "Convert float literal to real broken.";
+  Integer one(1U);
+  Assert((-exp) <= shiftLimit);
+  Integer q(one.multiplyByPow2((-exp).toUnsignedInt()));
+  Rational r(signedSignificand, q);
+  return PartialRational(r, true);
 }
 
-BitVector FloatingPoint::pack(void) const
-{
-#ifdef CVC4_USE_SYMFPU
-  BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf));
-#else
-  BitVector bv(4u, 0u);
-#endif
-  return bv;
-}
+BitVector FloatingPoint::pack(void) const { return d_fpl->pack(); }
 
 std::string FloatingPoint::toString(bool printAsIndexed) const
 {
@@ -790,9 +463,9 @@ std::string FloatingPoint::toString(bool printAsIndexed) const
   // retrive BV value
   BitVector bv(pack());
   uint32_t largestSignificandBit =
-      d_fp_size.significandWidth() - 2;  // -1 for -inclusive, -1 for hidden
+      getSize().significandWidth() - 2;  // -1 for -inclusive, -1 for hidden
   uint32_t largestExponentBit =
-      (d_fp_size.exponentWidth() - 1) + (largestSignificandBit + 1);
+      (getSize().exponentWidth() - 1) + (largestSignificandBit + 1);
   BitVector v[3];
   v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1);
   v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1);
@@ -836,7 +509,7 @@ std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps)
 
 std::ostream& operator<<(std::ostream& os, const FloatingPointConvertSort& fpcs)
 {
-  return os << "(_ to_fp " << fpcs.d_fp_size.exponentWidth() << " "
-            << fpcs.d_fp_size.significandWidth() << ")";
+  return os << "(_ to_fp " << fpcs.getSize().exponentWidth() << " "
+            << fpcs.getSize().significandWidth() << ")";
 }
 }/* CVC4 namespace */