diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-09-28 22:22:29 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-28 22:22:29 -0300 |
| commit | b9e889c6c126ecb6ffa8fa65977a2924b42d2812 (patch) | |
| tree | 277793107f0781837830ab2e570ab83fabdd2a8a /src/expr/proof_node.h | |
| parent | 85c509bc5c4005861f9c393931b426a776d4c0d6 (diff) | |
[proof-new] Adds a proof node hash function (#5154)
Diffstat (limited to 'src/expr/proof_node.h')
| -rw-r--r-- | src/expr/proof_node.h | 12 |
1 files changed, 12 insertions, 0 deletions
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. * |