summaryrefslogtreecommitdiff
path: root/src/expr/proof_node.h
diff options
context:
space:
mode:
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