From d0faa2b676130119c5d01e00851427fa97f44464 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 2 Oct 2017 22:48:00 -0700
Subject: [PATCH] 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.
---
 src/expr/node.h                       | 11 +++--------
 src/theory/ite_utilities.h            | 11 +++--------
 src/theory/theory_engine.h            |  4 +++-
 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 */
-- 
2.30.2