From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 14 Jan 2022 19:16:47 +0000 (-0800)
Subject: Add operator<<(RewriteStatus) (#7952)
X-Git-Tag: cvc5-1.0.0~544
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=96414f1c956dd4e2928fbd3b9f7f7e7af6660f1e;p=cvc5.git

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 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