summaryrefslogtreecommitdiff
path: root/src/theory/strings/infer_info.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/infer_info.h')
-rw-r--r--src/theory/strings/infer_info.h21
1 files changed, 21 insertions, 0 deletions
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 9d2f71b53..cfabe5c51 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,25 @@ enum class Inference : uint32_t
FLOOP,
NONE,
};
+
+/**
+ * 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
+ */
+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);
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback