3 files changed, 38 insertions, 15 deletions

diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index 77468687c..d3af9a836 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -20,19 +20,24 @@
 namespace CVC4 {
 namespace kind {
 
-std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
+const char* toString(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;
+  switch (k)
+  {
+    /* special cases */
+    case UNDEFINED_KIND: return "UNDEFINED_KIND";
+    case NULL_EXPR: return "NULL";
+    ${kind_printers}
+    case LAST_KIND: return "LAST_KIND";
+    default: return "?";
   }
+}
 
+std::ostream& operator<<(std::ostream& out, CVC4::Kind k)
+{
+  out << toString(k);
   return out;
 }
 
@@ -64,7 +69,7 @@ std::string kindToString(::CVC4::Kind k) {
 std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
   switch(typeConstant) {
 ${type_constant_descriptions}
-#line 68 "${template}"
+#line 73 "${template}"
   default:
     out << "UNKNOWN_TYPE_CONSTANT";
     break;
@@ -80,7 +85,7 @@ TheoryId kindToTheoryId(::CVC4::Kind k) {
   case kind::NULL_EXPR:
     break;
 ${kind_to_theory_id}
-#line 84 "${template}"
+#line 89 "${template}"
   case kind::LAST_KIND:
     break;
   }
@@ -92,7 +97,7 @@ TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
   switch (typeConstant)
   {
 ${type_constant_to_theory_id}
-#line 96 "${template}"
+#line 101 "${template}"
     case LAST_TYPE: break;
   }
   throw IllegalArgumentException(
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index da8e48a6f..50e2f372c 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -43,9 +43,27 @@ typedef ::CVC4::kind::Kind_t Kind;
 
 namespace kind {
 
+/**
+ * Converts an kind to a string. Note: This function is also used in
+ * `safe_print()`. Changing this functions name or signature will result in
+ * `safe_print()` printing "<unsupported>" instead of the proper strings for
+ * the enum values.
+ *
+ * @param k The kind
+ * @return The name of the kind
+ */
+const char* toString(CVC4::Kind k);
+
+/**
+ * Writes a kind name to a stream.
+ *
+ * @param out The stream to write to
+ * @param k The kind to write to the stream
+ * @return The stream
+ */
 std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
 
-#line 49 "${template}"
+#line 67 "${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
@@ -68,7 +86,7 @@ struct KindHashFunction {
 enum CVC4_PUBLIC TypeConstant
 {
   ${type_constant_list}
-#line 72 "${template}"
+#line 90 "${template}"
   LAST_TYPE
 }; /* enum TypeConstant */
 
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 8e45b94ba..fbf37eff4 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -341,7 +341,7 @@ function register_kind {
 
   kind_decls="${kind_decls}  $r, /**< $comment ($register_kind_counter) */
 "
-  kind_printers="${kind_printers}  case $r: out << \"$r\"; break;
+  kind_printers="${kind_printers}  case $r: return \"$r\";
 "
   kind_to_theory_id="${kind_to_theory_id}  case kind::$r: return $theory_id;
 "