feat(library/blast): basic tracing for blast

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

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);
+/** \brief Blast configuration object. */
-unsigned get_blast_init_depth(options const & o);
+struct config {
-unsigned get_blast_inc_depth(options const & o);
+    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();
 }}

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;
+    config m_config;
-    unsigned                   m_init_depth;
-    unsigned                   m_inc_depth;
 
     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<hypothesis_idx> 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<expr> 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<expr> 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;
+            d += m_config.m_inc_depth;
-            if (d > m_max_depth) {
+            if (d > m_config.m_max_depth) {
                 display_curr_state();
                 return none_expr();
             }
@@ -112,11 +157,8 @@ class simple_strategy {
     }
 
 public:
-    simple_strategy() {
+    simple_strategy():
-        options o = ios().get_options();
+        m_config(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);
     }
 
     optional<expr> operator()() {

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 {

src/library/blast/state.h

@@ -100,7 +100,11 @@ public:
 class branch {
     friend class state;
     typedef hypothesis_idx_map<hypothesis_idx_set> forward_deps;
-    typedef rb_map<double, hypothesis_idx, double_cmp>   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<double, hypothesis_idx, inv_double_cmp>   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<hypothesis_idx> & result, hypothesis_idx_set & already_found);
     bool safe_to_delete(buffer<hypothesis_idx> 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;