refactor(library/blast): blast strategy framework

src/library/blast/backward/backward_strategy.cpp

@@ -50,8 +50,6 @@ static backward_branch_extension & get_extension() {
 
 /** \brief Basic backwards chaining, inspired by Coq's [auto]. */
 class backward_strategy_fn : public strategy_fn {
-    virtual optional<expr> preprocess() override { return none_expr(); }
-
     virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
         Try(assumption_contradiction_actions(hidx));
         Try(subst_action(hidx));

src/library/blast/blast.cpp

@@ -30,7 +30,7 @@ Author: Leonardo de Moura
 #include "library/blast/congruence_closure.h"
 #include "library/blast/trace.h"
 #include "library/blast/options.h"
-#include "library/blast/strategies/simple_strategy.h"
+#include "library/blast/strategies/portfolio.h"
 
 namespace lean {
 namespace blast {
@@ -531,7 +531,7 @@ public:
 
     optional<expr> operator()(goal const & g) {
         init_state(g);
-        if (auto r = mk_simple_strategy()()) {
+        if (auto r = apply_strategy()) {
             return some_expr(to_tactic_proof(*r));
         } else {
             return none_expr();

src/library/blast/state.h

@@ -355,6 +355,23 @@ public:
        Proof steps
     *************************/
 
+    /** \brief Auxiliary object for checking whether m_proof_steps has new proof_step objects since
+        the check point was created */
+    class proof_steps_check_point {
+        proof_steps m_ps;
+    public:
+        proof_steps_check_point() {}
+        proof_steps_check_point(proof_steps const & ps):m_ps(ps) {}
+        bool has_new_proof_steps(state const & s) const {
+            lean_assert(is_suffix_eqp(m_ps, s.m_proof_steps));
+            return !is_eqp(s.m_proof_steps, m_ps);
+        }
+    };
+
+    proof_steps_check_point mk_proof_steps_check_point() const {
+        return proof_steps_check_point(m_proof_steps);
+    }
+
     void push_proof_step(proof_step const & ps) {
         if (!ps.is_silent())
             m_proof_depth++;
@@ -365,10 +382,6 @@ public:
         push_proof_step(proof_step(cell));
     }
 
-    bool has_proof_steps() const {
-        return static_cast<bool>(m_proof_steps);
-    }
-
     proof_step top_proof_step() const {
         return head(m_proof_steps);
     }
@@ -386,11 +399,6 @@ public:
         return m_proof_depth;
     }
 
-    void clear_proof_steps() {
-        m_proof_steps = list<proof_step>();
-        m_proof_depth = 0;
-    }
-
     /************************
        Assignment management
     *************************/

src/library/blast/strategies/CMakeLists.txt

@@ -1 +1,2 @@
-add_library(blast_strategies OBJECT simple_strategy.cpp)
+add_library(blast_strategies OBJECT simple_strategy.cpp iterative_deepening.cpp
+  preprocess_strategy.cpp portfolio.cpp)

src/library/blast/strategies/iterative_deepening.cpp

@@ -0,0 +1,33 @@
+/*
+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/options.h"
+
+namespace lean {
+namespace blast {
+strategy iterative_deepening(strategy const & S, unsigned init, unsigned inc, unsigned max) {
+    return [=]() {
+        state s      = curr_state();
+        unsigned ncs = get_num_choice_points();
+        unsigned d   = init;
+        while (true) {
+            flet<unsigned> set_depth(get_config().m_max_depth, d);
+            if (auto r = S())
+                return r;
+            d += inc;
+            if (d > max) {
+                if (get_config().m_show_failure)
+                    display_curr_state();
+                return none_expr();
+            }
+            curr_state() = s;
+            shrink_choice_points(ncs);
+        };
+    };
+}
+}}

src/library/blast/strategies/iterative_deepening.h

@@ -0,0 +1,12 @@
+/*
+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/strategy.h"
+namespace lean {
+namespace blast {
+strategy iterative_deepening(strategy const & s, unsigned init, unsigned inc, unsigned max);
+}}

src/library/blast/strategies/portfolio.cpp

@@ -0,0 +1,19 @@
+/*
+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/strategies/simple_strategy.h"
+#include "library/blast/strategies/preprocess_strategy.h"
+
+namespace lean {
+namespace blast {
+static optional<expr> apply_simple() {
+    return preprocess_and_then(mk_simple_strategy())();
+}
+
+optional<expr> apply_strategy() {
+    return apply_simple();
+}
+}}

src/library/blast/strategies/portfolio.h

@@ -0,0 +1,13 @@
+/*
+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 "kernel/expr.h"
+
+namespace lean {
+namespace blast {
+optional<expr> apply_strategy();
+}}

src/library/blast/strategies/preprocess_strategy.cpp

@@ -0,0 +1,76 @@
+/*
+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/trace.h"
+#include "library/blast/options.h"
+#include "library/blast/choice_point.h"
+#include "library/blast/simplifier/simplifier_actions.h"
+#include "library/blast/unit/unit_actions.h"
+#include "library/blast/actions/simple_actions.h"
+#include "library/blast/actions/intros_action.h"
+#include "library/blast/actions/subst_action.h"
+#include "library/blast/actions/no_confusion_action.h"
+#include "library/blast/actions/assert_cc_action.h"
+#include "library/blast/actions/recursor_action.h"
+#include "library/blast/strategies/preprocess_strategy.h"
+
+namespace lean {
+namespace blast {
+class preprocess_strategy_fn : public strategy_fn {
+    strategy m_main;
+    bool     m_simple;
+    bool     m_done{false};
+
+    virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
+        Try(assumption_contradiction_actions(hidx));
+        Try(simplify_hypothesis_action(hidx));
+        if (!m_simple)
+            Try(unit_preprocess(hidx));
+        Try(no_confusion_action(hidx));
+        if (!m_simple)
+            TrySolve(assert_cc_action(hidx));
+        Try(discard_action(hidx));
+        Try(subst_action(hidx));
+        return action_result::new_branch();
+    }
+
+    virtual action_result hypothesis_post_activation(hypothesis_idx hidx) override {
+        if (!m_simple) {
+            Try(unit_propagate(hidx));
+            Try(recursor_preprocess_action(hidx));
+        }
+        return action_result::new_branch();
+    }
+
+    virtual action_result next_action() override {
+        if (!m_done) {
+            Try(intros_action());
+            Try(assumption_action());
+            Try(activate_hypothesis());
+            Try(simplify_target_action());
+            m_done = true;
+        }
+        if (get_num_choice_points() > get_initial_num_choice_points())
+            throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points");
+        {
+            scope_trace s(get_config().m_trace);
+            TryStrategy(m_main);
+        }
+        return action_result::failed();
+    }
+public:
+    preprocess_strategy_fn(strategy const & S, bool simple):
+        m_main(S), m_simple(simple) {}
+};
+
+strategy preprocess_and_then(strategy const & S) {
+    return [=]() { scope_trace s(false); return preprocess_strategy_fn(S, false)(); };
+}
+
+strategy basic_preprocess_and_then(strategy const & S) {
+    return [=]() { scope_trace s(false); return preprocess_strategy_fn(S, true)(); };
+}
+}}

src/library/blast/strategies/preprocess_strategy.h

@@ -0,0 +1,14 @@
+/*
+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/strategy.h"
+
+namespace lean {
+namespace blast {
+strategy preprocess_and_then(strategy const & S);
+strategy basic_preprocess_and_then(strategy const & S);
+}}

src/library/blast/strategies/simple_strategy.cpp

@@ -29,7 +29,7 @@ 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_fn : public strategy_fn {
-    action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
+    virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
         Try(assumption_contradiction_actions(hidx));
         Try(simplify_hypothesis_action(hidx));
         Try(unit_preprocess(hidx));
@@ -40,32 +40,15 @@ class simple_strategy_fn : public strategy_fn {
         return action_result::new_branch();
     }
 
-    action_result hypothesis_post_activation(hypothesis_idx hidx) override {
+    virtual action_result hypothesis_post_activation(hypothesis_idx hidx) override {
         Try(unit_propagate(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<expr> preprocess() override {
-        trace("* Preprocess");
-        while (true) {
-            if (!failed(intros_action()))
-                continue;
-            auto r = activate_hypothesis(true);
-            if (solved(r)) return r.to_opt_expr();
-            if (failed(r)) break;
-        }
-        TrySolveToOptExpr(assumption_action());
-        TrySolveToOptExpr(simplify_target_action());
-        return none_expr();
-    }
-
     virtual action_result next_action() override {
         Try(intros_action());
-        Try(activate_hypothesis(false));
+        Try(activate_hypothesis());
         Try(trivial_action());
         Try(assumption_action());
         Try(recursor_action());
@@ -74,9 +57,6 @@ class simple_strategy_fn : public strategy_fn {
         Try(by_contradiction_action());
         TryStrategy(mk_backward_strategy());
         Try(qfc_action(list<gexpr>()));
-
-        // TODO(Leo): add more actions...
-
         return action_result::failed();
     }
 };

src/library/blast/strategy.cpp

@@ -15,8 +15,7 @@ namespace lean {
 namespace blast {
 strategy_fn::strategy_fn() {}
 
-action_result strategy_fn::activate_hypothesis(bool preprocess) {
-    scope_trace scope(!preprocess && get_config().m_trace);
+action_result strategy_fn::activate_hypothesis() {
     auto hidx = curr_state().select_hypothesis_to_activate();
     if (!hidx) return action_result::failed();
     auto r    = hypothesis_pre_activation(*hidx);
@@ -29,7 +28,7 @@ action_result strategy_fn::activate_hypothesis(bool preprocess) {
 }
 
 action_result strategy_fn::next_branch(expr pr) {
-    while (curr_state().has_proof_steps()) {
+    while (m_ps_check_point.has_new_proof_steps(curr_state())) {
         proof_step s     = curr_state().top_proof_step();
         action_result r  = s.resolve(unfold_hypotheses_ge(curr_state(), pr));
         switch (r.get_kind()) {
@@ -47,9 +46,14 @@ action_result strategy_fn::next_branch(expr pr) {
     return action_result::solved(pr);
 }
 
-optional<expr> strategy_fn::search_upto(unsigned depth) {
+optional<expr> strategy_fn::search() {
+    scope_choice_points scope1;
+    m_ps_check_point          = curr_state().mk_proof_steps_check_point();
+    m_init_num_choices        = get_num_choice_points();
+    unsigned init_proof_depth = curr_state().get_proof_depth();
+    unsigned max_depth        = get_config().m_max_depth;
     if (is_trace_enabled()) {
-        ios().get_diagnostic_channel() << "* Search upto depth " << depth << "\n\n";
+        ios().get_diagnostic_channel() << "* Search upto depth " << max_depth << "\n\n";
     }
     trace_curr_state();
     action_result r = next_action();
@@ -57,7 +61,7 @@ optional<expr> strategy_fn::search_upto(unsigned depth) {
     while (true) {
         check_system("blast");
         lean_assert(curr_state().check_invariant());
-        if (curr_state().get_proof_depth() > depth) {
+        if (curr_state().get_proof_depth() > max_depth) {
             trace(">>> maximum search depth reached <<<");
             r = action_result::failed();
         }
@@ -76,7 +80,7 @@ optional<expr> strategy_fn::search_upto(unsigned depth) {
             if (r.get_kind() == action_result::Solved) {
                 // all branches have been solved
                 trace("* found proof");
-                return some_expr(r.get_proof());
+                return some_expr(unfold_hypotheses_ge(curr_state(), r.get_proof(), init_proof_depth));
             }
             trace("* next branch");
             break;
@@ -87,51 +91,4 @@ optional<expr> strategy_fn::search_upto(unsigned depth) {
         trace_curr_state_if(r);
     }
 }
-
-optional<expr> strategy_fn::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<expr> strategy_fn::init_search() {
-    scope_choice_points scope1;
-    curr_state().clear_proof_steps();
-    m_init_num_choices = get_num_choice_points();
-    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");
-    return none_expr();
-}
-
-optional<expr> strategy_fn::iterative_deepening() {
-    state s    = curr_state();
-    unsigned d = get_config().m_init_depth;
-    while (true) {
-        if (auto r = search_upto(d))
-            return r;
-        d += get_config().m_inc_depth;
-        if (d > get_config().m_max_depth) {
-            if (get_config().m_show_failure)
-                display_curr_state();
-            return none_expr();
-        }
-        curr_state() = s;
-        shrink_choice_points(m_init_num_choices);
-    }
-}
-
-optional<expr> strategy_fn::search() {
-    if (auto r = init_search())
-        return r;
-    return iterative_deepening();
-}
 }}

src/library/blast/strategy.h

@@ -19,29 +19,24 @@ namespace blast {
     2- Next action to be performed (next_action method)
  */
 class strategy_fn {
-    unsigned m_init_num_choices;
+    unsigned                       m_init_num_choices{0};
+    state::proof_steps_check_point m_ps_check_point;
     optional<expr> invoke_preprocess();
 protected:
-    virtual optional<expr> 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 activate_hypothesis();
+    unsigned get_initial_num_choice_points() const { return m_init_num_choices; }
     action_result next_branch(expr pr);
-    optional<expr> search_upto(unsigned depth);
-    optional<expr> init_search();
-    optional<expr> iterative_deepening();
-    virtual optional<expr> search();
+    optional<expr> search();
 public:
     strategy_fn();
     optional<expr> operator()() { return search(); }
 };
 
-#define TryStrategy(S) {\
-        flet<state> save_state(curr_state(), curr_state());\
-        curr_state().clear_proof_steps();\
+#define TryStrategy(S) { \
+        flet<state> save_state(curr_state(), curr_state()); \
         if (optional<expr> pf = S()) { return action_result::solved(*pf); } \
     }