summaryrefslogtreecommitdiff
path: root/src/expr/proof_node.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-07-30 09:18:06 -0500
committerGitHub <noreply@github.com>2020-07-30 09:18:06 -0500
commit476ee33d566e87ed11d001a5485cb8b8c09f24dc (patch)
treefdd93536466dc6989e99d833cd9799dc0cc6599f /src/expr/proof_node.h
parentf5eb204df574d8f680e802601ca279f82eaf0146 (diff)
(proof-new) Stream output for ProofNode (#4789)
Diffstat (limited to 'src/expr/proof_node.h')
-rw-r--r--src/expr/proof_node.h9
1 files changed, 9 insertions, 0 deletions
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback