michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

perf(src/util/name): if the hashcodes are equal, then there is a high probability the names are equal

Browse source 
So, we use == before trying cmp.
Reason: == is much faster.
This commit is contained in:
Leonardo de Moura 2016-02-02 12:52:06 -08:00
parent a9cb9ff912
commit cb203c3272
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/util/name.h
View file

@ -175,10 +175,13 @@ public:
return 0; return 0;
unsigned h1 = a.hash(); unsigned h1 = a.hash();
unsigned h2 = b.hash(); unsigned h2 = b.hash();
if (h1 != h2) if (h1 != h2) {
return h1 < h2 ? -1 : 1; return h1 < h2 ? -1 : 1;
else } else if (a == b) {
return 0;
} else {
return cmp(a, b); return cmp(a, b);
}
} }
struct ptr_hash { unsigned operator()(name const & n) const { return std::hash<imp*>()(n.m_ptr); } }; struct ptr_hash { unsigned operator()(name const & n) const { return std::hash<imp*>()(n.m_ptr); } };