FloatingPoint: Clean up and document header, format. (#5453)

This cleans up the src/util/floatingpoint.h.in header to conform to the
code style guidelines of CVC4. This further attempts to fully document
the header. The main changes (except for added documentation) are
renames of member variables, getting rid of the redundant functions
FloatingPointSize::exponent() and FloatingPointSize::significand(),
and a more explicit naming of CVC4 wrapper types vs symFPU trait
types. Else, it's mainly reordering and formatting.

8 files changed, 1249 insertions, 848 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 24902b888..a7cc8e17f 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1433,10 +1433,10 @@ uint32_t Op::getIndices() const
     case INT_TO_BITVECTOR: i = d_node->getConst<IntToBitVector>().d_size; break;
     case IAND: i = d_node->getConst<IntAnd>().d_size; break;
     case FLOATINGPOINT_TO_UBV:
-      i = d_node->getConst<FloatingPointToUBV>().bvs.d_size;
+      i = d_node->getConst<FloatingPointToUBV>().d_bv_size.d_size;
       break;
     case FLOATINGPOINT_TO_SBV:
-      i = d_node->getConst<FloatingPointToSBV>().bvs.d_size;
+      i = d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size;
       break;
     case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break;
     case REGEXP_REPEAT:
@@ -1469,36 +1469,42 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const
   {
     CVC4::FloatingPointToFPIEEEBitVector ext =
         d_node->getConst<FloatingPointToFPIEEEBitVector>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
+                             ext.d_fp_size.significandWidth());
   }
   else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
   {
     CVC4::FloatingPointToFPFloatingPoint ext =
         d_node->getConst<FloatingPointToFPFloatingPoint>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
+                             ext.d_fp_size.significandWidth());
   }
   else if (k == FLOATINGPOINT_TO_FP_REAL)
   {
     CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
+                             ext.d_fp_size.significandWidth());
   }
   else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
   {
     CVC4::FloatingPointToFPSignedBitVector ext =
         d_node->getConst<FloatingPointToFPSignedBitVector>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
+                             ext.d_fp_size.significandWidth());
   }
   else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR)
   {
     CVC4::FloatingPointToFPUnsignedBitVector ext =
         d_node->getConst<FloatingPointToFPUnsignedBitVector>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
+                             ext.d_fp_size.significandWidth());
   }
   else if (k == FLOATINGPOINT_TO_FP_GENERIC)
   {
     CVC4::FloatingPointToFPGeneric ext =
         d_node->getConst<FloatingPointToFPGeneric>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+    indices = std::make_pair(ext.d_fp_size.exponentWidth(),
+                             ext.d_fp_size.significandWidth());
   }
   else if (k == REGEXP_LOOP)
   {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 90c1daf24..895e05093 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -1073,10 +1073,9 @@ inline bool TypeNode::isTester() const {
 /** Is this a floating-point type of with <code>exp</code> exponent bits
     and <code>sig</code> significand bits */
 inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {
-  return
-    ( getKind() == kind::FLOATINGPOINT_TYPE &&
-      getConst<FloatingPointSize>().exponent() == exp &&
-      getConst<FloatingPointSize>().significand() == sig );
+  return (getKind() == kind::FLOATINGPOINT_TYPE
+          && getConst<FloatingPointSize>().exponentWidth() == exp
+          && getConst<FloatingPointSize>().significandWidth() == sig);
 }
 
 /** Is this a bit-vector type of size <code>size</code> */
@@ -1088,13 +1087,13 @@ inline bool TypeNode::isBitVector(unsigned size) const {
 /** Get the exponent size of this floating-point type */
 inline unsigned TypeNode::getFloatingPointExponentSize() const {
   Assert(isFloatingPoint());
-  return getConst<FloatingPointSize>().exponent();
+  return getConst<FloatingPointSize>().exponentWidth();
 }
 
 /** Get the significand size of this floating-point type */
 inline unsigned TypeNode::getFloatingPointSignificandSize() const {
   Assert(isFloatingPoint());
-  return getConst<FloatingPointSize>().significand();
+  return getConst<FloatingPointSize>().significandWidth();
 }
 
 /** Get the size of this bit-vector type */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index d44842633..6628576dd 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -183,9 +183,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const
       break;
     case kind::FLOATINGPOINT_TYPE:
       out << "(_ FloatingPoint "
-          << n.getConst<FloatingPointSize>().exponent() << " "
-          << n.getConst<FloatingPointSize>().significand()
-          << ")";
+          << n.getConst<FloatingPointSize>().exponentWidth() << " "
+          << n.getConst<FloatingPointSize>().significandWidth() << ")";
       break;
     case kind::CONST_BITVECTOR:
     {
@@ -353,53 +352,69 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const
       break;
     case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
       out << "(_ to_fp "
-          << n.getConst<FloatingPointToFPIEEEBitVector>().t.exponent() << ' '
-          << n.getConst<FloatingPointToFPIEEEBitVector>().t.significand()
+          << n.getConst<FloatingPointToFPIEEEBitVector>()
+                 .d_fp_size.exponentWidth()
+          << ' '
+          << n.getConst<FloatingPointToFPIEEEBitVector>()
+                 .d_fp_size.significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
       out << "(_ to_fp "
-          << n.getConst<FloatingPointToFPFloatingPoint>().t.exponent() << ' '
-          << n.getConst<FloatingPointToFPFloatingPoint>().t.significand()
+          << n.getConst<FloatingPointToFPFloatingPoint>()
+                 .d_fp_size.exponentWidth()
+          << ' '
+          << n.getConst<FloatingPointToFPFloatingPoint>()
+                 .d_fp_size.significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_REAL_OP:
-      out << "(_ to_fp " << n.getConst<FloatingPointToFPReal>().t.exponent()
-          << ' ' << n.getConst<FloatingPointToFPReal>().t.significand() << ")";
+      out << "(_ to_fp "
+          << n.getConst<FloatingPointToFPReal>().d_fp_size.exponentWidth()
+          << ' '
+          << n.getConst<FloatingPointToFPReal>().d_fp_size.significandWidth()
+          << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
       out << "(_ to_fp "
-          << n.getConst<FloatingPointToFPSignedBitVector>().t.exponent() << ' '
-          << n.getConst<FloatingPointToFPSignedBitVector>().t.significand()
+          << n.getConst<FloatingPointToFPSignedBitVector>()
+                 .d_fp_size.exponentWidth()
+          << ' '
+          << n.getConst<FloatingPointToFPSignedBitVector>()
+                 .d_fp_size.significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
       out << "(_ to_fp_unsigned "
-          << n.getConst<FloatingPointToFPUnsignedBitVector>().t.exponent()
+          << n.getConst<FloatingPointToFPUnsignedBitVector>()
+                 .d_fp_size.exponentWidth()
           << ' '
-          << n.getConst<FloatingPointToFPUnsignedBitVector>().t.significand()
+          << n.getConst<FloatingPointToFPUnsignedBitVector>()
+                 .d_fp_size.significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
-      out << "(_ to_fp " << n.getConst<FloatingPointToFPGeneric>().t.exponent()
-          << ' ' << n.getConst<FloatingPointToFPGeneric>().t.significand()
+      out << "(_ to_fp "
+          << n.getConst<FloatingPointToFPGeneric>().d_fp_size.exponentWidth()
+          << ' '
+          << n.getConst<FloatingPointToFPGeneric>().d_fp_size.significandWidth()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_UBV_OP:
-      out << "(_ fp.to_ubv " << n.getConst<FloatingPointToUBV>().bvs.d_size
-          << ")";
+      out << "(_ fp.to_ubv "
+          << n.getConst<FloatingPointToUBV>().d_bv_size.d_size << ")";
       break;
     case kind::FLOATINGPOINT_TO_SBV_OP:
-      out << "(_ fp.to_sbv " << n.getConst<FloatingPointToSBV>().bvs.d_size
-          << ")";
+      out << "(_ fp.to_sbv "
+          << n.getConst<FloatingPointToSBV>().d_bv_size.d_size << ")";
       break;
     case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
       out << "(_ fp.to_ubv_total "
-          << n.getConst<FloatingPointToUBVTotal>().bvs.d_size << ")";
+          << n.getConst<FloatingPointToUBVTotal>().d_bv_size.d_size << ")";
       break;
     case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
       out << "(_ fp.to_sbv_total "
-          << n.getConst<FloatingPointToSBVTotal>().bvs.d_size << ")";
+          << n.getConst<FloatingPointToSBVTotal>().d_bv_size.d_size << ")";
       break;
     case kind::REGEXP_REPEAT_OP:
       out << "(_ re.^ " << n.getConst<RegExpRepeat>().d_repeatAmount << ")";
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 47a4af43e..0d088fe41 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -1578,7 +1578,7 @@ Node FpConverter::convert(TNode node)
                             symfpu::convertFloatToUBV<traits>(fpt(childType),
                                                               (*mode).second,
                                                               (*arg1).second,
-                                                              info.bvs,
+                                                              info.d_bv_size,
                                                               ubv(current[2])));
             i = d_ubvMap.find(current);
           }
@@ -1620,7 +1620,7 @@ Node FpConverter::convert(TNode node)
                             symfpu::convertFloatToSBV<traits>(fpt(childType),
                                                               (*mode).second,
                                                               (*arg1).second,
-                                                              info.bvs,
+                                                              info.d_bv_size,
                                                               sbv(current[2])));
 
             i = d_sbvMap.find(current);
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 120f71b6d..49b4e85c5 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -369,7 +369,7 @@ namespace constantFold {
     FloatingPoint arg1(node[1].getConst<FloatingPoint>());
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.plus(rm, arg2)));
   }
@@ -382,7 +382,7 @@ namespace constantFold {
     FloatingPoint arg1(node[1].getConst<FloatingPoint>());
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.mult(rm, arg2)));
   }
@@ -396,8 +396,8 @@ namespace constantFold {
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
     FloatingPoint arg3(node[3].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
-    Assert(arg1.t == arg3.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.d_fp_size == arg3.d_fp_size);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.fma(rm, arg2, arg3)));
   }
@@ -410,7 +410,7 @@ namespace constantFold {
     FloatingPoint arg1(node[1].getConst<FloatingPoint>());
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.div(rm, arg2)));
   }
@@ -442,7 +442,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.rem(arg2)));
   }
@@ -454,7 +454,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
 
     FloatingPoint::PartialFloatingPoint res(arg1.min(arg2));
 
@@ -474,7 +474,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
 
     FloatingPoint::PartialFloatingPoint res(arg1.max(arg2));
 
@@ -494,7 +494,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
 
     // Can be called with the third argument non-constant
     if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
@@ -524,7 +524,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
 
     // Can be called with the third argument non-constant
     if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
@@ -558,7 +558,7 @@ namespace constantFold {
       FloatingPoint arg1(node[0].getConst<FloatingPoint>());
       FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-      Assert(arg1.t == arg2.t);
+      Assert(arg1.d_fp_size == arg2.d_fp_size);
 
       return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 == arg2));
 
@@ -580,7 +580,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 <= arg2));
   }
@@ -593,7 +593,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.t == arg2.t);
+    Assert(arg1.d_fp_size == arg2.d_fp_size);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 < arg2));
   }
@@ -654,12 +654,12 @@ namespace constantFold {
     TNode op = node.getOperator();
     const FloatingPointToFPIEEEBitVector &param = op.getConst<FloatingPointToFPIEEEBitVector>();
     const BitVector &bv = node[0].getConst<BitVector>();
-    
-    Node lit =
-      NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(),
-						      param.t.significand(),
-						      bv));
-    
+
+    Node lit = NodeManager::currentNM()->mkConst(
+        FloatingPoint(param.d_fp_size.exponentWidth(),
+                      param.d_fp_size.significandWidth(),
+                      bv));
+
     return RewriteResponse(REWRITE_DONE, lit);
   }
 
@@ -671,7 +671,9 @@ namespace constantFold {
     FloatingPoint arg1(node[1].getConst<FloatingPoint>());
     FloatingPointToFPFloatingPoint info = node.getOperator().getConst<FloatingPointToFPFloatingPoint>();
 
-    return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.convert(info.t,rm)));
+    return RewriteResponse(
+        REWRITE_DONE,
+        NodeManager::currentNM()->mkConst(arg1.convert(info.d_fp_size, rm)));
   }
 
   RewriteResponse convertFromRealLiteral (TNode node, bool) {
@@ -683,8 +685,8 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     Rational arg(node[1].getConst<Rational>());
 
-    FloatingPoint res(param.t, rm, arg);
-    
+    FloatingPoint res(param.d_fp_size, rm, arg);
+
     Node lit = NodeManager::currentNM()->mkConst(res);
     
     return RewriteResponse(REWRITE_DONE, lit);
@@ -699,8 +701,8 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     BitVector arg(node[1].getConst<BitVector>());
 
-    FloatingPoint res(param.t, rm, arg, true);
-    
+    FloatingPoint res(param.d_fp_size, rm, arg, true);
+
     Node lit = NodeManager::currentNM()->mkConst(res);
     
     return RewriteResponse(REWRITE_DONE, lit);
@@ -715,8 +717,8 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     BitVector arg(node[1].getConst<BitVector>());
 
-    FloatingPoint res(param.t, rm, arg, false);
-    
+    FloatingPoint res(param.d_fp_size, rm, arg, false);
+
     Node lit = NodeManager::currentNM()->mkConst(res);
     
     return RewriteResponse(REWRITE_DONE, lit);
@@ -731,7 +733,8 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     FloatingPoint arg(node[1].getConst<FloatingPoint>());
 
-    FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, false));
+    FloatingPoint::PartialBitVector res(
+        arg.convertToBV(param.d_bv_size, rm, false));
 
     if (res.second) {
       Node lit = NodeManager::currentNM()->mkConst(res.first);
@@ -751,7 +754,8 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     FloatingPoint arg(node[1].getConst<FloatingPoint>());
 
-    FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, true));
+    FloatingPoint::PartialBitVector res(
+        arg.convertToBV(param.d_bv_size, rm, true));
 
     if (res.second) {
       Node lit = NodeManager::currentNM()->mkConst(res.first);
@@ -791,12 +795,14 @@ namespace constantFold {
     if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
       BitVector partialValue(node[2].getConst<BitVector>());
 
-      BitVector folded(arg.convertToBVTotal(param.bvs, rm, false, partialValue));
+      BitVector folded(
+          arg.convertToBVTotal(param.d_bv_size, rm, false, partialValue));
       Node lit = NodeManager::currentNM()->mkConst(folded);
       return RewriteResponse(REWRITE_DONE, lit);
 
     } else {
-      FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, false));
+      FloatingPoint::PartialBitVector res(
+          arg.convertToBV(param.d_bv_size, rm, false));
 
       if (res.second) {
 	Node lit = NodeManager::currentNM()->mkConst(res.first);
@@ -821,13 +827,14 @@ namespace constantFold {
     if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
       BitVector partialValue(node[2].getConst<BitVector>());
 
-      BitVector folded(arg.convertToBVTotal(param.bvs, rm, true, partialValue));
+      BitVector folded(
+          arg.convertToBVTotal(param.d_bv_size, rm, true, partialValue));
       Node lit = NodeManager::currentNM()->mkConst(folded);
       return RewriteResponse(REWRITE_DONE, lit);
 
     } else {
-
-      FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, true));
+      FloatingPoint::PartialBitVector res(
+          arg.convertToBV(param.d_bv_size, rm, true));
 
       if (res.second) {
 	Node lit = NodeManager::currentNM()->mkConst(res.first);
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index bff909a39..4d4f3c660 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -39,17 +39,20 @@ class FloatingPointConstantTypeRule {
 
     const FloatingPoint& f = n.getConst<FloatingPoint>();
 
-    if (check) {
-      if (!(validExponentSize(f.t.exponent()))) {
+    if (check)
+    {
+      if (!(validExponentSize(f.d_fp_size.exponentWidth())))
+      {
         throw TypeCheckingExceptionPrivate(
             n, "constant with invalid exponent size");
       }
-      if (!(validSignificandSize(f.t.significand()))) {
+      if (!(validSignificandSize(f.d_fp_size.significandWidth())))
+      {
         throw TypeCheckingExceptionPrivate(
             n, "constant with invalid significand size");
       }
     }
-    return nodeManager->mkFloatingPointType(f.t);
+    return nodeManager->mkFloatingPointType(f.d_fp_size);
   }
 };
 
@@ -252,13 +255,17 @@ class FloatingPointToFPIEEEBitVectorTypeRule {
     if (check) {
       TypeNode operandType = n[0].getType(check);
 
-      if (!(operandType.isBitVector())) {
+      if (!(operandType.isBitVector()))
+      {
         throw TypeCheckingExceptionPrivate(n,
                                            "conversion to floating-point from "
                                            "bit vector used with sort other "
                                            "than bit vector");
-      } else if (!(operandType.getBitVectorSize() ==
-                   info.t.exponent() + info.t.significand())) {
+      }
+      else if (!(operandType.getBitVectorSize()
+                 == info.d_fp_size.exponentWidth()
+                        + info.d_fp_size.significandWidth()))
+      {
         throw TypeCheckingExceptionPrivate(
             n,
             "conversion to floating-point from bit vector used with bit vector "
@@ -266,7 +273,7 @@ class FloatingPointToFPIEEEBitVectorTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.t);
+    return nodeManager->mkFloatingPointType(info.d_fp_size);
   }
 };
 
@@ -298,7 +305,7 @@ class FloatingPointToFPFloatingPointTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.t);
+    return nodeManager->mkFloatingPointType(info.d_fp_size);
   }
 };
 
@@ -330,7 +337,7 @@ class FloatingPointToFPRealTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.t);
+    return nodeManager->mkFloatingPointType(info.d_fp_size);
   }
 };
 
@@ -362,7 +369,7 @@ class FloatingPointToFPSignedBitVectorTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.t);
+    return nodeManager->mkFloatingPointType(info.d_fp_size);
   }
 };
 
@@ -394,7 +401,7 @@ class FloatingPointToFPUnsignedBitVectorTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.t);
+    return nodeManager->mkFloatingPointType(info.d_fp_size);
   }
 };
 
@@ -419,7 +426,7 @@ class FloatingPointToFPGenericTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.t);
+    return nodeManager->mkFloatingPointType(info.d_fp_size);
   }
 };
 
@@ -450,7 +457,7 @@ class FloatingPointToUBVTypeRule {
       }
     }
 
-    return nodeManager->mkBitVectorType(info.bvs);
+    return nodeManager->mkBitVectorType(info.d_bv_size);
   }
 };
 
@@ -481,7 +488,7 @@ class FloatingPointToSBVTypeRule {
       }
     }
 
-    return nodeManager->mkBitVectorType(info.bvs);
+    return nodeManager->mkBitVectorType(info.d_bv_size);
   }
 };
 
@@ -522,7 +529,7 @@ class FloatingPointToUBVTotalTypeRule {
       }
     }
 
-    return nodeManager->mkBitVectorType(info.bvs);
+    return nodeManager->mkBitVectorType(info.d_bv_size);
   }
 };
 
@@ -563,7 +570,7 @@ class FloatingPointToSBVTotalTypeRule {
       }
     }
 
-    return nodeManager->mkBitVectorType(info.bvs);
+    return nodeManager->mkBitVectorType(info.d_bv_size);
   }
 };
 
@@ -686,7 +693,7 @@ class FloatingPointComponentExponent
      * Here we use types from floatingpoint.h which are the literal
      * back-end but it should't make a difference. */
     FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
-    symfpuLiteral::fpt format(fps);  // The symfpu interface to type info
+    symfpuLiteral::CVC4FPSize format(fps);  // The symfpu interface to type info
     unsigned bw = FloatingPointLiteral::exponentWidth(format);
 #else
     unsigned bw = 2;
@@ -729,7 +736,7 @@ class FloatingPointComponentSignificand
 #ifdef CVC4_USE_SYMFPU
     /* As before we need to use some of sympfu. */
     FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
-    symfpuLiteral::fpt format(fps);
+    symfpuLiteral::CVC4FPSize format(fps);
     unsigned bw = FloatingPointLiteral::significandWidth(format);
 #else
     unsigned bw = 1;
@@ -791,8 +798,8 @@ public:
      *  =       5 + ((2^e)-1)*2^s
      */
 
-    Integer significandValues = Integer(2).pow(fps.significand());
-    Integer exponentValues = Integer(2).pow(fps.exponent());
+    Integer significandValues = Integer(2).pow(fps.significandWidth());
+    Integer exponentValues = Integer(2).pow(fps.exponentWidth());
     exponentValues -= Integer(1);
 
     return Integer(5) + exponentValues * significandValues;
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index c84779be0..6e8f8369a 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -43,16 +43,16 @@
 #ifdef CVC4_USE_SYMFPU
 namespace symfpu {
 
-#define CVC4_LIT_ITE_DFN(T)                                        \
-  template <>                                                      \
-  struct ite<::CVC4::symfpuLiteral::prop, T>                       \
-  {                                                                \
-    static const T &iteOp(const ::CVC4::symfpuLiteral::prop &cond, \
-                          const T &l,                              \
-                          const T &r)                              \
-    {                                                              \
-      return cond ? l : r;                                         \
-    }                                                              \
+#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);
@@ -70,16 +70,30 @@ CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
 
 namespace CVC4 {
 
-FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
+FloatingPointSize::FloatingPointSize(unsigned exp_size, unsigned sig_size)
+    : d_exp_size(exp_size), d_sig_size(sig_size)
 {
-  PrettyCheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
-  PrettyCheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
+  PrettyCheckArgument(validExponentSize(exp_size),
+                      exp_size,
+                      "Invalid exponent size : %d",
+                      exp_size);
+  PrettyCheckArgument(validSignificandSize(sig_size),
+                      sig_size,
+                      "Invalid significand size : %d",
+                      sig_size);
 }
 
-FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
+FloatingPointSize::FloatingPointSize(const FloatingPointSize& old)
+    : d_exp_size(old.d_exp_size), d_sig_size(old.d_sig_size)
 {
-  PrettyCheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
-  PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
+  PrettyCheckArgument(validExponentSize(d_exp_size),
+                      d_exp_size,
+                      "Invalid exponent size : %d",
+                      d_exp_size);
+  PrettyCheckArgument(validSignificandSize(d_sig_size),
+                      d_sig_size,
+                      "Invalid significand size : %d",
+                      d_sig_size);
 }
 
 namespace symfpuLiteral {
@@ -88,36 +102,40 @@ namespace symfpuLiteral {
 typedef traits t;
 
 template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(const bwt &w)
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(
+    const CVC4BitWidth& w)
 {
   return wrappedBitVector<isSigned>(w, 1);
 }
 
 template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(const bwt &w)
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(
+    const CVC4BitWidth& w)
 {
   return wrappedBitVector<isSigned>(w, 0);
 }
 
 template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(const bwt &w)
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(
+    const CVC4BitWidth& w)
 {
   return ~wrappedBitVector<isSigned>::zero(w);
 }
 
 template <bool isSigned>
-prop wrappedBitVector<isSigned>::isAllOnes() const
+CVC4Prop wrappedBitVector<isSigned>::isAllOnes() const
 {
   return (*this == wrappedBitVector<isSigned>::allOnes(this->getWidth()));
 }
 template <bool isSigned>
-prop wrappedBitVector<isSigned>::isAllZeros() const
+CVC4Prop wrappedBitVector<isSigned>::isAllZeros() const
 {
   return (*this == wrappedBitVector<isSigned>::zero(this->getWidth()));
 }
 
 template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(const bwt &w)
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(
+    const CVC4BitWidth& w)
 {
   if (isSigned)
   {
@@ -131,7 +149,8 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(const bwt &w)
 }
 
 template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(const bwt &w)
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(
+    const CVC4BitWidth& w)
 {
   if (isSigned)
   {
@@ -292,58 +311,64 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
 /*** Comparisons ***/
 
 template <bool isSigned>
-prop wrappedBitVector<isSigned>::operator==(
-    const wrappedBitVector<isSigned> &op) const
+CVC4Prop wrappedBitVector<isSigned>::operator==(
+    const wrappedBitVector<isSigned>& op) const
 {
   return this->BitVector::operator==(op);
 }
 
 template <>
-prop wrappedBitVector<true>::operator<=(const wrappedBitVector<true> &op) const
+CVC4Prop wrappedBitVector<true>::operator<=(
+    const wrappedBitVector<true>& op) const
 {
   return this->signedLessThanEq(op);
 }
 
 template <>
-prop wrappedBitVector<true>::operator>=(const wrappedBitVector<true> &op) const
+CVC4Prop wrappedBitVector<true>::operator>=(
+    const wrappedBitVector<true>& op) const
 {
   return !(this->signedLessThan(op));
 }
 
 template <>
-prop wrappedBitVector<true>::operator<(const wrappedBitVector<true> &op) const
+CVC4Prop wrappedBitVector<true>::operator<(
+    const wrappedBitVector<true>& op) const
 {
   return this->signedLessThan(op);
 }
 
 template <>
-prop wrappedBitVector<true>::operator>(const wrappedBitVector<true> &op) const
+CVC4Prop wrappedBitVector<true>::operator>(
+    const wrappedBitVector<true>& op) const
 {
   return !(this->signedLessThanEq(op));
 }
 
 template <>
-prop wrappedBitVector<false>::operator<=(
-    const wrappedBitVector<false> &op) const
+CVC4Prop wrappedBitVector<false>::operator<=(
+    const wrappedBitVector<false>& op) const
 {
   return this->unsignedLessThanEq(op);
 }
 
 template <>
-prop wrappedBitVector<false>::operator>=(
-    const wrappedBitVector<false> &op) const
+CVC4Prop wrappedBitVector<false>::operator>=(
+    const wrappedBitVector<false>& op) const
 {
   return !(this->unsignedLessThan(op));
 }
 
 template <>
-prop wrappedBitVector<false>::operator<(const wrappedBitVector<false> &op) const
+CVC4Prop wrappedBitVector<false>::operator<(
+    const wrappedBitVector<false>& op) const
 {
   return this->unsignedLessThan(op);
 }
 
 template <>
-prop wrappedBitVector<false>::operator>(const wrappedBitVector<false> &op) const
+CVC4Prop wrappedBitVector<false>::operator>(
+    const wrappedBitVector<false>& op) const
 {
   return !(this->unsignedLessThanEq(op));
 }
@@ -366,7 +391,7 @@ wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
-    bwt extension) const
+    CVC4BitWidth extension) const
 {
   if (isSigned)
   {
@@ -380,7 +405,7 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
-    bwt reduction) const
+    CVC4BitWidth reduction) const
 {
   PRECONDITION(this->getWidth() > reduction);
 
@@ -388,9 +413,10 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
 }
 
 template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize(bwt newSize) const
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize(
+    CVC4BitWidth newSize) const
 {
-  bwt width = this->getWidth();
+  CVC4BitWidth width = this->getWidth();
 
   if (newSize > width)
   {
@@ -423,8 +449,8 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
 
 // Inclusive of end points, thus if the same, extracts just one bit
 template <bool isSigned>
-wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(bwt upper,
-                                                               bwt lower) const
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(
+    CVC4BitWidth upper, CVC4BitWidth lower) const
 {
   PRECONDITION(upper >= lower);
   return this->BitVector::extract(upper, lower);
@@ -434,25 +460,25 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(bwt upper,
 template class wrappedBitVector<true>;
 template class wrappedBitVector<false>;
 
-rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; };
-rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; };
-rm traits::RTP(void) { return ::CVC4::roundTowardPositive; };
-rm traits::RTN(void) { return ::CVC4::roundTowardNegative; };
-rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
+traits::rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; };
+traits::rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; };
+traits::rm traits::RTP(void) { return ::CVC4::roundTowardPositive; };
+traits::rm traits::RTN(void) { return ::CVC4::roundTowardNegative; };
+traits::rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
 // This is a literal back-end so props are actually bools
 // so these can be handled in the same way as the internal assertions above
 
-void traits::precondition(const prop &p)
+void traits::precondition(const traits::prop& p)
 {
   Assert(p);
   return;
 }
-void traits::postcondition(const prop &p)
+void traits::postcondition(const traits::prop& p)
 {
   Assert(p);
   return;
 }
-void traits::invariant(const prop &p)
+void traits::invariant(const traits::prop& p)
 {
   Assert(p);
   return;
@@ -466,25 +492,26 @@ void FloatingPointLiteral::unfinished(void) const
 }
 #endif
 
-FloatingPoint::FloatingPoint(unsigned e, unsigned s, const BitVector &bv)
-    :
+FloatingPoint::FloatingPoint(unsigned d_exp_size,
+                             unsigned d_sig_size,
+                             const BitVector& bv)
+    : d_fp_size(d_exp_size, d_sig_size),
 #ifdef CVC4_USE_SYMFPU
-      fpl(symfpu::unpack<symfpuLiteral::traits>(symfpuLiteral::fpt(e, s), bv)),
+      d_fpl(symfpu::unpack<symfpuLiteral::traits>(
+          symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv))
 #else
-      fpl(e, s, 0.0),
+      d_fpl(d_exp_size, d_sig_size, 0.0)
 #endif
-      t(e, s)
 {
 }
 
 FloatingPoint::FloatingPoint(const FloatingPointSize& size, const BitVector& bv)
-    :
+    : d_fp_size(size),
 #ifdef CVC4_USE_SYMFPU
-      fpl(symfpu::unpack<symfpuLiteral::traits>(size, bv)),
+      d_fpl(symfpu::unpack<symfpuLiteral::traits>(size, bv))
 #else
-      fpl(size.exponent(), size.significand(), 0.0),
+      d_fpl(size.exponentWidth(), size.significandWidth(), 0.0)
 #endif
-      t(size)
 {
 }
 
@@ -499,17 +526,17 @@ static FloatingPointLiteral constructorHelperBitVector(
   {
     return FloatingPointLiteral(
         symfpu::convertSBVToFloat<symfpuLiteral::traits>(
-            symfpuLiteral::fpt(size),
-            symfpuLiteral::rm(rm),
-            symfpuLiteral::sbv(bv)));
+            symfpuLiteral::CVC4FPSize(size),
+            symfpuLiteral::CVC4RM(rm),
+            symfpuLiteral::CVC4SignedBitVector(bv)));
   }
   else
   {
     return FloatingPointLiteral(
         symfpu::convertUBVToFloat<symfpuLiteral::traits>(
-            symfpuLiteral::fpt(size),
-            symfpuLiteral::rm(rm),
-            symfpuLiteral::ubv(bv)));
+            symfpuLiteral::CVC4FPSize(size),
+            symfpuLiteral::CVC4RM(rm),
+            symfpuLiteral::CVC4UnsignedBitVector(bv)));
   }
 #else
   return FloatingPointLiteral(2, 2, 0.0);
@@ -521,7 +548,7 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size,
                              const RoundingMode& rm,
                              const BitVector& bv,
                              bool signedBV)
-    : fpl(constructorHelperBitVector(size, rm, bv, signedBV)), t(size)
+    : d_fp_size(size), d_fpl(constructorHelperBitVector(size, rm, bv, signedBV))
 {
 }
 
@@ -643,7 +670,7 @@ static FloatingPointLiteral constructorHelperRational(
 FloatingPoint::FloatingPoint(const FloatingPointSize& size,
                              const RoundingMode& rm,
                              const Rational& r)
-    : fpl(constructorHelperRational(size, rm, r)), t(size)
+    : d_fp_size(size), d_fpl(constructorHelperRational(size, rm, r))
 {
 }
 
@@ -714,265 +741,327 @@ FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size,
   return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
 }
 
-  /* Operations implemented using symfpu */
-  FloatingPoint FloatingPoint::absolute (void) const {
+/* Operations implemented using symfpu */
+FloatingPoint FloatingPoint::absolute(void) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return FloatingPoint(t, symfpu::absolute<symfpuLiteral::traits>(t, fpl));
+  return FloatingPoint(
+      d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_fpl));
 #else
-    return *this;
+  return *this;
 #endif
-  }
-  
-  FloatingPoint FloatingPoint::negate (void) const {
+}
+
+FloatingPoint FloatingPoint::negate(void) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return FloatingPoint(t, symfpu::negate<symfpuLiteral::traits>(t, fpl));
+  return FloatingPoint(d_fp_size,
+                       symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_fpl));
 #else
-    return *this;
+  return *this;
 #endif
-  }
-  
-  FloatingPoint FloatingPoint::plus (const RoundingMode &rm, const FloatingPoint &arg) const {
+}
+
+FloatingPoint FloatingPoint::plus(const RoundingMode& rm,
+                                  const FloatingPoint& arg) const
+{
 #ifdef CVC4_USE_SYMFPU
-    Assert(this->t == arg.t);
-    return FloatingPoint(
-        t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, true));
+  Assert(this->d_fp_size == arg.d_fp_size);
+  return FloatingPoint(d_fp_size,
+                       symfpu::add<symfpuLiteral::traits>(
+                           d_fp_size, rm, d_fpl, arg.d_fpl, true));
 #else
-    return *this;
+  return *this;
 #endif
-  }
+}
 
-  FloatingPoint FloatingPoint::sub (const RoundingMode &rm, const FloatingPoint &arg) const {
+FloatingPoint FloatingPoint::sub(const RoundingMode& rm,
+                                 const FloatingPoint& arg) const
+{
 #ifdef CVC4_USE_SYMFPU
-    Assert(this->t == arg.t);
-    return FloatingPoint(
-        t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, false));
+  Assert(this->d_fp_size == arg.d_fp_size);
+  return FloatingPoint(d_fp_size,
+                       symfpu::add<symfpuLiteral::traits>(
+                           d_fp_size, rm, d_fpl, arg.d_fpl, false));
 #else
-    return *this;
+  return *this;
 #endif
-  }
+}
 
-  FloatingPoint FloatingPoint::mult (const RoundingMode &rm, const FloatingPoint &arg) const {
+FloatingPoint FloatingPoint::mult(const RoundingMode& rm,
+                                  const FloatingPoint& arg) const
+{
 #ifdef CVC4_USE_SYMFPU
-    Assert(this->t == arg.t);
-    return FloatingPoint(
-        t, symfpu::multiply<symfpuLiteral::traits>(t, rm, fpl, arg.fpl));
+  Assert(this->d_fp_size == arg.d_fp_size);
+  return FloatingPoint(
+      d_fp_size,
+      symfpu::multiply<symfpuLiteral::traits>(d_fp_size, rm, d_fpl, arg.d_fpl));
 #else
-    return *this;
+  return *this;
 #endif
-  }
+}
 
-  FloatingPoint FloatingPoint::fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const {
+FloatingPoint FloatingPoint::fma(const RoundingMode& rm,
+                                 const FloatingPoint& arg1,
+                                 const FloatingPoint& arg2) const
+{
 #ifdef CVC4_USE_SYMFPU
-    Assert(this->t == arg1.t);
-    Assert(this->t == arg2.t);
-    return FloatingPoint(
-        t, symfpu::fma<symfpuLiteral::traits>(t, rm, fpl, arg1.fpl, arg2.fpl));
+  Assert(this->d_fp_size == arg1.d_fp_size);
+  Assert(this->d_fp_size == arg2.d_fp_size);
+  return FloatingPoint(d_fp_size,
+                       symfpu::fma<symfpuLiteral::traits>(
+                           d_fp_size, rm, d_fpl, arg1.d_fpl, arg2.d_fpl));
 #else
-    return *this;
+  return *this;
 #endif
-  }
+}
 
-  FloatingPoint FloatingPoint::div (const RoundingMode &rm, const FloatingPoint &arg) const {
+FloatingPoint FloatingPoint::div(const RoundingMode& rm,
+                                 const FloatingPoint& arg) const
+{
 #ifdef CVC4_USE_SYMFPU
-    Assert(this->t == arg.t);
-    return FloatingPoint(
-        t, symfpu::divide<symfpuLiteral::traits>(t, rm, fpl, arg.fpl));
+  Assert(this->d_fp_size == arg.d_fp_size);
+  return FloatingPoint(
+      d_fp_size,
+      symfpu::divide<symfpuLiteral::traits>(d_fp_size, rm, d_fpl, arg.d_fpl));
 #else
-    return *this;
+  return *this;
 #endif
-  }
+}
 
-  FloatingPoint FloatingPoint::sqrt (const RoundingMode &rm) const {
+FloatingPoint FloatingPoint::sqrt(const RoundingMode& rm) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return FloatingPoint(t, symfpu::sqrt<symfpuLiteral::traits>(t, rm, fpl));
+  return FloatingPoint(
+      d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_fpl));
 #else
-    return *this;
+  return *this;
 #endif
-  }
+}
 
-  FloatingPoint FloatingPoint::rti (const RoundingMode &rm) const {
+FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return FloatingPoint(
-        t, symfpu::roundToIntegral<symfpuLiteral::traits>(t, rm, fpl));
+  return FloatingPoint(
+      d_fp_size,
+      symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_fpl));
 #else
-    return *this;
+  return *this;
 #endif
-  }
+}
 
-  FloatingPoint FloatingPoint::rem (const FloatingPoint &arg) const {
+FloatingPoint FloatingPoint::rem(const FloatingPoint& arg) const
+{
 #ifdef CVC4_USE_SYMFPU
-    Assert(this->t == arg.t);
-    return FloatingPoint(
-        t, symfpu::remainder<symfpuLiteral::traits>(t, fpl, arg.fpl));
+  Assert(this->d_fp_size == arg.d_fp_size);
+  return FloatingPoint(
+      d_fp_size,
+      symfpu::remainder<symfpuLiteral::traits>(d_fp_size, d_fpl, arg.d_fpl));
 #else
-    return *this;
+  return *this;
 #endif
-  }
+}
 
-  FloatingPoint FloatingPoint::maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
+FloatingPoint FloatingPoint::maxTotal(const FloatingPoint& arg,
+                                      bool zeroCaseLeft) const
+{
 #ifdef CVC4_USE_SYMFPU
-    Assert(this->t == arg.t);
-    return FloatingPoint(
-        t, symfpu::max<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft));
+  Assert(this->d_fp_size == arg.d_fp_size);
+  return FloatingPoint(d_fp_size,
+                       symfpu::max<symfpuLiteral::traits>(
+                           d_fp_size, d_fpl, arg.d_fpl, zeroCaseLeft));
 #else
-    return *this;
+  return *this;
 #endif
-  }
-  
-  FloatingPoint FloatingPoint::minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
+}
+
+FloatingPoint FloatingPoint::minTotal(const FloatingPoint& arg,
+                                      bool zeroCaseLeft) const
+{
 #ifdef CVC4_USE_SYMFPU
-    Assert(this->t == arg.t);
-    return FloatingPoint(
-        t, symfpu::min<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft));
+  Assert(this->d_fp_size == arg.d_fp_size);
+  return FloatingPoint(d_fp_size,
+                       symfpu::min<symfpuLiteral::traits>(
+                           d_fp_size, d_fpl, arg.d_fpl, zeroCaseLeft));
 #else
-    return *this;
+  return *this;
 #endif
-  }
+}
 
-  FloatingPoint::PartialFloatingPoint FloatingPoint::max (const FloatingPoint &arg) const {
-    FloatingPoint tmp(maxTotal(arg, true));
-    return PartialFloatingPoint(tmp, tmp == maxTotal(arg, false));
-  }
+FloatingPoint::PartialFloatingPoint FloatingPoint::max(
+    const FloatingPoint& arg) const
+{
+  FloatingPoint tmp(maxTotal(arg, true));
+  return PartialFloatingPoint(tmp, tmp == maxTotal(arg, false));
+}
 
-  FloatingPoint::PartialFloatingPoint FloatingPoint::min (const FloatingPoint &arg) const {
-    FloatingPoint tmp(minTotal(arg, true));
-    return PartialFloatingPoint(tmp, tmp == minTotal(arg, false));
-  }
+FloatingPoint::PartialFloatingPoint FloatingPoint::min(
+    const FloatingPoint& arg) const
+{
+  FloatingPoint tmp(minTotal(arg, true));
+  return PartialFloatingPoint(tmp, tmp == minTotal(arg, false));
+}
 
-  bool FloatingPoint::operator ==(const FloatingPoint& fp) const {
+bool FloatingPoint::operator==(const FloatingPoint& fp) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return ((t == fp.t)
-            && symfpu::smtlibEqual<symfpuLiteral::traits>(t, fpl, fp.fpl));
+  return ((d_fp_size == fp.d_fp_size)
+          && symfpu::smtlibEqual<symfpuLiteral::traits>(
+              d_fp_size, d_fpl, fp.d_fpl));
 #else
-    return ( (t == fp.t) );
+  return ((d_fp_size == fp.d_fp_size));
 #endif
-  }
+}
 
-  bool FloatingPoint::operator <= (const FloatingPoint &arg) const {
+bool FloatingPoint::operator<=(const FloatingPoint& arg) const
+{
 #ifdef CVC4_USE_SYMFPU
-    Assert(this->t == arg.t);
-    return symfpu::lessThanOrEqual<symfpuLiteral::traits>(t, fpl, arg.fpl);
+  Assert(this->d_fp_size == arg.d_fp_size);
+  return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
+      d_fp_size, d_fpl, arg.d_fpl);
 #else
-    return false;
+  return false;
 #endif
-  }
+}
 
-  bool FloatingPoint::operator < (const FloatingPoint &arg) const {
+bool FloatingPoint::operator<(const FloatingPoint& arg) const
+{
 #ifdef CVC4_USE_SYMFPU
-    Assert(this->t == arg.t);
-    return symfpu::lessThan<symfpuLiteral::traits>(t, fpl, arg.fpl);
+  Assert(this->d_fp_size == arg.d_fp_size);
+  return symfpu::lessThan<symfpuLiteral::traits>(d_fp_size, d_fpl, arg.d_fpl);
 #else
-    return false;
+  return false;
 #endif
-  }
+}
 
-  bool FloatingPoint::isNormal (void) const {
+bool FloatingPoint::isNormal(void) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return symfpu::isNormal<symfpuLiteral::traits>(t, fpl);
+  return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_fpl);
 #else
-    return false;
+  return false;
 #endif
-  }
+}
 
-  bool FloatingPoint::isSubnormal (void) const {
+bool FloatingPoint::isSubnormal(void) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return symfpu::isSubnormal<symfpuLiteral::traits>(t, fpl);
+  return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_fpl);
 #else
-    return false;
+  return false;
 #endif
-  }
+}
 
-  bool FloatingPoint::isZero (void) const {
+bool FloatingPoint::isZero(void) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return symfpu::isZero<symfpuLiteral::traits>(t, fpl);
+  return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_fpl);
 #else
-    return false;
+  return false;
 #endif
-  }
+}
 
-  bool FloatingPoint::isInfinite (void) const {
+bool FloatingPoint::isInfinite(void) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return symfpu::isInfinite<symfpuLiteral::traits>(t, fpl);
+  return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_fpl);
 #else
-    return false;
+  return false;
 #endif
-  }
+}
 
-  bool FloatingPoint::isNaN (void) const {
+bool FloatingPoint::isNaN(void) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return symfpu::isNaN<symfpuLiteral::traits>(t, fpl);
+  return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_fpl);
 #else
-    return false;
+  return false;
 #endif
-  }
+}
 
-  bool FloatingPoint::isNegative (void) const {
+bool FloatingPoint::isNegative(void) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return symfpu::isNegative<symfpuLiteral::traits>(t, fpl);
+  return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_fpl);
 #else
-    return false;
+  return false;
 #endif
-  }
+}
 
-  bool FloatingPoint::isPositive (void) const {
+bool FloatingPoint::isPositive(void) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return symfpu::isPositive<symfpuLiteral::traits>(t, fpl);
+  return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_fpl);
 #else
-    return false;
+  return false;
 #endif
-  }
+}
 
-  FloatingPoint FloatingPoint::convert (const FloatingPointSize &target, const RoundingMode &rm) const {
+FloatingPoint FloatingPoint::convert(const FloatingPointSize& target,
+                                     const RoundingMode& rm) const
+{
 #ifdef CVC4_USE_SYMFPU
-    return FloatingPoint(
-        target,
-        symfpu::convertFloatToFloat<symfpuLiteral::traits>(t, target, rm, fpl));
+  return FloatingPoint(target,
+                       symfpu::convertFloatToFloat<symfpuLiteral::traits>(
+                           d_fp_size, target, rm, d_fpl));
 #else
-    return *this;
+  return *this;
 #endif
-  }
-  
-  BitVector FloatingPoint::convertToBVTotal (BitVectorSize width, const RoundingMode &rm, bool signedBV, BitVector undefinedCase) const {
+}
+
+BitVector FloatingPoint::convertToBVTotal(BitVectorSize width,
+                                          const RoundingMode& rm,
+                                          bool signedBV,
+                                          BitVector undefinedCase) const
+{
 #ifdef CVC4_USE_SYMFPU
     if (signedBV)
       return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
-          t, rm, fpl, width, undefinedCase);
+          d_fp_size, rm, d_fpl, width, undefinedCase);
     else
       return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
-          t, rm, fpl, width, undefinedCase);
+          d_fp_size, rm, d_fpl, width, undefinedCase);
 #else
-    return undefinedCase;
+  return undefinedCase;
 #endif
-  }
+}
 
-  Rational FloatingPoint::convertToRationalTotal (Rational undefinedCase) const {
-    PartialRational p(convertToRational());
+Rational FloatingPoint::convertToRationalTotal(Rational undefinedCase) const
+{
+  PartialRational p(convertToRational());
 
-    return p.second ? p.first : undefinedCase;
-  }
+  return p.second ? p.first : undefinedCase;
+}
 
-  FloatingPoint::PartialBitVector FloatingPoint::convertToBV (BitVectorSize width, const RoundingMode &rm, bool signedBV) const {
-    BitVector tmp(convertToBVTotal (width, rm, signedBV, BitVector(width, 0U)));
-    BitVector confirm(convertToBVTotal (width, rm, signedBV, BitVector(width, 1U)));
+FloatingPoint::PartialBitVector FloatingPoint::convertToBV(
+    BitVectorSize width, const RoundingMode& rm, bool signedBV) const
+{
+  BitVector tmp(convertToBVTotal(width, rm, signedBV, BitVector(width, 0U)));
+  BitVector confirm(
+      convertToBVTotal(width, rm, signedBV, BitVector(width, 1U)));
 
-    return PartialBitVector(tmp, tmp == confirm);
-  }
+  return PartialBitVector(tmp, tmp == confirm);
+}
 
-  FloatingPoint::PartialRational FloatingPoint::convertToRational (void) const {
-    if (this->isNaN() || this->isInfinite()) {
-      return PartialRational(Rational(0U, 1U), false);
-    }
-    if (this->isZero()) {
-      return PartialRational(Rational(0U, 1U), true);
-      
-    } else {
+FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const
+{
+  if (this->isNaN() || this->isInfinite())
+  {
+    return PartialRational(Rational(0U, 1U), false);
+  }
+  if (this->isZero())
+  {
+    return PartialRational(Rational(0U, 1U), true);
+  }
+  else
+  {
 #ifdef CVC4_USE_SYMFPU
-      Integer sign((this->fpl.getSign()) ? -1 : 1);
-      Integer exp(
-          this->fpl.getExponent().toSignedInteger()
-          - (Integer(t.significand()
-                     - 1)));  // -1 as forcibly normalised into the [1,2) range
-      Integer significand(this->fpl.getSignificand().toInteger());
+    Integer sign((this->d_fpl.getSign()) ? -1 : 1);
+    Integer exp(
+        this->d_fpl.getExponent().toSignedInteger()
+        - (Integer(d_fp_size.significandWidth()
+                   - 1)));  // -1 as forcibly normalised into the [1,2) range
+    Integer significand(this->d_fpl.getSignificand().toInteger());
 #else
       Integer sign(0);
       Integer exp(0);
@@ -1003,19 +1092,21 @@ FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size,
 	Rational r(signedSignificand, q);
 	return PartialRational(r, true);
       }
-    }
+  }
 
     Unreachable() << "Convert float literal to real broken.";
-  }
+}
 
-  BitVector FloatingPoint::pack (void) const {
+BitVector FloatingPoint::pack(void) const
+{
 #ifdef CVC4_USE_SYMFPU
-    BitVector bv(symfpu::pack<symfpuLiteral::traits>(this->t, this->fpl));
+  BitVector bv(
+      symfpu::pack<symfpuLiteral::traits>(this->d_fp_size, this->d_fpl));
 #else
-    BitVector bv(4u,0u);
+  BitVector bv(4u, 0u);
 #endif
-    return bv;
-  }
+  return bv;
+}
 
 std::string FloatingPoint::toString(bool printAsIndexed) const
 {
@@ -1023,9 +1114,9 @@ std::string FloatingPoint::toString(bool printAsIndexed) const
   // retrive BV value
   BitVector bv(pack());
   unsigned largestSignificandBit =
-      t.significand() - 2;  // -1 for -inclusive, -1 for hidden
+      d_fp_size.significandWidth() - 2;  // -1 for -inclusive, -1 for hidden
   unsigned largestExponentBit =
-      (t.exponent() - 1) + (largestSignificandBit + 1);
+      (d_fp_size.exponentWidth() - 1) + (largestSignificandBit + 1);
   BitVector v[3];
   v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1);
   v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1);
@@ -1055,4 +1146,21 @@ std::string FloatingPoint::toString(bool printAsIndexed) const
   return str;
 }
 
+std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp)
+{
+  // print in binary notation
+  return os << fp.toString();
+}
+
+std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps)
+{
+  return os << "(_ FloatingPoint " << fps.exponentWidth() << " "
+            << fps.significandWidth() << ")";
+}
+
+std::ostream& operator<<(std::ostream& os, const FloatingPointConvertSort& fpcs)
+{
+  return os << "(_ to_fp " << fpcs.d_fp_size.exponentWidth() << " "
+            << fpcs.d_fp_size.significandWidth() << ")";
+}
 }/* CVC4 namespace */
diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in
index 9e78c20c0..0d62e9c3e 100644
--- a/src/util/floatingpoint.h.in
+++ b/src/util/floatingpoint.h.in
@@ -20,587 +20,846 @@
 #ifndef CVC4__FLOATINGPOINT_H
 #define CVC4__FLOATINGPOINT_H
 
+#include <fenv.h>
+
 #include "util/bitvector.h"
 #include "util/rational.h"
 
-#include <fenv.h>
-
+// clang-format off
 #if @CVC4_USE_SYMFPU@
+// clang-format on
 #include <symfpu/core/unpackedFloat.h>
 #endif /* @CVC4_USE_SYMFPU@ */
 
 namespace CVC4 {
-  // Inline these!
-  inline bool CVC4_PUBLIC validExponentSize (unsigned e) { return e >= 2; }
-  inline bool CVC4_PUBLIC validSignificandSize (unsigned s) { return s >= 2; }
-
-  /**
-   * Floating point sorts are parameterised by two non-zero constants
-   * giving the width (in bits) of the exponent and significand
-   * (including the hidden bit).
-   */
-  class CVC4_PUBLIC FloatingPointSize {
-    /*
-      Class invariants:
-      * VALIDEXPONENTSIZE(e)
-      * VALIDSIGNIFCANDSIZE(s)
-     */
-
-  private :
-    unsigned e;
-    unsigned s;
-
-  public :
-    FloatingPointSize (unsigned _e, unsigned _s);
-    FloatingPointSize (const FloatingPointSize &old);
-
-    inline unsigned exponent (void) const {
-      return this->e;
-    }
-
-    inline unsigned significand (void) const {
-      return this->s;
-    }
-
-    bool operator ==(const FloatingPointSize& fps) const {
-      return (e == fps.e) && (s == fps.s);
-    }
-
-    // Implement the interface that symfpu uses for floating-point formats.
-    inline unsigned exponentWidth(void) const { return this->exponent(); }
-    inline unsigned significandWidth(void) const { return this->significand(); }
-    inline unsigned packedWidth(void) const
-    {
-      return this->exponentWidth() + this->significandWidth();
-    }
-    inline unsigned packedExponentWidth(void) const
-    {
-      return this->exponentWidth();
-    }
-    inline unsigned packedSignificandWidth(void) const
-    {
-      return this->significandWidth() - 1;
-    }
-
-  }; /* class FloatingPointSize */
-
-  struct CVC4_PUBLIC FloatingPointSizeHashFunction {
-    static inline size_t ROLL(size_t X, size_t N) {
-      return (((X) << (N)) | ((X) >> (8*sizeof((X)) - (N)) ));
-    }
-
-    inline size_t operator() (const FloatingPointSize& t) const {
-      return size_t(ROLL(t.exponent(), 4*sizeof(unsigned)) |
-		    t.significand());
-    }
-  }; /* struct FloatingPointSizeHashFunction */
+// Inline these!
+inline bool CVC4_PUBLIC validExponentSize(unsigned e) { return e >= 2; }
+inline bool CVC4_PUBLIC validSignificandSize(unsigned s) { return s >= 2; }
+
+/* -------------------------------------------------------------------------- */
+
+/**
+ * Floating point sorts are parameterised by two constants > 1 giving the
+ * width (in bits) of the exponent and significand (including the hidden bit).
+ * So, IEEE-754 single precision, a.k.a. float, is described as 8 24.
+ */
+class CVC4_PUBLIC FloatingPointSize
+{
+ public:
+  /** Constructors. */
+  FloatingPointSize(unsigned exp_size, unsigned sig_size);
+  FloatingPointSize(const FloatingPointSize& old);
+
+  /** Operator overload for equality comparison. */
+  bool operator==(const FloatingPointSize& fps) const
+  {
+    return (d_exp_size == fps.d_exp_size) && (d_sig_size == fps.d_sig_size);
+  }
 
+  /** Implement the interface that symfpu uses for floating-point formats. */
 
+  /** Get the exponent bit-width of this floating-point format. */
+  inline unsigned exponentWidth(void) const { return this->d_exp_size; }
+  /** Get the significand bit-width of this floating-point format. */
+  inline unsigned significandWidth(void) const { return this->d_sig_size; }
   /**
-   * A concrete instance of the rounding mode sort
+   * Get the bit-width of the packed representation of this floating-point
+   * format (= exponent + significand bit-width, convenience wrapper).
    */
-  enum CVC4_PUBLIC RoundingMode {
-    roundNearestTiesToEven = FE_TONEAREST,
-    roundTowardPositive = FE_UPWARD,
-    roundTowardNegative = FE_DOWNWARD,
-    roundTowardZero = FE_TOWARDZERO,
-    // Initializes this to the diagonalization of the 4 other values.
-    roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) |
-                              ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8))
-  }; /* enum RoundingMode */
-
-  struct CVC4_PUBLIC RoundingModeHashFunction {
-    inline size_t operator() (const RoundingMode& rm) const {
-      return size_t(rm);
-    }
-  }; /* struct RoundingModeHashFunction */
-
+  inline unsigned packedWidth(void) const
+  {
+    return this->exponentWidth() + this->significandWidth();
+  }
   /**
-   * This is a symfpu literal "back-end".  It allows the library to be used as
-   * an arbitrary precision floating-point implementation.  This is effectively
-   * the glue between symfpu's notion of "signed bit-vector" and CVC4's
-   * BitVector.
+   * Get the exponent bit-width of the packed representation of this
+   * floating-point format (= exponent bit-width).
    */
-  namespace symfpuLiteral {
-  // Forward declaration of wrapper so that traits can be defined early and so
-  // used in the implementation of wrappedBitVector.
-  template <bool T>
-  class wrappedBitVector;
-
-  // This is the template parameter for symfpu's templates.
-  class traits
+  inline unsigned packedExponentWidth(void) const
   {
-   public:
-    // The six key types that symfpu uses.
-    using bwt = uint32_t;
-    using prop = bool;
-    using rm = ::CVC4::RoundingMode;
-    using fpt = ::CVC4::FloatingPointSize;
-    using sbv = wrappedBitVector<true>;
-    using ubv = wrappedBitVector<false>;
-
-    // Give concrete instances of each rounding mode, mainly for comparisons.
-    static rm RNE(void);
-    static rm RNA(void);
-    static rm RTP(void);
-    static rm RTN(void);
-    static rm RTZ(void);
-
-    // The sympfu properties.
-    static void precondition(const prop &p);
-    static void postcondition(const prop &p);
-    static void invariant(const prop &p);
-  };
-
-  // Use the same type names as symfpu.
-  using bwt = traits::bwt;
-  using prop = traits::prop;
-  using rm = traits::rm;
-  using fpt = traits::fpt;
-  using ubv = traits::ubv;
-  using sbv = traits::sbv;
-
-  // Type function for mapping between types
-  template <bool T>
-  struct signedToLiteralType;
-
-  template <>
-  struct signedToLiteralType<true>
-  {
-    using literalType = int32_t;
-  };
-  template <>
-  struct signedToLiteralType<false>
+    return this->exponentWidth();
+  }
+  /**
+   * Get the significand bit-width of the packed representation of this
+   * floating-point format (= significand bit-width - 1).
+   */
+  inline unsigned packedSignificandWidth(void) const
   {
-    using literalType = uint32_t;
-  };
-
-  // This is an additional interface for CVC4::BitVector.
-  // The template parameter distinguishes signed and unsigned bit-vectors, a
-  // distinction symfpu uses.
-  template <bool isSigned>
-  class wrappedBitVector : public BitVector
+    return this->significandWidth() - 1;
+  }
+
+ private:
+  /** Exponent bit-width. */
+  unsigned d_exp_size;
+  /** Significand bit-width. */
+  unsigned d_sig_size;
+
+}; /* class FloatingPointSize */
+
+/**
+ * Hash function for floating point formats.
+ */
+struct CVC4_PUBLIC FloatingPointSizeHashFunction
+{
+  static inline size_t ROLL(size_t X, size_t N)
   {
-   protected:
-    using literalType = typename signedToLiteralType<isSigned>::literalType;
+    return (((X) << (N)) | ((X) >> (8 * sizeof((X)) - (N))));
+  }
 
-    friend wrappedBitVector<!isSigned>;  // To allow conversion between the
-                                         // types
+  inline size_t operator()(const FloatingPointSize& t) const
+  {
+    return size_t(ROLL(t.exponentWidth(), 4 * sizeof(unsigned))
+                  | t.significandWidth());
+  }
+}; /* struct FloatingPointSizeHashFunction */
+
+/* -------------------------------------------------------------------------- */
+
+/**
+ * A concrete instance of the rounding mode sort
+ */
+enum CVC4_PUBLIC RoundingMode
+{
+  roundNearestTiesToEven = FE_TONEAREST,
+  roundTowardPositive = FE_UPWARD,
+  roundTowardNegative = FE_DOWNWARD,
+  roundTowardZero = FE_TOWARDZERO,
+  // Initializes this to the diagonalization of the 4 other values.
+  roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2)
+                            | ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8))
+}; /* enum RoundingMode */
+
+/**
+ * Hash function for rounding mode values.
+ */
+struct CVC4_PUBLIC RoundingModeHashFunction
+{
+  inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); }
+}; /* struct RoundingModeHashFunction */
+
+/* -------------------------------------------------------------------------- */
+
+/**
+ * This is a symfpu literal "back-end".  It allows the library to be used as
+ * an arbitrary precision floating-point implementation.  This is effectively
+ * the glue between symfpu's notion of "signed bit-vector" and CVC4's
+ * BitVector.
+ */
+namespace symfpuLiteral {
+
+/**
+ * Forward declaration of wrapper so that traits can be defined early and so
+ * used in the implementation of wrappedBitVector.
+ */
+template <bool T>
+class wrappedBitVector;
+
+using CVC4BitWidth = uint32_t;
+using CVC4Prop = bool;
+using CVC4RM = ::CVC4::RoundingMode;
+using CVC4FPSize = ::CVC4::FloatingPointSize;
+using CVC4UnsignedBitVector = wrappedBitVector<false>;
+using CVC4SignedBitVector = wrappedBitVector<true>;
+
+/**
+ * This is the template parameter for symfpu's templates.
+ */
+class traits
+{
+ public:
+  /** The six key types that symfpu uses. */
+  using bwt = CVC4BitWidth;           // bit-width type
+  using prop = CVC4Prop;              // boolean type
+  using rm = CVC4RM;                  // rounding-mode type
+  using fpt = CVC4FPSize;             // floating-point format type
+  using ubv = CVC4UnsignedBitVector;  // unsigned bit-vector type
+  using sbv = CVC4SignedBitVector;    // signed bit-vector type
+
+  /** Give concrete instances of each rounding mode, mainly for comparisons. */
+  static rm RNE(void);
+  static rm RNA(void);
+  static rm RTP(void);
+  static rm RTN(void);
+  static rm RTZ(void);
+
+  /** The sympfu properties. */
+  static void precondition(const prop& p);
+  static void postcondition(const prop& p);
+  static void invariant(const prop& p);
+};
+
+/**
+ * Type function for mapping between types.
+ */
+template <bool T>
+struct signedToLiteralType;
+
+template <>
+struct signedToLiteralType<true>
+{
+  using literalType = int32_t;
+};
+template <>
+struct signedToLiteralType<false>
+{
+  using literalType = uint32_t;
+};
+
+/**
+ * This extends the interface for CVC4::BitVector for compatibility with symFPU.
+ * The template parameter distinguishes signed and unsigned bit-vectors, a
+ * distinction symfpu uses.
+ */
+template <bool isSigned>
+class wrappedBitVector : public BitVector
+{
+ protected:
+  using literalType = typename signedToLiteralType<isSigned>::literalType;
+  friend wrappedBitVector<!isSigned>;  // To allow conversion between types
+
+// clang-format off
 #if @CVC4_USE_SYMFPU@
-    friend ::symfpu::ite<prop, wrappedBitVector<isSigned> >;  // For ITE
+  // clang-format on
+  friend ::symfpu::ite<CVC4Prop, wrappedBitVector<isSigned> >;  // For ITE
 #endif /* @CVC4_USE_SYMFPU@ */
 
-   public:
-    wrappedBitVector(const bwt w, const unsigned v) : BitVector(w, v) {}
-    wrappedBitVector(const prop &p) : BitVector(1, p ? 1U : 0U) {}
-    wrappedBitVector(const wrappedBitVector<isSigned> &old) : BitVector(old) {}
-    wrappedBitVector(const BitVector &old) : BitVector(old) {}
-    bwt getWidth(void) const { return getSize(); }
-    /*** Constant creation and test ***/
-
-    static wrappedBitVector<isSigned> one(const bwt &w);
-    static wrappedBitVector<isSigned> zero(const bwt &w);
-    static wrappedBitVector<isSigned> allOnes(const bwt &w);
-
-    prop isAllOnes() const;
-    prop isAllZeros() const;
-
-    static wrappedBitVector<isSigned> maxValue(const bwt &w);
-    static wrappedBitVector<isSigned> minValue(const bwt &w);
-
-    /*** Operators ***/
-    wrappedBitVector<isSigned> operator<<(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> operator>>(
-        const wrappedBitVector<isSigned> &op) const;
-
-    /* Inherited but ...
-     * *sigh* if we use the inherited version then it will return a
-     * CVC4::BitVector which can be converted back to a
-     * wrappedBitVector<isSigned> but isn't done automatically when working
-     * out types for templates instantiation.  ITE is a particular
-     * problem as expressions and constants no longer derive the
-     * same type.  There aren't any good solutions in C++, we could
-     * use CRTP but Liana wouldn't appreciate that, so the following
-     * pointless wrapping functions are needed.
-     */
-    wrappedBitVector<isSigned> operator|(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> operator&(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> operator+(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> operator-(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> operator*(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> operator/(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> operator%(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> operator-(void) const;
-    wrappedBitVector<isSigned> operator~(void)const;
-
-    wrappedBitVector<isSigned> increment() const;
-    wrappedBitVector<isSigned> decrement() const;
-    wrappedBitVector<isSigned> signExtendRightShift(
-        const wrappedBitVector<isSigned> &op) const;
-
-    /*** Modular opertaions ***/
-    // No overflow checking so these are the same as other operations
-    wrappedBitVector<isSigned> modularLeftShift(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> modularRightShift(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> modularIncrement() const;
-    wrappedBitVector<isSigned> modularDecrement() const;
-    wrappedBitVector<isSigned> modularAdd(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> modularNegate() const;
-
-    /*** Comparisons ***/
-    // Inherited ... ish ...
-    prop operator==(const wrappedBitVector<isSigned> &op) const;
-    prop operator<=(const wrappedBitVector<isSigned> &op) const;
-    prop operator>=(const wrappedBitVector<isSigned> &op) const;
-    prop operator<(const wrappedBitVector<isSigned> &op) const;
-    prop operator>(const wrappedBitVector<isSigned> &op) const;
-
-    /*** Type conversion ***/
-    wrappedBitVector<true> toSigned(void) const;
-    wrappedBitVector<false> toUnsigned(void) const;
-
-    /*** Bit hacks ***/
-    wrappedBitVector<isSigned> extend(bwt extension) const;
-    wrappedBitVector<isSigned> contract(bwt reduction) const;
-    wrappedBitVector<isSigned> resize(bwt newSize) const;
-    wrappedBitVector<isSigned> matchWidth(
-        const wrappedBitVector<isSigned> &op) const;
-    wrappedBitVector<isSigned> append(
-        const wrappedBitVector<isSigned> &op) const;
-
-    // Inclusive of end points, thus if the same, extracts just one bit
-    wrappedBitVector<isSigned> extract(bwt upper, bwt lower) const;
-  };
-  }
+ public:
+  /** Constructors. */
+  wrappedBitVector(const CVC4BitWidth w, const unsigned v) : BitVector(w, v) {}
+  wrappedBitVector(const CVC4Prop& p) : BitVector(1, p ? 1U : 0U) {}
+  wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {}
+  wrappedBitVector(const BitVector& old) : BitVector(old) {}
+
+  /** Get the bit-width of this wrapped bit-vector. */
+  CVC4BitWidth getWidth(void) const { return getSize(); }
+
+  /** Create a zero value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> one(const CVC4BitWidth& w);
+  /** Create a one value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> zero(const CVC4BitWidth& w);
+  /** Create a ones value (all bits 1) of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> allOnes(const CVC4BitWidth& w);
+  /** Create a maximum signed/unsigned value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> maxValue(const CVC4BitWidth& w);
+  /** Create a minimum signed/unsigned value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> minValue(const CVC4BitWidth& w);
+
+  /** Return true if this a bit-vector representing a ones value. */
+  CVC4Prop isAllOnes() const;
+  /** Return true if this a bit-vector representing a zero value. */
+  CVC4Prop isAllZeros() const;
+
+  /** Left shift. */
+  wrappedBitVector<isSigned> operator<<(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Logical (unsigned) and arithmetic (signed) right shift. */
+  wrappedBitVector<isSigned> operator>>(
+      const wrappedBitVector<isSigned>& op) const;
+
+  /**
+   * Inherited but ...
+   * *sigh* if we use the inherited version then it will return a
+   * CVC4::BitVector which can be converted back to a
+   * wrappedBitVector<isSigned> but isn't done automatically when working
+   * out types for templates instantiation.  ITE is a particular
+   * problem as expressions and constants no longer derive the
+   * same type.  There aren't any good solutions in C++, we could
+   * use CRTP but Liana wouldn't appreciate that, so the following
+   * pointless wrapping functions are needed.
+   */
+
+  /** Bit-wise or. */
+  wrappedBitVector<isSigned> operator|(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-wise and. */
+  wrappedBitVector<isSigned> operator&(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector addition. */
+  wrappedBitVector<isSigned> operator+(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector subtraction. */
+  wrappedBitVector<isSigned> operator-(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector multiplication. */
+  wrappedBitVector<isSigned> operator*(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned division. */
+  wrappedBitVector<isSigned> operator/(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned remainder. */
+  wrappedBitVector<isSigned> operator%(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector negation. */
+  wrappedBitVector<isSigned> operator-(void) const;
+  /** Bit-wise not. */
+  wrappedBitVector<isSigned> operator~(void) const;
+
+  /** Bit-vector increment. */
+  wrappedBitVector<isSigned> increment() const;
+  /** Bit-vector decrement. */
+  wrappedBitVector<isSigned> decrement() const;
+  /**
+   * Bit-vector logical/arithmetic right shift where 'op' extended to the
+   * bit-width of this wrapped bit-vector.
+   */
+  wrappedBitVector<isSigned> signExtendRightShift(
+      const wrappedBitVector<isSigned>& op) const;
 
   /**
-   * A concrete floating point number
+   * Modular operations.
+   * Note: No overflow checking so these are the same as other operations.
    */
+  wrappedBitVector<isSigned> modularLeftShift(
+      const wrappedBitVector<isSigned>& op) const;
+  wrappedBitVector<isSigned> modularRightShift(
+      const wrappedBitVector<isSigned>& op) const;
+  wrappedBitVector<isSigned> modularIncrement() const;
+  wrappedBitVector<isSigned> modularDecrement() const;
+  wrappedBitVector<isSigned> modularAdd(
+      const wrappedBitVector<isSigned>& op) const;
+  wrappedBitVector<isSigned> modularNegate() const;
+
+  /** Bit-vector equality. */
+  CVC4Prop operator==(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned less or equal than. */
+  CVC4Prop operator<=(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector sign/unsigned greater or equal than. */
+  CVC4Prop operator>=(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned less than. */
+  CVC4Prop operator<(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector sign/unsigned greater or equal than. */
+  CVC4Prop operator>(const wrappedBitVector<isSigned>& op) const;
+
+  /** Convert this bit-vector to a signed bit-vector. */
+  wrappedBitVector<true> toSigned(void) const;
+  /** Convert this bit-vector to an unsigned bit-vector. */
+  wrappedBitVector<false> toUnsigned(void) const;
+
+  /** Bit-vector signed/unsigned (zero) extension. */
+  wrappedBitVector<isSigned> extend(CVC4BitWidth extension) const;
+  /**
+   * Create a "contracted" bit-vector by cutting off the 'reduction' number of
+   * most significant bits, i.e., by extracting the (bit-width - reduction)
+   * least significant bits.
+   */
+  wrappedBitVector<isSigned> contract(CVC4BitWidth reduction) const;
+  /**
+   * Create a "resized" bit-vector of given size bei either extending (if new
+   * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
+   */
+  wrappedBitVector<isSigned> resize(CVC4BitWidth newSize) const;
+  /**
+   * Create an extension of this bit-vector that matches the bit-width of the
+   * given bit-vector.
+   * Note: The size of the given bit-vector may not be larger than the size of
+   * this bit-vector.
+   */
+  wrappedBitVector<isSigned> matchWidth(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector concatenation. */
+  wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
+
+  /** Inclusive of end points, thus if the same, extracts just one bit. */
+  wrappedBitVector<isSigned> extract(CVC4BitWidth upper,
+                                     CVC4BitWidth lower) const;
+};
+}  // namespace symfpuLiteral
+
+/**
+ * A concrete floating point value.
+ */
+// clang-format off
 #if @CVC4_USE_SYMFPU@
-  using FloatingPointLiteral = ::symfpu::unpackedFloat<symfpuLiteral::traits>;
+// clang-format on
+using FloatingPointLiteral = ::symfpu::unpackedFloat<symfpuLiteral::traits>;
 #else
-  class CVC4_PUBLIC FloatingPointLiteral {
-  public :
-    // This intentional left unfinished as the choice of literal
-    // representation is solver specific.
-    void unfinished (void) const;
-
-    FloatingPointLiteral(unsigned, unsigned, double) { unfinished(); }
-    FloatingPointLiteral(unsigned, unsigned, const std::string &) { unfinished(); }
-    FloatingPointLiteral(const FloatingPointLiteral &) { unfinished(); }
-    bool operator == (const FloatingPointLiteral &op) const {
-      unfinished();
-      return false;
-    }
-
-    size_t hash (void) const {
-      unfinished();
-      return 23;
-    }
-  };
-#endif /* @CVC4_USE_SYMFPU@ */
+class CVC4_PUBLIC FloatingPointLiteral
+{
+ public:
+  // This intentional left unfinished as the choice of literal
+  // representation is solver specific.
+  void unfinished(void) const;
+
+  FloatingPointLiteral(unsigned, unsigned, double) { unfinished(); }
+  FloatingPointLiteral(unsigned, unsigned, const std::string&) { unfinished(); }
+  FloatingPointLiteral(const FloatingPointLiteral&) { unfinished(); }
+  bool operator==(const FloatingPointLiteral& op) const
+  {
+    unfinished();
+    return false;
+  }
 
-  class CVC4_PUBLIC FloatingPoint {
-  protected :
-    FloatingPointLiteral fpl;
-
-  public :
-    FloatingPointSize t;
-
-    /** Constructors. */
-    FloatingPoint(unsigned e, unsigned s, const BitVector& bv);
-    FloatingPoint(const FloatingPointSize& size, const BitVector& bv);
-
-    FloatingPoint(const FloatingPointSize& oldt,
-                  const FloatingPointLiteral& oldfpl)
-        : fpl(oldfpl), t(oldt)
-    {
-    }
-
-    FloatingPoint(const FloatingPoint& fp) : fpl(fp.fpl), t(fp.t) {}
-    FloatingPoint(const FloatingPointSize& size,
-                  const RoundingMode& rm,
-                  const BitVector& bv,
-                  bool signedBV);
-    FloatingPoint(const FloatingPointSize& size,
-                  const RoundingMode& rm,
-                  const Rational& r);
-
-    /**
-     * Create a FP NaN value of given size.
-     * t: The FP size (format).
-     */
-    static FloatingPoint makeNaN (const FloatingPointSize &size);
-    /**
-     * Create a FP infinity value of given size.
-     * t:    The FP size (format).
-     * sign: True for +oo, false otherwise.
-     */
-    static FloatingPoint makeInf(const FloatingPointSize& size, bool sign);
-    /**
-     * Create a FP zero value of given size.
-     * t:    The FP size (format).
-     * sign: True for +zero, false otherwise.
-     */
-    static FloatingPoint makeZero(const FloatingPointSize& size, bool sign);
-    /**
-     * Create the smallest subnormal FP value of given size.
-     * t:    The FP size (format).
-     * sign: True for positive sign, false otherwise.
-     */
-    static FloatingPoint makeMinSubnormal(const FloatingPointSize& size,
-                                          bool sign);
-    /**
-     * Create the largest subnormal FP value of given size.
-     * t:    The FP size (format).
-     * sign: True for positive sign, false otherwise.
-     */
-    static FloatingPoint makeMaxSubnormal(const FloatingPointSize& size,
-                                          bool sign);
-    /**
-     * Create the smallest normal FP value of given size.
-     * t:    The FP size (format).
-     * sign: True for positive sign, false otherwise.
-     */
-    static FloatingPoint makeMinNormal(const FloatingPointSize& size,
-                                       bool sign);
-    /**
-     * Create the largest normal FP value of given size.
-     * t:    The FP size (format).
-     * sign: True for positive sign, false otherwise.
-     */
-    static FloatingPoint makeMaxNormal(const FloatingPointSize& size,
-                                          bool sign);
-
-    const FloatingPointLiteral& getLiteral(void) const { return this->fpl; }
-
-    /* Return string representation.
-     *
-     * If printAsIndexed is true then it prints
-     * the bit-vector components of the FP value as indexed symbols, otherwise
-     * in binary notation. */
-    std::string toString(bool printAsIndexed = false) const;
-
-    // Gives the corresponding IEEE-754 transfer format
-    BitVector pack (void) const;
-
-
-    FloatingPoint absolute (void) const;
-    FloatingPoint negate (void) const;
-    FloatingPoint plus (const RoundingMode &rm, const FloatingPoint &arg) const;
-    FloatingPoint sub (const RoundingMode &rm, const FloatingPoint &arg) const;
-    FloatingPoint mult (const RoundingMode &rm, const FloatingPoint &arg) const;
-    FloatingPoint div (const RoundingMode &rm, const FloatingPoint &arg) const;
-    FloatingPoint fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const;
-    FloatingPoint sqrt (const RoundingMode &rm) const;
-    FloatingPoint rti (const RoundingMode &rm) const;
-    FloatingPoint rem (const FloatingPoint &arg) const;
-
-    // zeroCase is whether the left or right is returned in the case of min/max(-0,+0) or (+0,-0)
-    FloatingPoint maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const;
-    FloatingPoint minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const;
-
-    // These detect when the answer is defined
-    typedef std::pair<FloatingPoint, bool> PartialFloatingPoint;
-
-    PartialFloatingPoint max (const FloatingPoint &arg) const;
-    PartialFloatingPoint min (const FloatingPoint &arg) const;
-
-
-    bool operator ==(const FloatingPoint& fp) const;
-    bool operator <= (const FloatingPoint &arg) const;
-    bool operator < (const FloatingPoint &arg) const;
-
-    bool isNormal (void) const;
-    bool isSubnormal (void) const;
-    bool isZero (void) const;
-    bool isInfinite (void) const;
-    bool isNaN (void) const;
-    bool isNegative (void) const;
-    bool isPositive (void) const;
-
-    FloatingPoint convert (const FloatingPointSize &target, const RoundingMode &rm) const;
-
-    // These require a value to return in the undefined case
-    BitVector convertToBVTotal (BitVectorSize width, const RoundingMode &rm,
-				bool signedBV, BitVector undefinedCase) const;
-    Rational convertToRationalTotal (Rational undefinedCase) const;
-
-    // These detect when the answer is defined
-    typedef std::pair<BitVector, bool> PartialBitVector;
-    typedef std::pair<Rational, bool> PartialRational;
-
-    PartialBitVector convertToBV (BitVectorSize width, const RoundingMode &rm,
-				bool signedBV) const;
-    PartialRational convertToRational (void) const;
-
-  }; /* class FloatingPoint */
-
-
-  struct CVC4_PUBLIC FloatingPointHashFunction {
-    size_t operator() (const FloatingPoint& fp) const {
-      FloatingPointSizeHashFunction fpshf;
-      BitVectorHashFunction bvhf;
-
-      return fpshf(fp.t) ^ bvhf(fp.pack());
-    }
-  }; /* struct FloatingPointHashFunction */
+  size_t hash(void) const
+  {
+    unfinished();
+    return 23;
+  }
+};
+#endif /* @CVC4_USE_SYMFPU@ */
 
+class CVC4_PUBLIC FloatingPoint
+{
+ public:
   /**
-   * The parameter type for the conversions to floating point.
+   * Wrappers to represent results of non-total functions (e.g., min/max).
+   * The Boolean flag is true if the result is defined, and false otherwise.
    */
-  class CVC4_PUBLIC FloatingPointConvertSort {
-  public :
-    FloatingPointSize t;
+  using PartialFloatingPoint = std::pair<FloatingPoint, bool>;
+  using PartialBitVector = std::pair<BitVector, bool>;
+  using PartialRational = std::pair<Rational, bool>;
 
-    FloatingPointConvertSort (unsigned _e, unsigned _s)
-      : t(_e,_s) {}
-    FloatingPointConvertSort (const FloatingPointSize &fps)
-      : t(fps) {}
+  /** Constructors. */
+  FloatingPoint(unsigned e, unsigned s, const BitVector& bv);
+  FloatingPoint(const FloatingPointSize& size, const BitVector& bv);
 
-    bool operator ==(const FloatingPointConvertSort& fpcs) const {
-      return t == fpcs.t;
-    }
+  FloatingPoint(const FloatingPointSize& fp_size,
+                const FloatingPointLiteral& fpl)
+      : d_fp_size(fp_size), d_fpl(fpl)
+  {
+  }
 
-  };
+  FloatingPoint(const FloatingPoint& fp)
+      : d_fp_size(fp.d_fp_size), d_fpl(fp.d_fpl)
+  {
+  }
+  FloatingPoint(const FloatingPointSize& size,
+                const RoundingMode& rm,
+                const BitVector& bv,
+                bool signedBV);
+  FloatingPoint(const FloatingPointSize& size,
+                const RoundingMode& rm,
+                const Rational& r);
 
   /**
-   * As different conversions are different parameterised kinds, there
-   * is a need for different (C++) types for each one.
+   * Create a FP NaN value of given size.
+   * size: The FP size (format).
    */
+  static FloatingPoint makeNaN(const FloatingPointSize& size);
+  /**
+   * Create a FP infinity value of given size.
+   * size: The FP size (format).
+   * sign: True for -oo, false otherwise.
+   */
+  static FloatingPoint makeInf(const FloatingPointSize& size, bool sign);
+  /**
+   * Create a FP zero value of given size.
+   * size: The FP size (format).
+   * sign: True for -zero, false otherwise.
+   */
+  static FloatingPoint makeZero(const FloatingPointSize& size, bool sign);
+  /**
+   * Create the smallest subnormal FP value of given size.
+   * size: The FP size (format).
+   * sign: True for negative sign, false otherwise.
+   */
+  static FloatingPoint makeMinSubnormal(const FloatingPointSize& size,
+                                        bool sign);
+  /**
+   * Create the largest subnormal FP value of given size.
+   * size: The FP size (format).
+   * sign: True for negative sign, false otherwise.
+   */
+  static FloatingPoint makeMaxSubnormal(const FloatingPointSize& size,
+                                        bool sign);
+  /**
+   * Create the smallest normal FP value of given size.
+   * size: The FP size (format).
+   * sign: True for negative sign, false otherwise.
+   */
+  static FloatingPoint makeMinNormal(const FloatingPointSize& size, bool sign);
+  /**
+   * Create the largest normal FP value of given size.
+   * size: The FP size (format).
+   * sign: True for negative sign, false otherwise.
+   */
+  static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign);
 
-  class CVC4_PUBLIC FloatingPointToFPIEEEBitVector : public FloatingPointConvertSort {
-  public :
-    FloatingPointToFPIEEEBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
-    FloatingPointToFPIEEEBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
-  };
-
-  class CVC4_PUBLIC FloatingPointToFPFloatingPoint : public FloatingPointConvertSort {
-  public :
-    FloatingPointToFPFloatingPoint (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
-    FloatingPointToFPFloatingPoint (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
-  };
-
-  class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort {
-  public :
-    FloatingPointToFPReal (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
-    FloatingPointToFPReal (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
-  };
-
-  class CVC4_PUBLIC FloatingPointToFPSignedBitVector : public FloatingPointConvertSort {
-  public :
-    FloatingPointToFPSignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
-    FloatingPointToFPSignedBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
-  };
+  /** Get the wrapped floating-point value. */
+  const FloatingPointLiteral& getLiteral(void) const { return this->d_fpl; }
 
-  class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort {
-  public :
-    FloatingPointToFPUnsignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
-    FloatingPointToFPUnsignedBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
-  };
+  /**
+   * Return a string representation of this floating-point.
+   *
+   * If printAsIndexed is true then it prints the bit-vector components of the
+   * FP value as indexed symbols, otherwise in binary notation.
+   */
+  std::string toString(bool printAsIndexed = false) const;
+
+  /** Return the packed (IEEE-754) representation of this floating-point. */
+  BitVector pack(void) const;
+
+  /** Floating-point absolute value. */
+  FloatingPoint absolute(void) const;
+  /** Floating-point negation. */
+  FloatingPoint negate(void) const;
+  /** Floating-point addition. */
+  FloatingPoint plus(const RoundingMode& rm, const FloatingPoint& arg) const;
+  /** Floating-point subtraction. */
+  FloatingPoint sub(const RoundingMode& rm, const FloatingPoint& arg) const;
+  /** Floating-point multiplication. */
+  FloatingPoint mult(const RoundingMode& rm, const FloatingPoint& arg) const;
+  /** Floating-point division. */
+  FloatingPoint div(const RoundingMode& rm, const FloatingPoint& arg) const;
+  /** Floating-point fused multiplication and addition. */
+  FloatingPoint fma(const RoundingMode& rm,
+                    const FloatingPoint& arg1,
+                    const FloatingPoint& arg2) const;
+  /** Floating-point square root. */
+  FloatingPoint sqrt(const RoundingMode& rm) const;
+  /** Floating-point round to integral. */
+  FloatingPoint rti(const RoundingMode& rm) const;
+  /** Floating-point remainder. */
+  FloatingPoint rem(const FloatingPoint& arg) const;
 
-  class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort {
-  public :
-    FloatingPointToFPGeneric (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
-    FloatingPointToFPGeneric (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
-  };
+  /**
+   * Floating-point max (total version).
+   * zeroCase: true to return the left (rather than the right operand) in case
+   *           of max(-0,+0) or max(+0,-0).
+   */
+  FloatingPoint maxTotal(const FloatingPoint& arg, bool zeroCaseLeft) const;
+  /**
+   * Floating-point min (total version).
+   * zeroCase: true to return the left (rather than the right operand) in case
+   *           of min(-0,+0) or min(+0,-0).
+   */
+  FloatingPoint minTotal(const FloatingPoint& arg, bool zeroCaseLeft) const;
 
+  /**
+   * Floating-point max.
+   *
+   * Returns a partial floating-point, which is a pair of FloatingPoint and
+   * bool. The boolean flag is true if the result is defined, and false if it
+   * is undefined.
+   */
+  PartialFloatingPoint max(const FloatingPoint& arg) const;
+  /** Floating-point min.
+   *
+   * Returns a partial floating-point, which is a pair of FloatingPoint and
+   * bool. The boolean flag is true if the result is defined, and false if it
+   * is undefined.
+   */
+  PartialFloatingPoint min(const FloatingPoint& arg) const;
+
+  /** Equality (NOT: fp.eq but =) over floating-point values. */
+  bool operator==(const FloatingPoint& fp) const;
+  /** Floating-point less or equal than. */
+  bool operator<=(const FloatingPoint& arg) const;
+  /** Floating-point less than. */
+  bool operator<(const FloatingPoint& arg) const;
+
+  /** Return true if this floating-point represents a normal value. */
+  bool isNormal(void) const;
+  /** Return true if this floating-point represents a subnormal value. */
+  bool isSubnormal(void) const;
+  /** Return true if this floating-point represents a zero value. */
+  bool isZero(void) const;
+  /** Return true if this floating-point represents an infinite value. */
+  bool isInfinite(void) const;
+  /** Return true if this floating-point represents a NaN value. */
+  bool isNaN(void) const;
+  /** Return true if this floating-point represents a negative value. */
+  bool isNegative(void) const;
+  /** Return true if this floating-point represents a positive value. */
+  bool isPositive(void) const;
 
+  /**
+   * Convert this floating-point to a floating-point of given size, with
+   * respect to given rounding mode.
+   */
+  FloatingPoint convert(const FloatingPointSize& target,
+                        const RoundingMode& rm) const;
 
-  template <unsigned key>
-  struct CVC4_PUBLIC FloatingPointConvertSortHashFunction {
-    inline size_t operator() (const FloatingPointConvertSort& fpcs) const {
-      FloatingPointSizeHashFunction f;
-      return f(fpcs.t) ^ (0x00005300 | (key << 24));
-    }
-  }; /* struct FloatingPointConvertSortHashFunction */
+  /**
+   * Convert this floating-point to a bit-vector of given size, with
+   * respect to given rounding mode (total version).
+   * Returns given bit-vector 'undefinedCase' in the undefined case.
+   */
+  BitVector convertToBVTotal(BitVectorSize width,
+                             const RoundingMode& rm,
+                             bool signedBV,
+                             BitVector undefinedCase) const;
+  /**
+   * Convert this floating-point to a rational, with respect to given rounding
+   * mode (total version).
+   * Returns given rational 'undefinedCase' in the undefined case.
+   */
+  Rational convertToRationalTotal(Rational undefinedCase) const;
 
+  /**
+   * Convert this floating-point to a bit-vector of given size.
+   *
+   * Returns a partial bit-vector, which is a pair of BitVector and bool.
+   * The boolean flag is true if the result is defined, and false if it
+   * is undefined.
+   */
+  PartialBitVector convertToBV(BitVectorSize width,
+                               const RoundingMode& rm,
+                               bool signedBV) const;
+  /**
+   * Convert this floating-point to a Rational.
+   *
+   * Returns a partial Rational, which is a pair of Rational and bool.
+   * The boolean flag is true if the result is defined, and false if it
+   * is undefined.
+   */
+  PartialRational convertToRational(void) const;
 
+  /** The floating-point size of this floating-point value. */
+  FloatingPointSize d_fp_size;
 
+ protected:
+  /** The floating-point literal of this floating-point value. */
+  FloatingPointLiteral d_fpl;
 
+}; /* class FloatingPoint */
 
+/**
+ * Hash function for floating-point values.
+ */
+struct CVC4_PUBLIC FloatingPointHashFunction
+{
+  size_t operator()(const FloatingPoint& fp) const
+  {
+    FloatingPointSizeHashFunction fpshf;
+    BitVectorHashFunction bvhf;
 
+    return fpshf(fp.d_fp_size) ^ bvhf(fp.pack());
+  }
+}; /* struct FloatingPointHashFunction */
+
+/* -------------------------------------------------------------------------- */
+
+/**
+ * The parameter type for the conversions to floating point.
+ */
+class CVC4_PUBLIC FloatingPointConvertSort
+{
+ public:
+  /** Constructors. */
+  FloatingPointConvertSort(unsigned _e, unsigned _s) : d_fp_size(_e, _s) {}
+  FloatingPointConvertSort(const FloatingPointSize& fps) : d_fp_size(fps) {}
+
+  /** Operator overload for comparison of conversion sorts. */
+  bool operator==(const FloatingPointConvertSort& fpcs) const
+  {
+    return d_fp_size == fpcs.d_fp_size;
+  }
 
+  /** The floating-point size of this sort. */
+  FloatingPointSize d_fp_size;
+};
 
-  /**
-   * The parameter type for the conversion to bit vector.
-   */
-  class CVC4_PUBLIC FloatingPointToBV {
-  public :
-    BitVectorSize bvs;
-
-    FloatingPointToBV (unsigned s)
-      : bvs(s) {}
-    FloatingPointToBV (const FloatingPointToBV &old) : bvs(old.bvs) {}
-    FloatingPointToBV (const BitVectorSize &old) : bvs(old) {}
-    operator unsigned () const { return bvs; }
-  };
-
-  class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV {
-  public : FloatingPointToUBV (unsigned _s) : FloatingPointToBV(_s) {}
-    FloatingPointToUBV (const FloatingPointToBV &old) : FloatingPointToBV(old) {}
-  };
-  class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV {
-  public : FloatingPointToSBV (unsigned _s) : FloatingPointToBV(_s) {}
-    FloatingPointToSBV (const FloatingPointToBV &old) : FloatingPointToBV(old) {}
-  };
-  class CVC4_PUBLIC FloatingPointToUBVTotal : public FloatingPointToBV {
-  public : FloatingPointToUBVTotal (unsigned _s) : FloatingPointToBV(_s) {}
-    FloatingPointToUBVTotal (const FloatingPointToBV &old) : FloatingPointToBV(old) {}
-  };
-  class CVC4_PUBLIC FloatingPointToSBVTotal : public FloatingPointToBV {
-  public : FloatingPointToSBVTotal (unsigned _s) : FloatingPointToBV(_s) {}
-    FloatingPointToSBVTotal (const FloatingPointToBV &old) : FloatingPointToBV(old) {}
-  };
-
-
-  template <unsigned key>
-  struct CVC4_PUBLIC FloatingPointToBVHashFunction {
-    inline size_t operator() (const FloatingPointToBV& fptbv) const {
-      UnsignedHashFunction< ::CVC4::BitVectorSize > f;
-      return 	(key ^ 0x46504256) ^ f(fptbv.bvs);
-    }
-  }; /* struct FloatingPointToBVHashFunction */
-
-
-  // It is not possible to pack a number without a size to pack to,
-  // thus it is difficult to implement this in a sensible way.  Use
-  // FloatingPoint instead...
-  /*
-  inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) CVC4_PUBLIC;
-  inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) {
-    return os << "FloatingPointLiteral";
+/** Hash function for conversion sorts. */
+template <unsigned key>
+struct CVC4_PUBLIC FloatingPointConvertSortHashFunction
+{
+  inline size_t operator()(const FloatingPointConvertSort& fpcs) const
+  {
+    FloatingPointSizeHashFunction f;
+    return f(fpcs.d_fp_size) ^ (0x00005300 | (key << 24));
   }
-  */
-
-  inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC;
-  inline std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp)
+}; /* struct FloatingPointConvertSortHashFunction */
+
+/**
+ * As different conversions are different parameterised kinds, there
+ * is a need for different (C++) types for each one.
+ */
+
+/**
+ * Conversion from floating-point to IEEE bit-vector (first bit represents the
+ * sign, the following exponent width bits the exponent, and the remaining bits
+ * the significand).
+ */
+class CVC4_PUBLIC FloatingPointToFPIEEEBitVector
+    : public FloatingPointConvertSort
+{
+ public:
+  /** Constructors. */
+  FloatingPointToFPIEEEBitVector(unsigned _e, unsigned _s)
+      : FloatingPointConvertSort(_e, _s)
   {
-    // print in binary notation
-    return os << fp.toString();
   }
-
-  inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) CVC4_PUBLIC;
-  inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) {
-    return os << "(_ FloatingPoint " << fps.exponent() << " " << fps.significand() << ")";
+  FloatingPointToFPIEEEBitVector(const FloatingPointConvertSort& old)
+      : FloatingPointConvertSort(old)
+  {
   }
-
-  inline std::ostream& operator <<(std::ostream& os, const FloatingPointConvertSort& fpcs) CVC4_PUBLIC;
-  inline std::ostream& operator <<(std::ostream& os, const FloatingPointConvertSort& fpcs) {
-    return os << "(_ to_fp " << fpcs.t.exponent() << " " << fpcs.t.significand() << ")";
+};
+
+/**
+ * Conversion from floating-point to another floating-point (of possibly
+ * different size).
+ */
+class CVC4_PUBLIC FloatingPointToFPFloatingPoint
+    : public FloatingPointConvertSort
+{
+ public:
+  /** Constructors. */
+  FloatingPointToFPFloatingPoint(unsigned _e, unsigned _s)
+      : FloatingPointConvertSort(_e, _s)
+  {
+  }
+  FloatingPointToFPFloatingPoint(const FloatingPointConvertSort& old)
+      : FloatingPointConvertSort(old)
+  {
+  }
+};
+
+/**
+ * Conversion from floating-point to Real.
+ */
+class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort
+{
+ public:
+  /** Constructors. */
+  FloatingPointToFPReal(unsigned _e, unsigned _s)
+      : FloatingPointConvertSort(_e, _s)
+  {
+  }
+  FloatingPointToFPReal(const FloatingPointConvertSort& old)
+      : FloatingPointConvertSort(old)
+  {
+  }
+};
+
+/**
+ * Conversion from floating-point to signed bit-vector value.
+ */
+class CVC4_PUBLIC FloatingPointToFPSignedBitVector
+    : public FloatingPointConvertSort
+{
+ public:
+  /** Constructors. */
+  FloatingPointToFPSignedBitVector(unsigned _e, unsigned _s)
+      : FloatingPointConvertSort(_e, _s)
+  {
+  }
+  FloatingPointToFPSignedBitVector(const FloatingPointConvertSort& old)
+      : FloatingPointConvertSort(old)
+  {
+  }
+};
+
+/**
+ * Conversion from floating-point to unsigned bit-vector value.
+ */
+class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector
+    : public FloatingPointConvertSort
+{
+ public:
+  /** Constructors. */
+  FloatingPointToFPUnsignedBitVector(unsigned _e, unsigned _s)
+      : FloatingPointConvertSort(_e, _s)
+  {
+  }
+  FloatingPointToFPUnsignedBitVector(const FloatingPointConvertSort& old)
+      : FloatingPointConvertSort(old)
+  {
+  }
+};
+
+class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort
+{
+ public:
+  /** Constructors. */
+  FloatingPointToFPGeneric(unsigned _e, unsigned _s)
+      : FloatingPointConvertSort(_e, _s)
+  {
+  }
+  FloatingPointToFPGeneric(const FloatingPointConvertSort& old)
+      : FloatingPointConvertSort(old)
+  {
+  }
+};
+
+/**
+ * Base type for floating-point to bit-vector conversion.
+ */
+class CVC4_PUBLIC FloatingPointToBV
+{
+ public:
+  /** Constructors. */
+  FloatingPointToBV(unsigned s) : d_bv_size(s) {}
+  FloatingPointToBV(const FloatingPointToBV& old) : d_bv_size(old.d_bv_size) {}
+  FloatingPointToBV(const BitVectorSize& old) : d_bv_size(old) {}
+
+  /** Return the bit-width of the bit-vector to convert to. */
+  operator unsigned() const { return d_bv_size; }
+
+  /** The bit-width of the bit-vector to converto to. */
+  BitVectorSize d_bv_size;
+};
+
+/**
+ * Conversion from floating-point to unsigned bit-vector value.
+ */
+class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV
+{
+ public:
+  FloatingPointToUBV(unsigned _s) : FloatingPointToBV(_s) {}
+  FloatingPointToUBV(const FloatingPointToBV& old) : FloatingPointToBV(old) {}
+};
+
+/**
+ * Conversion from floating-point to signed bit-vector value.
+ */
+class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV
+{
+ public:
+  FloatingPointToSBV(unsigned _s) : FloatingPointToBV(_s) {}
+  FloatingPointToSBV(const FloatingPointToBV& old) : FloatingPointToBV(old) {}
+};
+
+/**
+ * Conversion from floating-point to unsigned bit-vector value (total version).
+ */
+class CVC4_PUBLIC FloatingPointToUBVTotal : public FloatingPointToBV
+{
+ public:
+  FloatingPointToUBVTotal(unsigned _s) : FloatingPointToBV(_s) {}
+  FloatingPointToUBVTotal(const FloatingPointToBV& old) : FloatingPointToBV(old)
+  {
   }
+};
+
+/**
+ * Conversion from floating-point to signed bit-vector value (total version).
+ */
+class CVC4_PUBLIC FloatingPointToSBVTotal : public FloatingPointToBV
+{
+ public:
+  FloatingPointToSBVTotal(unsigned _s) : FloatingPointToBV(_s) {}
+  FloatingPointToSBVTotal(const FloatingPointToBV& old) : FloatingPointToBV(old)
+  {
+  }
+};
+
+/**
+ * Hash function for floating-point to bit-vector conversions.
+ */
+template <unsigned key>
+struct CVC4_PUBLIC FloatingPointToBVHashFunction
+{
+  inline size_t operator()(const FloatingPointToBV& fptbv) const
+  {
+    UnsignedHashFunction< ::CVC4::BitVectorSize> f;
+    return (key ^ 0x46504256) ^ f(fptbv.d_bv_size);
+  }
+}; /* struct FloatingPointToBVHashFunction */
+
+/* Note: It is not possible to pack a number without a size to pack to,
+ * thus it is difficult to implement output stream operator overloads for
+ * FloatingPointLiteral in a sensible way. Use FloatingPoint instead. */
+
+/** Output stream operator overloading for floating-point values. */
+std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC;
+
+/** Output stream operator overloading for floating-point formats. */
+std::ostream& operator<<(std::ostream& os,
+                         const FloatingPointSize& fps) CVC4_PUBLIC;
+
+/** Output stream operator overloading for floating-point conversion sorts. */
+std::ostream& operator<<(std::ostream& os,
+                         const FloatingPointConvertSort& fpcs) CVC4_PUBLIC;
 
-}/* CVC4 namespace */
+}  // namespace CVC4
 
 #endif /* CVC4__FLOATINGPOINT_H */