From 73b97084f7e060ba2ba3d02fc3d5bba8c3f807db Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 1 Feb 2018 12:39:14 -0800
Subject: [PATCH] chore(library/tactic): ac_manager ==> ac_manager_old

We will build the new one in `library/`
---
 src/library/tactic/ac_tactics.cpp  | 20 ++++++++++----------
 src/library/tactic/ac_tactics.h    |  6 +++---
 src/library/tactic/smt/theory_ac.h |  2 +-
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/library/tactic/ac_tactics.cpp b/src/library/tactic/ac_tactics.cpp
index e21dcc057a..5eff233f38 100644
--- a/src/library/tactic/ac_tactics.cpp
+++ b/src/library/tactic/ac_tactics.cpp
@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 #include "library/tactic/ac_tactics.h"
 
 namespace lean {
-struct ac_manager::cache {
+struct ac_manager_old::cache {
     environment                     m_env;
     unsigned                        m_reducibility_fingerprint;
     unsigned                        m_instance_fingerprint;
@@ -30,18 +30,18 @@ struct ac_manager::cache {
         m_instance_fingerprint(get_instance_fingerprint(env)) {}
 };
 
-MK_THREAD_LOCAL_GET_DEF(ac_manager::cache_ptr, get_cache_ptr);
+MK_THREAD_LOCAL_GET_DEF(ac_manager_old::cache_ptr, get_cache_ptr);
 
-static ac_manager::cache_ptr get_cache(environment const & env) {
+static ac_manager_old::cache_ptr get_cache(environment const & env) {
     auto & cache_ptr = get_cache_ptr();
     if (!cache_ptr ||
         !env.is_descendant(cache_ptr->m_env) ||
         get_reducibility_fingerprint(env) != cache_ptr->m_reducibility_fingerprint ||
         get_instance_fingerprint(env)     != cache_ptr->m_instance_fingerprint) {
         cache_ptr.reset();
-        return std::make_shared<ac_manager::cache>(env);
+        return std::make_shared<ac_manager_old::cache>(env);
     }
-    ac_manager::cache_ptr r = cache_ptr;
+    ac_manager_old::cache_ptr r = cache_ptr;
     cache_ptr.reset();
     r->m_env = env;
     if (!is_decl_eqp(env, r->m_env)) {
@@ -52,20 +52,20 @@ static ac_manager::cache_ptr get_cache(environment const & env) {
     return r;
 }
 
-static void recycle_cache(ac_manager::cache_ptr const & cache) {
+static void recycle_cache(ac_manager_old::cache_ptr const & cache) {
     get_cache_ptr() = cache;
 }
 
-ac_manager::ac_manager(type_context & ctx):
+ac_manager_old::ac_manager_old(type_context & ctx):
     m_ctx(ctx),
     m_cache_ptr(get_cache(ctx.env())) {
 }
 
-ac_manager::~ac_manager() {
+ac_manager_old::~ac_manager_old() {
     recycle_cache(m_cache_ptr);
 }
 
-optional<expr> ac_manager::is_assoc(expr const & e) {
+optional<expr> ac_manager_old::is_assoc(expr const & e) {
     auto op = get_binary_op(e);
     if (!op) return none_expr();
     bool idx = has_local(e);
@@ -82,7 +82,7 @@ optional<expr> ac_manager::is_assoc(expr const & e) {
     return r;
 }
 
-optional<expr> ac_manager::is_comm(expr const & e) {
+optional<expr> ac_manager_old::is_comm(expr const & e) {
     auto op = get_binary_op(e);
     if (!op) return none_expr();
     bool idx = has_local(e);
diff --git a/src/library/tactic/ac_tactics.h b/src/library/tactic/ac_tactics.h
index 1fa56a0565..4dc504553e 100644
--- a/src/library/tactic/ac_tactics.h
+++ b/src/library/tactic/ac_tactics.h
@@ -61,7 +61,7 @@ namespace lean {
 
    Summary: we need to move this module to `library/`, we need to extend it, and add missing optimizations.
 */
-class ac_manager {
+class ac_manager_old {
 public:
     struct cache;
     typedef std::shared_ptr<cache> cache_ptr;
@@ -69,8 +69,8 @@ private:
     type_context & m_ctx;
     cache_ptr      m_cache_ptr;
 public:
-    ac_manager(type_context & ctx);
-    ~ac_manager();
+    ac_manager_old(type_context & ctx);
+    ~ac_manager_old();
     /* If e is of the form (op a b), and op is associative (i.e., there is an instance (is_associative _ op)), then
        return proof term for forall x y z, op (op x y) z = op x (op y z) */
     optional<expr> is_assoc(expr const & e);
diff --git a/src/library/tactic/smt/theory_ac.h b/src/library/tactic/smt/theory_ac.h
index a241cdc23f..33d27a1b15 100644
--- a/src/library/tactic/smt/theory_ac.h
+++ b/src/library/tactic/smt/theory_ac.h
@@ -92,7 +92,7 @@ private:
     type_context &       m_ctx;
     congruence_closure & m_cc;
     state &              m_state;
-    ac_manager           m_ac_manager;
+    ac_manager_old       m_ac_manager;
     buffer<expr_triple>  m_todo;
 
     expr convert(expr const & op, expr const & e, buffer<expr> & args);