From 9fa1a7a01cf5700dba37de2dc2c6cb266c62def2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Jan 2016 17:29:48 -0800 Subject: [PATCH] refactor(abstract_expr_manager): use get_specialization_prefix_size to improve performance of abstract_expr_manager --- src/library/abstract_expr_manager.cpp | 85 ++++++++++++++------------- src/library/congr_lemma_manager.cpp | 8 ++- src/library/congr_lemma_manager.h | 1 + src/library/fun_info_manager.cpp | 4 +- src/library/fun_info_manager.h | 2 +- 5 files changed, 56 insertions(+), 44 deletions(-) diff --git a/src/library/abstract_expr_manager.cpp b/src/library/abstract_expr_manager.cpp index cd968d88c..8b9ef2ac8 100644 --- a/src/library/abstract_expr_manager.cpp +++ b/src/library/abstract_expr_manager.cpp @@ -32,23 +32,24 @@ unsigned abstract_expr_manager::hash(expr const & e) { m_locals.pop_back(); return h; case expr_kind::App: - // TODO(Leo): in the past we only had to apply instantiate_rev to the function. - // We have to improve this. - // One idea is to compute and cache the specialization prefix for f. - // Then, we only need to apply instantiate_rev to f + prefix. - // expr f = instantiate_rev(get_app_args(e, args), m_locals.size(), m_locals.data()); - expr new_e = instantiate_rev(e, m_locals.size(), m_locals.data()); - optional f_congr = m_congr_lemma_manager.mk_specialized_congr(new_e); buffer args; - expr const & f = get_app_args(new_e, args); - h = hash(f); - if (!f_congr) { - for (expr const & arg : args) { - h = ::lean::hash(h, hash(arg)); + expr const & f = get_app_args(e, args); + unsigned prefix_sz = m_congr_lemma_manager.get_specialization_prefix_size(f, args.size()); + expr new_f = e; + unsigned rest_sz = args.size() - prefix_sz; + for (unsigned i = 0; i < rest_sz; i++) + new_f = app_fn(new_f); + new_f = instantiate_rev(new_f, m_locals.size(), m_locals.data()); + optional congr = m_congr_lemma_manager.mk_congr(new_f, rest_sz); + h = hash(new_f); + if (!congr) { + for (unsigned i = prefix_sz; i < args.size(); i++) { + h = ::lean::hash(h, hash(args[i])); } } else { - unsigned i = 0; - for_each(f_congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) { + lean_assert(length(congr->get_arg_kinds()) == rest_sz); + unsigned i = prefix_sz; + for_each(congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) { if (c_kind != congr_arg_kind::Cast) { h = ::lean::hash(h, hash(args[i])); } @@ -88,40 +89,44 @@ bool abstract_expr_manager::is_equal(expr const & a, expr const & b) { } return true; case expr_kind::App: - if (!is_equal(get_app_fn(a), get_app_fn(b))) { - return false; - } - if (get_app_num_args(a) != get_app_num_args(b)) { - return false; - } - // See comment in the hash function - expr new_a = instantiate_rev(a, m_locals.size(), m_locals.data()); - expr new_b = instantiate_rev(b, m_locals.size(), m_locals.data()); - optional congra = m_congr_lemma_manager.mk_specialized_congr(new_a); - optional congrb = m_congr_lemma_manager.mk_specialized_congr(new_b); buffer a_args, b_args; - get_app_args(new_a, a_args); - get_app_args(new_b, b_args); + expr const & f_a = get_app_args(a, a_args); + expr const & f_b = get_app_args(b, b_args); + if (!is_equal(f_a, f_b)) + return false; + if (a_args.size() != b_args.size()) + return false; + unsigned prefix_sz = m_congr_lemma_manager.get_specialization_prefix_size(f_a, a_args.size()); + for (unsigned i = 0; i < prefix_sz; i++) { + if (!is_equal(a_args[i], b_args[i])) + return false; + } + expr new_f_a = a; + unsigned rest_sz = a_args.size() - prefix_sz; + for (unsigned i = 0; i < rest_sz; i++) { + new_f_a = app_fn(new_f_a); + } + new_f_a = instantiate_rev(new_f_a, m_locals.size(), m_locals.data()); + optional congr = m_congr_lemma_manager.mk_congr(new_f_a, rest_sz); bool not_equal = false; - if (!congra || !congrb) { - for (unsigned i = 0; i < a_args.size(); ++i) { + if (!congr) { + for (unsigned i = prefix_sz; i < a_args.size(); ++i) { if (!is_equal(a_args[i], b_args[i])) { not_equal = true; break; } } } else { - unsigned i = 0; - for_each2(congra->get_arg_kinds(), - congrb->get_arg_kinds(), - [&](congr_arg_kind const & ca_kind, congr_arg_kind const & cb_kind) { - if (not_equal) - return; - if (ca_kind != cb_kind || (ca_kind != congr_arg_kind::Cast && !is_equal(a_args[i], b_args[i]))) { - not_equal = true; - } - i++; - }); + lean_assert(length(congr->get_arg_kinds()) == rest_sz); + unsigned i = prefix_sz; + for_each(congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) { + if (not_equal) + return; + if (c_kind != congr_arg_kind::Cast && !is_equal(a_args[i], b_args[i])) { + not_equal = true; + } + i++; + }); } return !not_equal; } diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp index 0f1ac0360..14f618b03 100644 --- a/src/library/congr_lemma_manager.cpp +++ b/src/library/congr_lemma_manager.cpp @@ -586,6 +586,10 @@ public: optional mk_rel_eq_congr(expr const & R) { return mk_rel_congr(R, false); } + + unsigned get_specialization_prefix_size(expr const & fn, unsigned nargs) { + return m_fmanager.get_specialization_prefix_size(fn, nargs); + } }; congr_lemma_manager::congr_lemma_manager(app_builder & b, fun_info_manager & fm): @@ -618,10 +622,12 @@ auto congr_lemma_manager::mk_specialized_congr(expr const & fn) -> optional optional { return m_ptr->mk_rel_iff_congr(R); } - auto congr_lemma_manager::mk_rel_eq_congr(expr const & R) -> optional { return m_ptr->mk_rel_eq_congr(R); } +unsigned congr_lemma_manager::get_specialization_prefix_size(expr const & fn, unsigned nargs) { + return m_ptr->get_specialization_prefix_size(fn, nargs); +} void initialize_congr_lemma_manager() { register_trace_class("congruence_manager"); diff --git a/src/library/congr_lemma_manager.h b/src/library/congr_lemma_manager.h index 41da55d91..b759a0fec 100644 --- a/src/library/congr_lemma_manager.h +++ b/src/library/congr_lemma_manager.h @@ -46,6 +46,7 @@ public: typedef congr_lemma result; type_context & ctx(); + unsigned get_specialization_prefix_size(expr const & fn, unsigned nargs); optional mk_congr_simp(expr const & fn); optional mk_congr_simp(expr const & fn, unsigned nargs); diff --git a/src/library/fun_info_manager.cpp b/src/library/fun_info_manager.cpp index 9b01937aa..1e99fb265 100644 --- a/src/library/fun_info_manager.cpp +++ b/src/library/fun_info_manager.cpp @@ -164,7 +164,7 @@ void fun_info_manager::trace_if_unsupported(expr const & fn, buffer const } } -unsigned fun_info_manager::get_prefix(expr const & fn, unsigned nargs) { +unsigned fun_info_manager::get_specialization_prefix_size(expr const & fn, unsigned nargs) { /* We say a function is "cheap" if it is of the form: @@ -222,7 +222,7 @@ fun_info fun_info_manager::get_specialized(expr const & a) { lean_assert(is_app(a)); buffer args; expr const & fn = get_app_args(a, args); - unsigned prefix_sz = get_prefix(fn, args.size()); + unsigned prefix_sz = get_specialization_prefix_size(fn, args.size()); unsigned num_rest_args = args.size() - prefix_sz; expr g = a; for (unsigned i = 0; i < num_rest_args; i++) diff --git a/src/library/fun_info_manager.h b/src/library/fun_info_manager.h index c14b1322d..662c6bb0e 100644 --- a/src/library/fun_info_manager.h +++ b/src/library/fun_info_manager.h @@ -122,7 +122,7 @@ public: c) (inv : Pi {A : Type} [s : has_inv A] (x : A) (h : invertible x), A) result 2 */ - unsigned get_prefix(expr const & fn, unsigned nargs); + unsigned get_specialization_prefix_size(expr const & fn, unsigned nargs); }; void initialize_fun_info_manager();