From f38cbeda5ff2cc2a2a3d169ed16a11d5786d0c60 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 8 Nov 2018 17:03:34 -0800
Subject: [PATCH] perf(library/compiler/csimp): avoid unnecessary local decl

---
 src/library/compiler/csimp.cpp | 19 +++++++++++++------
 src/library/compiler/util.cpp  |  4 ++--
 src/library/compiler/util.h    |  2 +-
 3 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp
index 6425041661..0e572eeec2 100644
--- a/src/library/compiler/csimp.cpp
+++ b/src/library/compiler/csimp.cpp
@@ -481,13 +481,20 @@ class csimp_fn {
     }
 
     /* Given `e[x]`, create a let-decl `y := v`, and return `e[y]`
-       Note that, this transformation may produce type incorrect terms. */
+       Note that, this transformation may produce type incorrect terms.
+
+       Remove: if `v` is an atom, we do not create `y`. */
     expr apply_at(expr const & x, expr const & e, expr const & v) {
-        local_decl x_decl      = m_lctx.get_local_decl(x);
-        expr y                 = m_lctx.mk_local_decl(ngen(), x_decl.get_user_name(), x_decl.get_type(), v);
-        expr e_y               = replace_fvar(e, x, y);
-        m_fvars.push_back(y);
-        return visit(e_y, false);
+        if (is_lcnf_atom(v)) {
+            expr e_v = replace_fvar(e, x, v);
+            return visit(e_v, false);
+        } else {
+            local_decl x_decl      = m_lctx.get_local_decl(x);
+            expr y                 = m_lctx.mk_local_decl(ngen(), x_decl.get_user_name(), x_decl.get_type(), v);
+            expr e_y               = replace_fvar(e, x, y);
+            m_fvars.push_back(y);
+            return visit(e_y, false);
+        }
     }
 
     expr_pair mk_jp_cache_key(expr const & x, expr const & e, expr const & jp) {
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 5269d7a6b9..18670eca1a 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -269,12 +269,12 @@ void mark_used_fvars(expr const & e, buffer<expr> const & fvars, buffer<bool> &
         });
 }
 
-expr replace_fvar(expr const & e, expr const & fvar, expr const & new_fvar) {
+expr replace_fvar(expr const & e, expr const & fvar, expr const & new_term) {
     if (!has_fvar(e)) return e;
     return replace(e, [&](expr const & e, unsigned) {
             if (!has_fvar(e)) return some_expr(e);
             if (is_fvar(e) && fvar_name(fvar) == fvar_name(e))
-                return some_expr(new_fvar);
+                return some_expr(new_term);
             return none_expr();
         });
 }
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index ae7c0fd68d..3187dd2db6 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -107,7 +107,7 @@ void mark_used_fvars(expr const & e, buffer<expr> const & fvars, buffer<bool> &
 /* Return true if `e` contains the free variable `fvar` */
 bool has_fvar(expr const & e, expr const & fvar);
 
-expr replace_fvar(expr const & e, expr const & fvar, expr const & new_fvar);
+expr replace_fvar(expr const & e, expr const & fvar, expr const & new_term);
 
 void sort_fvars(local_ctx const & lctx, buffer<expr> & fvars);