Support async-signal-safe printing of inferences (#4148)

Commit c9b7c3d 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.

1 files changed, 19 insertions, 16 deletions

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index aa7fe8974..cdf764aa8 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -14,30 +14,33 @@
 
 #include "theory/strings/infer_info.h"
 
-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;
 }