Move function definitions from kind.h to kind.cpp (#217)

3 files changed, 117 insertions, 81 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 2400468a2..06a252b3c 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -67,6 +67,7 @@ libexpr_la_SOURCES = \
 
 nodist_libexpr_la_SOURCES = \
 	kind.h \
+	kind.cpp \
 	metakind.h \
 	type_properties.h \
 	expr.h \
@@ -83,6 +84,7 @@ EXTRA_DIST = \
 	datatype.i \
 	emptyset.i \
 	kind_template.h \
+	kind_template.cpp \
 	metakind_template.h \
 	type_properties_template.h \
 	expr_manager_template.h \
@@ -105,6 +107,7 @@ EXTRA_DIST = \
 
 BUILT_SOURCES = \
 	kind.h \
+	kind.cpp \
 	metakind.h \
 	type_properties.h \
 	expr.h \
@@ -116,6 +119,7 @@ BUILT_SOURCES = \
 
 CLEANFILES = \
 	kind.h \
+	kind.cpp \
 	metakind.h \
 	expr.h \
 	expr.cpp \
@@ -142,6 +146,14 @@ kind.h: kind_template.h mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_
 		`cat @top_builddir@/src/expr/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
+kind.cpp: kind_template.cpp 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
+	$(AM_V_GEN)(@srcdir@/mkkind \
+		$< \
+		`cat @top_builddir@/src/expr/.subdirs` \
+	> $@) || (rm -f $@ && exit 1)
+
 metakind.h: metakind_template.h 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
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
new file mode 100644
index 000000000..5f92af622
--- /dev/null
+++ b/src/expr/kind_template.cpp
@@ -0,0 +1,95 @@
+#include "expr/kind.h"
+
+namespace CVC4 {
+namespace kind {
+
+std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
+  using namespace CVC4::kind;
+
+  switch(k) {
+
+  /* special cases */
+  case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
+  case NULL_EXPR: out << "NULL"; break;
+${kind_printers}
+  case LAST_KIND: out << "LAST_KIND"; break;
+  default: out << "UNKNOWNKIND!" << int(k); break;
+  }
+
+  return out;
+}
+
+/** Returns true if the given kind is associative. This is used by ExprManager to
+ * decide whether it's safe to modify big expressions by changing the grouping of
+ * the arguments. */
+/* TODO: This could be generated. */
+bool isAssociative(::CVC4::Kind k) {
+  switch(k) {
+  case kind::AND:
+  case kind::OR:
+  case kind::MULT:
+  case kind::PLUS:
+    return true;
+
+  default:
+    return false;
+  }
+}
+
+std::string kindToString(::CVC4::Kind k) {
+  std::stringstream ss;
+  ss << k;
+  return ss.str();
+}
+
+}/* CVC4::kind namespace */
+
+std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
+  switch(typeConstant) {
+${type_constant_descriptions}
+#line 51 "${template}"
+  default:
+    out << "UNKNOWN_TYPE_CONSTANT";
+    break;
+  }
+  return out;
+}
+
+namespace theory {
+
+std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
+  switch(theoryId) {
+${theory_descriptions}
+#line 64 "${template}"
+  default:
+    out << "UNKNOWN_THEORY";
+    break;
+  }
+  return out;
+}
+
+TheoryId kindToTheoryId(::CVC4::Kind k) {
+  switch(k) {
+  case kind::UNDEFINED_KIND:
+  case kind::NULL_EXPR:
+    break;
+${kind_to_theory_id}
+#line 78 "${template}"
+  case kind::LAST_KIND:
+    break;
+  }
+  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
+}
+
+TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
+  switch(typeConstant) {
+${type_constant_to_theory_id}
+#line 88 "${template}"
+  case LAST_TYPE:
+    break;
+  }
+  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
+}
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index d8c96ffa1..4f5b1eecd 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -20,7 +20,6 @@
 #define __CVC4__KIND_H
 
 #include <iosfwd>
-#include <sstream>
 
 #include "base/exception.h"
 
@@ -43,47 +42,16 @@ typedef ::CVC4::kind::Kind_t Kind;
 
 namespace kind {
 
-inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
-  using namespace CVC4::kind;
+std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
 
-  switch(k) {
-
-  /* special cases */
-  case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
-  case NULL_EXPR: out << "NULL"; break;
-${kind_printers}
-  case LAST_KIND: out << "LAST_KIND"; break;
-  default: out << "UNKNOWNKIND!" << int(k); break;
-  }
-
-  return out;
-}
-
-#line 64 "${template}"
+#line 48 "${template}"
 
 /** Returns true if the given kind is associative. This is used by ExprManager to
  * decide whether it's safe to modify big expressions by changing the grouping of
  * the arguments. */
 /* TODO: This could be generated. */
-inline bool isAssociative(::CVC4::Kind k) {
-  switch(k) {
-  case kind::AND:
-  case kind::OR:
-  case kind::MULT:
-  case kind::PLUS:
-    return true;
-
-  default:
-    return false;
-  }
-}
-
-inline std::string kindToString(::CVC4::Kind k) {
-  std::stringstream ss;
-  ss << k;
-  return ss.str();
-}
+bool isAssociative(::CVC4::Kind k) CVC4_PUBLIC;
+std::string kindToString(::CVC4::Kind k) CVC4_PUBLIC;
 
 struct KindHashFunction {
   inline size_t operator()(::CVC4::Kind k) const {
@@ -98,7 +66,7 @@ struct KindHashFunction {
  */
 enum TypeConstant {
 ${type_constant_list}
-#line 102 "${template}"
+#line 70 "${template}"
   LAST_TYPE
 };/* enum TypeConstant */
 
@@ -111,22 +79,13 @@ struct TypeConstantHashFunction {
   }
 };/* struct TypeConstantHashFunction */
 
-inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
-  switch(typeConstant) {
-${type_constant_descriptions}
-#line 118 "${template}"
-  default:
-    out << "UNKNOWN_TYPE_CONSTANT";
-    break;
-  }
-  return out;
-}
+std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
 
 namespace theory {
 
 enum TheoryId {
 ${theory_enum}
-#line 130 "${template}"
+#line 89 "${template}"
   THEORY_LAST
 };/* enum TheoryId */
 
@@ -137,39 +96,9 @@ inline TheoryId& operator ++ (TheoryId& id) {
   return id = static_cast<TheoryId>(((int)id) + 1);
 }
 
-inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
-  switch(theoryId) {
-${theory_descriptions}
-#line 144 "${template}"
-  default:
-    out << "UNKNOWN_THEORY";
-    break;
-  }
-  return out;
-}
-
-inline TheoryId kindToTheoryId(::CVC4::Kind k) {
-  switch(k) {
-  case kind::UNDEFINED_KIND:
-  case kind::NULL_EXPR:
-    break;
-${kind_to_theory_id}
-#line 158 "${template}"
-  case kind::LAST_KIND:
-    break;
-  }
-  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
-}
-
-inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
-  switch(typeConstant) {
-${type_constant_to_theory_id}
-#line 168 "${template}"
-  case LAST_TYPE:
-    break;
-  }
-  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
-}
+std::ostream& operator<<(std::ostream& out, TheoryId theoryId);
+TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC;
+TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant);
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */