From 7cc3dd0b4d8011bf3aa28c3163f76a533d0fbaf2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Oct 2014 14:20:35 -0700 Subject: [PATCH] chore(kernel/replace_fn): "name" constant --- src/kernel/replace_fn.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp index 9cd2981a1..e424941b0 100644 --- a/src/kernel/replace_fn.cpp +++ b/src/kernel/replace_fn.cpp @@ -13,6 +13,10 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_REPLACE_CACHE_CAPACITY 1024*8 #endif +#ifndef LEAN_REPLACE_SMALL_TERM_THRESHOLD +#define LEAN_REPLACE_SMALL_TERM_THRESHOLD 10000 +#endif + namespace lean { struct replace_cache { struct entry { @@ -253,7 +257,7 @@ public: }; expr replace(expr const & e, std::function(expr const &, unsigned)> const & f) { - if (get_weight(e) < 10000) + if (get_weight(e) < LEAN_REPLACE_SMALL_TERM_THRESHOLD) return replace_rec_fn(f)(e); else return replace_fn(f)(e);