diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-10-02 22:48:00 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-02 22:48:00 -0700 |
commit | d0faa2b676130119c5d01e00851427fa97f44464 (patch) | |
tree | 76e25b4558e6752d75230c7ac297af97f870ea24 | |
parent | 6861f66d2e2b54fc31d9151b4dbeb2964ea07f94 (diff) |
Unify hash functions for pairs (#1161)
CVC4 was implementing multiple, slightly different hash functions for
pairs. With pull request #1157, we have a decent generic hash function
for pairs. This commit replaces the existing hash function
implementations with a typedef of the generic hash function.
-rw-r--r-- | src/expr/node.h | 11 | ||||
-rw-r--r-- | src/theory/ite_utilities.h | 11 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 4 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_types.h | 18 |
4 files changed, 18 insertions, 26 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 9b2ea1935..66f8b0a47 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -44,6 +44,7 @@ #include "expr/expr_iomanip.h" #include "options/language.h" #include "options/set_language.h" +#include "util/hash.h" #include "util/utility.h" namespace CVC4 { @@ -959,14 +960,8 @@ inline size_t TNodeHashFunction::operator()(TNode node) const { return node.getId(); } -struct TNodePairHashFunction { - size_t operator()(const std::pair<CVC4::TNode, CVC4::TNode>& pair ) const { - TNode n1 = pair.first; - TNode n2 = pair.second; - - return (size_t) (n1.getId() * 0x9e3779b9 + n2.getId()); - } -};/* struct TNodePairHashFunction */ +using TNodePairHashFunction = + PairHashFunction<TNode, TNode, TNodeHashFunction, TNodeHashFunction>; template <bool ref_count> inline size_t NodeTemplate<ref_count>::getNumChildren() const { diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h index 4aad9a3f0..096393de2 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -26,6 +26,7 @@ #include <vector> #include "expr/node.h" +#include "util/hash.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -240,14 +241,8 @@ private: uint32_t d_citeEqConstApplications; typedef std::pair<Node, Node> NodePair; - struct NodePairHashFunction { - size_t operator () (const NodePair& pair) const { - size_t hash = 0; - hash = 0x9e3779b9 + NodeHashFunction().operator()(pair.first); - hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2); - return hash; - } - };/* struct ITESimplifier::NodePairHashFunction */ + using NodePairHashFunction = + PairHashFunction<Node, Node, NodeHashFunction, NodeHashFunction>; typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap; NodePairMap d_constantIteEqualsConstantCache; NodePairMap d_replaceOverCache; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3ae0b840b..a897f9456 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -44,6 +44,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" +#include "util/hash.h" #include "util/statistics_registry.h" #include "util/unsafe_interrupt_exception.h" @@ -74,7 +75,8 @@ struct NodeTheoryPairHashFunction { NodeHashFunction hashFunction; // Hash doesn't take into account the timestamp size_t operator()(const NodeTheoryPair& pair) const { - return hashFunction(pair.node)*0x9e3779b9 + pair.theory; + uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.node)); + return static_cast<size_t>(fnv1a::fnv1a_64(pair.theory, hash)); } };/* struct NodeTheoryPairHashFunction */ diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index ed0afa904..b3b8ac7d6 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -17,10 +17,15 @@ #include "cvc4_private.h" +#ifndef __CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H +#define __CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H + #include <string> #include <iostream> #include <sstream> +#include "util/hash.h" + namespace CVC4 { namespace theory { namespace eq { @@ -264,15 +269,8 @@ public: /** A pair of ids */ typedef std::pair<EqualityNodeId, EqualityNodeId> EqualityPair; - -struct EqualityPairHashFunction { - size_t operator () (const EqualityPair& pair) const { - size_t hash = 0; - hash = 0x9e3779b9 + pair.first; - hash ^= 0x9e3779b9 + pair.second + (hash << 6) + (hash >> 2); - return hash; - } -}; +using EqualityPairHashFunction = + PairHashFunction<EqualityNodeId, EqualityNodeId>; enum FunctionApplicationType { /** This application is an equality a = b */ @@ -362,3 +360,5 @@ struct TriggerInfo { } // namespace eq } // namespace theory } // namespace CVC4 + +#endif /* __CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */ |