BV: Move implementation of type rules from header to .cpp. (#6360)

3 files changed, 388 insertions, 337 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 81e598f2b..662df7254 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -554,6 +554,7 @@ libcvc4_add_sources(
   theory/bv/theory_bv_rewrite_rules_simplification.h
   theory/bv/theory_bv_rewriter.cpp
   theory/bv/theory_bv_rewriter.h
+  theory/bv/theory_bv_type_rules.cpp
   theory/bv/theory_bv_type_rules.h
   theory/bv/theory_bv_utils.cpp
   theory/bv/theory_bv_utils.h
diff --git a/src/theory/bv/theory_bv_type_rules.cpp b/src/theory/bv/theory_bv_type_rules.cpp
new file mode 100644
index 000000000..304a2b9cf
--- /dev/null
+++ b/src/theory/bv/theory_bv_type_rules.cpp
@@ -0,0 +1,348 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Dejan Jovanovic, Christopher L. Conway
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * Bitvector theory typing rules.
+ */
+
+#include "theory/bv/theory_bv_type_rules.h"
+
+#include <algorithm>
+
+#include "expr/type_node.h"
+#include "util/integer.h"
+
+namespace cvc5 {
+namespace theory {
+namespace bv {
+
+Cardinality CardinalityComputer::computeCardinality(TypeNode type)
+{
+  Assert(type.getKind() == kind::BITVECTOR_TYPE);
+
+  uint32_t size = type.getConst<BitVectorSize>();
+  if (size == 0)
+  {
+    return 0;
+  }
+  return Integer(2).pow(size);
+}
+
+TypeNode BitVectorConstantTypeRule::computeType(NodeManager* nodeManager,
+                                                TNode n,
+                                                bool check)
+{
+  if (check)
+  {
+    if (n.getConst<BitVector>().getSize() == 0)
+    {
+      throw TypeCheckingExceptionPrivate(n, "constant of size 0");
+    }
+  }
+  return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
+}
+
+TypeNode BitVectorFixedWidthTypeRule::computeType(NodeManager* nodeManager,
+                                                  TNode n,
+                                                  bool check)
+{
+  TNode::iterator it = n.begin();
+  TypeNode t = (*it).getType(check);
+  if (check)
+  {
+    if (!t.isBitVector())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+    }
+    TNode::iterator it_end = n.end();
+    for (++it; it != it_end; ++it)
+    {
+      if ((*it).getType(check) != t)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting bit-vector terms of the same width");
+      }
+    }
+  }
+  return t;
+}
+
+TypeNode BitVectorPredicateTypeRule::computeType(NodeManager* nodeManager,
+                                                 TNode n,
+                                                 bool check)
+{
+  if (check)
+  {
+    TypeNode lhsType = n[0].getType(check);
+    if (!lhsType.isBitVector())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+    }
+    TypeNode rhsType = n[1].getType(check);
+    if (lhsType != rhsType)
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting bit-vector terms of the same width");
+    }
+  }
+  return nodeManager->booleanType();
+}
+
+TypeNode BitVectorUnaryPredicateTypeRule::computeType(NodeManager* nodeManager,
+                                                      TNode n,
+                                                      bool check)
+{
+  if (check)
+  {
+    TypeNode type = n[0].getType(check);
+    if (!type.isBitVector())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+    }
+  }
+  return nodeManager->booleanType();
+}
+
+TypeNode BitVectorBVPredTypeRule::computeType(NodeManager* nodeManager,
+                                              TNode n,
+                                              bool check)
+{
+  if (check)
+  {
+    TypeNode lhs = n[0].getType(check);
+    TypeNode rhs = n[1].getType(check);
+    if (!lhs.isBitVector() || lhs != rhs)
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting bit-vector terms of the same width");
+    }
+  }
+  return nodeManager->mkBitVectorType(1);
+}
+
+TypeNode BitVectorConcatTypeRule::computeType(NodeManager* nodeManager,
+                                              TNode n,
+                                              bool check)
+{
+  uint32_t size = 0;
+  for (const auto& child : n)
+  {
+    TypeNode t = child.getType(check);
+    // NOTE: We're throwing a type-checking exception here even
+    // when check is false, bc if we don't check that the arguments
+    // are bit-vectors the result type will be inaccurate
+    if (!t.isBitVector())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+    }
+    size += t.getBitVectorSize();
+  }
+  return nodeManager->mkBitVectorType(size);
+}
+
+TypeNode BitVectorITETypeRule::computeType(NodeManager* nodeManager,
+                                           TNode n,
+                                           bool check)
+{
+  Assert(n.getNumChildren() == 3);
+  TypeNode thenpart = n[1].getType(check);
+  if (check)
+  {
+    TypeNode cond = n[0].getType(check);
+    if (cond != nodeManager->mkBitVectorType(1))
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting condition to be bit-vector term size 1");
+    }
+    TypeNode elsepart = n[2].getType(check);
+    if (thenpart != elsepart)
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting then and else parts to have same type");
+    }
+  }
+  return thenpart;
+}
+
+TypeNode BitVectorBitOfTypeRule::computeType(NodeManager* nodeManager,
+                                             TNode n,
+                                             bool check)
+{
+  if (check)
+  {
+    BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
+    TypeNode t = n[0].getType(check);
+
+    if (!t.isBitVector())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+    }
+    if (info.d_bitIndex >= t.getBitVectorSize())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "extract index is larger than the bitvector size");
+    }
+  }
+  return nodeManager->booleanType();
+}
+
+TypeNode BitVectorExtractTypeRule::computeType(NodeManager* nodeManager,
+                                               TNode n,
+                                               bool check)
+{
+  BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
+
+  // NOTE: We're throwing a type-checking exception here even
+  // if check is false, bc if we allow high < low the resulting
+  // type will be illegal
+  if (extractInfo.d_high < extractInfo.d_low)
+  {
+    throw TypeCheckingExceptionPrivate(
+        n, "high extract index is smaller than the low extract index");
+  }
+
+  if (check)
+  {
+    TypeNode t = n[0].getType(check);
+    if (!t.isBitVector())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+    }
+    if (extractInfo.d_high >= t.getBitVectorSize())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "high extract index is bigger than the size of the bit-vector");
+    }
+  }
+  return nodeManager->mkBitVectorType(extractInfo.d_high - extractInfo.d_low
+                                      + 1);
+}
+
+TypeNode BitVectorRepeatTypeRule::computeType(NodeManager* nodeManager,
+                                              TNode n,
+                                              bool check)
+{
+  TypeNode t = n[0].getType(check);
+  // NOTE: We're throwing a type-checking exception here even
+  // when check is false, bc if the argument isn't a bit-vector
+  // the result type will be inaccurate
+  if (!t.isBitVector())
+  {
+    throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+  }
+  uint32_t repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
+  if (repeatAmount == 0)
+  {
+    throw TypeCheckingExceptionPrivate(n, "expecting number of repeats > 0");
+  }
+  return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
+}
+
+TypeNode BitVectorExtendTypeRule::computeType(NodeManager* nodeManager,
+                                              TNode n,
+                                              bool check)
+{
+  TypeNode t = n[0].getType(check);
+  // NOTE: We're throwing a type-checking exception here even
+  // when check is false, bc if the argument isn't a bit-vector
+  // the result type will be inaccurate
+  if (!t.isBitVector())
+  {
+    throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+  }
+  uint32_t extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND
+                              ? n.getOperator().getConst<BitVectorSignExtend>()
+                              : n.getOperator().getConst<BitVectorZeroExtend>();
+  return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
+}
+
+TypeNode IntToBitVectorOpTypeRule::computeType(NodeManager* nodeManager,
+                                               TNode n,
+                                               bool check)
+{
+  Assert(n.getKind() == kind::INT_TO_BITVECTOR_OP);
+  size_t bvSize = n.getConst<IntToBitVector>();
+  if (bvSize == 0)
+  {
+    throw TypeCheckingExceptionPrivate(n, "expecting bit-width > 0");
+  }
+  return nodeManager->mkFunctionType(nodeManager->integerType(),
+                                     nodeManager->mkBitVectorType(bvSize));
+}
+
+TypeNode BitVectorConversionTypeRule::computeType(NodeManager* nodeManager,
+                                                  TNode n,
+                                                  bool check)
+{
+  if (n.getKind() == kind::BITVECTOR_TO_NAT)
+  {
+    if (check && !n[0].getType(check).isBitVector())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+    }
+    return nodeManager->integerType();
+  }
+
+  Assert(n.getKind() == kind::INT_TO_BITVECTOR);
+  size_t bvSize = n.getOperator().getConst<IntToBitVector>();
+  if (check && !n[0].getType(check).isInteger())
+  {
+    throw TypeCheckingExceptionPrivate(n, "expecting integer term");
+  }
+  return nodeManager->mkBitVectorType(bvSize);
+}
+
+TypeNode BitVectorEagerAtomTypeRule::computeType(NodeManager* nodeManager,
+                                                 TNode n,
+                                                 bool check)
+{
+  if (check)
+  {
+    TypeNode lhsType = n[0].getType(check);
+    if (!lhsType.isBoolean())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting boolean term");
+    }
+  }
+  return nodeManager->booleanType();
+}
+
+TypeNode BitVectorAckermanizationUdivTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  TypeNode lhsType = n[0].getType(check);
+  if (check)
+  {
+    if (!lhsType.isBitVector())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+    }
+  }
+  return lhsType;
+}
+
+TypeNode BitVectorAckermanizationUremTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  TypeNode lhsType = n[0].getType(check);
+  if (check)
+  {
+    if (!lhsType.isBitVector())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+    }
+  }
+  return lhsType;
+}
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 3c3ae0780..6594e9fa7 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -13,14 +13,17 @@
  * Bitvector theory typing rules.
  */
 
-#include <algorithm>
-
 #include "cvc5_private.h"
 
 #ifndef CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
 #define CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
 
+#include "expr/node.h"
+
 namespace cvc5 {
+
+class TypeNode;
+
 namespace theory {
 namespace bv {
 
@@ -29,137 +32,44 @@ namespace bv {
 class CardinalityComputer
 {
  public:
-  inline static Cardinality computeCardinality(TypeNode type)
-  {
-    Assert(type.getKind() == kind::BITVECTOR_TYPE);
-
-    unsigned size = type.getConst<BitVectorSize>();
-    if (size == 0)
-    {
-      return 0;
-    }
-    Integer i = Integer(2).pow(size);
-    return i;
-  }
-}; /* class CardinalityComputer */
+  static Cardinality computeCardinality(TypeNode type);
+};
 
 /* -------------------------------------------------------------------------- */
 
 class BitVectorConstantTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      if (n.getConst<BitVector>().getSize() == 0)
-      {
-        throw TypeCheckingExceptionPrivate(n, "constant of size 0");
-      }
-    }
-    return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
-  }
-}; /* class BitVectorConstantTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 /* -------------------------------------------------------------------------- */
 
 class BitVectorFixedWidthTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TNode::iterator it = n.begin();
-    TypeNode t = (*it).getType(check);
-    if (check)
-    {
-      if (!t.isBitVector())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
-      }
-      TNode::iterator it_end = n.end();
-      for (++it; it != it_end; ++it)
-      {
-        if ((*it).getType(check) != t)
-        {
-          throw TypeCheckingExceptionPrivate(
-              n, "expecting bit-vector terms of the same width");
-        }
-      }
-    }
-    return t;
-  }
-}; /* class BitVectorFixedWidthTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 /* -------------------------------------------------------------------------- */
 
 class BitVectorPredicateTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      TypeNode lhsType = n[0].getType(check);
-      if (!lhsType.isBitVector())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
-      }
-      TypeNode rhsType = n[1].getType(check);
-      if (lhsType != rhsType)
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting bit-vector terms of the same width");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-}; /* class BitVectorPredicateTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class BitVectorUnaryPredicateTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      TypeNode type = n[0].getType(check);
-      if (!type.isBitVector())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-}; /* class BitVectorUnaryPredicateTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class BitVectorBVPredTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      TypeNode lhs = n[0].getType(check);
-      TypeNode rhs = n[1].getType(check);
-      if (!lhs.isBitVector() || lhs != rhs)
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting bit-vector terms of the same width");
-      }
-    }
-    return nodeManager->mkBitVectorType(1);
-  }
-}; /* class BitVectorBVPredTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 /* -------------------------------------------------------------------------- */
 /* non-parameterized operator kinds                                           */
@@ -168,56 +78,14 @@ class BitVectorBVPredTypeRule
 class BitVectorConcatTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    unsigned size = 0;
-    TNode::iterator it = n.begin();
-    TNode::iterator it_end = n.end();
-    for (; it != it_end; ++it)
-    {
-      TypeNode t = (*it).getType(check);
-      // NOTE: We're throwing a type-checking exception here even
-      // when check is false, bc if we don't check that the arguments
-      // are bit-vectors the result type will be inaccurate
-      if (!t.isBitVector())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
-      }
-      size += t.getBitVectorSize();
-    }
-    return nodeManager->mkBitVectorType(size);
-  }
-}; /* class BitVectorConcatTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class BitVectorITETypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getNumChildren() == 3);
-    TypeNode thenpart = n[1].getType(check);
-    if (check)
-    {
-      TypeNode cond = n[0].getType(check);
-      if (cond != nodeManager->mkBitVectorType(1))
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting condition to be bit-vector term size 1");
-      }
-      TypeNode elsepart = n[2].getType(check);
-      if (thenpart != elsepart)
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting then and else parts to have same type");
-      }
-    }
-    return thenpart;
-  }
-}; /* class BitVectorITETypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 /* -------------------------------------------------------------------------- */
 /* parameterized operator kinds                                               */
@@ -226,165 +94,38 @@ class BitVectorITETypeRule
 class BitVectorBitOfTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
-      TypeNode t = n[0].getType(check);
-
-      if (!t.isBitVector())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
-      }
-      if (info.d_bitIndex >= t.getBitVectorSize())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "extract index is larger than the bitvector size");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-}; /* class BitVectorBitOfTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class BitVectorExtractTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
-
-    // NOTE: We're throwing a type-checking exception here even
-    // if check is false, bc if we allow high < low the resulting
-    // type will be illegal
-    if (extractInfo.d_high < extractInfo.d_low)
-    {
-      throw TypeCheckingExceptionPrivate(
-          n, "high extract index is smaller than the low extract index");
-    }
-
-    if (check)
-    {
-      TypeNode t = n[0].getType(check);
-      if (!t.isBitVector())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
-      }
-      if (extractInfo.d_high >= t.getBitVectorSize())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "high extract index is bigger than the size of the bit-vector");
-      }
-    }
-    return nodeManager->mkBitVectorType(extractInfo.d_high - extractInfo.d_low
-                                        + 1);
-  }
-}; /* class BitVectorExtractTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class BitVectorRepeatTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TypeNode t = n[0].getType(check);
-    // NOTE: We're throwing a type-checking exception here even
-    // when check is false, bc if the argument isn't a bit-vector
-    // the result type will be inaccurate
-    if (!t.isBitVector())
-    {
-      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
-    }
-    unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
-    if (repeatAmount == 0)
-    {
-      throw TypeCheckingExceptionPrivate(n, "expecting number of repeats > 0");
-    }
-    return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
-  }
-}; /* class BitVectorRepeatTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class BitVectorExtendTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TypeNode t = n[0].getType(check);
-    // NOTE: We're throwing a type-checking exception here even
-    // when check is false, bc if the argument isn't a bit-vector
-    // the result type will be inaccurate
-    if (!t.isBitVector())
-    {
-      throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
-    }
-    unsigned extendAmount =
-        n.getKind() == kind::BITVECTOR_SIGN_EXTEND
-            ? (unsigned)n.getOperator().getConst<BitVectorSignExtend>()
-            : (unsigned)n.getOperator().getConst<BitVectorZeroExtend>();
-    return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
-  }
-}; /* class BitVectorExtendTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class IntToBitVectorOpTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (n.getKind() == kind::INT_TO_BITVECTOR_OP)
-    {
-      size_t bvSize = n.getConst<IntToBitVector>();
-      if (bvSize == 0)
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-width > 0");
-      }
-      return nodeManager->mkFunctionType(nodeManager->integerType(),
-                                         nodeManager->mkBitVectorType(bvSize));
-    }
-
-    InternalError()
-        << "bv-conversion typerule invoked for non-bv-conversion kind";
-  }
-}; /* class IntToBitVectorOpTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class BitVectorConversionTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (n.getKind() == kind::BITVECTOR_TO_NAT)
-    {
-      if (check && !n[0].getType(check).isBitVector())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
-      }
-      return nodeManager->integerType();
-    }
-
-    if (n.getKind() == kind::INT_TO_BITVECTOR)
-    {
-      size_t bvSize = n.getOperator().getConst<IntToBitVector>();
-      if (check && !n[0].getType(check).isInteger())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting integer term");
-      }
-      return nodeManager->mkBitVectorType(bvSize);
-    }
-
-    InternalError()
-        << "bv-conversion typerule invoked for non-bv-conversion kind";
-  }
-}; /* class BitVectorConversionTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 /* -------------------------------------------------------------------------- */
 /* internal                                                                   */
@@ -393,59 +134,20 @@ class BitVectorConversionTypeRule
 class BitVectorEagerAtomTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      TypeNode lhsType = n[0].getType(check);
-      if (!lhsType.isBoolean())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting boolean term");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-}; /* class BitVectorEagerAtomTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class BitVectorAckermanizationUdivTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TypeNode lhsType = n[0].getType(check);
-    if (check)
-    {
-      if (!lhsType.isBitVector())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
-      }
-    }
-    return lhsType;
-  }
-}; /* class BitVectorAckermanizationUdivTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 class BitVectorAckermanizationUremTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TypeNode lhsType = n[0].getType(check);
-    if (check)
-    {
-      if (!lhsType.isBitVector())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
-      }
-    }
-    return lhsType;
-  }
-}; /* class BitVectorAckermanizationUremTypeRule */
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
 
 }  // namespace bv
 }  // namespace theory