[proof-new] Adds a proof node hash function (#5154)

diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index d6ead49f20f4dba64d50e948ffbec0ea7788ab91..6d7db7b2586db53978b64bc56438385a35e09239 100644 (file)
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -25,6 +25,12 @@
 namespace CVC4 {
 
 class ProofNodeManager;
+class ProofNode;
+
+struct ProofNodeHashFunction
+{
+  inline size_t operator()(std::shared_ptr<ProofNode> pfn) const;
+}; /* struct ProofNodeHashFunction */
 
 /** A node in a proof
  *
@@ -117,6 +123,12 @@ class ProofNode
   Node d_proven;
 };
 
+inline size_t ProofNodeHashFunction::operator()(
+    std::shared_ptr<ProofNode> pfn) const
+{
+  return pfn->getResult().getId() + static_cast<unsigned>(pfn->getRule());
+}
+
 /**
  * Serializes a given proof node to the given stream.
  *