From 0fcf8ed7d2458411e0eb8e6c4507fe218bed0195 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Nov 2015 18:22:26 -0800 Subject: [PATCH] refactor(library/blast): hypothesis activation protocol --- .../blast/backward/backward_strategy.cpp | 16 +++++----- src/library/blast/simple_strategy.cpp | 29 +++++++++---------- src/library/blast/state.cpp | 9 ++++-- src/library/blast/state.h | 5 ++-- src/library/blast/strategy.cpp | 13 +++++++++ src/library/blast/strategy.h | 3 ++ 6 files changed, 47 insertions(+), 28 deletions(-) diff --git a/src/library/blast/backward/backward_strategy.cpp b/src/library/blast/backward/backward_strategy.cpp index abbf50f26..3dfded2bd 100644 --- a/src/library/blast/backward/backward_strategy.cpp +++ b/src/library/blast/backward/backward_strategy.cpp @@ -52,15 +52,15 @@ static backward_branch_extension & get_extension() { class backward_strategy : public strategy { virtual optional preprocess() override { return none_expr(); } - action_result activate_hypothesis() { - optional hidx = curr_state().activate_hypothesis(); - if (!hidx) return action_result::failed(); - trace_action("activate"); + 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)); + return action_result::new_branch(); + } - Try(assumption_contradiction_actions(*hidx)); - Try(subst_action(*hidx)); - Try(no_confusion_action(*hidx)); - Try(discard_action(*hidx)); + virtual action_result hypothesis_post_activation(hypothesis_idx hidx) override { return action_result::new_branch(); } diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index 26ede5599..113cad2ef 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -26,28 +26,27 @@ 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 : public strategy { - action_result activate_hypothesis(bool preprocess) { - scope_trace scope(!preprocess && get_config().m_trace); - auto hidx = curr_state().activate_hypothesis(); - if (!hidx) return action_result::failed(); - trace_action("activate"); + action_result hypothesis_pre_activation(hypothesis_idx hidx) override { + Try(assumption_contradiction_actions(hidx)); + Try(simplify_hypothesis_action(hidx)); + Try(no_confusion_action(hidx)); + TrySolve(assert_cc_action(hidx)); + Try(discard_action(hidx)); + Try(subst_action(hidx)); + return action_result::new_branch(); + } - Try(assumption_contradiction_actions(*hidx)); - Try(simplify_hypothesis_action(*hidx)); - TrySolve(assert_cc_action(*hidx)); - Try(subst_action(*hidx)); - Try(no_confusion_action(*hidx)); - Try(discard_action(*hidx)); - Try(forward_action(*hidx)); - Try(recursor_preprocess_action(*hidx)); + action_result hypothesis_post_activation(hypothesis_idx hidx) override { + Try(forward_action(hidx)); + Try(recursor_preprocess_action(hidx)); return action_result::new_branch(); } /* \brief Preprocess state It keeps applying intros, activating and finally simplify target. Return an expression if the goal has been proved during preprocessing step. */ - virtual optional preprocess() { + virtual optional preprocess() override { trace("* Preprocess"); while (true) { if (!failed(intros_action())) @@ -61,7 +60,7 @@ class simple_strategy : public strategy { return none_expr(); } - virtual action_result next_action() { + virtual action_result next_action() override { Try(intros_action()); Try(activate_hypothesis(false)); Try(trivial_action()); diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index b45e5956e..9732f9ad5 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -765,20 +765,23 @@ void state::remove_from_indices(hypothesis const & h, hypothesis_idx hidx) { m_branch.m_head_to_hyps.erase(*i, hidx); } -optional state::activate_hypothesis() { +optional state::select_hypothesis_to_activate() { while (true) { if (m_branch.m_todo_queue.empty()) return optional(); unsigned hidx = m_branch.m_todo_queue.erase_min(); hypothesis const & h_decl = get_hypothesis_decl(hidx); if (!h_decl.is_dead()) { - m_branch.m_active.insert(hidx); - update_indices(hidx); return optional(hidx); } } } +void state::activate_hypothesis(hypothesis_idx hidx) { + m_branch.m_active.insert(hidx); + update_indices(hidx); +} + bool state::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const { if (auto s = m_branch.m_forward_deps.find(hidx_provider)) { return s->contains(hidx_user); diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 06e36af16..a639bfa74 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -293,8 +293,9 @@ public: }); } - /** \brief Activate the next hypothesis in the TODO queue, return none if the TODO queue is empty. */ - optional activate_hypothesis(); + /** \brief Select next hypothesis in the TODO queue, return none if the TODO queue is empty. */ + optional select_hypothesis_to_activate(); + void activate_hypothesis(hypothesis_idx hidx); /** \brief Store in \c r the hypotheses in this branch sorted by dependency depth */ void get_sorted_hypotheses(hypothesis_idx_buffer & r) const; diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp index ea0e2ce7c..61ecb98c7 100644 --- a/src/library/blast/strategy.cpp +++ b/src/library/blast/strategy.cpp @@ -14,6 +14,19 @@ namespace lean { namespace blast { strategy::strategy() {} +action_result strategy::activate_hypothesis(bool preprocess) { + scope_trace scope(!preprocess && get_config().m_trace); + auto hidx = curr_state().select_hypothesis_to_activate(); + if (!hidx) return action_result::failed(); + auto r = hypothesis_pre_activation(*hidx); + if (!solved(r) && !failed(r)) { + curr_state().activate_hypothesis(*hidx); + return hypothesis_post_activation(*hidx); + } else { + return r; + } +} + action_result strategy::next_branch(expr pr) { while (curr_state().has_proof_steps()) { proof_step s = curr_state().top_proof_step(); diff --git a/src/library/blast/strategy.h b/src/library/blast/strategy.h index 77effe623..6136c16ad 100644 --- a/src/library/blast/strategy.h +++ b/src/library/blast/strategy.h @@ -24,7 +24,10 @@ class strategy { protected: virtual optional preprocess() = 0; virtual action_result next_action() = 0; + virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) = 0; + virtual action_result hypothesis_post_activation(hypothesis_idx hidx) = 0; + action_result activate_hypothesis(bool preprocess = false); action_result next_branch(expr pr); optional search_upto(unsigned depth); optional search();