From f1a3f8ec9d4167e3073ccea87f693de304ec585f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Nov 2015 14:24:59 -0800
Subject: [PATCH] feat(library/blast/congruence_closure): add blast.trace_cc
 option

---
 src/library/blast/congruence_closure.cpp |  7 +++++++
 src/library/blast/options.cpp            | 14 +++++++++++++-
 src/library/blast/options.h              |  1 +
 3 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index b9e02329e..16a0cbeef 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/blast/util.h"
 #include "library/blast/blast.h"
 #include "library/blast/trace.h"
+#include "library/blast/options.h"
 
 namespace lean {
 namespace blast {
@@ -831,6 +832,11 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
             s.mk_hypothesis(type, pr);
         }
     }
+
+    if (get_config().m_trace_cc) {
+        diagnostic(env(), ios()) << "added equivalence " << ppb(e1) << " [" << R << "] " << ppb(e2) << "\n";
+        display();
+    }
 }
 
 void congruence_closure::process_todo() {
@@ -1283,6 +1289,7 @@ void congruence_closure::display() const {
     diagnostic(env(), ios()) << "congruence closure state\n";
     display_eqcs();
     display_parents();
+    diagnostic(env(), ios()) << "\n";
 }
 
 bool congruence_closure::check_eqc(name const & R, expr const & e) const {
diff --git a/src/library/blast/options.cpp b/src/library/blast/options.cpp
index dea7a765e..4b74a5059 100644
--- a/src/library/blast/options.cpp
+++ b/src/library/blast/options.cpp
@@ -31,6 +31,9 @@ Author: Leonardo de Moura
 #ifndef LEAN_DEFAULT_BLAST_CC
 #define LEAN_DEFAULT_BLAST_CC true
 #endif
+#ifndef LEAN_DEFAULT_BLAST_TRACE_CC
+#define LEAN_DEFAULT_BLAST_TRACE_CC false
+#endif
 #ifndef LEAN_DEFAULT_BLAST_RECURSOR
 #define LEAN_DEFAULT_BLAST_RECURSOR true
 #endif
@@ -46,6 +49,7 @@ static name * g_blast_trace        = nullptr;
 static name * g_blast_subst        = nullptr;
 static name * g_blast_simp         = nullptr;
 static name * g_blast_cc           = nullptr;
+static name * g_blast_trace_cc     = nullptr;
 static name * g_blast_recursor     = nullptr;
 static name * g_blast_show_failure = nullptr;
 
@@ -70,6 +74,9 @@ bool get_blast_simp(options const & o) {
 bool get_blast_cc(options const & o) {
     return o.get_bool(*g_blast_cc, LEAN_DEFAULT_BLAST_CC);
 }
+bool get_blast_trace_cc(options const & o) {
+    return o.get_bool(*g_blast_trace_cc, LEAN_DEFAULT_BLAST_TRACE_CC);
+}
 bool get_blast_recursor(options const & o) {
     return o.get_bool(*g_blast_recursor, LEAN_DEFAULT_BLAST_RECURSOR);
 }
@@ -85,6 +92,7 @@ config::config(options const & o) {
     m_subst        = get_blast_subst(o);
     m_simp         = get_blast_simp(o);
     m_cc           = get_blast_cc(o);
+    m_trace_cc     = get_blast_trace_cc(o);
     m_recursor     = get_blast_recursor(o);
     m_show_failure = get_blast_show_failure(o);
 }
@@ -114,6 +122,7 @@ void initialize_options() {
     g_blast_subst        = new name{"blast", "subst"};
     g_blast_simp         = new name{"blast", "simp"};
     g_blast_cc           = new name{"blast", "cc"};
+    g_blast_trace_cc     = new name{"blast", "trace_cc"};
     g_blast_recursor     = new name{"blast", "recursor"};
     g_blast_show_failure = new name{"blast", "show_failure"};
 
@@ -131,9 +140,11 @@ void initialize_options() {
                          "(blast) enable simplier actions");
     register_bool_option(*blast::g_blast_cc, LEAN_DEFAULT_BLAST_CC,
                          "(blast) enable congruence closure");
+    register_bool_option(*blast::g_blast_trace_cc, LEAN_DEFAULT_BLAST_TRACE_CC,
+                         "(blast) (for debugging purposes) trace congruence closure");
     register_bool_option(*blast::g_blast_recursor, LEAN_DEFAULT_BLAST_RECURSOR,
                          "(blast) enable recursor action");
-    register_bool_option(*blast::g_blast_cc, LEAN_DEFAULT_BLAST_SHOW_FAILURE,
+    register_bool_option(*blast::g_blast_show_failure, LEAN_DEFAULT_BLAST_SHOW_FAILURE,
                          "(blast) show failure state");
 }
 void finalize_options() {
@@ -144,6 +155,7 @@ void finalize_options() {
     delete g_blast_subst;
     delete g_blast_simp;
     delete g_blast_cc;
+    delete g_blast_trace_cc;
     delete g_blast_recursor;
     delete g_blast_show_failure;
 }
diff --git a/src/library/blast/options.h b/src/library/blast/options.h
index 71f14e516..7162f509b 100644
--- a/src/library/blast/options.h
+++ b/src/library/blast/options.h
@@ -19,6 +19,7 @@ struct config {
     bool                       m_simp;
     bool                       m_recursor;
     bool                       m_cc;
+    bool                       m_trace_cc;
     bool                       m_show_failure;
     config(options const & o);
 };