From 51fcb10b2ff0e4496a3c0c2ed7c32f0876c9ee49 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 2 Aug 2024 20:00:45 -0700
Subject: [PATCH] shave some overhead from fingerprint hash function #7281
---
src/smt/fingerprints.cpp | 28 ++++++++++++++++++++++++++--
src/smt/fingerprints.h | 8 +-------
2 files changed, 27 insertions(+), 9 deletions(-)
diff --git a/src/smt/fingerprints.cpp b/src/smt/fingerprints.cpp
index 447c2b2a1..ac13999d0 100644
--- a/src/smt/fingerprints.cpp
+++ b/src/smt/fingerprints.cpp
@@ -63,6 +63,26 @@ namespace smt {
fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def) {
+
+ struct arg_data {
+ unsigned data_hash;
+ enode* const* args;
+ };
+ struct khash {
+ unsigned operator()(arg_data const& d) const {
+ return d.data_hash;
+ }
+ };
+ struct arghash {
+ unsigned operator()(arg_data const& d, unsigned i) const {
+ return d.args[i]->hash();
+ }
+ };
+ arg_data arg_data({ data_hash, args });
+ khash kh;
+ arghash ah;
+ data_hash = get_composite_hash(arg_data, num_args, kh, ah);
+
fingerprint * d = mk_dummy(data, data_hash, num_args, args);
if (m_set.contains(d))
return nullptr;
@@ -107,8 +127,12 @@ namespace smt {
unsigned new_lvl = lvl - num_scopes;
unsigned old_size = m_scopes[new_lvl];
unsigned size = m_fingerprints.size();
- for (unsigned i = old_size; i < size; i++)
- m_set.erase(m_fingerprints[i]);
+ if (old_size == 0 && size > 0)
+ m_set.reset();
+ else {
+ for (unsigned i = old_size; i < size; i++)
+ m_set.erase(m_fingerprints[i]);
+ }
m_fingerprints.shrink(old_size);
m_defs.shrink(old_size);
m_scopes.shrink(new_lvl);
diff --git a/src/smt/fingerprints.h b/src/smt/fingerprints.h
index b1904a4ee..a602f25cd 100644
--- a/src/smt/fingerprints.h
+++ b/src/smt/fingerprints.h
@@ -48,15 +48,9 @@ namespace smt {
class fingerprint_set {
- struct fingerprint_khasher {
- unsigned operator()(fingerprint const * f) const { return f->get_data_hash(); }
- };
- struct fingerprint_chasher {
- unsigned operator()(fingerprint const * f, unsigned idx) const { return f->get_arg(idx)->hash(); }
- };
struct fingerprint_hash_proc {
unsigned operator()(fingerprint const * f) const {
- return get_composite_hash<fingerprint *, fingerprint_khasher, fingerprint_chasher>(const_cast<fingerprint*>(f), f->get_num_args());
+ return f->get_data_hash();
}
};
struct fingerprint_eq_proc { bool operator()(fingerprint const * f1, fingerprint const * f2) const; };