diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index b0c7f41b9..f2af40100 100644 --- a/src/library/blast/CMakeLists.txt +++ b/src/library/blast/CMakeLists.txt @@ -2,4 +2,4 @@ add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp init_module.cpp simplifier.cpp simple_actions.cpp intros_action.cpp proof_expr.cpp options.cpp choice_point.cpp simple_strategy.cpp backward_action.cpp util.cpp gexpr.cpp revert_action.cpp subst_action.cpp no_confusion_action.cpp - simplify_actions.cpp) + simplify_actions.cpp strategy.cpp) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 8c8a97eb9..483a7e1aa 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "library/blast/proof_expr.h" #include "library/blast/blast_exception.h" #include "library/blast/simple_strategy.h" +#include "library/blast/choice_point.h" namespace lean { namespace blast { @@ -412,6 +413,7 @@ public: m_tctx(*this), m_normalizer(m_tctx) { init_uref_mref_href_idxs(); + clear_choice_points(); } ~blastenv() { diff --git a/src/library/blast/choice_point.cpp b/src/library/blast/choice_point.cpp index 0198b798f..12ba2b933 100644 --- a/src/library/blast/choice_point.cpp +++ b/src/library/blast/choice_point.cpp @@ -20,10 +20,10 @@ void push_choice_point(choice_point const & c) { get_choice_points().push_back(c); } -action_result next_choice_point() { +action_result next_choice_point(unsigned base) { auto & cs = get_choice_points(); while (true) { - if (cs.empty()) + if (cs.size() == base) return action_result::failed(); action_result r = cs.back().next(); if (!failed(r)) diff --git a/src/library/blast/choice_point.h b/src/library/blast/choice_point.h index 800ed9bf5..22ed2d6da 100644 --- a/src/library/blast/choice_point.h +++ b/src/library/blast/choice_point.h @@ -61,7 +61,7 @@ inline void push_choice_point(choice_point_cell * cell) { push_choice_point(choice_point(cell)); } /** \brief Keep executing choice points until one of them doesn't fail. */ -action_result next_choice_point(); +action_result next_choice_point(unsigned base = 0); /** \brief Return size of the choice point stack */ unsigned get_num_choice_points(); /** \brief Shrink the size of the choice point stack. @@ -69,4 +69,11 @@ unsigned get_num_choice_points(); void shrink_choice_points(unsigned n); /** \brief Clear/remove all choice points */ void clear_choice_points(); + +class scope_choice_points { + unsigned m_num_choices; +public: + scope_choice_points():m_num_choices(get_num_choice_points()) {} + ~scope_choice_points() { shrink_choice_points(m_num_choices); } +}; }} diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index 77b529059..9148655c7 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -14,41 +14,14 @@ Author: Leonardo de Moura #include "library/blast/backward_action.h" #include "library/blast/no_confusion_action.h" #include "library/blast/simplify_actions.h" +#include "library/blast/recursor_action.h" +#include "library/blast/strategy.h" namespace lean { 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 { - config m_config; - - enum status { NoAction, ClosedBranch, Continue }; - - void display_msg(char const * msg) { - if (m_config.m_trace) { - 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(); - } - +class simple_strategy : public strategy { optional activate_hypothesis() { return curr_state().activate_hypothesis(); } @@ -56,7 +29,7 @@ class simple_strategy { /* \brief Preprocess state It keeps applying intros, activating and finally simplify target. Return an expression if the goal has been proved during preprocessing step. */ - optional preprocess_core() { + virtual optional preprocess() { display_msg("* Preprocess"); while (true) { if (intros_action()) @@ -79,20 +52,7 @@ class simple_strategy { return simplify_target_action().to_opt_expr(); } - optional preprocess() { - if (auto pr = preprocess_core()) { - auto r = next_branch(*pr); - if (!solved(r)) { - throw exception("invalid blast preprocessing action, preprocessing actions should not create branches"); - } else { - return r.to_opt_expr(); - } - } else { - return none_expr(); - } - } - - action_result next_action() { + virtual action_result next_action() { if (intros_action()) { display_action("intros"); return action_result::new_branch(); @@ -139,96 +99,6 @@ class simple_strategy { 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(unfold_hypotheses_ge(curr_state(), pr)); - switch (r.get_kind()) { - case action_result::Failed: - display_msg(">>> next-branch FAILED <<<"); - return r; - case action_result::Solved: - pr = r.get_proof(); - curr_state().pop_proof_step(); - break; - case action_result::NewBranch: - return action_result::new_branch(); - } - } - return action_result::solved(pr); - } - - 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) { - 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() { - clear_choice_points(); - curr_state().set_simp_rule_sets(get_simp_rule_sets(env())); - if (auto pr = preprocess()) - return pr; - if (get_num_choice_points() > 0) - throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points"); - state s = curr_state(); - unsigned d = m_config.m_init_depth; - while (true) { - if (auto r = search_upto(d)) - return r; - d += m_config.m_inc_depth; - if (d > m_config.m_max_depth) { - display_curr_state(); - return none_expr(); - } - curr_state() = s; - clear_choice_points(); - } - } - -public: - simple_strategy(): - m_config(ios().get_options()) { - } - - optional operator()() { - return search(); - } }; optional apply_simple_strategy() { diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp new file mode 100644 index 000000000..a7822ab58 --- /dev/null +++ b/src/library/blast/strategy.cpp @@ -0,0 +1,137 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/blast/strategy.h" +#include "library/blast/choice_point.h" +#include "library/blast/blast.h" +#include "library/blast/proof_expr.h" + +namespace lean { +namespace blast { +strategy::strategy(): + m_config(ios().get_options()) { +} + +void strategy::display_msg(char const * msg) { + if (m_config.m_trace) { + ios().get_diagnostic_channel() << msg << "\n\n"; + } +} + +void strategy::display_action(char const * name) { + if (m_config.m_trace) { + ios().get_diagnostic_channel() << "== action: " << name << " ==>\n\n"; + } +} + +void strategy::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 strategy::display_if(action_result r) { + if (m_config.m_trace && !failed(r)) + display(); +} + +action_result strategy::next_branch(expr pr) { + while (curr_state().has_proof_steps()) { + proof_step s = curr_state().top_proof_step(); + action_result r = s.resolve(unfold_hypotheses_ge(curr_state(), pr)); + switch (r.get_kind()) { + case action_result::Failed: + display_msg(">>> next-branch FAILED <<<"); + return r; + case action_result::Solved: + pr = r.get_proof(); + curr_state().pop_proof_step(); + break; + case action_result::NewBranch: + return action_result::new_branch(); + } + } + return action_result::solved(pr); +} + +optional strategy::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) { + display_msg(">>> maximum search depth reached <<<"); + r = action_result::failed(); + } + switch (r.get_kind()) { + case action_result::Failed: + r = next_choice_point(m_init_num_choices); + 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 strategy::invoke_preprocess() { + if (auto pr = preprocess()) { + auto r = next_branch(*pr); + if (!solved(r)) { + throw exception("invalid blast preprocessing action, preprocessing actions should not create branches"); + } else { + return r.to_opt_expr(); + } + } else { + return none_expr(); + } +} + +optional strategy::search() { + scope_choice_points scope1; + m_init_num_choices = get_num_choice_points(); + curr_state().set_simp_rule_sets(get_simp_rule_sets(env())); + if (auto pr = invoke_preprocess()) + return pr; + if (get_num_choice_points() > m_init_num_choices) + throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points"); + state s = curr_state(); + unsigned d = m_config.m_init_depth; + while (true) { + if (auto r = search_upto(d)) + return r; + d += m_config.m_inc_depth; + if (d > m_config.m_max_depth) { + display_curr_state(); + return none_expr(); + } + curr_state() = s; + shrink_choice_points(m_init_num_choices); + } +} +}} diff --git a/src/library/blast/strategy.h b/src/library/blast/strategy.h new file mode 100644 index 000000000..1dfd4fb92 --- /dev/null +++ b/src/library/blast/strategy.h @@ -0,0 +1,39 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/blast/action_result.h" +#include "library/blast/options.h" + +namespace lean { +namespace blast { +/** Generic strategy for synthesizing proofs using the blast framework. + There are two main configuration options: + + 1- Preprocessing (preprocess method) + 2- Next action to be performed (next_action method) + */ +class strategy { + config m_config; + unsigned m_init_num_choices; + optional invoke_preprocess(); +protected: + virtual optional preprocess() = 0; + virtual action_result next_action() = 0; + + void display_msg(char const * msg); + void display_action(char const * name); + void display(); + void display_if(action_result r); + + action_result next_branch(expr pr); + optional search_upto(unsigned depth); + optional search(); +public: + strategy(); + optional operator()() { return search(); } +}; +}}