From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 5 Apr 2020 16:42:59 +0000 (-0700)
Subject: Add safe_print() support for Kind enum (#4213)
X-Git-Tag: cvc5-1.0.0~3405
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=baefe18cead33e6d190bb0b144b7c656f77ddf1e;p=cvc5.git

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 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;
 "
diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h
index 047042191..d1b777c0d 100644
--- 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();