Move function definitions from metakind.h to cpp (#218)

4 files changed, 227 insertions, 164 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 06a252b3c..bf4ad9acd 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -69,6 +69,7 @@ nodist_libexpr_la_SOURCES = \
 	kind.h \
 	kind.cpp \
 	metakind.h \
+	metakind.cpp \
 	type_properties.h \
 	expr.h \
 	expr.cpp \
@@ -86,6 +87,7 @@ EXTRA_DIST = \
 	kind_template.h \
 	kind_template.cpp \
 	metakind_template.h \
+	metakind_template.cpp \
 	type_properties_template.h \
 	expr_manager_template.h \
 	expr_manager_template.cpp \
@@ -109,6 +111,7 @@ BUILT_SOURCES = \
 	kind.h \
 	kind.cpp \
 	metakind.h \
+	metakind.cpp \
 	type_properties.h \
 	expr.h \
 	expr.cpp \
@@ -121,6 +124,7 @@ CLEANFILES = \
 	kind.h \
 	kind.cpp \
 	metakind.h \
+	metakind.cpp \
 	expr.h \
 	expr.cpp \
 	expr_manager.h \
@@ -162,6 +166,14 @@ metakind.h: metakind_template.h mkmetakind @top_builddir@/src/expr/.subdirs $(if
 		`cat @top_builddir@/src/expr/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
+metakind.cpp: metakind_template.cpp mkmetakind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds
+	$(AM_V_at)chmod +x @srcdir@/mkmetakind
+	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
+	$(AM_V_GEN)(@srcdir@/mkmetakind \
+		$< \
+		`cat @top_builddir@/src/expr/.subdirs` \
+	> $@) || (rm -f $@ && exit 1)
+
 type_properties.h: type_properties_template.h mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkkind
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp
new file mode 100644
index 000000000..3e262db8c
--- /dev/null
+++ b/src/expr/metakind_template.cpp
@@ -0,0 +1,176 @@
+#include "expr/metakind.h"
+
+#include <iostream>
+
+namespace CVC4 {
+namespace kind {
+
+/**
+ * Get the metakind for a particular kind.
+ */
+MetaKind metaKindOf(Kind k) {
+  static const MetaKind metaKinds[] = {
+    metakind::INVALID, /* UNDEFINED_KIND */
+    metakind::INVALID, /* NULL_EXPR */
+${metakind_kinds}
+    metakind::INVALID /* LAST_KIND */
+  };/* metaKinds[] */
+
+  Assert(k >= kind::NULL_EXPR && k < kind::LAST_KIND);
+
+  // We've asserted that k >= NULL_EXPR (which is 0), but we still
+  // handle the UNDEFINED_KIND (-1) case.  If we don't, the compiler
+  // emits warnings for non-assertion builds, since the check isn't done.
+  return metaKinds[k + 1];
+}/* metaKindOf(k) */
+
+}/* CVC4::kind namespace */
+
+namespace expr {
+
+${metakind_constantMaps}
+
+}/* CVC4::expr namespace */
+
+namespace kind {
+namespace metakind {
+
+size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv) {
+  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
+
+  switch(nv->d_kind) {
+${metakind_constHashes}
+  default:
+    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
+  }
+}
+
+template <bool pool>
+bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1,
+                               const ::CVC4::expr::NodeValue* nv2) {
+  if(nv1->d_kind != nv2->d_kind) {
+    return false;
+  }
+
+  if(nv1->getMetaKind() == kind::metakind::CONSTANT) {
+    switch(nv1->d_kind) {
+${metakind_compares}
+    default:
+      Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind));
+    }
+  }
+
+  if(nv1->d_nchildren != nv2->d_nchildren) {
+    return false;
+  }
+
+  ::CVC4::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
+  ::CVC4::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
+  ::CVC4::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();
+
+  while(i != i_end) {
+    if((*i) != (*j)) {
+      return false;
+    }
+    ++i;
+    ++j;
+  }
+
+  return true;
+}
+
+template bool NodeValueCompare::compare<true>(const ::CVC4::expr::NodeValue* nv1,
+                                              const ::CVC4::expr::NodeValue* nv2);
+template bool NodeValueCompare::compare<false>(const ::CVC4::expr::NodeValue* nv1,
+                                               const ::CVC4::expr::NodeValue* nv2);
+
+void NodeValueConstPrinter::toStream(std::ostream& out,
+                                            const ::CVC4::expr::NodeValue* nv) {
+  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
+
+  switch(nv->d_kind) {
+${metakind_constPrinters}
+  default:
+    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
+  }
+}
+
+void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) {
+  toStream(out, n.d_nv);
+}
+
+// The reinterpret_cast of d_children to various constant payload types
+// in deleteNodeValueConstant(), below, can flag a "strict aliasing"
+// warning; it should actually be okay, because we never access the
+// embedded constant as a NodeValue* child, and never access an embedded
+// NodeValue* child as a constant.
+#pragma GCC diagnostic ignored "-Wstrict-aliasing"
+
+/**
+ * Cleanup to be performed when a NodeValue zombie is collected, and
+ * it has CONSTANT metakind.  This calls the destructor for the underlying
+ * C++ type representing the constant value.  See
+ * NodeManager::reclaimZombies() for more information.
+ *
+ * This doesn't support "non-inlined" NodeValues, which shouldn't need this
+ * kind of cleanup.
+ */
+void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv) {
+  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
+
+  switch(nv->d_kind) {
+${metakind_constDeleters}
+  default:
+    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
+  }
+}
+
+// re-enable the strict-aliasing warning
+# pragma GCC diagnostic warning "-Wstrict-aliasing"
+
+unsigned getLowerBoundForKind(::CVC4::Kind k) {
+  static const unsigned lbs[] = {
+    0, /* NULL_EXPR */
+${metakind_lbchildren}
+
+    0 /* LAST_KIND */
+  };
+
+  return lbs[k];
+}
+
+unsigned getUpperBoundForKind(::CVC4::Kind k) {
+  static const unsigned ubs[] = {
+    0, /* NULL_EXPR */
+${metakind_ubchildren}
+
+    0, /* LAST_KIND */
+  };
+
+  return ubs[k];
+}
+
+}/* CVC4::metakind namespace */
+
+/**
+ * Map a kind of the operator to the kind of the enclosing expression. For
+ * example, since the kind of functions is just VARIABLE, it should map
+ * VARIABLE to APPLY_UF.
+ */
+Kind operatorToKind(::CVC4::expr::NodeValue* nv) {
+  if(nv->getKind() == kind::BUILTIN) {
+    return nv->getConst<Kind>();
+  } else if(nv->getKind() == kind::LAMBDA) {
+    return kind::APPLY_UF;
+  }
+
+  switch(Kind k CVC4_UNUSED = nv->getKind()) {
+${metakind_operatorKinds}
+
+  default:
+    return kind::UNDEFINED_KIND;  /* LAST_KIND */
+  };
+}
+
+}/* CVC4::kind namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index b2e88c1ff..6f7aef5ed 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -19,7 +19,7 @@
 #ifndef __CVC4__KIND__METAKIND_H
 #define __CVC4__KIND__METAKIND_H
 
-#include <iostream>
+#include <iosfwd>
 
 #include "base/cvc4_assert.h"
 #include "expr/kind.h"
@@ -81,9 +81,9 @@ struct NodeValueConstCompare {
 
 struct NodeValueCompare {
   template <bool pool>
-  inline static bool compare(const ::CVC4::expr::NodeValue* nv1,
-                             const ::CVC4::expr::NodeValue* nv2);
-  inline static size_t constHash(const ::CVC4::expr::NodeValue* nv);
+  static bool compare(const ::CVC4::expr::NodeValue* nv1,
+                      const ::CVC4::expr::NodeValue* nv2);
+  static size_t constHash(const ::CVC4::expr::NodeValue* nv);
 };/* struct NodeValueCompare */
 
 /**
@@ -111,28 +111,9 @@ typedef ::CVC4::kind::metakind::MetaKind_t MetaKind;
 /**
  * Get the metakind for a particular kind.
  */
-static inline MetaKind metaKindOf(Kind k) {
-  static const MetaKind metaKinds[] = {
-    metakind::INVALID, /* UNDEFINED_KIND */
-    metakind::INVALID, /* NULL_EXPR */
-${metakind_kinds}
-    metakind::INVALID /* LAST_KIND */
-  };/* metaKinds[] */
-
-  Assert(k >= kind::NULL_EXPR && k < kind::LAST_KIND);
-
-  // We've asserted that k >= NULL_EXPR (which is 0), but we still
-  // handle the UNDEFINED_KIND (-1) case.  If we don't, the compiler
-  // emits warnings for non-assertion builds, since the check isn't done.
-  return metaKinds[k + 1];
-}/* metaKindOf(k) */
-
+MetaKind metaKindOf(Kind k);
 }/* CVC4::kind namespace */
 
-namespace expr {
-  class NodeValue;
-}/* CVC4::expr namespace */
-
 namespace kind {
 namespace metakind {
 
@@ -169,6 +150,11 @@ ${metakind_includes}
 #ifdef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
 
 namespace CVC4 {
+
+namespace expr {
+${metakind_getConst_decls}
+}/* CVC4::expr namespace */
+
 namespace kind {
 namespace metakind {
 
@@ -197,80 +183,14 @@ inline size_t NodeValueConstCompare<k, pool>::constHash(const ::CVC4::expr::Node
   return nv->getConst<T>().hash();
 }
 
-${metakind_constantMaps}
-
-template <bool pool>
-inline bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1,
-                                      const ::CVC4::expr::NodeValue* nv2) {
-  if(nv1->d_kind != nv2->d_kind) {
-    return false;
-  }
-
-  if(nv1->getMetaKind() == kind::metakind::CONSTANT) {
-    switch(nv1->d_kind) {
-${metakind_compares}
-    default:
-      Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind));
-    }
-  }
-
-  if(nv1->d_nchildren != nv2->d_nchildren) {
-    return false;
-  }
-
-  ::CVC4::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
-  ::CVC4::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
-  ::CVC4::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();
-
-  while(i != i_end) {
-    if((*i) != (*j)) {
-      return false;
-    }
-    ++i;
-    ++j;
-  }
-
-  return true;
-}
-
-inline size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv) {
-  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
-
-  switch(nv->d_kind) {
-${metakind_constHashes}
-  default:
-    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
-  }
-}
+${metakind_constantMaps_decls}
 
 struct NodeValueConstPrinter {
-  inline static void toStream(std::ostream& out,
+  static void toStream(std::ostream& out,
                               const ::CVC4::expr::NodeValue* nv);
-  inline static void toStream(std::ostream& out, TNode n);
+  static void toStream(std::ostream& out, TNode n);
 };
 
-inline void NodeValueConstPrinter::toStream(std::ostream& out,
-                                            const ::CVC4::expr::NodeValue* nv) {
-  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
-
-  switch(nv->d_kind) {
-${metakind_constPrinters}
-  default:
-    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
-  }
-}
-
-inline void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) {
-  toStream(out, n.d_nv);
-}
-
-// The reinterpret_cast of d_children to various constant payload types
-// in deleteNodeValueConstant(), below, can flag a "strict aliasing"
-// warning; it should actually be okay, because we never access the
-// embedded constant as a NodeValue* child, and never access an embedded
-// NodeValue* child as a constant.
-#pragma GCC diagnostic ignored "-Wstrict-aliasing"
-
 /**
  * Cleanup to be performed when a NodeValue zombie is collected, and
  * it has CONSTANT metakind.  This calls the destructor for the underlying
@@ -280,40 +200,10 @@ inline void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) {
  * This doesn't support "non-inlined" NodeValues, which shouldn't need this
  * kind of cleanup.
  */
-inline void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv) {
-  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
-
-  switch(nv->d_kind) {
-${metakind_constDeleters}
-  default:
-    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
-  }
-}
+void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv);
 
-// re-enable the strict-aliasing warning
-# pragma GCC diagnostic warning "-Wstrict-aliasing"
-
-inline unsigned getLowerBoundForKind(::CVC4::Kind k) {
-  static const unsigned lbs[] = {
-    0, /* NULL_EXPR */
-${metakind_lbchildren}
-
-    0 /* LAST_KIND */
-  };
-
-  return lbs[k];
-}
-
-inline unsigned getUpperBoundForKind(::CVC4::Kind k) {
-  static const unsigned ubs[] = {
-    0, /* NULL_EXPR */
-${metakind_ubchildren}
-
-    0, /* LAST_KIND */
-  };
-
-  return ubs[k];
-}
+unsigned getLowerBoundForKind(::CVC4::Kind k);
+unsigned getUpperBoundForKind(::CVC4::Kind k);
 
 }/* CVC4::kind::metakind namespace */
 
@@ -322,24 +212,11 @@ ${metakind_ubchildren}
  * example, since the kind of functions is just VARIABLE, it should map
  * VARIABLE to APPLY_UF.
  */
-static inline Kind operatorToKind(::CVC4::expr::NodeValue* nv) {
-  if(nv->getKind() == kind::BUILTIN) {
-    return nv->getConst<Kind>();
-  } else if(nv->getKind() == kind::LAMBDA) {
-    return kind::APPLY_UF;
-  }
-
-  switch(Kind k CVC4_UNUSED = nv->getKind()) {
-${metakind_operatorKinds}
-
-  default:
-    return kind::UNDEFINED_KIND;  /* LAST_KIND */
-  };
-}
+Kind operatorToKind(::CVC4::expr::NodeValue* nv);
 
 }/* CVC4::kind namespace */
 
-#line 343 "${template}"
+#line 220 "${template}"
 
 namespace theory {
 
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 19e6e2244..1cfcf253a 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -229,17 +229,29 @@ function constant {
     echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFunction)" >&2
   fi
 
-  if [ -n "$4" ]; then
+  # Avoid including the same header multiple times
+  if [ -n "$4" ] && [[ "${metakind_includes}" != *"#include \"$4\""* ]]; then
     metakind_includes="${metakind_includes}
 #include \"$4\""
   fi
   register_metakind CONSTANT "$1" 0
-  metakind_constantMaps="${metakind_constantMaps}
-}/* CVC4::kind::metakind namespace */
-}/* CVC4::kind namespace */
-
-namespace expr {
+  metakind_getConst_decls="${metakind_getConst_decls}
+template <>
+$2 const& NodeValue::getConst< $2 >() const;
+"
+  metakind_constantMaps_decls="${metakind_constantMaps_decls}
+template <>
+struct ConstantMap< $2 > {
+  // typedef $theory_class OwningTheory;
+  enum { kind = ::CVC4::kind::$1 };
+};/* ConstantMap< $2 > */
 
+template <>
+struct ConstantMapReverse< ::CVC4::kind::$1 > {
+  typedef $2 T;
+};/* ConstantMapReverse< ::CVC4::kind::$1 > */
+  "
+  metakind_constantMaps="${metakind_constantMaps}
 // The reinterpret_cast of d_children to \"$2 const*\"
 // flags a \"strict aliasing\" warning; it's okay, because we never access
 // the embedded constant as a NodeValue* child, and never access an embedded
@@ -247,7 +259,7 @@ namespace expr {
 #pragma GCC diagnostic ignored \"-Wstrict-aliasing\"
 
 template <>
-inline $2 const& NodeValue::getConst< $2 >() const {
+$2 const& NodeValue::getConst< $2 >() const {
   AssertArgument(getKind() == ::CVC4::kind::$1, *this,
                  \"Improper kind for getConst<$2>()\");
   // To support non-inlined CONSTANT-kinded NodeValues (those that are
@@ -261,22 +273,6 @@ inline $2 const& NodeValue::getConst< $2 >() const {
 // re-enable the warning
 #pragma GCC diagnostic warning \"-Wstrict-aliasing\"
 
-}/* CVC4::expr namespace */
-
-namespace kind {
-namespace metakind {
-
-template <>
-struct ConstantMap< $2 > {
-  // typedef $theory_class OwningTheory;
-  enum { kind = ::CVC4::kind::$1 };
-};/* ConstantMap< $2 > */
-
-template <>
-struct ConstantMapReverse< ::CVC4::kind::$1 > {
-  typedef $2 T;
-};/* ConstantMapReverse< ::CVC4::kind::$1 > */
-
 "
   metakind_compares="${metakind_compares}
     case kind::$1:
@@ -423,6 +419,8 @@ for var in \
     metakind_includes \
     metakind_kinds \
     metakind_constantMaps \
+    metakind_constantMaps_decls \
+    metakind_getConst_decls \
     metakind_compares \
     metakind_constHashes \
     metakind_constPrinters \