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

chore(kernel/replace_fn): "name" constant

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-17 14:20:35 -07:00
parent b6afbcb7f5
commit 7cc3dd0b4d
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/replace_fn.cpp
View file

@ -13,6 +13,10 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_REPLACE_CACHE_CAPACITY 1024*8 #define LEAN_DEFAULT_REPLACE_CACHE_CAPACITY 1024*8
#endif #endif
#ifndef LEAN_REPLACE_SMALL_TERM_THRESHOLD
#define LEAN_REPLACE_SMALL_TERM_THRESHOLD 10000
#endif
namespace lean { namespace lean {
struct replace_cache { struct replace_cache {
struct entry { struct entry {
@ -253,7 +257,7 @@ public:
}; };
expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f) { expr replace(expr const & e, std::function<optional<expr>(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); return replace_rec_fn(f)(e);
else else
return replace_fn(f)(e); return replace_fn(f)(e);