From cb2f93ee6ac1827c5da4864ea26c901bb663b32f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Sep 2015 17:25:13 -0700
Subject: [PATCH] fix(kernel/expr,kernel/level): performance problem

The method unordered_set::clear takes time O(n) where n is the number of
buckets in the hashtable used to implement the set.
Moreover, it does not reduce the number of buckets to 0.
That is, it keeps `n` empty buckets.

This creates performance problems if the number of buckets gets really
huge at one point.
The tst6 at tests/kernel/expr.cpp demonstrates the problem
---
 src/kernel/expr.cpp  | 3 ++-
 src/kernel/level.cpp | 9 +++++----
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 51526911f..34d2ca6f1 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -312,7 +312,8 @@ bool enable_expr_caching(bool f) {
     bool r2 = g_expr_cache_enabled;
     lean_verify(r1 == r2);
     g_expr_cache_enabled = f;
-    get_expr_cache().clear();
+    expr_cache new_cache;
+    get_expr_cache().swap(new_cache);
     return r2;
 }
 inline expr cache(expr const & e) {
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index d26c4a12a..8aec6c222 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -261,20 +261,21 @@ level const & mk_level_zero() { return *g_level_zero; }
 level const & mk_level_one() { return *g_level_one; }
 bool is_one(level const & l) { return l == mk_level_one(); }
 
-typedef typename std::unordered_set<level, level_hash> level_table;
+typedef typename std::unordered_set<level, level_hash> level_cache;
 LEAN_THREAD_VALUE(bool, g_level_cache_enabled, true);
-MK_THREAD_LOCAL_GET_DEF(level_table, get_level_cache);
+MK_THREAD_LOCAL_GET_DEF(level_cache, get_level_cache);
 bool enable_level_caching(bool f) {
     bool r = g_level_cache_enabled;
     g_level_cache_enabled = f;
-    get_level_cache().clear();
+    level_cache new_cache;
+    get_level_cache().swap(new_cache);
     get_level_cache().insert(mk_level_zero());
     get_level_cache().insert(mk_level_one());
     return r;
 }
 level cache(level const & e) {
     if (g_level_cache_enabled) {
-        level_table & cache = get_level_cache();
+        level_cache & cache = get_level_cache();
         auto it = cache.find(e);
         if (it != cache.end()) {
             return *it;