Support async-signal-safe printing of inferences

Commit c9b7c3d6fcd49b6d75a85e1316e9918374d1ebbe introduced code for
counting the number of string inferences done per type of inference.
However, it did not add support for printing the inference names in an
async-signal-safe manner via `safe_print()` (note that printing in
signal handlers is done differently from the regular stats printing).
This commit adds the corresponding code, s.t. we get the inference names
when printing the stats when CVC4 is interrupted or crashes.

2 files changed, 62 insertions, 14 deletions

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index aa7fe8974..c87e5e93d 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -14,30 +14,37 @@
 
 #include "theory/strings/infer_info.h"
 
+#include <cstring>
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace theory {
 namespace strings {
 
-std::ostream& operator<<(std::ostream& out, Inference i)
+const char* toString(Inference i)
 {
   switch (i)
   {
-    case Inference::N_ENDPOINT_EMP: out << "N_EndpointEmp"; break;
-    case Inference::N_UNIFY: out << "N_Unify"; break;
-    case Inference::N_ENDPOINT_EQ: out << "N_EndpointEq"; break;
-    case Inference::N_CONST: out << "N_Const"; break;
-    case Inference::INFER_EMP: out << "Infer-Emp"; break;
-    case Inference::SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
-    case Inference::SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
-    case Inference::LEN_SPLIT: out << "Len-Split(Len)"; break;
-    case Inference::LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
-    case Inference::SSPLIT_CST: out << "S-Split(CST-P)"; break;
-    case Inference::SSPLIT_VAR: out << "S-Split(VAR)"; break;
-    case Inference::FLOOP: out << "F-Loop"; break;
-    default: out << "?"; break;
+    case Inference::N_ENDPOINT_EMP: return "N_EndpointEmp";
+    case Inference::N_UNIFY: return "N_Unify";
+    case Inference::N_ENDPOINT_EQ: return "N_EndpointEq";
+    case Inference::N_CONST: return "N_Const";
+    case Inference::INFER_EMP: return "Infer-Emp";
+    case Inference::SSPLIT_CST_PROP: return "S-Split(CST-P)-prop";
+    case Inference::SSPLIT_VAR_PROP: return "S-Split(VAR)-prop";
+    case Inference::LEN_SPLIT: return "Len-Split(Len)";
+    case Inference::LEN_SPLIT_EMP: return "Len-Split(Emp)";
+    case Inference::SSPLIT_CST: return "S-Split(CST-P)";
+    case Inference::SSPLIT_VAR: return "S-Split(VAR)";
+    case Inference::FLOOP: return "F-Loop";
+    default: return "?";
   }
+}
+
+std::ostream& operator<<(std::ostream& out, Inference i)
+{
+  out << toString(i);
   return out;
 }
 
@@ -45,4 +52,16 @@ InferInfo::InferInfo() : d_id(Inference::NONE), d_index(0), d_rev(false) {}
 
 }  // namespace strings
 }  // namespace theory
+
+template <>
+void safe_print(int fd, const theory::strings::Inference& i)
+{
+  const char* s = toString(i);
+  ssize_t slen = static_cast<ssize_t>(strlen(s));
+  if (write(fd, s, slen) != slen)
+  {
+    abort();
+  }
+}
+
 }  // namespace CVC4
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 9d2f71b53..45f4f0bab 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -19,7 +19,9 @@
 
 #include <map>
 #include <vector>
+
 #include "expr/node.h"
+#include "util/safe_print.h"
 
 namespace CVC4 {
 namespace theory {
@@ -94,6 +96,22 @@ enum class Inference : uint32_t
   FLOOP,
   NONE,
 };
+
+/**
+ * Converts an inference to a string.
+ *
+ * @param i The inference
+ * @return The name of the inference
+ */
+const char* toString(Inference i);
+
+/**
+ * Writes an inference name to a stream.
+ *
+ * @param out The stream to write to
+ * @param i The inference to write to the stream
+ * @return The stream
+ */
 std::ostream& operator<<(std::ostream& out, Inference i);
 
 /**
@@ -173,6 +191,17 @@ class InferInfo
 
 }  // namespace strings
 }  // namespace theory
+
+/**
+ * Provides a template specialization for printing inference names in an
+ * async-signal-safe manner.
+ *
+ * @param fd The file descriptor to print to
+ * @param i The inference to print
+ */
+template <>
+void safe_print(int fd, const theory::strings::Inference& i);
+
 }  // namespace CVC4
 
 #endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */