michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast/congruence_closure): use new tracing infrastructure

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-08 15:17:24 -08:00
parent 7da64a768f
commit b145a7332a
7 changed files with 43 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/blast/blast.cpp
View file

@ -1149,9 +1149,13 @@ optional<expr> blast_goal(environment const & env, io_state const & ios, list<na
}
void initialize_blast() {
register_trace_class("blast");
register_trace_class(name{"blast", "all"});
register_trace_class(name({"blast", "event"}));
register_trace_class_alias("app_builder", name({"blast", "event"}));
register_trace_class_alias(name({"simplifier", "failure"}), name({"blast", "event"}));
register_trace_class_alias("app_builder", name({"blast", "all"}));
register_trace_class_alias(name({"simplifier", "failure"}), name({"blast", "all"}));
register_trace_class_alias(name({"congruence_closure", "merge"}), name({"blast", "all"}));
blast::g_prefix = new name(name::mk_internal_unique_name());
blast::g_tmp_prefix = new name(name::mk_internal_unique_name());
blast::g_ref_prefix = new name(name::mk_internal_unique_name());

42
src/library/blast/congruence_closure.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include <algorithm>
#include <vector>
#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]")));

8
src/library/blast/congruence_closure.h
View file

@ -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;
};

12
src/library/blast/options.cpp
View file

@ -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;

1
src/library/blast/options.h
View file

@ -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;

2
tests/lean/run/blast_cc1.lean
View file

@ -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

11
tests/lean/run/simplifier1.lean Normal file
View file

@ -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