From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 29 Sep 2020 01:22:29 +0000 (-0300)
Subject: [proof-new] Adds a proof node hash function (#5154)
X-Git-Tag: cvc5-1.0.0~2796
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b9e889c6c126ecb6ffa8fa65977a2924b42d2812;p=cvc5.git

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

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.
  *