Add operator<<(RewriteStatus) (#7952)

Adds a streaming operator for RewriteStatus. I found it helpful while refactoring / debugging the rewriter.

diff --git a/src/theory/theory_rewriter.cpp b/src/theory/theory_rewriter.cpp
index 42e9148c2f0230146715d43dd88a9c2c8db280cb..5324cd30240946e5772196a927c60f1c89faafa3 100644 (file)
--- a/src/theory/theory_rewriter.cpp
+++ b/src/theory/theory_rewriter.cpp
@@ -20,6 +20,18 @@
 namespace cvc5 {
 namespace theory {
 
+std::ostream& operator<<(std::ostream& os, RewriteStatus rs)
+{
+  switch (rs)
+  {
+    case RewriteStatus::REWRITE_DONE:       return os << "DONE";
+    case RewriteStatus::REWRITE_AGAIN:      return os << "AGAIN";
+    case RewriteStatus::REWRITE_AGAIN_FULL: return os << "AGAIN_FULL";
+  }
+  Unreachable();
+  return os;
+}
+
 TrustRewriteResponse::TrustRewriteResponse(RewriteStatus status,
                                            Node n,
                                            Node nr,

diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h
index eca1e4e56dbe7037d04d7257168c8b575e492697..d411dc73b416f60b15bcd5f479abd9ba352a585d 100644 (file)
--- a/src/theory/theory_rewriter.h
+++ b/src/theory/theory_rewriter.h
@@ -42,6 +42,9 @@ enum RewriteStatus
   REWRITE_AGAIN_FULL
 }; /* enum RewriteStatus */
 
+/** Print a RewriteStatus to an output stream */
+std::ostream& operator<<(std::ostream& os, RewriteStatus rs);
+
 /**
  * Instances of this class serve as response codes from
  * TheoryRewriter::preRewrite() and TheoryRewriter::postRewrite(). The response