Set incomplete if not applying ho extensionality (#6281)

[cvc5.git] / src / util / hash.h

diff --git a/src/util/hash.h b/src/util/hash.h
index b04fb8bb567556cdae6a67f1062bfe4bee96ad19..6ba4534d1b6e975888e736071e2e75bda4fda242 100644 (file)
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -2,10 +2,10 @@
 /*! \file hash.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Paul Meng
+ **   Morgan Deters, Andres Noetzli, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__HASH_H
-#define __CVC4__HASH_H
+#ifndef CVC4__HASH_H
+#define CVC4__HASH_H
 
 #include <functional>
 #include <string>
@@ -38,16 +38,32 @@ struct hash<uint64_t> {
 
 }/* std namespace */
 
-namespace CVC4 {
+namespace cvc5 {
 
+namespace fnv1a {
+
+/**
+ * FNV-1a hash algorithm for 64-bit numbers.
+ *
+ * More details here: http://www.isthe.com/chongo/tech/comp/fnv/index.html
+ */
+inline uint64_t fnv1a_64(uint64_t v, uint64_t hash = 14695981039346656037U) {
+  hash ^= v;
+  // Compute (hash * 1099511628211)
+  return hash + (hash << 1) + (hash << 4) + (hash << 5) + (hash << 7) +
+         (hash << 8) + (hash << 40);
+}
+
+}  // namespace fnv1a
 
 template <class T, class U, class HashT = std::hash<T>, class HashU = std::hash<U> >
 struct PairHashFunction {
   size_t operator()(const std::pair<T, U>& pr) const {
-    return HashT()(pr.first) ^ HashU()(pr.second);
+    uint64_t hash = fnv1a::fnv1a_64(HashT()(pr.first));
+    return static_cast<size_t>(fnv1a::fnv1a_64(HashU()(pr.second), hash));
   }
 };/* struct PairHashFunction */
 
-}/* CVC4 namespace */
+}  // namespace cvc5
 
-#endif /* __CVC4__HASH_H */
+#endif /* CVC4__HASH_H */