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

feat(kernel/expr_eq_fn): add small optimization

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-01 09:19:36 -07:00
parent 0f64a6e545
commit 667f647b27
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/expr_eq_fn.cpp
View file

@ -28,6 +28,8 @@ struct eq_cache {
eq_cache():m_capacity(LEAN_EQ_CACHE_CAPACITY), m_cache(LEAN_EQ_CACHE_CAPACITY) {}
bool check(expr const & a, expr const & b) {
if (!is_shared(a) || !is_shared(b))
return false;
unsigned i = hash(a.hash_alloc(), b.hash_alloc()) % m_capacity;
if (m_cache[i].m_a == a.raw() && m_cache[i].m_b == b.raw()) {
return true;