From cd7708d5568e879dcc55bb028163198e541dd882 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Jan 2016 17:07:15 -0800 Subject: [PATCH] feat(library/blast/backward/backward_strategy): add extensible backward chaining strategy --- .../blast/backward/backward_strategy.cpp | 67 ++++++++++++++++--- .../blast/backward/backward_strategy.h | 16 +++++ 2 files changed, 75 insertions(+), 8 deletions(-) diff --git a/src/library/blast/backward/backward_strategy.cpp b/src/library/blast/backward/backward_strategy.cpp index 4cf00488d7..d9ec4c9e24 100644 --- a/src/library/blast/backward/backward_strategy.cpp +++ b/src/library/blast/backward/backward_strategy.cpp @@ -1,7 +1,7 @@ /* Copyright (c) 2015 Daniel Selsam. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam +Author: Daniel Selsam, Leonardo de Moura */ #include "util/sexpr/option_declarations.h" #include "library/attribute_manager.h" @@ -65,21 +65,32 @@ static backward_branch_extension & get_extension() { return static_cast(curr_state().get_extension(g_ext_id)); } -/** \brief Basic backwards chaining, inspired by Coq's [auto]. */ +/** \brief Extensible backward chaining strategy */ class backward_strategy_fn : public strategy_fn { unsigned m_max_rounds; virtual char const * get_name() const override { return "backward"; } + /* action to be executed before hypothesis is activated */ + virtual action_result pre(hypothesis_idx) { return action_result::failed(); } + /* action to be executed after hypothesis is activated */ + virtual action_result post(hypothesis_idx) { return action_result::failed(); } + /* action to be executed before trying backward chaining */ + virtual action_result pre_next() { return action_result::failed(); } + /* action to be executed after trying backward chaining */ + virtual action_result post_next() { return action_result::failed(); } + virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override { Try(assumption_contradiction_actions(hidx)); Try(subst_action(hidx)); Try(no_confusion_action(hidx)); Try(discard_action(hidx)); + Try(pre(hidx)); return action_result::new_branch(); } - virtual action_result hypothesis_post_activation(hypothesis_idx) override { + virtual action_result hypothesis_post_activation(hypothesis_idx hidx) override { + Try(post(hidx)); return action_result::new_branch(); } @@ -88,18 +99,47 @@ class backward_strategy_fn : public strategy_fn { Try(activate_hypothesis()); Try(trivial_action()); Try(assumption_action()); - auto & ext = get_extension(); - if (ext.m_num_rounds < m_max_rounds) { - list backward_rules = ext.get_backward_lemmas().find(head_index(curr_state().get_target())); - ext.m_num_rounds++; - Try(backward_action(backward_rules, true)); + Try(pre_next()); + if (get_extension().m_num_rounds < m_max_rounds) { + list backward_rules = get_extension().get_backward_lemmas().find(head_index(curr_state().get_target())); + action_result r = backward_action(backward_rules, true); + if (!failed(r)) { + get_extension().m_num_rounds++; + return r; + } } + Try(post_next()); return action_result::failed(); } public: backward_strategy_fn(unsigned max_rounds):m_max_rounds(max_rounds) {} }; +/* Backward strategy that can be extended using closures. */ +class xbackward_strategy_fn : public backward_strategy_fn { + char const * m_name; + std::function m_pre; + std::function m_post; + std::function m_pre_next; + std::function m_post_next; + + virtual char const * get_name() const override { return m_name; } + virtual action_result pre(hypothesis_idx hidx) { return m_pre(hidx); } + virtual action_result post(hypothesis_idx hidx) { return m_post(hidx); } + virtual action_result pre_next() { return m_pre_next(); } + virtual action_result post_next() { return m_post_next(); } +public: + xbackward_strategy_fn( + char const * n, + unsigned max_rounds, + std::function const & pre, + std::function const & post, + std::function const & pre_next, + std::function const & post_next): + backward_strategy_fn(max_rounds), + m_name(n), m_pre(pre), m_post(post), m_pre_next(pre_next), m_post_next(post_next) {} +}; + strategy mk_backward_strategy() { if (!get_config().m_backward) return []() { return none_expr(); }; // NOLINT @@ -108,4 +148,15 @@ strategy mk_backward_strategy() { return backward_strategy_fn(max_rounds)(); }; } + +strategy mk_xbackward_strategy(char const * n, + std::function const & pre, + std::function const & post, + std::function const & pre_next, + std::function const & post_next) { + return [=]() { // NOLINT + unsigned max_rounds = get_blast_backward_max_rounds(ios().get_options()); + return xbackward_strategy_fn(n, max_rounds, pre, post, pre_next, post_next)(); + }; +} }} diff --git a/src/library/blast/backward/backward_strategy.h b/src/library/blast/backward/backward_strategy.h index 344cd339b2..4c48cfd472 100644 --- a/src/library/blast/backward/backward_strategy.h +++ b/src/library/blast/backward/backward_strategy.h @@ -9,6 +9,22 @@ namespace lean { namespace blast { strategy mk_backward_strategy(); +/* Extensible backward chaining strategy + - n : name of the new strategy + - pre : action to be executed before given hypothesis is activated + - post : action to be executed after given hypothesis is activated + - pre_next : action to be executed before backward chaining, + i.e., backward chaining will only be considered when this action fails + - post_next : action to be executed after backward chaining cannot be applied anymore + because maximum number of rounds has been reached or no [intro] lemma + is applicable + */ +strategy mk_xbackward_strategy(char const * n, + std::function const & pre, + std::function const & post, + std::function const & pre_next, + std::function const & post_next); + void initialize_backward_strategy(); void finalize_backward_strategy(); }}