From bc8c5a3f68e5ab3332ca30699976a1aa728f4d73 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Nov 2015 13:05:20 -0800 Subject: [PATCH] feat(library/blast): basic tracing for blast --- src/library/blast/options.cpp | 19 +++++++ src/library/blast/options.h | 11 ++-- src/library/blast/simple_strategy.cpp | 74 +++++++++++++++++++++------ src/library/blast/state.cpp | 14 ++++- src/library/blast/state.h | 8 ++- 5 files changed, 105 insertions(+), 21 deletions(-) diff --git a/src/library/blast/options.cpp b/src/library/blast/options.cpp index 1e59f37bf..a4ae253a9 100644 --- a/src/library/blast/options.cpp +++ b/src/library/blast/options.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sexpr/option_declarations.h" +#include "library/blast/options.h" #ifndef LEAN_DEFAULT_BLAST_MAX_DEPTH #define LEAN_DEFAULT_BLAST_MAX_DEPTH 128 @@ -15,6 +16,9 @@ Author: Leonardo de Moura #ifndef LEAN_DEFAULT_BLAST_INC_DEPTH #define LEAN_DEFAULT_BLAST_INC_DEPTH 5 #endif +#ifndef LEAN_DEFAULT_BLAST_TRACE +#define LEAN_DEFAULT_BLAST_TRACE false +#endif namespace lean { namespace blast { @@ -22,6 +26,7 @@ namespace blast { static name * g_blast_max_depth = nullptr; static name * g_blast_init_depth = nullptr; static name * g_blast_inc_depth = nullptr; +static name * g_blast_trace = nullptr; unsigned get_blast_max_depth(options const & o) { return o.get_unsigned(*g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH); @@ -32,11 +37,22 @@ unsigned get_blast_init_depth(options const & o) { unsigned get_blast_inc_depth(options const & o) { return o.get_unsigned(*g_blast_inc_depth, LEAN_DEFAULT_BLAST_INC_DEPTH); } +bool get_blast_trace(options const & o) { + return o.get_bool(*g_blast_trace, LEAN_DEFAULT_BLAST_TRACE); +} + +config::config(options const & o) { + m_max_depth = get_blast_max_depth(o); + m_init_depth = get_blast_init_depth(o); + m_inc_depth = get_blast_inc_depth(o); + m_trace = get_blast_trace(o); +} void initialize_options() { g_blast_max_depth = new name{"blast", "max_depth"}; g_blast_init_depth = new name{"blast", "init_depth"}; g_blast_inc_depth = new name{"blast", "inc_depth"}; + g_blast_trace = new name{"blast", "trace"}; register_unsigned_option(*blast::g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH, "(blast) max search depth for blast"); @@ -44,10 +60,13 @@ void initialize_options() { "(blast) initial search depth for blast (remark: blast uses iteration deepening)"); register_unsigned_option(*blast::g_blast_inc_depth, LEAN_DEFAULT_BLAST_INC_DEPTH, "(blast) search depth increment for blast (remark: blast uses iteration deepening)"); + register_bool_option(*blast::g_blast_trace, LEAN_DEFAULT_BLAST_TRACE, + "(blast) trace"); } void finalize_options() { delete g_blast_max_depth; delete g_blast_init_depth; delete g_blast_inc_depth; + delete g_blast_trace; } }} diff --git a/src/library/blast/options.h b/src/library/blast/options.h index b26f42eca..93edfdb58 100644 --- a/src/library/blast/options.h +++ b/src/library/blast/options.h @@ -9,9 +9,14 @@ Author: Leonardo de Moura namespace lean { namespace blast { -unsigned get_blast_max_depth(options const & o); -unsigned get_blast_init_depth(options const & o); -unsigned get_blast_inc_depth(options const & o); +/** \brief Blast configuration object. */ +struct config { + unsigned m_max_depth; + unsigned m_init_depth; + unsigned m_inc_depth; + bool m_trace; + config(options const & o); +}; void initialize_options(); void finalize_options(); }} diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index efc510800..185e90c8b 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -16,45 +16,78 @@ namespace blast { /** \brief Implement a simple proof strategy for blast. We use it mainly for testing new actions and the whole blast infra-structure. */ class simple_strategy { - unsigned m_max_depth; - unsigned m_init_depth; - unsigned m_inc_depth; + config m_config; enum status { NoAction, ClosedBranch, Continue }; + void display_msg(char const * msg) { + ios().get_diagnostic_channel() << msg << "\n\n"; + } + + void display_action(char const * name) { + if (m_config.m_trace) { + ios().get_diagnostic_channel() << "== action: " << name << " ==>\n\n"; + } + } + + void display() { + if (m_config.m_trace) { + auto out = diagnostic(env(), ios()); + out << "state [" << curr_state().get_proof_depth() << "], #choice: " << get_num_choice_points() << "\n"; + display_curr_state(); + } + } + + void display_if(action_result r) { + if (m_config.m_trace && !failed(r)) + display(); + } + optional activate_hypothesis() { return curr_state().activate_hypothesis(); } action_result next_action() { - if (intros_action()) + if (intros_action()) { + display_action("intros"); return action_result::new_branch(); + } if (auto hidx = activate_hypothesis()) { - if (auto pr = assumption_contradiction_actions(*hidx)) + display_action("activate"); + if (auto pr = assumption_contradiction_actions(*hidx)) { + display_action("assumption-contradiction"); return action_result::solved(*pr); + } return action_result::new_branch(); } if (auto pr = assumption_action()) { // Remark: this action is only relevant // when the target has been modified. + display_action("assumption"); return action_result::solved(*pr); } action_result r = constructor_action(); - if (!failed(r)) return r; + if (!failed(r)) { + display_action("constructor"); + return r; + } // TODO(Leo): add more actions... + + display_msg(">>> FAILED <<<"); return action_result::failed(); } action_result next_branch(expr pr) { while (curr_state().has_proof_steps()) { proof_step s = curr_state().top_proof_step(); - action_result r = s.resolve(pr); + action_result r = s.resolve(pr); switch (r.get_kind()) { case action_result::Failed: + display_msg(">>> next-branch FAILED <<<"); return r; case action_result::Solved: pr = r.get_proof(); @@ -68,41 +101,53 @@ class simple_strategy { } optional search_upto(unsigned depth) { + if (m_config.m_trace) { + ios().get_diagnostic_channel() << "* Search upto depth " << depth << "\n\n"; + } + display(); action_result r = next_action(); + display_if(r); while (true) { lean_assert(curr_state().check_invariant()); - if (curr_state().get_proof_depth() > depth) + if (curr_state().get_proof_depth() > depth) { + display_msg(">>> maximum search depth reached <<<"); r = action_result::failed(); + } switch (r.get_kind()) { case action_result::Failed: r = next_choice_point(); if (failed(r)) { // all choice points failed... + display_msg(">>> proof not found, no choice points left <<<"); return none_expr(); } + display_msg("* next choice point"); break; case action_result::Solved: r = next_branch(r.get_proof()); if (r.get_kind() == action_result::Solved) { // all branches have been solved + display_msg("* found proof"); return some_expr(r.get_proof()); } + display_msg("* next branch"); break; case action_result::NewBranch: r = next_action(); break; } + display_if(r); } } optional search() { state s = curr_state(); - unsigned d = m_init_depth; + unsigned d = m_config.m_init_depth; while (true) { if (auto r = search_upto(d)) return r; - d += m_inc_depth; - if (d > m_max_depth) { + d += m_config.m_inc_depth; + if (d > m_config.m_max_depth) { display_curr_state(); return none_expr(); } @@ -112,11 +157,8 @@ class simple_strategy { } public: - simple_strategy() { - options o = ios().get_options(); - m_max_depth = get_blast_max_depth(o); - m_init_depth = get_blast_init_depth(o); - m_inc_depth = get_blast_inc_depth(o); + simple_strategy(): + m_config(ios().get_options()) { } optional operator()() { diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index d438fd230..b8bc649a4 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -109,9 +109,21 @@ goal state::to_goal() const { return goal(new_meta, new_target); } +void state::display_active(output_channel & out) const { + out << "active := {"; + bool first = true; + m_branch.m_active.for_each([&](hypothesis_idx hidx) { + if (first) first = false; else out << ", "; + out << get_hypothesis_decl(hidx)->get_name(); + }); + out << "}\n"; +} + void state::display(environment const & env, io_state const & ios) const { formatter fmt = ios.get_formatter_factory()(env, ios.get_options()); - ios.get_diagnostic_channel() << mk_pair(to_goal().pp(fmt), ios.get_options()); + auto & out = ios.get_diagnostic_channel(); + out << mk_pair(to_goal().pp(fmt), ios.get_options()) << "\n"; + display_active(out); } bool state::has_assigned_uref(level const & l) const { diff --git a/src/library/blast/state.h b/src/library/blast/state.h index e58d2df7a..92a76726f 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -100,7 +100,11 @@ public: class branch { friend class state; typedef hypothesis_idx_map forward_deps; - typedef rb_map todo_queue; + /* trick to make sure the rb_map::erase_min removes the hypothesis with biggest weight */ + struct inv_double_cmp { + int operator()(double const & d1, double const & d2) const { return d1 > d2 ? -1 : (d1 < d2 ? 1 : 0); } + }; + typedef rb_map todo_queue; // Hypothesis/facts in the current state hypothesis_decls m_hyp_decls; // We break the set of hypotheses in m_hyp_decls in 4 sets that are not necessarily disjoint: @@ -167,6 +171,8 @@ class state { void collect_forward_deps(hypothesis_idx hidx, buffer & result, hypothesis_idx_set & already_found); bool safe_to_delete(buffer const & to_delete); + void display_active(output_channel & out) const; + #ifdef LEAN_DEBUG bool check_hypothesis(expr const & e, hypothesis_idx hidx, hypothesis const & h) const; bool check_hypothesis(hypothesis_idx hidx, hypothesis const & h) const;