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.

diff --git a/src/expr/node.h b/src/expr/node.h
index 9b2ea19350e27b59d26fac9dd6b6e4a4704762ee..66f8b0a4742db6c07486cf1ac918fc957a7bc798 100644 (file)
--- 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 4aad9a3f0b18889caa688e4daf510b831df6c4ac..096393de20de16bfc81fe2087fb237f5a72cad2f 100644 (file)
--- 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 3ae0b840b74091e3e7c5b85d9d0bdfca05c986c6..a897f9456becfd9137d703907b64908f0f2cba5f 100644 (file)
--- 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 ed0afa904cdb9e596553ac4809b14406250e182e..b3b8ac7d6099ae9f8dfd77113abb90807c40b3b5 100644 (file)
--- 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 */