Add safe_print() support for Kind enum (#4213)

This commit changes the mkkind script to generate a toString()
method for the Kind enum. This method can be used by the
safe_print() function to print statistics if CVC4 has been terminated
before solving a problem. The stats for strings include statistics that
rely on printing kinds (e.g. the number of reductions done of each
kind).

diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index 77468687c589f69f0becc4246c8b87cb4520cfba..d3af9a836ccac42f6456e5582b631b7df8301b55 100644 (file)
--- 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 da8e48a6f464af572962fec60aa2f799d98df602..50e2f372c979383c9155f9bbab33f122565f6eed 100644 (file)
--- 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 8e45b94ba9f4b1cf9065d29dff6ad2d5511ab002..fbf37eff4da2f1b0e717ecdc153571d317a29f60 100755 (executable)
--- 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;
 "

diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h
index 047042191504977b94a0b2f2dc4b650caf60746e..d1b777c0d81433913c6b4299209e5cfa0557c014 100644 (file)
--- a/test/unit/expr/kind_black.h
+++ b/test/unit/expr/kind_black.h
@@ -82,7 +82,7 @@ class KindBlack : public CxxTest::TestSuite {
 
     stringstream act, exp;
     act << undefined << null << last << unknown;
-    exp << "UNDEFINED_KIND" << "NULL" << "LAST_KIND" << "UNKNOWNKIND!"<< beyond;
+    exp << "UNDEFINED_KIND" << "NULL" << "LAST_KIND" << "?";
     
     string actCreated = act.str();
     string expCreated = exp.str();