From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 25 Mar 2021 19:18:51 +0000 (-0700)
Subject: FP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206)
X-Git-Tag: cvc5-1.0.0~2028
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=99a74de90a064133a8e3d03ee9334d59be34ba1d;p=cvc5.git

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.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index dce190460..f33095a4b 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1920,42 +1920,42 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const
   {
     CVC4::FloatingPointToFPIEEEBitVector ext =
         d_node->getConst<FloatingPointToFPIEEEBitVector>();
-    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
-                             ext.d_fp_size.significandWidth());
+    indices = std::make_pair(ext.getSize().exponentWidth(),
+                             ext.getSize().significandWidth());
   }
   else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
   {
     CVC4::FloatingPointToFPFloatingPoint ext =
         d_node->getConst<FloatingPointToFPFloatingPoint>();
-    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
-                             ext.d_fp_size.significandWidth());
+    indices = std::make_pair(ext.getSize().exponentWidth(),
+                             ext.getSize().significandWidth());
   }
   else if (k == FLOATINGPOINT_TO_FP_REAL)
   {
     CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>();
-    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
-                             ext.d_fp_size.significandWidth());
+    indices = std::make_pair(ext.getSize().exponentWidth(),
+                             ext.getSize().significandWidth());
   }
   else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
   {
     CVC4::FloatingPointToFPSignedBitVector ext =
         d_node->getConst<FloatingPointToFPSignedBitVector>();
-    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
-                             ext.d_fp_size.significandWidth());
+    indices = std::make_pair(ext.getSize().exponentWidth(),
+                             ext.getSize().significandWidth());
   }
   else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR)
   {
     CVC4::FloatingPointToFPUnsignedBitVector ext =
         d_node->getConst<FloatingPointToFPUnsignedBitVector>();
-    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
-                             ext.d_fp_size.significandWidth());
+    indices = std::make_pair(ext.getSize().exponentWidth(),
+                             ext.getSize().significandWidth());
   }
   else if (k == FLOATINGPOINT_TO_FP_GENERIC)
   {
     CVC4::FloatingPointToFPGeneric ext =
         d_node->getConst<FloatingPointToFPGeneric>();
-    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
-                             ext.d_fp_size.significandWidth());
+    indices = std::make_pair(ext.getSize().exponentWidth(),
+                             ext.getSize().significandWidth());
   }
   else if (k == REGEXP_LOOP)
   {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e1a4058e8..3e99267cc 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -344,51 +344,59 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
       out << "(_ to_fp "
           << n.getConst<FloatingPointToFPIEEEBitVector>()
-                 .d_fp_size.exponentWidth()
+                 .getSize()
+                 .exponentWidth()
           << ' '
           << n.getConst<FloatingPointToFPIEEEBitVector>()
-                 .d_fp_size.significandWidth()
+                 .getSize()
+                 .significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
       out << "(_ to_fp "
           << n.getConst<FloatingPointToFPFloatingPoint>()
-                 .d_fp_size.exponentWidth()
+                 .getSize()
+                 .exponentWidth()
           << ' '
           << n.getConst<FloatingPointToFPFloatingPoint>()
-                 .d_fp_size.significandWidth()
+                 .getSize()
+                 .significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_REAL_OP:
       out << "(_ to_fp "
-          << n.getConst<FloatingPointToFPReal>().d_fp_size.exponentWidth()
+          << n.getConst<FloatingPointToFPReal>().getSize().exponentWidth()
           << ' '
-          << n.getConst<FloatingPointToFPReal>().d_fp_size.significandWidth()
+          << n.getConst<FloatingPointToFPReal>().getSize().significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
       out << "(_ to_fp "
           << n.getConst<FloatingPointToFPSignedBitVector>()
-                 .d_fp_size.exponentWidth()
+                 .getSize()
+                 .exponentWidth()
           << ' '
           << n.getConst<FloatingPointToFPSignedBitVector>()
-                 .d_fp_size.significandWidth()
+                 .getSize()
+                 .significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
       out << "(_ to_fp_unsigned "
           << n.getConst<FloatingPointToFPUnsignedBitVector>()
-                 .d_fp_size.exponentWidth()
+                 .getSize()
+                 .exponentWidth()
           << ' '
           << n.getConst<FloatingPointToFPUnsignedBitVector>()
-                 .d_fp_size.significandWidth()
+                 .getSize()
+                 .significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
       out << "(_ to_fp "
-          << n.getConst<FloatingPointToFPGeneric>().d_fp_size.exponentWidth()
+          << n.getConst<FloatingPointToFPGeneric>().getSize().exponentWidth()
           << ' '
-          << n.getConst<FloatingPointToFPGeneric>().d_fp_size.significandWidth()
+          << n.getConst<FloatingPointToFPGeneric>().getSize().significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_UBV_OP:
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index d4d47731d..3e03bbdbe 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -370,7 +370,7 @@ namespace constantFold {
     FloatingPoint arg1(node[1].getConst<FloatingPoint>());
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.plus(rm, arg2)));
   }
@@ -383,7 +383,7 @@ namespace constantFold {
     FloatingPoint arg1(node[1].getConst<FloatingPoint>());
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.mult(rm, arg2)));
   }
@@ -397,8 +397,8 @@ namespace constantFold {
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
     FloatingPoint arg3(node[3].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
-    Assert(arg1.d_fp_size == arg3.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
+    Assert(arg1.getSize() == arg3.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.fma(rm, arg2, arg3)));
   }
@@ -411,7 +411,7 @@ namespace constantFold {
     FloatingPoint arg1(node[1].getConst<FloatingPoint>());
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.div(rm, arg2)));
   }
@@ -443,7 +443,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.rem(arg2)));
   }
@@ -455,7 +455,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     FloatingPoint::PartialFloatingPoint res(arg1.min(arg2));
 
@@ -475,7 +475,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     FloatingPoint::PartialFloatingPoint res(arg1.max(arg2));
 
@@ -495,7 +495,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     // Can be called with the third argument non-constant
     if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
@@ -525,7 +525,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     // Can be called with the third argument non-constant
     if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
@@ -559,7 +559,7 @@ namespace constantFold {
       FloatingPoint arg1(node[0].getConst<FloatingPoint>());
       FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-      Assert(arg1.d_fp_size == arg2.d_fp_size);
+      Assert(arg1.getSize() == arg2.getSize());
 
       return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 == arg2));
 
@@ -581,7 +581,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 <= arg2));
   }
@@ -594,7 +594,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 < arg2));
   }
@@ -657,8 +657,8 @@ namespace constantFold {
     const BitVector &bv = node[0].getConst<BitVector>();
 
     Node lit = NodeManager::currentNM()->mkConst(
-        FloatingPoint(param.d_fp_size.exponentWidth(),
-                      param.d_fp_size.significandWidth(),
+        FloatingPoint(param.getSize().exponentWidth(),
+                      param.getSize().significandWidth(),
                       bv));
 
     return RewriteResponse(REWRITE_DONE, lit);
@@ -674,7 +674,7 @@ namespace constantFold {
 
     return RewriteResponse(
         REWRITE_DONE,
-        NodeManager::currentNM()->mkConst(arg1.convert(info.d_fp_size, rm)));
+        NodeManager::currentNM()->mkConst(arg1.convert(info.getSize(), rm)));
   }
 
   RewriteResponse convertFromRealLiteral (TNode node, bool) {
@@ -686,7 +686,7 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     Rational arg(node[1].getConst<Rational>());
 
-    FloatingPoint res(param.d_fp_size, rm, arg);
+    FloatingPoint res(param.getSize(), rm, arg);
 
     Node lit = NodeManager::currentNM()->mkConst(res);
     
@@ -702,7 +702,7 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     BitVector arg(node[1].getConst<BitVector>());
 
-    FloatingPoint res(param.d_fp_size, rm, arg, true);
+    FloatingPoint res(param.getSize(), rm, arg, true);
 
     Node lit = NodeManager::currentNM()->mkConst(res);
     
@@ -718,7 +718,7 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     BitVector arg(node[1].getConst<BitVector>());
 
-    FloatingPoint res(param.d_fp_size, rm, arg, false);
+    FloatingPoint res(param.getSize(), rm, arg, false);
 
     Node lit = NodeManager::currentNM()->mkConst(res);
     
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index 32c718654..ab193d7ba 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -42,18 +42,18 @@ class FloatingPointConstantTypeRule {
 
     if (check)
     {
-      if (!(validExponentSize(f.d_fp_size.exponentWidth())))
+      if (!(validExponentSize(f.getSize().exponentWidth())))
       {
         throw TypeCheckingExceptionPrivate(
             n, "constant with invalid exponent size");
       }
-      if (!(validSignificandSize(f.d_fp_size.significandWidth())))
+      if (!(validSignificandSize(f.getSize().significandWidth())))
       {
         throw TypeCheckingExceptionPrivate(
             n, "constant with invalid significand size");
       }
     }
-    return nodeManager->mkFloatingPointType(f.d_fp_size);
+    return nodeManager->mkFloatingPointType(f.getSize());
   }
 };
 
@@ -243,7 +243,8 @@ class FloatingPointParametricOpTypeRule {
   }
 };
 
-class FloatingPointToFPIEEEBitVectorTypeRule {
+class FloatingPointToFPIEEEBitVectorTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -264,8 +265,8 @@ class FloatingPointToFPIEEEBitVectorTypeRule {
                                            "than bit vector");
       }
       else if (!(operandType.getBitVectorSize()
-                 == info.d_fp_size.exponentWidth()
-                        + info.d_fp_size.significandWidth()))
+                 == info.getSize().exponentWidth()
+                        + info.getSize().significandWidth()))
       {
         throw TypeCheckingExceptionPrivate(
             n,
@@ -274,11 +275,12 @@ class FloatingPointToFPIEEEBitVectorTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
-class FloatingPointToFPFloatingPointTypeRule {
+class FloatingPointToFPFloatingPointTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -306,11 +308,12 @@ class FloatingPointToFPFloatingPointTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
-class FloatingPointToFPRealTypeRule {
+class FloatingPointToFPRealTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -338,11 +341,12 @@ class FloatingPointToFPRealTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
-class FloatingPointToFPSignedBitVectorTypeRule {
+class FloatingPointToFPSignedBitVectorTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -370,11 +374,12 @@ class FloatingPointToFPSignedBitVectorTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
-class FloatingPointToFPUnsignedBitVectorTypeRule {
+class FloatingPointToFPUnsignedBitVectorTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -402,11 +407,12 @@ class FloatingPointToFPUnsignedBitVectorTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
-class FloatingPointToFPGenericTypeRule {
+class FloatingPointToFPGenericTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -427,7 +433,7 @@ class FloatingPointToFPGenericTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
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 */
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index 758d51bc5..b6c1bfb53 100644
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -48,28 +48,43 @@ class FloatingPoint
 
   /**
    * Get the number of exponent bits in the unpacked format corresponding to a
-   * given packed format.  These is the unpacked counter-parts of
+   * given packed format.  This is the unpacked counter-part of
    * FloatingPointSize::exponentWidth().
    */
   static uint32_t getUnpackedExponentWidth(FloatingPointSize& size);
   /**
    * Get the number of exponent bits in the unpacked format corresponding to a
-   * given packed format.  These is the unpacked counter-parts of
+   * given packed format.  This is the unpacked counter-part of
    * FloatingPointSize::significandWidth().
    */
   static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
 
   /** Constructors. */
+
+  /** Create a FP value from its IEEE bit-vector representation. */
   FloatingPoint(uint32_t e, uint32_t s, const BitVector& bv);
   FloatingPoint(const FloatingPointSize& size, const BitVector& bv);
-  FloatingPoint(const FloatingPoint& fp);
+
+  /**
+   * Create a FP value from a signed or unsigned bit-vector value with
+   * respect to given rounding mode.
+   */
   FloatingPoint(const FloatingPointSize& size,
                 const RoundingMode& rm,
                 const BitVector& bv,
                 bool signedBV);
+
+  /**
+   * Create a FP value from a rational value with respect to given rounding
+   * mode.
+   */
   FloatingPoint(const FloatingPointSize& size,
                 const RoundingMode& rm,
                 const Rational& r);
+
+  /** Copy constructor. */
+  FloatingPoint(const FloatingPoint& fp);
+
   /** Destructor. */
   ~FloatingPoint();
 
@@ -117,6 +132,9 @@ class FloatingPoint
    */
   static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign);
 
+  /** Return the size of this FP value. */
+  const FloatingPointSize& getSize() const;
+
   /** Get the wrapped floating-point value. */
   const FloatingPointLiteral* getLiteral(void) const { return d_fpl.get(); }
 
@@ -254,9 +272,6 @@ class FloatingPoint
    */
   PartialRational convertToRational(void) const;
 
-  /** The floating-point size of this floating-point value. */
-  FloatingPointSize d_fp_size;
-
  private:
   /**
    * Constructor.
@@ -264,7 +279,7 @@ class FloatingPoint
    * Note: This constructor takes ownership of 'fpl' and is not intended for
    *       public use.
    */
-  FloatingPoint(const FloatingPointSize& fp_size, FloatingPointLiteral* fpl);
+  FloatingPoint(FloatingPointLiteral* fpl);
 
   /** The floating-point literal of this floating-point value. */
   std::unique_ptr<FloatingPointLiteral> d_fpl;
@@ -281,7 +296,7 @@ struct FloatingPointHashFunction
     FloatingPointSizeHashFunction fpshf;
     BitVectorHashFunction bvhf;
 
-    return fpshf(fp.d_fp_size) ^ bvhf(fp.pack());
+    return fpshf(fp.getSize()) ^ bvhf(fp.pack());
   }
 }; /* struct FloatingPointHashFunction */
 
@@ -303,6 +318,10 @@ class FloatingPointConvertSort
     return d_fp_size == fpcs.d_fp_size;
   }
 
+  /** Return the size of this FP convert sort. */
+  FloatingPointSize getSize() const { return d_fp_size; }
+
+ private:
   /** The floating-point size of this sort. */
   FloatingPointSize d_fp_size;
 };
@@ -314,7 +333,7 @@ struct FloatingPointConvertSortHashFunction
   inline size_t operator()(const FloatingPointConvertSort& fpcs) const
   {
     FloatingPointSizeHashFunction f;
-    return f(fpcs.d_fp_size) ^ (0x00005300 | (key << 24));
+    return f(fpcs.getSize()) ^ (0x00005300 | (key << 24));
   }
 }; /* struct FloatingPointConvertSortHashFunction */
 
diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp
index 05a219251..59b14001d 100644
--- a/src/util/floatingpoint_literal_symfpu.cpp
+++ b/src/util/floatingpoint_literal_symfpu.cpp
@@ -15,23 +15,512 @@
 
 #include "base/check.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
+}  // namespace symfpu
+#endif
+
+/* -------------------------------------------------------------------------- */
+
 namespace CVC4 {
 
-#ifndef CVC4_USE_SYMFPU
-void FloatingPointLiteral::unfinished(void) const
+uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size)
+{
+#ifdef CVC4_USE_SYMFPU
+  return SymFPUUnpackedFloatLiteral::exponentWidth(size);
+#else
+  unimplemented();
+  return 2;
+#endif
+}
+
+uint32_t FloatingPointLiteral::getUnpackedSignificandWidth(
+    FloatingPointSize& size)
+{
+#ifdef CVC4_USE_SYMFPU
+  return SymFPUUnpackedFloatLiteral::significandWidth(size);
+#else
+  unimplemented();
+  return 2;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::makeNaN(
+    const FloatingPointSize& size)
+{
+#ifdef CVC4_USE_SYMFPU
+  return FloatingPointLiteral(size, SymFPUUnpackedFloatLiteral::makeNaN(size));
+#else
+  unimplemented();
+  return FloatingPointLiteral(size, BitVector(4u, 0u));
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::makeInf(
+    const FloatingPointSize& size, bool sign)
+{
+#ifdef CVC4_USE_SYMFPU
+  return FloatingPointLiteral(size,
+                              SymFPUUnpackedFloatLiteral::makeInf(size, sign));
+#else
+  unimplemented();
+  return FloatingPointLiteral(size, BitVector(4u, 0u));
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::makeZero(
+    const FloatingPointSize& size, bool sign)
+{
+#ifdef CVC4_USE_SYMFPU
+  return FloatingPointLiteral(size,
+                              SymFPUUnpackedFloatLiteral::makeZero(size, sign));
+#else
+  unimplemented();
+  return FloatingPointLiteral(size, BitVector(4u, 0u));
+#endif
+}
+
+FloatingPointLiteral::FloatingPointLiteral(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_symuf(symfpu::unpack<symfpuLiteral::traits>(
+          symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv))
+#endif
+{
+}
+
+FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
+                                           const BitVector& bv)
+    : d_fp_size(size)
+#ifdef CVC4_USE_SYMFPU
+      ,
+      d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv))
+#endif
+{
+}
+
+FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
+                                           const RoundingMode& rm,
+                                           const BitVector& bv,
+                                           bool signedBV)
+    : d_fp_size(size)
+#ifdef CVC4_USE_SYMFPU
+      ,
+      d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>(
+                  symfpuLiteral::CVC4FPSize(size),
+                  symfpuLiteral::CVC4RM(rm),
+                  symfpuLiteral::CVC4SignedBitVector(bv))
+                       : symfpu::convertUBVToFloat<symfpuLiteral::traits>(
+                           symfpuLiteral::CVC4FPSize(size),
+                           symfpuLiteral::CVC4RM(rm),
+                           symfpuLiteral::CVC4UnsignedBitVector(bv)))
+#endif
+{
+}
+
+BitVector FloatingPointLiteral::pack(void) const
 {
-  Unimplemented() << "Floating-point literals not yet implemented.";
+#ifdef CVC4_USE_SYMFPU
+  BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf));
+#else
+  unimplemented();
+  BitVector bv(4u, 0u);
+#endif
+  return bv;
+}
+
+FloatingPointLiteral FloatingPointLiteral::absolute(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return FloatingPointLiteral(
+      d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::negate(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return FloatingPointLiteral(
+      d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::add(
+    const RoundingMode& rm, const FloatingPointLiteral& arg) const
+{
+#ifdef CVC4_USE_SYMFPU
+  Assert(d_fp_size == arg.d_fp_size);
+  return FloatingPointLiteral(d_fp_size,
+                              symfpu::add<symfpuLiteral::traits>(
+                                  d_fp_size, rm, d_symuf, arg.d_symuf, true));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::sub(
+    const RoundingMode& rm, const FloatingPointLiteral& arg) const
+{
+#ifdef CVC4_USE_SYMFPU
+  Assert(d_fp_size == arg.d_fp_size);
+  return FloatingPointLiteral(d_fp_size,
+                              symfpu::add<symfpuLiteral::traits>(
+                                  d_fp_size, rm, d_symuf, arg.d_symuf, false));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::mult(
+    const RoundingMode& rm, const FloatingPointLiteral& arg) const
+{
+#ifdef CVC4_USE_SYMFPU
+  Assert(d_fp_size == arg.d_fp_size);
+  return FloatingPointLiteral(d_fp_size,
+                              symfpu::multiply<symfpuLiteral::traits>(
+                                  d_fp_size, rm, d_symuf, arg.d_symuf));
+#else
+  unimplemented();
+  return *this;
+#endif
 }
 
-bool FloatingPointLiteral::operator==(const FloatingPointLiteral& other) const
+FloatingPointLiteral FloatingPointLiteral::div(
+    const RoundingMode& rm, const FloatingPointLiteral& arg) const
 {
-  unfinished();
+#ifdef CVC4_USE_SYMFPU
+  Assert(d_fp_size == arg.d_fp_size);
+  return FloatingPointLiteral(d_fp_size,
+                              symfpu::divide<symfpuLiteral::traits>(
+                                  d_fp_size, rm, d_symuf, arg.d_symuf));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::fma(
+    const RoundingMode& rm,
+    const FloatingPointLiteral& arg1,
+    const FloatingPointLiteral& arg2) const
+{
+#ifdef CVC4_USE_SYMFPU
+  Assert(d_fp_size == arg1.d_fp_size);
+  Assert(d_fp_size == arg2.d_fp_size);
+  return FloatingPointLiteral(
+      d_fp_size,
+      symfpu::fma<symfpuLiteral::traits>(
+          d_fp_size, rm, d_symuf, arg1.d_symuf, arg2.d_symuf));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return FloatingPointLiteral(
+      d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return FloatingPointLiteral(
+      d_fp_size,
+      symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::rem(
+    const FloatingPointLiteral& arg) const
+{
+#ifdef CVC4_USE_SYMFPU
+  Assert(d_fp_size == arg.d_fp_size);
+  return FloatingPointLiteral(d_fp_size,
+                              symfpu::remainder<symfpuLiteral::traits>(
+                                  d_fp_size, d_symuf, arg.d_symuf));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::maxTotal(
+    const FloatingPointLiteral& arg, bool zeroCaseLeft) const
+{
+#ifdef CVC4_USE_SYMFPU
+  Assert(d_fp_size == arg.d_fp_size);
+  return FloatingPointLiteral(
+      d_fp_size,
+      symfpu::max<symfpuLiteral::traits>(
+          d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::minTotal(
+    const FloatingPointLiteral& arg, bool zeroCaseLeft) const
+{
+#ifdef CVC4_USE_SYMFPU
+  Assert(d_fp_size == arg.d_fp_size);
+  return FloatingPointLiteral(
+      d_fp_size,
+      symfpu::min<symfpuLiteral::traits>(
+          d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return ((d_fp_size == fp.d_fp_size)
+          && symfpu::smtlibEqual<symfpuLiteral::traits>(
+              d_fp_size, d_symuf, fp.d_symuf));
+#else
+  unimplemented();
+  return ((d_fp_size == fp.d_fp_size));
+#endif
+}
+
+bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const
+{
+#ifdef CVC4_USE_SYMFPU
+  Assert(d_fp_size == arg.d_fp_size);
+  return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
+      d_fp_size, d_symuf, arg.d_symuf);
+#else
+  unimplemented();
   return false;
+#endif
+}
+
+bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const
+{
+#ifdef CVC4_USE_SYMFPU
+  Assert(d_fp_size == arg.d_fp_size);
+  return symfpu::lessThan<symfpuLiteral::traits>(
+      d_fp_size, d_symuf, arg.d_symuf);
+#else
+  unimplemented();
+  return false;
+#endif
+}
+
+BitVector FloatingPointLiteral::getExponent() const
+{
+#ifdef CVC4_USE_SYMFPU
+  return d_symuf.exponent;
+#else
+  unimplemented();
+  Unreachable() << "no concrete implementation of FloatingPointLiteral";
+  return BitVector();
+#endif
+}
+
+BitVector FloatingPointLiteral::getSignificand() const
+{
+#ifdef CVC4_USE_SYMFPU
+  return d_symuf.significand;
+#else
+  unimplemented();
+  Unreachable() << "no concrete implementation of FloatingPointLiteral";
+  return BitVector();
+#endif
+}
+
+bool FloatingPointLiteral::getSign() const
+{
+#ifdef CVC4_USE_SYMFPU
+  return d_symuf.sign;
+#else
+  unimplemented();
+  Unreachable() << "no concrete implementation of FloatingPointLiteral";
+  return false;
+#endif
+}
+
+bool FloatingPointLiteral::isNormal(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+  unimplemented();
+  return false;
+#endif
+}
+
+bool FloatingPointLiteral::isSubnormal(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+  unimplemented();
+  return false;
+#endif
+}
+
+bool FloatingPointLiteral::isZero(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+  unimplemented();
+  return false;
+#endif
+}
+
+bool FloatingPointLiteral::isInfinite(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+  unimplemented();
+  return false;
+#endif
+}
+
+bool FloatingPointLiteral::isNaN(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+  unimplemented();
+  return false;
+#endif
+}
+
+bool FloatingPointLiteral::isNegative(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+  unimplemented();
+  return false;
+#endif
+}
+
+bool FloatingPointLiteral::isPositive(void) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf);
+#else
+  unimplemented();
+  return false;
+#endif
+}
+
+FloatingPointLiteral FloatingPointLiteral::convert(
+    const FloatingPointSize& target, const RoundingMode& rm) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return FloatingPointLiteral(
+      target,
+      symfpu::convertFloatToFloat<symfpuLiteral::traits>(
+          d_fp_size, target, rm, d_symuf));
+#else
+  unimplemented();
+  return *this;
+#endif
+}
+
+BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width,
+                                                  const RoundingMode& rm,
+                                                  BitVector undefinedCase) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
+      d_fp_size, rm, d_symuf, width, undefinedCase);
+#else
+  unimplemented();
+  return undefinedCase;
+#endif
+}
+
+BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width,
+                                                  const RoundingMode& rm,
+                                                  BitVector undefinedCase) const
+{
+#ifdef CVC4_USE_SYMFPU
+  return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
+      d_fp_size, rm, d_symuf, width, undefinedCase);
+#else
+  unimplemented();
+  return undefinedCase;
+#endif
+}
+
+#ifndef CVC4_USE_SYMFPU
+void FloatingPointLiteral::unimplemented(void)
+{
+  Unimplemented() << "no concrete implementation of FloatingPointLiteral";
 }
 
 size_t FloatingPointLiteral::hash(void) const
 {
-  unfinished();
+  unimplemented();
   return 23;
 }
 #endif
diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in
index 3040dae78..d7e1a2241 100644
--- a/src/util/floatingpoint_literal_symfpu.h.in
+++ b/src/util/floatingpoint_literal_symfpu.h.in
@@ -19,6 +19,7 @@
 #define CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
 
 #include "util/bitvector.h"
+#include "util/floatingpoint_size.h"
 #include "util/roundingmode.h"
 
 // clang-format off
@@ -32,7 +33,7 @@
 namespace CVC4 {
 
 class FloatingPointSize;
-class FloatingPoint;
+class FloatingPointLiteral;
 
 /* -------------------------------------------------------------------------- */
 
@@ -277,23 +278,69 @@ class wrappedBitVector : public BitVector
 // clang-format off
 #if @CVC4_USE_SYMFPU@
 // clang-format on
-using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat<symfpuLiteral::traits>;
+using SymFPUUnpackedFloatLiteral =
+    ::symfpu::unpackedFloat<symfpuLiteral::traits>;
 #endif
 
 class FloatingPointLiteral
 {
   friend class FloatingPoint;
+
  public:
-  /** Constructors. */
+  /**
+   * Get the number of exponent bits in the unpacked format corresponding to a
+   * given packed format.  This is the unpacked counter-part of
+   * FloatingPointSize::exponentWidth().
+   */
+  static uint32_t getUnpackedExponentWidth(FloatingPointSize& size);
+  /**
+   * Get the number of exponent bits in the unpacked format corresponding to a
+   * given packed format.  This is the unpacked counter-part of
+   * FloatingPointSize::significandWidth().
+   */
+  static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
 
-  /** Create an FP literal from a FloatingPoint. */
-  FloatingPointLiteral(FloatingPoint& other);
+  /**
+   * Create a FP NaN literal of given size.
+   * size: The FP size (format).
+   */
+  static FloatingPointLiteral makeNaN(const FloatingPointSize& size);
+  /**
+   * Create a FP infinity literal of given size.
+   * size: The FP size (format).
+   * sign: True for -oo, false otherwise.
+   */
+  static FloatingPointLiteral makeInf(const FloatingPointSize& size, bool sign);
+  /**
+   * Create a FP zero literal of given size.
+   * size: The FP size (format).
+   * sign: True for -zero, false otherwise.
+   */
+  static FloatingPointLiteral makeZero(const FloatingPointSize& size,
+                                       bool sign);
 // clang-format off
-#if @CVC4_USE_SYMFPU@
-// clang-format on
+#if !@CVC4_USE_SYMFPU@
+  // clang-format on
+  /** Catch-all for unimplemented functions. */
+  static void unimplemented(void);
+#endif
 
-  /** Create an FP literal from a symFPU unpacked float. */
-  FloatingPointLiteral(SymFPUUnpackedFloatLiteral symuf) : d_symuf(symuf){};
+  /** Constructors. */
+
+  /** Create a FP literal from its IEEE bit-vector representation. */
+  FloatingPointLiteral(uint32_t d_exp_size,
+                       uint32_t d_sig_size,
+                       const BitVector& bv);
+  FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv);
+
+  /**
+   * Create a FP literal from a signed or unsigned bit-vector value with
+   * respect to given rounding mode.
+   */
+  FloatingPointLiteral(const FloatingPointSize& size,
+                       const RoundingMode& rm,
+                       const BitVector& bv,
+                       bool signedBV);
 
   /**
    * Create a FP literal from unpacked representation.
@@ -305,43 +352,155 @@ class FloatingPointLiteral
    * representation -- for this, the above constructor is to be used while
    * creating a SymFPUUnpackedFloatLiteral via symfpu::unpack.
    */
-  FloatingPointLiteral(const bool sign,
+  FloatingPointLiteral(const FloatingPointSize& size,
+                       const bool sign,
                        const BitVector& exp,
                        const BitVector& sig)
-      : d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
+      : d_fp_size(size)
+// clang-format off
+#if @CVC4_USE_SYMFPU@
+        // clang-format on
+        ,
+        d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
+#endif
   {
   }
-#else
-  FloatingPointLiteral(uint32_t, uint32_t, double) { unfinished(); };
+
+// clang-format off
+#if @CVC4_USE_SYMFPU@
+  // clang-format on
+
+  /** Create a FP literal from a symFPU unpacked float. */
+  FloatingPointLiteral(const FloatingPointSize& size,
+                       SymFPUUnpackedFloatLiteral symuf)
+      : d_fp_size(size), d_symuf(symuf){};
 #endif
+
   ~FloatingPointLiteral() {}
 
+  /** Return the size of this FP literal. */
+  const FloatingPointSize& getSize() const { return d_fp_size; };
+
+  /** Return the packed (IEEE-754) representation of this literal. */
+  BitVector pack(void) const;
+
+  /** Floating-point absolute value literal. */
+  FloatingPointLiteral absolute(void) const;
+  /** Floating-point negation literal. */
+  FloatingPointLiteral negate(void) const;
+  /** Floating-point addition literal. */
+  FloatingPointLiteral add(const RoundingMode& rm,
+                           const FloatingPointLiteral& arg) const;
+  /** Floating-point subtraction literal. */
+  FloatingPointLiteral sub(const RoundingMode& rm,
+                           const FloatingPointLiteral& arg) const;
+  /** Floating-point multiplication literal. */
+  FloatingPointLiteral mult(const RoundingMode& rm,
+                            const FloatingPointLiteral& arg) const;
+  /** Floating-point division literal. */
+  FloatingPointLiteral div(const RoundingMode& rm,
+                           const FloatingPointLiteral& arg) const;
+  /** Floating-point fused multiplication and addition literal. */
+  FloatingPointLiteral fma(const RoundingMode& rm,
+                           const FloatingPointLiteral& arg1,
+                           const FloatingPointLiteral& arg2) const;
+  /** Floating-point square root literal. */
+  FloatingPointLiteral sqrt(const RoundingMode& rm) const;
+  /** Floating-point round to integral literal. */
+  FloatingPointLiteral rti(const RoundingMode& rm) const;
+  /** Floating-point remainder literal. */
+  FloatingPointLiteral rem(const FloatingPointLiteral& arg) const;
+
+  /**
+   * Floating-point max literal (total version).
+   * zeroCase: true to return the left (rather than the right operand) in case
+   *           of max(-0,+0) or max(+0,-0).
+   */
+  FloatingPointLiteral maxTotal(const FloatingPointLiteral& arg,
+                                bool zeroCaseLeft) const;
+  /**
+   * Floating-point min literal (total version).
+   * zeroCase: true to return the left (rather than the right operand) in case
+   *           of min(-0,+0) or min(+0,-0).
+   */
+  FloatingPointLiteral minTotal(const FloatingPointLiteral& arg,
+                                bool zeroCaseLeft) const;
+
+  /** Equality literal (NOT: fp.eq but =) over floating-point values. */
+  bool operator==(const FloatingPointLiteral& fp) const;
+  /** Floating-point less or equal than literal. */
+  bool operator<=(const FloatingPointLiteral& arg) const;
+  /** Floating-point less than literal. */
+  bool operator<(const FloatingPointLiteral& arg) const;
+
+  /** Get the exponent of this floating-point value. */
+  BitVector getExponent() const;
+  /** Get the significand of this floating-point value. */
+  BitVector getSignificand() const;
+  /** True if this value is a negative value. */
+  bool getSign() const;
+
+  /** Return true if this literal represents a normal value. */
+  bool isNormal(void) const;
+  /** Return true if this  literal represents a subnormal value. */
+  bool isSubnormal(void) const;
+  /** Return true if this literal represents a zero value. */
+  bool isZero(void) const;
+  /** Return true if this literal represents an infinite value. */
+  bool isInfinite(void) const;
+  /** Return true if this literal represents a NaN value. */
+  bool isNaN(void) const;
+  /** Return true if this literal represents a negative value. */
+  bool isNegative(void) const;
+  /** Return true if this literal represents a positive value. */
+  bool isPositive(void) const;
+
+  /**
+   * Convert this floating-point literal to a literal of given size, with
+   * respect to given rounding mode.
+   */
+  FloatingPointLiteral convert(const FloatingPointSize& target,
+                               const RoundingMode& rm) const;
+
+  /**
+   * Convert this floating-point literal to a signed bit-vector of given size,
+   * with respect to given rounding mode (total version).
+   * Returns given bit-vector 'undefinedCase' in the undefined case.
+   */
+  BitVector convertToSBVTotal(BitVectorSize width,
+                              const RoundingMode& rm,
+                              BitVector undefinedCase) const;
+  /**
+   * Convert this floating-point literal to an unsigned bit-vector of given
+   * size, with respect to given rounding mode (total version).
+   * Returns given bit-vector 'undefinedCase' in the undefined case.
+   */
+  BitVector convertToUBVTotal(BitVectorSize width,
+                              const RoundingMode& rm,
+                              BitVector undefinedCase) const;
 // clang-format off
 #if @CVC4_USE_SYMFPU@
-// clang-format on
+  // clang-format on
   /** Return wrapped floating-point literal. */
   const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; }
 #else
-  /** Catch-all for unimplemented functions. */
-  void unfinished(void) const;
   /** Dummy hash function. */
   size_t hash(void) const;
-  /** Dummy comparison operator overload. */
-  bool operator==(const FloatingPointLiteral& other) const;
 #endif
 
  private:
+  /** The floating-point size of this floating-point literal. */
+  FloatingPointSize d_fp_size;
 // clang-format off
 #if @CVC4_USE_SYMFPU@
-// clang-format on
+  // clang-format on
   /** The actual floating-point value, a SymFPU unpackedFloat. */
   SymFPUUnpackedFloatLiteral d_symuf;
 #endif
 };
 
-
 /* -------------------------------------------------------------------------- */
 
-}
+}  // namespace CVC4
 
 #endif