feat(kernel/expr): replace "opportunistic" caching with precise caching

We also removed compilation option LEAN_CACHE_EXPRS

src/CMakeLists.txt

@@ -18,7 +18,6 @@ option(BOOST              "BOOST"              OFF)
 option(STATIC             "STATIC"             OFF)
 option(SPLIT_STACK        "SPLIT_STACK"        OFF)
 option(READLINE           "READLINE"           OFF)
-option(CACHE_EXPRS        "CACHE_EXPRS"        ON)
 option(TCMALLOC           "TCMALLOC"           ON)
 option(JEMALLOC           "JEMALLOC"           OFF)
 # IGNORE_SORRY is a tempory option (hack). It allows us to build
@@ -81,11 +80,6 @@ else()
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_MULTI_THREAD")
 endif()
 
-if(CACHE_EXPRS)
-  message(STATUS "Lean expression caching enabled (aka partial hashconsing)")
-  set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_CACHE_EXPRS")
-endif()
-
 if(AUTO_THREAD_FINALIZATION)
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_AUTO_THREAD_FINALIZATION")
 endif()

src/kernel/expr.cpp

@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "util/memory_pool.h"
 #include "kernel/expr.h"
 #include "kernel/expr_eq_fn.h"
+#include "kernel/expr_sets.h"
 #include "kernel/free_vars.h"
 #include "kernel/for_each_fn.h"
 
@@ -303,27 +304,29 @@ expr_macro::~expr_macro() {
 
 // =======================================
 // Constructors
-
-#ifdef LEAN_CACHE_EXPRS
-typedef lru_cache<expr, expr_hash, is_bi_equal_proc> expr_cache;
 LEAN_THREAD_VALUE(bool, g_expr_cache_enabled, true);
-MK_THREAD_LOCAL_GET(expr_cache, get_expr_cache, LEAN_INITIAL_EXPR_CACHE_CAPACITY);
+MK_THREAD_LOCAL_GET_DEF(expr_struct_set, get_expr_cache);
 bool enable_expr_caching(bool f) {
     bool r = g_expr_cache_enabled;
     g_expr_cache_enabled = f;
+    get_expr_cache().clear();
     return r;
 }
 inline expr cache(expr const & e) {
     if (g_expr_cache_enabled) {
-        if (auto r = get_expr_cache().insert(e))
+        expr_struct_set & cache = get_expr_cache();
-            return *r;
+        auto it = cache.find(e);
+        if (it != cache.end()) {
+            return *it;
+        } else {
+            cache.insert(e);
+        }
     }
     return e;
 }
-#else
+bool is_cached(expr const & e) {
-inline expr cache(expr && e) { return e; }
+    return get_expr_cache().find(e) != get_expr_cache().end();
-bool enable_expr_caching(bool) { return true; } // NOLINT
+}
-#endif
 
 expr mk_var(unsigned idx, tag g) {
     return cache(expr(new (get_var_allocator().allocate()) expr_var(idx, g)));

src/kernel/expr.h

@@ -484,6 +484,8 @@ struct scoped_expr_caching {
     scoped_expr_caching(bool f) { m_old = enable_expr_caching(f); }
     ~scoped_expr_caching() { enable_expr_caching(m_old); }
 };
+/** \brief Return true iff \c e is in the cache */
+bool is_cached(expr const & e);
 // =======================================
 
 // =======================================