From b145a7332a683bb7b32a076edc3dec8ec9e1c812 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Dec 2015 15:17:24 -0800 Subject: [PATCH] feat(library/blast/congruence_closure): use new tracing infrastructure --- src/library/blast/blast.cpp | 4 +++ src/library/blast/congruence_closure.cpp | 42 +++++++++++++----------- src/library/blast/congruence_closure.h | 8 ++--- src/library/blast/options.cpp | 12 ------- src/library/blast/options.h | 1 - tests/lean/run/blast_cc1.lean | 2 ++ tests/lean/run/simplifier1.lean | 11 +++++++ 7 files changed, 43 insertions(+), 37 deletions(-) create mode 100644 tests/lean/run/simplifier1.lean diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index c33c347272..42a862b163 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -1149,9 +1149,13 @@ optional blast_goal(environment const & env, io_state const & ios, list #include #include "kernel/abstract.h" +#include "library/trace.h" #include "library/constants.h" #include "library/blast/simplifier/simp_rule_set.h" #include "library/blast/congruence_closure.h" @@ -846,10 +847,8 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con update_mt(R, e2_root); - if (get_config().m_trace_cc) { - diagnostic(env(), ios()) << "added equivalence " << ppb(e1) << " [" << R << "] " << ppb(e2) << "\n"; - display(); - } + lean_trace(name({"congruence_closure", "merge"}), tout() << ppb(e1) << " [" << R << "] " << ppb(e2) << "\n";); + lean_trace(name({"congruence_closure", "state"}), trace();); } void congruence_closure::process_todo() { @@ -1275,8 +1274,8 @@ void congruence_closure::freeze_partitions() { m_entries = new_entries; } -void congruence_closure::display_eqc(name const & R, expr const & e) const { - auto out = diagnostic(env(), ios()); +void congruence_closure::trace_eqc(name const & R, expr const & e) const { + auto out = tout(); bool first = true; expr it = e; out << R << " {"; @@ -1289,42 +1288,42 @@ void congruence_closure::display_eqc(name const & R, expr const & e) const { out << "}"; } -void congruence_closure::display_eqcs() const { - auto out = diagnostic(env(), ios()); +void congruence_closure::trace_eqcs() const { + auto out = tout(); m_entries.for_each([&](eqc_key const & k, entry const & n) { if (k.m_expr == n.m_root) { - display_eqc(k.m_R, k.m_expr); + trace_eqc(k.m_R, k.m_expr); out << "\n"; } }); } -static void display_rel(io_state_stream & out, name const & R) { +static void trace_rel(io_state_stream & out, name const & R) { if (R != get_eq_name()) - out << "[" << R << "] "; + out << "(" << R << ") "; } -void congruence_closure::display_parents() const { - auto out = diagnostic(env(), ios()); +void congruence_closure::trace_parents() const { + auto out = tout(); m_parents.for_each([&](child_key const & k, parent_occ_set const & ps) { - display_rel(out, k.m_R); + trace_rel(out, k.m_R); out << ppb(k.m_expr); out << ", parents: {"; bool first = true; ps.for_each([&](parent_occ const & o) { if (first) first = false; else out << ", "; - display_rel(out, o.m_R); + trace_rel(out, o.m_R); out << ppb(o.m_expr); }); out << "}\n"; }); } -void congruence_closure::display() const { - diagnostic(env(), ios()) << "congruence closure state\n"; - display_eqcs(); - display_parents(); - diagnostic(env(), ios()) << "\n"; +void congruence_closure::trace() const { + tout() << "\n"; + trace_eqcs(); + trace_parents(); + tout() << "\n"; } bool congruence_closure::check_eqc(name const & R, expr const & e) const { @@ -1376,6 +1375,9 @@ congruence_closure & get_cc() { } void initialize_congruence_closure() { + register_trace_class("congruence_closure"); + register_trace_class({"congruence_closure", "state"}); + register_trace_class({"congruence_closure", "merge"}); 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]"))); diff --git a/src/library/blast/congruence_closure.h b/src/library/blast/congruence_closure.h index d7cdf12ba6..5d49461b59 100644 --- a/src/library/blast/congruence_closure.h +++ b/src/library/blast/congruence_closure.h @@ -143,7 +143,7 @@ class congruence_closure { expr mk_congr_proof(name const & R, expr const & lhs, expr const & rhs) const; expr mk_proof(name const & R, expr const & lhs, expr const & rhs, expr const & H) const; - void display_eqc(name const & R, expr const & e) const; + void trace_eqc(name const & R, expr const & e) const; public: void initialize(); @@ -220,9 +220,9 @@ public: unsigned get_mt(name const & R, expr const & e) const; /** \brief dump for debugging purposes. */ - void display() const; - void display_eqcs() const; - void display_parents() const; + void trace() const; + void trace_eqcs() const; + void trace_parents() const; bool check_eqc(name const & R, expr const & e) const; bool check_invariant() const; }; diff --git a/src/library/blast/options.cpp b/src/library/blast/options.cpp index cc50b10749..32c05c4c30 100644 --- a/src/library/blast/options.cpp +++ b/src/library/blast/options.cpp @@ -35,9 +35,6 @@ 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 @@ -65,7 +62,6 @@ static name * g_blast_trace_pre = 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_ematch = nullptr; static name * g_blast_backward = nullptr; @@ -97,9 +93,6 @@ 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); } @@ -128,7 +121,6 @@ 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_ematch = get_blast_ematch(o); m_backward = get_blast_backward(o); @@ -163,7 +155,6 @@ 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_ematch = new name{"blast", "ematch"}; g_blast_backward = new name{"blast", "backward"}; @@ -187,8 +178,6 @@ 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_ematch, LEAN_DEFAULT_BLAST_EMATCH, @@ -213,7 +202,6 @@ 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_ematch; delete g_blast_backward; diff --git a/src/library/blast/options.h b/src/library/blast/options.h index b306af9a98..e16ed4e496 100644 --- a/src/library/blast/options.h +++ b/src/library/blast/options.h @@ -22,7 +22,6 @@ struct config { bool m_ematch; bool m_cc; bool m_backward; - bool m_trace_cc; bool m_show_failure; char const * m_strategy; unsigned m_pattern_max_steps; diff --git a/tests/lean/run/blast_cc1.lean b/tests/lean/run/blast_cc1.lean index 81d764cfc3..a17c319580 100644 --- a/tests/lean/run/blast_cc1.lean +++ b/tests/lean/run/blast_cc1.lean @@ -18,5 +18,7 @@ open perm example (a b c d : list nat) : a ~ b → c ~ b → d ~ c → a ~ d := by blast +set_option trace.congruence_closure true + example (a b c d : list nat) : a ~ b → c ~ b → d = c → a ~ d := by blast diff --git a/tests/lean/run/simplifier1.lean b/tests/lean/run/simplifier1.lean new file mode 100644 index 0000000000..daedc6317f --- /dev/null +++ b/tests/lean/run/simplifier1.lean @@ -0,0 +1,11 @@ +constant P : Type₁ +constant P_sub : subsingleton P +attribute P_sub [instance] +constant q : P → nat → Prop + +set_option blast.simp false +set_option blast.trace true +set_option trace.congruence_closure true + +example (a : nat) (h₁ h₂ : P) : q h₁ a = q h₂ a := +by blast