From 96414f1c956dd4e2928fbd3b9f7f7e7af6660f1e Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 14 Jan 2022 11:16:47 -0800
Subject: [PATCH] Add operator<<(RewriteStatus) (#7952)

Adds a streaming operator for RewriteStatus. I found it helpful while refactoring / debugging the rewriter.
---
 src/theory/theory_rewriter.cpp | 12 ++++++++++++
 src/theory/theory_rewriter.h   |  3 +++
 2 files changed, 15 insertions(+)

diff --git a/src/theory/theory_rewriter.cpp b/src/theory/theory_rewriter.cpp
index 42e9148c2..5324cd302 100644
--- 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 eca1e4e56..d411dc73b 100644
--- 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
-- 
2.30.2