Faster hasing for `cvc5::String` (#7742)

Previously, our hashing algorithm for cvc5::String would create an
std::string representation of the string and then call
std::hash<std::string> on the result. Creating the temporary
std::string is quite expensive and can be avoided by computing the
hash directly on the elements of the vector of characters in
cvc5::String.

This change improves our solving time on an industrial benchmark from
about 59s to 55s.

diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp
index 6b15f33e0a5ddab1d6fd7d77f88c417dba686b03..82c83e0eabdd709b8365121beac8e4ab403c9c5b 100644 (file)
--- a/src/expr/sequence.cpp
+++ b/src/expr/sequence.cpp
@@ -371,13 +371,13 @@ std::ostream& operator<<(std::ostream& os, const Sequence& s)
 
 size_t SequenceHashFunction::operator()(const Sequence& s) const
 {
-  size_t ret = 0;
+  uint64_t ret = fnv1a::offsetBasis;
   const std::vector<Node>& vec = s.getVec();
   for (const Node& n : vec)
   {
     ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(n));
   }
-  return ret;
+  return static_cast<size_t>(ret);
 }
 
 }  // namespace cvc5

diff --git a/src/util/hash.h b/src/util/hash.h
index db280984b3d29dee816444444c20b9b59e90bf59..ef8bf4a2a3dc304b07ed78f1e7c13e60043e1bc2 100644 (file)
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -43,12 +43,15 @@ namespace cvc5 {
 
 namespace fnv1a {
 
+constexpr uint64_t offsetBasis = 14695981039346656037U;
+
 /**
  * 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) {
+inline uint64_t fnv1a_64(uint64_t v, uint64_t hash = offsetBasis)
+{
   hash ^= v;
   // Compute (hash * 1099511628211)
   return hash + (hash << 1) + (hash << 4) + (hash << 5) + (hash << 7) +

diff --git a/src/util/string.cpp b/src/util/string.cpp
index 50b0a7199a34d29b594abe6897ff447092f95783..2235ac5eeaed9203e82182abcc50930c23a6e3f1 100644 (file)
--- a/src/util/string.cpp
+++ b/src/util/string.cpp
@@ -23,6 +23,7 @@
 
 #include "base/check.h"
 #include "base/exception.h"
+#include "util/hash.h"
 
 using namespace std;
 
@@ -519,6 +520,20 @@ Rational String::toNumber() const
   return Rational(toString());
 }
 
+namespace strings {
+
+size_t StringHashFunction::operator()(const ::cvc5::String& s) const
+{
+  uint64_t ret = fnv1a::offsetBasis;
+  for (unsigned c : s.d_str)
+  {
+    ret = fnv1a::fnv1a_64(c, ret);
+  }
+  return static_cast<size_t>(ret);
+}
+
+}  // namespace strings
+
 std::ostream &operator<<(std::ostream &os, const String &s) {
   return os << "\"" << s.toString() << "\"";
 }

diff --git a/src/util/string.h b/src/util/string.h
index 3f638408202340c12f6fdb148f6b3c4612c6f694..017c60fb8b64c280b8bb726361df9bc70134672e 100644 (file)
--- a/src/util/string.h
+++ b/src/util/string.h
@@ -26,6 +26,10 @@
 
 namespace cvc5 {
 
+namespace strings {
+struct StringHashFunction;
+}
+
 /** The cvc5 string class
  *
  * This data structure is the domain of values for the string type. It can also
@@ -33,6 +37,8 @@ namespace cvc5 {
  */
 class String
 {
+  friend strings::StringHashFunction;
+
  public:
   /**
    * This is the cardinality of the alphabet that is representable by this
@@ -267,10 +273,7 @@ namespace strings {
 
 struct StringHashFunction
 {
-  size_t operator()(const ::cvc5::String& s) const
-  {
-    return std::hash<std::string>()(s.toString());
-  }
+  size_t operator()(const ::cvc5::String& s) const;
 }; /* struct StringHashFunction */
 
 }  // namespace strings