mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

shave some overhead from fingerprint hash function #7281

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-08-02 20:00:45 -07:00
parent 7c30cbfe48
commit 51fcb10b2f
2 changed files with 27 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/smt/fingerprints.cpp
View file

@ -63,6 +63,26 @@ namespace smt {
fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def) { 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); fingerprint * d = mk_dummy(data, data_hash, num_args, args);
if (m_set.contains(d)) if (m_set.contains(d))
return nullptr; return nullptr;
@ -107,8 +127,12 @@ namespace smt {
unsigned new_lvl = lvl - num_scopes; unsigned new_lvl = lvl - num_scopes;
unsigned old_size = m_scopes[new_lvl]; unsigned old_size = m_scopes[new_lvl];
unsigned size = m_fingerprints.size(); unsigned size = m_fingerprints.size();
for (unsigned i = old_size; i < size; i++) if (old_size == 0 && size > 0)
m_set.erase(m_fingerprints[i]); m_set.reset();
else {
for (unsigned i = old_size; i < size; i++)
m_set.erase(m_fingerprints[i]);
}
m_fingerprints.shrink(old_size); m_fingerprints.shrink(old_size);
m_defs.shrink(old_size); m_defs.shrink(old_size);
m_scopes.shrink(new_lvl); m_scopes.shrink(new_lvl);

8
src/smt/fingerprints.h
View file

@ -48,15 +48,9 @@ namespace smt {
class fingerprint_set { 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 { struct fingerprint_hash_proc {
unsigned operator()(fingerprint const * f) const { 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; }; struct fingerprint_eq_proc { bool operator()(fingerprint const * f1, fingerprint const * f2) const; };