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

chore(library/blast/blast): reorg blast tracing

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-08 15:57:25 -08:00
parent f0c42defc8
commit 78533cde0a
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1149,13 +1149,17 @@ 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_detailed"});
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"}));
register_trace_class_alias("blast", "blast_detailed");
register_trace_class_alias("app_builder", "blast_detailed");
register_trace_class_alias(name({"simplifier", "failure"}), "blast_detailed");
register_trace_class_alias(name({"congruence_closure", "merge"}), "blast_detailed");
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());