FP: Move implementation of type rules from header to .cpp file. (#6241)

2 files changed, 934 insertions, 699 deletions

diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp
new file mode 100644
index 000000000..165c9b924
--- /dev/null
+++ b/src/theory/fp/theory_fp_type_rules.cpp
@@ -0,0 +1,815 @@
+/*********************                                                        */
+/*! \file theory_fp_type_rules.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Martin Brain, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Type rules for the theory of floating-point arithmetic.
+ **/
+
+#include "theory/fp/theory_fp_type_rules.h"
+
+// This is only needed for checking that components are only applied to leaves.
+#include "theory/theory.h"
+#include "util/roundingmode.h"
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+#define TRACE(FUNCTION)                                                \
+  Trace("fp-type") << FUNCTION "::computeType(" << check << "): " << n \
+                   << std::endl
+
+TypeNode FloatingPointConstantTypeRule::computeType(NodeManager* nodeManager,
+                                                    TNode n,
+                                                    bool check)
+{
+  TRACE("FloatingPointConstantTypeRule");
+
+  const FloatingPoint& f = n.getConst<FloatingPoint>();
+
+  if (check)
+  {
+    if (!(validExponentSize(f.getSize().exponentWidth())))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "constant with invalid exponent size");
+    }
+    if (!(validSignificandSize(f.getSize().significandWidth())))
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "constant with invalid significand size");
+    }
+  }
+  return nodeManager->mkFloatingPointType(f.getSize());
+}
+
+TypeNode RoundingModeConstantTypeRule::computeType(NodeManager* nodeManager,
+                                                   TNode n,
+                                                   bool check)
+{
+  TRACE("RoundingModeConstantTypeRule");
+
+  // Nothing to check!
+  return nodeManager->roundingModeType();
+}
+
+TypeNode FloatingPointFPTypeRule::computeType(NodeManager* nodeManager,
+                                              TNode n,
+                                              bool check)
+{
+  TRACE("FloatingPointFPTypeRule");
+
+  TypeNode signType = n[0].getType(check);
+  TypeNode exponentType = n[1].getType(check);
+  TypeNode significandType = n[2].getType(check);
+
+  if (!signType.isBitVector() || !exponentType.isBitVector()
+      || !significandType.isBitVector())
+  {
+    throw TypeCheckingExceptionPrivate(n,
+                                       "arguments to fp must be bit vectors");
+  }
+
+  uint32_t signBits = signType.getBitVectorSize();
+  uint32_t exponentBits = exponentType.getBitVectorSize();
+  uint32_t significandBits = significandType.getBitVectorSize();
+
+  if (check)
+  {
+    if (signBits != 1)
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "sign bit vector in fp must be 1 bit long");
+    }
+    else if (!(validExponentSize(exponentBits)))
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "exponent bit vector in fp is an invalid size");
+    }
+    else if (!(validSignificandSize(significandBits)))
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "significand bit vector in fp is an invalid size");
+    }
+  }
+
+  // The +1 is for the implicit hidden bit
+  return nodeManager->mkFloatingPointType(exponentBits, significandBits + 1);
+}
+
+TypeNode FloatingPointTestTypeRule::computeType(NodeManager* nodeManager,
+                                                TNode n,
+                                                bool check)
+{
+  TRACE("FloatingPointTestTypeRule");
+
+  if (check)
+  {
+    TypeNode firstOperand = n[0].getType(check);
+
+    if (!firstOperand.isFloatingPoint())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "floating-point test applied to a non floating-point sort");
+    }
+
+    size_t children = n.getNumChildren();
+    for (size_t i = 1; i < children; ++i)
+    {
+      if (!(n[i].getType(check) == firstOperand))
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "floating-point test applied to mixed sorts");
+      }
+    }
+  }
+
+  return nodeManager->booleanType();
+}
+
+TypeNode FloatingPointOperationTypeRule::computeType(NodeManager* nodeManager,
+                                                     TNode n,
+                                                     bool check)
+{
+  TRACE("FloatingPointOperationTypeRule");
+
+  TypeNode firstOperand = n[0].getType(check);
+
+  if (check)
+  {
+    if (!firstOperand.isFloatingPoint())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "floating-point operation applied to a non floating-point sort");
+    }
+
+    size_t children = n.getNumChildren();
+    for (size_t i = 1; i < children; ++i)
+    {
+      if (!(n[i].getType(check) == firstOperand))
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "floating-point test applied to mixed sorts");
+      }
+    }
+  }
+
+  return firstOperand;
+}
+
+TypeNode FloatingPointRoundingOperationTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  TRACE("FloatingPointRoundingOperationTypeRule");
+
+  if (check)
+  {
+    TypeNode roundingModeType = n[0].getType(check);
+
+    if (!roundingModeType.isRoundingMode())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument must be a rounding mode");
+    }
+  }
+
+  TypeNode firstOperand = n[1].getType(check);
+
+  if (check)
+  {
+    if (!firstOperand.isFloatingPoint())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "floating-point operation applied to a non floating-point sort");
+    }
+
+    size_t children = n.getNumChildren();
+    for (size_t i = 2; i < children; ++i)
+    {
+      if (!(n[i].getType(check) == firstOperand))
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "floating-point operation applied to mixed sorts");
+      }
+    }
+  }
+
+  return firstOperand;
+}
+
+TypeNode FloatingPointPartialOperationTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  TRACE("FloatingPointOperationTypeRule");
+  AlwaysAssert(n.getNumChildren() > 0);
+
+  TypeNode firstOperand = n[0].getType(check);
+
+  if (check)
+  {
+    if (!firstOperand.isFloatingPoint())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "floating-point operation applied to a non floating-point sort");
+    }
+
+    const size_t children = n.getNumChildren();
+    for (size_t i = 1; i < children - 1; ++i)
+    {
+      if (n[i].getType(check) != firstOperand)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "floating-point partial operation applied to mixed sorts");
+      }
+    }
+
+    TypeNode UFValueType = n[children - 1].getType(check);
+
+    if (!(UFValueType.isBitVector()) || !(UFValueType.getBitVectorSize() == 1))
+    {
+      throw TypeCheckingExceptionPrivate(
+          n,
+          "floating-point partial operation final argument must be a "
+          "bit-vector of length 1");
+    }
+  }
+
+  return firstOperand;
+}
+
+TypeNode FloatingPointParametricOpTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  TRACE("FloatingPointParametricOpTypeRule");
+
+  return nodeManager->builtinOperatorType();
+}
+
+TypeNode FloatingPointToFPIEEEBitVectorTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  TRACE("FloatingPointToFPIEEEBitVectorTypeRule");
+  AlwaysAssert(n.getNumChildren() == 1);
+
+  FloatingPointToFPIEEEBitVector info =
+      n.getOperator().getConst<FloatingPointToFPIEEEBitVector>();
+
+  if (check)
+  {
+    TypeNode operandType = n[0].getType(check);
+
+    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.getSize().exponentWidth()
+                      + info.getSize().significandWidth()))
+    {
+      throw TypeCheckingExceptionPrivate(
+          n,
+          "conversion to floating-point from bit vector used with bit vector "
+          "length that does not match floating point parameters");
+    }
+  }
+
+  return nodeManager->mkFloatingPointType(info.getSize());
+}
+
+TypeNode FloatingPointToFPFloatingPointTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  TRACE("FloatingPointToFPFloatingPointTypeRule");
+  AlwaysAssert(n.getNumChildren() == 2);
+
+  FloatingPointToFPFloatingPoint info =
+      n.getOperator().getConst<FloatingPointToFPFloatingPoint>();
+
+  if (check)
+  {
+    TypeNode roundingModeType = n[0].getType(check);
+
+    if (!roundingModeType.isRoundingMode())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument must be a rounding mode");
+    }
+
+    TypeNode operandType = n[1].getType(check);
+
+    if (!(operandType.isFloatingPoint()))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "conversion to floating-point from "
+                                         "floating-point used with sort "
+                                         "other than floating-point");
+    }
+  }
+
+  return nodeManager->mkFloatingPointType(info.getSize());
+}
+
+TypeNode FloatingPointToFPRealTypeRule::computeType(NodeManager* nodeManager,
+                                                    TNode n,
+                                                    bool check)
+{
+  TRACE("FloatingPointToFPRealTypeRule");
+  AlwaysAssert(n.getNumChildren() == 2);
+
+  FloatingPointToFPReal info =
+      n.getOperator().getConst<FloatingPointToFPReal>();
+
+  if (check)
+  {
+    TypeNode roundingModeType = n[0].getType(check);
+
+    if (!roundingModeType.isRoundingMode())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument must be a rounding mode");
+    }
+
+    TypeNode operandType = n[1].getType(check);
+
+    if (!(operandType.isReal()))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "conversion to floating-point from "
+                                         "real used with sort other than "
+                                         "real");
+    }
+  }
+
+  return nodeManager->mkFloatingPointType(info.getSize());
+}
+
+TypeNode FloatingPointToFPSignedBitVectorTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  TRACE("FloatingPointToFPSignedBitVectorTypeRule");
+  AlwaysAssert(n.getNumChildren() == 2);
+
+  FloatingPointToFPSignedBitVector info =
+      n.getOperator().getConst<FloatingPointToFPSignedBitVector>();
+
+  if (check)
+  {
+    TypeNode roundingModeType = n[0].getType(check);
+
+    if (!roundingModeType.isRoundingMode())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument must be a rounding mode");
+    }
+
+    TypeNode operandType = n[1].getType(check);
+
+    if (!(operandType.isBitVector()))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "conversion to floating-point from "
+                                         "signed bit vector used with sort "
+                                         "other than bit vector");
+    }
+  }
+
+  return nodeManager->mkFloatingPointType(info.getSize());
+}
+
+TypeNode FloatingPointToFPUnsignedBitVectorTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  TRACE("FloatingPointToFPUnsignedBitVectorTypeRule");
+  AlwaysAssert(n.getNumChildren() == 2);
+
+  FloatingPointToFPUnsignedBitVector info =
+      n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>();
+
+  if (check)
+  {
+    TypeNode roundingModeType = n[0].getType(check);
+
+    if (!roundingModeType.isRoundingMode())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument must be a rounding mode");
+    }
+
+    TypeNode operandType = n[1].getType(check);
+
+    if (!(operandType.isBitVector()))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "conversion to floating-point from "
+                                         "unsigned bit vector used with sort "
+                                         "other than bit vector");
+    }
+  }
+
+  return nodeManager->mkFloatingPointType(info.getSize());
+}
+
+TypeNode FloatingPointToFPGenericTypeRule::computeType(NodeManager* nodeManager,
+                                                       TNode n,
+                                                       bool check)
+{
+  TRACE("FloatingPointToFPGenericTypeRule");
+
+  FloatingPointToFPGeneric info =
+      n.getOperator().getConst<FloatingPointToFPGeneric>();
+
+  if (check)
+  {
+    /* As this is a generic kind intended only for parsing,
+     * the checking here is light.  For better checking, use
+     * expandDefinitions first.
+     */
+
+    size_t children = n.getNumChildren();
+    for (size_t i = 0; i < children; ++i)
+    {
+      n[i].getType(check);
+    }
+  }
+
+  return nodeManager->mkFloatingPointType(info.getSize());
+}
+
+TypeNode FloatingPointToUBVTypeRule::computeType(NodeManager* nodeManager,
+                                                 TNode n,
+                                                 bool check)
+{
+  TRACE("FloatingPointToUBVTypeRule");
+  AlwaysAssert(n.getNumChildren() == 2);
+
+  FloatingPointToUBV info = n.getOperator().getConst<FloatingPointToUBV>();
+
+  if (check)
+  {
+    TypeNode roundingModeType = n[0].getType(check);
+
+    if (!roundingModeType.isRoundingMode())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument must be a rounding mode");
+    }
+
+    TypeNode operandType = n[1].getType(check);
+
+    if (!(operandType.isFloatingPoint()))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "conversion to unsigned bit vector "
+                                         "used with a sort other than "
+                                         "floating-point");
+    }
+  }
+
+  return nodeManager->mkBitVectorType(info.d_bv_size);
+}
+
+TypeNode FloatingPointToSBVTypeRule::computeType(NodeManager* nodeManager,
+                                                 TNode n,
+                                                 bool check)
+{
+  TRACE("FloatingPointToSBVTypeRule");
+  AlwaysAssert(n.getNumChildren() == 2);
+
+  FloatingPointToSBV info = n.getOperator().getConst<FloatingPointToSBV>();
+
+  if (check)
+  {
+    TypeNode roundingModeType = n[0].getType(check);
+
+    if (!roundingModeType.isRoundingMode())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument must be a rounding mode");
+    }
+
+    TypeNode operandType = n[1].getType(check);
+
+    if (!(operandType.isFloatingPoint()))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "conversion to signed bit vector "
+                                         "used with a sort other than "
+                                         "floating-point");
+    }
+  }
+
+  return nodeManager->mkBitVectorType(info.d_bv_size);
+}
+
+TypeNode FloatingPointToUBVTotalTypeRule::computeType(NodeManager* nodeManager,
+                                                      TNode n,
+                                                      bool check)
+{
+  TRACE("FloatingPointToUBVTotalTypeRule");
+  AlwaysAssert(n.getNumChildren() == 3);
+
+  FloatingPointToUBVTotal info =
+      n.getOperator().getConst<FloatingPointToUBVTotal>();
+
+  if (check)
+  {
+    TypeNode roundingModeType = n[0].getType(check);
+
+    if (!roundingModeType.isRoundingMode())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument must be a rounding mode");
+    }
+
+    TypeNode operandType = n[1].getType(check);
+
+    if (!(operandType.isFloatingPoint()))
+    {
+      throw TypeCheckingExceptionPrivate(
+          n,
+          "conversion to unsigned bit vector total"
+          "used with a sort other than "
+          "floating-point");
+    }
+
+    TypeNode defaultValueType = n[2].getType(check);
+
+    if (!(defaultValueType.isBitVector())
+        || !(defaultValueType.getBitVectorSize() == info))
+    {
+      throw TypeCheckingExceptionPrivate(
+          n,
+          "conversion to unsigned bit vector total"
+          "needs a bit vector of the same length"
+          "as last argument");
+    }
+  }
+
+  return nodeManager->mkBitVectorType(info.d_bv_size);
+}
+
+TypeNode FloatingPointToSBVTotalTypeRule::computeType(NodeManager* nodeManager,
+                                                      TNode n,
+                                                      bool check)
+{
+  TRACE("FloatingPointToSBVTotalTypeRule");
+  AlwaysAssert(n.getNumChildren() == 3);
+
+  FloatingPointToSBVTotal info =
+      n.getOperator().getConst<FloatingPointToSBVTotal>();
+
+  if (check)
+  {
+    TypeNode roundingModeType = n[0].getType(check);
+
+    if (!roundingModeType.isRoundingMode())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "first argument must be a rounding mode");
+    }
+
+    TypeNode operandType = n[1].getType(check);
+
+    if (!(operandType.isFloatingPoint()))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "conversion to signed bit vector "
+                                         "used with a sort other than "
+                                         "floating-point");
+    }
+
+    TypeNode defaultValueType = n[2].getType(check);
+
+    if (!(defaultValueType.isBitVector())
+        || !(defaultValueType.getBitVectorSize() == info))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "conversion to signed bit vector total"
+                                         "needs a bit vector of the same length"
+                                         "as last argument");
+    }
+  }
+
+  return nodeManager->mkBitVectorType(info.d_bv_size);
+}
+
+TypeNode FloatingPointToRealTypeRule::computeType(NodeManager* nodeManager,
+                                                  TNode n,
+                                                  bool check)
+{
+  TRACE("FloatingPointToRealTypeRule");
+  AlwaysAssert(n.getNumChildren() == 1);
+
+  if (check)
+  {
+    TypeNode operandType = n[0].getType(check);
+
+    if (!operandType.isFloatingPoint())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "floating-point to real applied to a non floating-point sort");
+    }
+  }
+
+  return nodeManager->realType();
+}
+
+TypeNode FloatingPointToRealTotalTypeRule::computeType(NodeManager* nodeManager,
+                                                       TNode n,
+                                                       bool check)
+{
+  TRACE("FloatingPointToRealTotalTypeRule");
+  AlwaysAssert(n.getNumChildren() == 2);
+
+  if (check)
+  {
+    TypeNode operandType = n[0].getType(check);
+
+    if (!operandType.isFloatingPoint())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n,
+          "floating-point to real total applied to a non floating-point sort");
+    }
+
+    TypeNode defaultValueType = n[1].getType(check);
+
+    if (!defaultValueType.isReal())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "floating-point to real total needs a real second argument");
+    }
+  }
+
+  return nodeManager->realType();
+}
+
+TypeNode FloatingPointComponentBit::computeType(NodeManager* nodeManager,
+                                                TNode n,
+                                                bool check)
+{
+  TRACE("FloatingPointComponentBit");
+
+  if (check)
+  {
+    TypeNode operandType = n[0].getType(check);
+
+    if (!operandType.isFloatingPoint())
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "floating-point bit component "
+                                         "applied to a non floating-point "
+                                         "sort");
+    }
+    if (!(Theory::isLeafOf(n[0], THEORY_FP)
+          || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "floating-point bit component "
+                                         "applied to a non leaf / to_fp leaf "
+                                         "node");
+    }
+  }
+
+  return nodeManager->mkBitVectorType(1);
+}
+
+TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager,
+                                                     TNode n,
+                                                     bool check)
+{
+  TRACE("FloatingPointComponentExponent");
+
+  TypeNode operandType = n[0].getType(check);
+
+  if (check)
+  {
+    if (!operandType.isFloatingPoint())
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "floating-point exponent component "
+                                         "applied to a non floating-point "
+                                         "sort");
+    }
+    if (!(Theory::isLeafOf(n[0], THEORY_FP)
+          || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "floating-point exponent component "
+                                         "applied to a non leaf / to_fp "
+                                         "node");
+    }
+  }
+
+#ifdef CVC4_USE_SYMFPU
+  /* Need to create some symfpu objects as the size of bit-vector
+   * that is needed for this component is dependent on the encoding
+   * used (i.e. whether subnormals are forcibly normalised or not).
+   * 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>();
+  uint32_t bw = FloatingPoint::getUnpackedExponentWidth(fps);
+#else
+  uint32_t bw = 2;
+#endif
+  return nodeManager->mkBitVectorType(bw);
+}
+
+TypeNode FloatingPointComponentSignificand::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  TRACE("FloatingPointComponentSignificand");
+
+  TypeNode operandType = n[0].getType(check);
+
+  if (check)
+  {
+    if (!operandType.isFloatingPoint())
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "floating-point significand "
+                                         "component applied to a non "
+                                         "floating-point sort");
+    }
+    if (!(Theory::isLeafOf(n[0], THEORY_FP)
+          || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+    {
+      throw TypeCheckingExceptionPrivate(n,
+                                         "floating-point significand "
+                                         "component applied to a non leaf / "
+                                         "to_fp node");
+    }
+  }
+
+#ifdef CVC4_USE_SYMFPU
+  /* As before we need to use some of sympfu. */
+  FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
+  uint32_t bw = FloatingPoint::getUnpackedSignificandWidth(fps);
+#else
+  uint32_t bw = 1;
+#endif
+  return nodeManager->mkBitVectorType(bw);
+}
+
+TypeNode RoundingModeBitBlast::computeType(NodeManager* nodeManager,
+                                           TNode n,
+                                           bool check)
+{
+  TRACE("RoundingModeBitBlast");
+
+  if (check)
+  {
+    TypeNode operandType = n[0].getType(check);
+
+    if (!operandType.isRoundingMode())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "rounding mode bit-blast applied to a non rounding-mode sort");
+    }
+    if (!Theory::isLeafOf(n[0], THEORY_FP))
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "rounding mode bit-blast applied to a non leaf node");
+    }
+  }
+
+  return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES);
+}
+
+Cardinality CardinalityComputer::computeCardinality(TypeNode type)
+{
+  Assert(type.getKind() == kind::FLOATINGPOINT_TYPE);
+
+  FloatingPointSize fps = type.getConst<FloatingPointSize>();
+
+  /*
+   * 1                    NaN
+   * 2*1                  Infinities
+   * 2*1                  Zeros
+   * 2*2^(s-1)            Subnormal
+   * 2*((2^e)-2)*2^(s-1)  Normal
+   *
+   *  = 1 + 2*2 + 2*((2^e)-1)*2^(s-1)
+   *  =       5 + ((2^e)-1)*2^s
+   */
+
+  Integer significandValues = Integer(2).pow(fps.significandWidth());
+  Integer exponentValues = Integer(2).pow(fps.exponentWidth());
+  exponentValues -= Integer(1);
+
+  return Integer(5) + exponentValues * significandValues;
+}
+
+}  // namespace fp
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index ab193d7ba..aef2d0a50 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -2,813 +2,233 @@
 /*! \file theory_fp_type_rules.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Martin Brain, Tim King, Aina Niemetz
+ **   Aina Niemetz, Martin Brain, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** \brief Type rules for the theory of floating-point arithmetic.
  **/
 
 #include "cvc4_private.h"
 
-// This is only needed for checking that components are only applied to leaves.
-#include "theory/theory.h"
-#include "util/roundingmode.h"
-
 #ifndef CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
 #define CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
 
+#include "expr/node.h"
+#include "expr/type_node.h"
+
 namespace CVC4 {
+
+class NodeManager;
+
 namespace theory {
 namespace fp {
 
-#define TRACE(FUNCTION)                                                \
-  Trace("fp-type") << FUNCTION "::computeType(" << check << "): " << n \
-                   << std::endl
-
-class FloatingPointConstantTypeRule {
+/** Type rule for floating-point values. */
+class FloatingPointConstantTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointConstantTypeRule");
-
-    const FloatingPoint& f = n.getConst<FloatingPoint>();
-
-    if (check)
-    {
-      if (!(validExponentSize(f.getSize().exponentWidth())))
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "constant with invalid exponent size");
-      }
-      if (!(validSignificandSize(f.getSize().significandWidth())))
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "constant with invalid significand size");
-      }
-    }
-    return nodeManager->mkFloatingPointType(f.getSize());
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class RoundingModeConstantTypeRule {
+/** Type rule for roundingmode values. */
+class RoundingModeConstantTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("RoundingModeConstantTypeRule");
-
-    // Nothing to check!
-    return nodeManager->roundingModeType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointFPTypeRule {
+/** Type rule for (fp ...) operator. */
+class FloatingPointFPTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointFPTypeRule");
-
-    TypeNode signType = n[0].getType(check);
-    TypeNode exponentType = n[1].getType(check);
-    TypeNode significandType = n[2].getType(check);
-
-    if (!signType.isBitVector() || !exponentType.isBitVector() ||
-        !significandType.isBitVector()) {
-      throw TypeCheckingExceptionPrivate(n,
-                                         "arguments to fp must be bit vectors");
-    }
-
-    unsigned signBits = signType.getBitVectorSize();
-    unsigned exponentBits = exponentType.getBitVectorSize();
-    unsigned significandBits = significandType.getBitVectorSize();
-
-    if (check) {
-      if (signBits != 1) {
-        throw TypeCheckingExceptionPrivate(
-            n, "sign bit vector in fp must be 1 bit long");
-      } else if (!(validExponentSize(exponentBits))) {
-        throw TypeCheckingExceptionPrivate(
-            n, "exponent bit vector in fp is an invalid size");
-      } else if (!(validSignificandSize(significandBits))) {
-        throw TypeCheckingExceptionPrivate(
-            n, "significand bit vector in fp is an invalid size");
-      }
-    }
-
-    // The +1 is for the implicit hidden bit
-    return nodeManager->mkFloatingPointType(exponentBits, significandBits + 1);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointTestTypeRule {
+/**
+ * Type rule for floating-point predicates to check if all arguments are
+ * floating-points of the same sort.
+ */
+class FloatingPointTestTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointTestTypeRule");
-
-    if (check) {
-      TypeNode firstOperand = n[0].getType(check);
-
-      if (!firstOperand.isFloatingPoint()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "floating-point test applied to a non floating-point sort");
-      }
-
-      size_t children = n.getNumChildren();
-      for (size_t i = 1; i < children; ++i) {
-        if (!(n[i].getType(check) == firstOperand)) {
-          throw TypeCheckingExceptionPrivate(
-              n, "floating-point test applied to mixed sorts");
-        }
-      }
-    }
-
-    return nodeManager->booleanType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointOperationTypeRule {
+/**
+ * Type rule for floating-point operators which expect that all operands are
+ * floating-points to check if all operands are floating-points of the same
+ * sort.
+ */
+class FloatingPointOperationTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointOperationTypeRule");
-
-    TypeNode firstOperand = n[0].getType(check);
-
-    if (check) {
-      if (!firstOperand.isFloatingPoint()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "floating-point operation applied to a non floating-point sort");
-      }
-
-      size_t children = n.getNumChildren();
-      for (size_t i = 1; i < children; ++i) {
-        if (!(n[i].getType(check) == firstOperand)) {
-          throw TypeCheckingExceptionPrivate(
-              n, "floating-point test applied to mixed sorts");
-        }
-      }
-    }
-
-    return firstOperand;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointRoundingOperationTypeRule {
+/**
+ * Type rule for floating-point operators which expect a roundingmode as first
+ * operand and floating-points for the remaining operands. Checks if the
+ * floating-point operands are of the same sort.
+ */
+class FloatingPointRoundingOperationTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointRoundingOperationTypeRule");
-
-    if (check) {
-      TypeNode roundingModeType = n[0].getType(check);
-
-      if (!roundingModeType.isRoundingMode()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument must be a rounding mode");
-      }
-    }
-
-    TypeNode firstOperand = n[1].getType(check);
-
-    if (check) {
-      if (!firstOperand.isFloatingPoint()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "floating-point operation applied to a non floating-point sort");
-      }
-
-      size_t children = n.getNumChildren();
-      for (size_t i = 2; i < children; ++i) {
-        if (!(n[i].getType(check) == firstOperand)) {
-          throw TypeCheckingExceptionPrivate(
-              n, "floating-point operation applied to mixed sorts");
-        }
-      }
-    }
-
-    return firstOperand;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointPartialOperationTypeRule {
+/**
+ * Type rule for floating-point partial operators (min, max) which expect that
+ * all operands are floating-points to check if all operands are
+ * floating-points of the same sort.
+ */
+class FloatingPointPartialOperationTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointOperationTypeRule");
-    AlwaysAssert(n.getNumChildren() > 0);
-
-    TypeNode firstOperand = n[0].getType(check);
-
-    if (check) {
-      if (!firstOperand.isFloatingPoint()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "floating-point operation applied to a non floating-point sort");
-      }
-
-      const size_t children = n.getNumChildren();
-      for (size_t i = 1; i < children - 1; ++i) {
-        if (n[i].getType(check) != firstOperand) {
-          throw TypeCheckingExceptionPrivate(
-              n, "floating-point partial operation applied to mixed sorts");
-        }
-      }
-
-      TypeNode UFValueType = n[children - 1].getType(check);
-
-      if (!(UFValueType.isBitVector()) ||
-	  !(UFValueType.getBitVectorSize() == 1)) {
-	throw TypeCheckingExceptionPrivate(
-	    n, "floating-point partial operation final argument must be a bit-vector of length 1");
-      }
-    }
-
-    return firstOperand;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-
-class FloatingPointParametricOpTypeRule {
+/**
+ * Type rule for floating-point parametric operators (to_fp, to_fp_unsigned)
+ * which expect that all operands are floating-points to check if all operands
+ * are floating-points of the same sort.
+ */
+class FloatingPointParametricOpTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointParametricOpTypeRule");
-
-    return nodeManager->builtinOperatorType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Type rule for floating-point to_fp conversion from IEEE bit-vector. */
 class FloatingPointToFPIEEEBitVectorTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToFPIEEEBitVectorTypeRule");
-    AlwaysAssert(n.getNumChildren() == 1);
-
-    FloatingPointToFPIEEEBitVector info =
-        n.getOperator().getConst<FloatingPointToFPIEEEBitVector>();
-
-    if (check) {
-      TypeNode operandType = n[0].getType(check);
-
-      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.getSize().exponentWidth()
-                        + info.getSize().significandWidth()))
-      {
-        throw TypeCheckingExceptionPrivate(
-            n,
-            "conversion to floating-point from bit vector used with bit vector "
-            "length that does not match floating point parameters");
-      }
-    }
-
-    return nodeManager->mkFloatingPointType(info.getSize());
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Type rule for floating-point to_fp conversion from floating-point. */
 class FloatingPointToFPFloatingPointTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToFPFloatingPointTypeRule");
-    AlwaysAssert(n.getNumChildren() == 2);
-
-    FloatingPointToFPFloatingPoint info =
-        n.getOperator().getConst<FloatingPointToFPFloatingPoint>();
-
-    if (check) {
-      TypeNode roundingModeType = n[0].getType(check);
-
-      if (!roundingModeType.isRoundingMode()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument must be a rounding mode");
-      }
-
-      TypeNode operandType = n[1].getType(check);
-
-      if (!(operandType.isFloatingPoint())) {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "conversion to floating-point from "
-                                           "floating-point used with sort "
-                                           "other than floating-point");
-      }
-    }
-
-    return nodeManager->mkFloatingPointType(info.getSize());
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Type rule for floating-point to_fp conversion from real. */
 class FloatingPointToFPRealTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToFPRealTypeRule");
-    AlwaysAssert(n.getNumChildren() == 2);
-
-    FloatingPointToFPReal info =
-        n.getOperator().getConst<FloatingPointToFPReal>();
-
-    if (check) {
-      TypeNode roundingModeType = n[0].getType(check);
-
-      if (!roundingModeType.isRoundingMode()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument must be a rounding mode");
-      }
-
-      TypeNode operandType = n[1].getType(check);
-
-      if (!(operandType.isReal())) {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "conversion to floating-point from "
-                                           "real used with sort other than "
-                                           "real");
-      }
-    }
-
-    return nodeManager->mkFloatingPointType(info.getSize());
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Type rule for floating-point to_fp conversion from signed bit-vector. */
 class FloatingPointToFPSignedBitVectorTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToFPSignedBitVectorTypeRule");
-    AlwaysAssert(n.getNumChildren() == 2);
-
-    FloatingPointToFPSignedBitVector info =
-        n.getOperator().getConst<FloatingPointToFPSignedBitVector>();
-
-    if (check) {
-      TypeNode roundingModeType = n[0].getType(check);
-
-      if (!roundingModeType.isRoundingMode()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument must be a rounding mode");
-      }
-
-      TypeNode operandType = n[1].getType(check);
-
-      if (!(operandType.isBitVector())) {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "conversion to floating-point from "
-                                           "signed bit vector used with sort "
-                                           "other than bit vector");
-      }
-    }
-
-    return nodeManager->mkFloatingPointType(info.getSize());
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Type rule for floating-point to_fp conversion from unsigned bit-vector. */
 class FloatingPointToFPUnsignedBitVectorTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToFPUnsignedBitVectorTypeRule");
-    AlwaysAssert(n.getNumChildren() == 2);
-
-    FloatingPointToFPUnsignedBitVector info =
-        n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>();
-
-    if (check) {
-      TypeNode roundingModeType = n[0].getType(check);
-
-      if (!roundingModeType.isRoundingMode()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument must be a rounding mode");
-      }
-
-      TypeNode operandType = n[1].getType(check);
-
-      if (!(operandType.isBitVector())) {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "conversion to floating-point from "
-                                           "unsigned bit vector used with sort "
-                                           "other than bit vector");
-      }
-    }
-
-    return nodeManager->mkFloatingPointType(info.getSize());
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Generic type rule for floating-point to_fp conversion. */
 class FloatingPointToFPGenericTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToFPGenericTypeRule");
-
-    FloatingPointToFPGeneric info =
-        n.getOperator().getConst<FloatingPointToFPGeneric>();
-
-    if (check) {
-      /* As this is a generic kind intended only for parsing,
-       * the checking here is light.  For better checking, use
-       * expandDefinitions first.
-       */
-
-      size_t children = n.getNumChildren();
-      for (size_t i = 0; i < children; ++i) {
-        n[i].getType(check);
-      }
-    }
-
-    return nodeManager->mkFloatingPointType(info.getSize());
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointToUBVTypeRule {
+/** Type rule for conversion from floating-point to unsigned bit-vector. */
+class FloatingPointToUBVTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToUBVTypeRule");
-    AlwaysAssert(n.getNumChildren() == 2);
-
-    FloatingPointToUBV info = n.getOperator().getConst<FloatingPointToUBV>();
-
-    if (check) {
-      TypeNode roundingModeType = n[0].getType(check);
-
-      if (!roundingModeType.isRoundingMode()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument must be a rounding mode");
-      }
-
-      TypeNode operandType = n[1].getType(check);
-
-      if (!(operandType.isFloatingPoint())) {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "conversion to unsigned bit vector "
-                                           "used with a sort other than "
-                                           "floating-point");
-      }
-    }
-
-    return nodeManager->mkBitVectorType(info.d_bv_size);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointToSBVTypeRule {
+/** Type rule for conversion from floating-point to signed bit-vector. */
+class FloatingPointToSBVTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToSBVTypeRule");
-    AlwaysAssert(n.getNumChildren() == 2);
-
-    FloatingPointToSBV info = n.getOperator().getConst<FloatingPointToSBV>();
-
-    if (check) {
-      TypeNode roundingModeType = n[0].getType(check);
-
-      if (!roundingModeType.isRoundingMode()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument must be a rounding mode");
-      }
-
-      TypeNode operandType = n[1].getType(check);
-
-      if (!(operandType.isFloatingPoint())) {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "conversion to signed bit vector "
-                                           "used with a sort other than "
-                                           "floating-point");
-      }
-    }
-
-    return nodeManager->mkBitVectorType(info.d_bv_size);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointToUBVTotalTypeRule {
+/**
+ * Type rule for conversion from floating-point to unsigned bit-vector (total
+ * version).
+ */
+class FloatingPointToUBVTotalTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToUBVTotalTypeRule");
-    AlwaysAssert(n.getNumChildren() == 3);
-
-    FloatingPointToUBVTotal info = n.getOperator().getConst<FloatingPointToUBVTotal>();
-
-    if (check) {
-      TypeNode roundingModeType = n[0].getType(check);
-
-      if (!roundingModeType.isRoundingMode()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument must be a rounding mode");
-      }
-
-      TypeNode operandType = n[1].getType(check);
-
-      if (!(operandType.isFloatingPoint())) {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "conversion to unsigned bit vector total"
-                                           "used with a sort other than "
-                                           "floating-point");
-      }
-
-      TypeNode defaultValueType = n[2].getType(check);
-
-      if (!(defaultValueType.isBitVector()) ||
-	  !(defaultValueType.getBitVectorSize() == info)) {
-	throw TypeCheckingExceptionPrivate(n,
-					   "conversion to unsigned bit vector total"
-					   "needs a bit vector of the same length"
-					   "as last argument");
-      }
-    }
-
-    return nodeManager->mkBitVectorType(info.d_bv_size);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointToSBVTotalTypeRule {
+/**
+ * Type rule for conversion from floating-point to signed bit-vector (total
+ * version).
+ */
+class FloatingPointToSBVTotalTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToSBVTotalTypeRule");
-    AlwaysAssert(n.getNumChildren() == 3);
-
-    FloatingPointToSBVTotal info = n.getOperator().getConst<FloatingPointToSBVTotal>();
-
-    if (check) {
-      TypeNode roundingModeType = n[0].getType(check);
-
-      if (!roundingModeType.isRoundingMode()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "first argument must be a rounding mode");
-      }
-
-      TypeNode operandType = n[1].getType(check);
-
-      if (!(operandType.isFloatingPoint())) {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "conversion to signed bit vector "
-                                           "used with a sort other than "
-                                           "floating-point");
-      }
-
-      TypeNode defaultValueType = n[2].getType(check);
-
-      if (!(defaultValueType.isBitVector()) ||
-	  !(defaultValueType.getBitVectorSize() == info)) {
-	throw TypeCheckingExceptionPrivate(n,
-					   "conversion to signed bit vector total"
-					   "needs a bit vector of the same length"
-					   "as last argument");
-      }
-    }
-
-    return nodeManager->mkBitVectorType(info.d_bv_size);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointToRealTypeRule {
+/** Type rule for conversion from floating-point to real. */
+class FloatingPointToRealTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToRealTypeRule");
-    AlwaysAssert(n.getNumChildren() == 1);
-
-    if (check) {
-      TypeNode operandType = n[0].getType(check);
-
-      if (!operandType.isFloatingPoint()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "floating-point to real applied to a non floating-point sort");
-      }
-    }
-
-    return nodeManager->realType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class FloatingPointToRealTotalTypeRule {
+/** Type rule for conversion from floating-point to real (total version). */
+class FloatingPointToRealTotalTypeRule
+{
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check) {
-    TRACE("FloatingPointToRealTotalTypeRule");
-    AlwaysAssert(n.getNumChildren() == 2);
-
-    if (check) {
-      TypeNode operandType = n[0].getType(check);
-
-      if (!operandType.isFloatingPoint()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "floating-point to real total applied to a non floating-point sort");
-      }
-
-      TypeNode defaultValueType = n[1].getType(check);
-
-      if (!defaultValueType.isReal()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "floating-point to real total needs a real second argument");
-      }
-
-    }
-
-    return nodeManager->realType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Type rule for floating-point components of bit-width 1. */
 class FloatingPointComponentBit
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TRACE("FloatingPointComponentBit");
-
-    if (check)
-    {
-      TypeNode operandType = n[0].getType(check);
-
-      if (!operandType.isFloatingPoint())
-      {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "floating-point bit component "
-                                           "applied to a non floating-point "
-                                           "sort");
-      }
-      if (!(Theory::isLeafOf(n[0], THEORY_FP)
-            || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
-      {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "floating-point bit component "
-                                           "applied to a non leaf / to_fp leaf "
-                                           "node");
-      }
-    }
-
-    return nodeManager->mkBitVectorType(1);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Type rule for floating-point exponent component. */
 class FloatingPointComponentExponent
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TRACE("FloatingPointComponentExponent");
-
-    TypeNode operandType = n[0].getType(check);
-
-    if (check)
-    {
-      if (!operandType.isFloatingPoint())
-      {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "floating-point exponent component "
-                                           "applied to a non floating-point "
-                                           "sort");
-      }
-      if (!(Theory::isLeafOf(n[0], THEORY_FP)
-            || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
-      {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "floating-point exponent component "
-                                           "applied to a non leaf / to_fp "
-                                           "node");
-      }
-    }
-
-#ifdef CVC4_USE_SYMFPU
-    /* Need to create some symfpu objects as the size of bit-vector
-     * that is needed for this component is dependent on the encoding
-     * used (i.e. whether subnormals are forcibly normalised or not).
-     * 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>();
-    unsigned bw = FloatingPoint::getUnpackedExponentWidth(fps);
-#else
-    unsigned bw = 2;
-#endif
-    return nodeManager->mkBitVectorType(bw);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Type rule for floating-point significand component. */
 class FloatingPointComponentSignificand
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TRACE("FloatingPointComponentSignificand");
-
-    TypeNode operandType = n[0].getType(check);
-
-    if (check)
-    {
-      if (!operandType.isFloatingPoint())
-      {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "floating-point significand "
-                                           "component applied to a non "
-                                           "floating-point sort");
-      }
-      if (!(Theory::isLeafOf(n[0], THEORY_FP)
-            || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
-      {
-        throw TypeCheckingExceptionPrivate(n,
-                                           "floating-point significand "
-                                           "component applied to a non leaf / "
-                                           "to_fp node");
-      }
-    }
-
-#ifdef CVC4_USE_SYMFPU
-    /* As before we need to use some of sympfu. */
-    FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
-    unsigned bw = FloatingPoint::getUnpackedSignificandWidth(fps);
-#else
-    unsigned bw = 1;
-#endif
-    return nodeManager->mkBitVectorType(bw);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/** Type rule for the ROUNDINGMODE_BITBLAST operator. */
 class RoundingModeBitBlast
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TRACE("RoundingModeBitBlast");
-
-    if (check)
-    {
-      TypeNode operandType = n[0].getType(check);
-
-      if (!operandType.isRoundingMode())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "rounding mode bit-blast applied to a non rounding-mode sort");
-      }
-      if (!Theory::isLeafOf(n[0], THEORY_FP))
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "rounding mode bit-blast applied to a non leaf node");
-      }
-    }
-
-    return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES);
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class CardinalityComputer {
-public:
-  inline static Cardinality computeCardinality(TypeNode type) {
-    Assert(type.getKind() == kind::FLOATINGPOINT_TYPE);
-
-    FloatingPointSize fps = type.getConst<FloatingPointSize>();
-
-    /*
-     * 1                    NaN
-     * 2*1                  Infinities
-     * 2*1                  Zeros
-     * 2*2^(s-1)            Subnormal
-     * 2*((2^e)-2)*2^(s-1)  Normal
-     *
-     *  = 1 + 2*2 + 2*((2^e)-1)*2^(s-1)
-     *  =       5 + ((2^e)-1)*2^s
-     */
-
-    Integer significandValues = Integer(2).pow(fps.significandWidth());
-    Integer exponentValues = Integer(2).pow(fps.exponentWidth());
-    exponentValues -= Integer(1);
-
-    return Integer(5) + exponentValues * significandValues;
-  }
-};/* class CardinalityComputer */
-
-
-
+/** Cardinality computation for floating-point sorts. */
+class CardinalityComputer
+{
+ public:
+  static Cardinality computeCardinality(TypeNode type);
+};
 
-}/* CVC4::theory::fp namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace fp
+}  // namespace theory
+}  // namespace CVC4
 
-#endif /* CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */
+#endif