From 712f60d003c51b0107613f8922f791bc31995c8d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Nov 2015 14:41:22 -0800
Subject: [PATCH] feat(library/blast/congruence_closure): expose get_cc()

---
 src/library/blast/assert_cc_action.cpp   | 21 ---------------------
 src/library/blast/assert_cc_action.h     |  3 ---
 src/library/blast/congruence_closure.cpp | 16 ++++++++++++++++
 src/library/blast/congruence_closure.h   |  3 +++
 src/library/blast/init_module.cpp        |  3 ---
 5 files changed, 19 insertions(+), 27 deletions(-)

diff --git a/src/library/blast/assert_cc_action.cpp b/src/library/blast/assert_cc_action.cpp
index a797977c4..47f78d8f3 100644
--- a/src/library/blast/assert_cc_action.cpp
+++ b/src/library/blast/assert_cc_action.cpp
@@ -12,27 +12,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
-static unsigned g_ext_id = 0;
-struct cc_branch_extension : public branch_extension {
-    congruence_closure m_cc;
-    cc_branch_extension() {}
-    cc_branch_extension(cc_branch_extension const & o):m_cc(o.m_cc) {}
-    virtual ~cc_branch_extension() {}
-    virtual branch_extension * clone() override { return new cc_branch_extension(*this); }
-    virtual void initialized() override { m_cc.initialize(); }
-    virtual void target_updated() override { m_cc.internalize(curr_state().get_target()); }
-};
-
-void initialize_assert_cc_action() {
-    g_ext_id = register_branch_extension(new cc_branch_extension());
-}
-
-void finalize_assert_cc_action() {}
-
-static congruence_closure & get_cc() {
-    return static_cast<cc_branch_extension&>(curr_state().get_extension(g_ext_id)).m_cc;
-}
-
 action_result assert_cc_action(hypothesis_idx hidx) {
     if (!get_config().m_cc)
         return action_result::failed();
diff --git a/src/library/blast/assert_cc_action.h b/src/library/blast/assert_cc_action.h
index a5c58075e..1d8852cad 100644
--- a/src/library/blast/assert_cc_action.h
+++ b/src/library/blast/assert_cc_action.h
@@ -12,7 +12,4 @@ namespace lean {
 namespace blast {
 /** \brief Assert the given hypothesis into the congruence closure module */
 action_result assert_cc_action(hypothesis_idx hidx);
-
-void initialize_assert_cc_action();
-void finalize_assert_cc_action();
 }}
diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index cfb1c57a0..0e7bc2f19 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -1324,7 +1324,23 @@ bool congruence_closure::check_invariant() const {
     return true;
 }
 
+static unsigned g_ext_id = 0;
+struct cc_branch_extension : public branch_extension {
+    congruence_closure m_cc;
+    cc_branch_extension() {}
+    cc_branch_extension(cc_branch_extension const & o):m_cc(o.m_cc) {}
+    virtual ~cc_branch_extension() {}
+    virtual branch_extension * clone() override { return new cc_branch_extension(*this); }
+    virtual void initialized() override { m_cc.initialize(); }
+    virtual void target_updated() override { m_cc.internalize(curr_state().get_target()); }
+};
+
+congruence_closure & get_cc() {
+    return static_cast<cc_branch_extension&>(curr_state().get_extension(g_ext_id)).m_cc;
+}
+
 void initialize_congruence_closure() {
+    g_ext_id = register_branch_extension(new cc_branch_extension());
     name prefix = name::mk_internal_unique_name();
     g_congr_mark    = new expr(mk_constant(name(prefix, "[congruence]")));
     g_iff_true_mark = new expr(mk_constant(name(prefix, "[iff-true]")));
diff --git a/src/library/blast/congruence_closure.h b/src/library/blast/congruence_closure.h
index 3d46ca1d3..00ec0b79d 100644
--- a/src/library/blast/congruence_closure.h
+++ b/src/library/blast/congruence_closure.h
@@ -216,6 +216,9 @@ public:
     ~scope_congruence_closure();
 };
 
+/** \brief Return the congruence closure object associated with the current state */
+congruence_closure & get_cc();
+
 void initialize_congruence_closure();
 void finalize_congruence_closure();
 }}
diff --git a/src/library/blast/init_module.cpp b/src/library/blast/init_module.cpp
index 47a9659d9..7f06925a8 100644
--- a/src/library/blast/init_module.cpp
+++ b/src/library/blast/init_module.cpp
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "library/blast/options.h"
 #include "library/blast/congruence_closure.h"
 #include "library/blast/recursor_action.h"
-#include "library/blast/assert_cc_action.h"
 #include "library/blast/simplifier/init_module.h"
 #include "library/blast/backward/init_module.h"
 #include "library/blast/forward/init_module.h"
@@ -29,12 +28,10 @@ void initialize_blast_module() {
     blast::initialize_unit_module();
     initialize_blast_tactic();
     blast::initialize_recursor_action();
-    blast::initialize_assert_cc_action();
     blast::initialize_congruence_closure();
 }
 void finalize_blast_module() {
     blast::finalize_congruence_closure();
-    blast::finalize_assert_cc_action();
     blast::finalize_recursor_action();
     finalize_blast_tactic();
     blast::finalize_unit_module();