From 4efa9a92dff634eb94e034363d4c2f44ca77274b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 29 Jul 2013 20:59:15 -0700
Subject: [PATCH] Fix performance issue

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/deep_copy.cpp        |  4 +++-
 src/kernel/expr.h               | 20 ++++---------------
 src/kernel/replace.h            |  4 +++-
 src/tests/kernel/CMakeLists.txt |  3 +++
 src/tests/kernel/replace.cpp    | 35 +++++++++++++++++++++++++++++++++
 5 files changed, 48 insertions(+), 18 deletions(-)
 create mode 100644 src/tests/kernel/replace.cpp

diff --git a/src/kernel/deep_copy.cpp b/src/kernel/deep_copy.cpp
index 2174fc64e1..057c33ca88 100644
--- a/src/kernel/deep_copy.cpp
+++ b/src/kernel/deep_copy.cpp
@@ -14,10 +14,12 @@ class deep_copy_fn {
     expr_cell_map<expr> m_cache;
 
     expr apply(expr const & a) {
+        bool sh = false;
         if (is_shared(a)) {
             auto r = m_cache.find(a.raw());
             if (r != m_cache.end())
                 return r->second;
+            sh = true;
         }
         expr r;
         switch (a.kind()) {
@@ -33,7 +35,7 @@ class deep_copy_fn {
         case expr_kind::Lambda:   r = lambda(abst_name(a), apply(abst_type(a)), apply(abst_body(a))); break;
         case expr_kind::Pi:       r = pi(abst_name(a), apply(abst_type(a)), apply(abst_body(a))); break;
         }
-        if (is_shared(a))
+        if (sh)
             m_cache.insert(std::make_pair(a.raw(), r));
         return r;
     }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 832dfb4f99..b40e577039 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -77,21 +77,10 @@ public:
 
     friend void swap(expr & a, expr & b) { std::swap(a.m_ptr, b.m_ptr); }
 
-    expr & operator=(expr const & s) {
-        if (s.m_ptr)
-            s.m_ptr->inc_ref();
-        if (m_ptr)
-            m_ptr->dec_ref();
-        m_ptr = s.m_ptr;
-        return *this;
-    }
-    expr & operator=(expr && s) {
-        if (m_ptr)
-            m_ptr->dec_ref();
-        m_ptr = s.m_ptr;
-        s.m_ptr = 0;
-        return *this;
-    }
+    void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; }
+
+    expr & operator=(expr const & s) { LEAN_COPY_REF(expr, s); }
+    expr & operator=(expr && s) { LEAN_MOVE_REF(expr, s); }
 
     expr_kind kind() const { return m_ptr->kind(); }
     unsigned  hash() const { return m_ptr->hash(); }
@@ -345,5 +334,4 @@ struct args {
 */
 expr copy(expr const & e);
 // =======================================
-
 }
diff --git a/src/kernel/replace.h b/src/kernel/replace.h
index 9d699b2b0d..9bc1cec8ec 100644
--- a/src/kernel/replace.h
+++ b/src/kernel/replace.h
@@ -25,11 +25,13 @@ class replace_fn {
     F                          m_f;
 
     expr apply(expr const & e, unsigned offset) {
+        bool sh = false;
         if (is_shared(e)) {
             expr_cell_offset p(e.raw(), offset);
             auto it = m_cache.find(p);
             if (it != m_cache.end())
                 return it->second;
+            sh = true;
         }
 
         expr r = m_f(e, offset);
@@ -68,7 +70,7 @@ class replace_fn {
             }}
         }
 
-        if (is_shared(e))
+        if (sh)
             m_cache.insert(std::make_pair(expr_cell_offset(e.raw(), offset), r));
 
         return r;
diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt
index 8f3a1dcc58..4fb7a2b108 100644
--- a/src/tests/kernel/CMakeLists.txt
+++ b/src/tests/kernel/CMakeLists.txt
@@ -13,3 +13,6 @@ add_test(free_vars ${CMAKE_CURRENT_BINARY_DIR}/free_vars)
 add_executable(level level.cpp)
 target_link_libraries(level ${EXTRA_LIBS})
 add_test(level ${CMAKE_CURRENT_BINARY_DIR}/level)
+add_executable(replace replace.cpp)
+target_link_libraries(replace ${EXTRA_LIBS})
+add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace)
diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp
new file mode 100644
index 0000000000..2e76deb381
--- /dev/null
+++ b/src/tests/kernel/replace.cpp
@@ -0,0 +1,35 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "expr.h"
+#include "abstract.h"
+#include "deep_copy.h"
+#include "name.h"
+#include "test.h"
+using namespace lean;
+
+expr mk_big(expr f, unsigned depth, unsigned val) {
+    if (depth == 1)
+        return constant(name(val));
+    else
+        return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
+}
+
+static void tst1() {
+    expr f = constant("f");
+    expr r = mk_big(f, 16, 0);
+    expr n = constant(name(0u));
+    for (unsigned i = 0; i < 20; i++) {
+        r = abstract(n, r);
+    }
+}
+
+int main() {
+    continue_on_violation(true);
+    tst1();
+    std::cout << "done" << "\n";
+    return has_violations() ? 1 : 0;
+}