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 /src/theory/ite_utilities.h | |
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.
Diffstat (limited to 'src/theory/ite_utilities.h')
-rw-r--r-- | src/theory/ite_utilities.h | 11 |
1 files changed, 3 insertions, 8 deletions
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; |