From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Jul 2020 14:18:06 +0000 (-0500)
Subject: (proof-new) Stream output for ProofNode (#4789)
X-Git-Tag: cvc5-1.0.0~3070
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=476ee33d566e87ed11d001a5485cb8b8c09f24dc;p=cvc5.git

(proof-new) Stream output for ProofNode (#4789)
---

diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index fd8f50415..be2c22c1e 100644
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -49,12 +49,7 @@ bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy)
   std::shared_ptr<ProofNode> apf = getProofFor(f);
   if (apf != nullptr)
   {
-    if (Trace.isOn("pfgen"))
-    {
-      std::stringstream ss;
-      apf->printDebug(ss);
-      Trace("pfgen") << "...got proof " << ss.str() << std::endl;
-    }
+    Trace("pfgen") << "...got proof " << *apf.get() << std::endl;
     // Add the proof, without deep copying.
     if (pf->addProof(apf, opolicy, false))
     {
diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp
index d817cbd65..5f34127df 100644
--- a/src/expr/proof_node.cpp
+++ b/src/expr/proof_node.cpp
@@ -75,4 +75,10 @@ void ProofNode::printDebug(std::ostream& os) const
   os << ps;
 }
 
+std::ostream& operator<<(std::ostream& out, const ProofNode& pn)
+{
+  pn.printDebug(out);
+  return out;
+}
+
 }  // namespace CVC4
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index bca86f44f..930badbb1 100644
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -117,6 +117,15 @@ class ProofNode
   Node d_proven;
 };
 
+/**
+ * Serializes a given proof node to the given stream.
+ *
+ * @param out the output stream to use
+ * @param pn the proof node to output to the stream
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const ProofNode& pn);
+
 }  // namespace CVC4
 
 #endif /* CVC4__EXPR__PROOF_NODE_H */