From 2dd44bdf1a50b93f57108cd91672b511b66fbb0a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Oct 2013 14:52:08 -0700
Subject: [PATCH] perf(kernel/for_each): delay initialization of visited set

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/for_each.h | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/kernel/for_each.h b/src/kernel/for_each.h
index 15dbfb83a..e33f7199b 100644
--- a/src/kernel/for_each.h
+++ b/src/kernel/for_each.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <memory>
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"
 
@@ -19,17 +20,19 @@ namespace lean {
 */
 template<typename F>
 class for_each_fn {
-    expr_cell_offset_set m_visited;
-    F                    m_f;
+    std::unique_ptr<expr_cell_offset_set> m_visited;
+    F                                     m_f;
     static_assert(std::is_same<typename std::result_of<F(expr const &, unsigned)>::type, void>::value,
                   "for_each_fn: return type of m_f is not void");
 
     void apply(expr const & e, unsigned offset) {
         if (is_shared(e)) {
             expr_cell_offset p(e.raw(), offset);
-            if (m_visited.find(p) != m_visited.end())
+            if (!m_visited)
+                m_visited.reset(new expr_cell_offset_set());
+            if (m_visited->find(p) != m_visited->end())
                 return;
-            m_visited.insert(p);
+            m_visited->insert(p);
         }
 
         m_f(e, offset);