From 969afa824562b87657226cabcb7d69a59d5a06f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Aug 2014 18:28:23 -0700 Subject: [PATCH] perf(library/unifier): improve check_imitation performance Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 2c467624a..f5927b81e 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1232,7 +1232,15 @@ struct unifier_fn { /** \brief Check if term \c e (produced by an imitation step) is type correct, and store generated constraints in \c cs. Include \c j in all generated constraints */ - bool check_imitation(expr const & e, justification const & j, bool relax, buffer & cs) { + bool check_imitation(expr e, justification const & j, bool relax, buffer & cs) { + buffer ls; + while (is_lambda(e)) { + expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); + expr l = mk_local(m_ngen.next(), binding_name(e), d, binding_info(e)); + ls.push_back(l); + e = binding_body(e); + } + e = instantiate_rev(e, ls.size(), ls.data());; try { buffer aux; m_tc[relax]->check(e, aux);