From b9e889c6c126ecb6ffa8fa65977a2924b42d2812 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 28 Sep 2020 22:22:29 -0300
Subject: [proof-new] Adds a proof node hash function (#5154)

---
 src/expr/proof_node.h | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'src')

diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index d6ead49f2..6d7db7b25 100644
--- 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.
  *
-- 
cgit v1.2.3