max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf: use lean::unordered_set for expr_eq_fn (#11731)

Browse source 
This PR makes the cache in expr_eq_fn use mimalloc for a small
performance win across the board.
This commit is contained in:
Henrik Böving 2025-12-18 15:24:50 +01:00 • committed by GitHub
parent eb11ccb234
commit 34d619bf93
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/expr_eq_fn.cpp
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include "runtime/thread.h"
#include "kernel/expr.h"
#include "kernel/expr_sets.h"
#include "util/alloc.h"
namespace lean {
/**
@ -26,7 +27,7 @@ class expr_eq_fn {
return hash((size_t)p.first >> 3, (size_t)p.second >> 3);
}
};
typedef std::unordered_set<std::pair<lean_object *, lean_object *>, key_hasher> cache;
typedef lean::unordered_set<std::pair<lean_object *, lean_object *>, key_hasher> cache;
cache * m_cache = nullptr;
size_t m_max_stack_depth = 0;
size_t m_counter = 0;