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

diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index fd8f50415acf40ec8ee5b802e083a8d4531357c2..be2c22c1e617d74d0c53be5215d120b407649632 100644 (file)
--- 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 d817cbd65de151bbbee30f04d30abf772ef3bdb1..5f34127df13aabcd22983458f4fb3c004792d257 100644 (file)
--- 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 bca86f44f45ceaf083fc0c1948b35ab38eac6d72..930badbb198ce35eb0590eaf7813b1d6ccdc1c3c 100644 (file)
--- 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 */