From 4e67a351798714cd2792cab1bb8ff86d115bff3e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 1 Mar 2016 13:47:43 -0800 Subject: [PATCH] feat(library/blast/blast): add missing Let case, and comment to indicate performance problem --- src/library/blast/blast.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 86f99daad6..b364c42a31 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -950,6 +950,8 @@ public: } expr normalize_instances(expr const & e) { + // TODO(Leo, Dan): This procedure is traversing the expression \c e ignoring sharing. + // That is, it traverses a DAG as a Tree. This may generate serious performance prooblems. expr b, l, d; switch (e.kind()) { case expr_kind::Constant: @@ -965,6 +967,8 @@ public: l = mk_fresh_local(d, binding_info(e)); b = abstract(normalize_instances(instantiate(binding_body(e), l)), l); return update_binding(e, d, b); + case expr_kind::Let: + return normalize_instances(instantiate(let_body(e), let_value(e))); case expr_kind::App: buffer args; expr const & f = get_app_args(e, args);