Address offline discussion

3 files changed, 51 insertions, 27 deletions

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index c87e5e93d..e2697e58c 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -52,16 +52,4 @@ 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 45f4f0bab..cfabe5c51 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -98,7 +98,10 @@ enum class Inference : uint32_t
 };
 
 /**
- * Converts an inference to a string.
+ * Converts an inference 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 i The inference
  * @return The name of the inference
@@ -191,17 +194,6 @@ 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 */
diff --git a/src/util/safe_print.h b/src/util/safe_print.h
index 75a517b18..1b56c1c89 100644
--- a/src/util/safe_print.h
+++ b/src/util/safe_print.h
@@ -21,6 +21,11 @@
  ** in statistics_registry.h would require specialization or we would have to
  ** use function overloading).
  **
+ ** If there exists a function `toString(obj)` for a given object, it will be
+ ** used automatically. This is useful for printing enum values for example.
+ ** IMPORTANT: The `toString(obj)` function *must not* perform any allocations
+ ** or call other functions that are not async-signal-safe.
+ **
  ** This header is a "cvc4_private_library.h" header because it is private but
  ** the safe_print functions are used in the driver. See also the description
  ** of "statistics_registry.h" for more information on
@@ -40,6 +45,8 @@
 #endif
 
 #include <unistd.h>
+#include <cstring>
+#include <type_traits>
 
 #include "lib/clock_gettime.h"
 #include "util/result.h"
@@ -58,10 +65,47 @@ void CVC4_PUBLIC safe_print(int fd, const char (&msg)[N]) {
   }
 }
 
-/** Prints a variable of type T. Safe to use in a signal handler. */
+/**
+ * The default method for converting an object to a string for safe printing.
+ * This method simply returns "<unsupported>". The `long` argument is used to
+ * indicate that we do not prefer this method over the version that calls
+ * `toString()`.
+ */
+template <typename T>
+const char* toStringImpl(const T& obj, long) {
+  return "<unsupported>";
+}
+
+/**
+ * Returns the result of calling `toString(obj)`. This method is only defined
+ * if such an overload of `toString()` exists. To detect the existence of such
+ * a method, we use SFINAE and a trailing return type. The trailing return type
+ * is necessary because it allows us to refer to `obj`. The `int` argument is
+ * used to prefer this version of the function instead of the one that prints
+ * "<unsupported>".
+ */
 template <typename T>
-void CVC4_PUBLIC safe_print(int fd, const T& msg) {
-  safe_print(fd, "<unsupported>");
+auto toStringImpl(const T& obj, int) -> decltype(toString(obj)) {
+  return toString(obj);
+}
+
+/**
+ * Prints a variable of type T. Safe to use in a signal handler. The default
+ * implementation either prints "<unsupported>" or the result of calling
+ * `toString(obj)` if such a method exists (this is useful for printing enum
+ * values for example without implementing a template specialization here).
+ *
+ * @param fd The file descriptor to print to
+ * @param obj The object to print
+ */
+template <typename T>
+void CVC4_PUBLIC safe_print(int fd, const T& obj) {
+  const char* s = toStringImpl(obj, /* prefer the method that uses `toString()` */ 0);
+  ssize_t slen = static_cast<ssize_t>(strlen(s));
+  if (write(fd, s, slen) != slen)
+  {
+    abort();
+  }
 }
 
 template <>