From 6340b1ae5b0f4fb45f494d4cfb88099aaa9040bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Nov 2015 17:29:47 -0800 Subject: [PATCH] feat(library/blast): very basic search procedure and iterative deepening --- src/library/blast/blast.cpp | 149 +++++++++++++++++++++++++++++++++-- src/library/blast/blast.h | 4 +- src/library/blast/branch.cpp | 24 +++++- src/library/blast/branch.h | 16 +++- src/library/blast/state.h | 57 +++++++++++++- 5 files changed, 237 insertions(+), 13 deletions(-) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 10490c521..b1bd9297f 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/sstream.h" +#include "util/sexpr/option_declarations.h" #include "kernel/for_each_fn.h" #include "kernel/type_checker.h" #include "library/replace_visitor.h" @@ -22,11 +23,36 @@ Author: Leonardo de Moura #include "library/blast/blast.h" #include "library/blast/blast_exception.h" +#ifndef LEAN_DEFAULT_BLAST_MAX_DEPTH +#define LEAN_DEFAULT_BLAST_MAX_DEPTH 128 +#endif +#ifndef LEAN_DEFAULT_BLAST_INIT_DEPTH +#define LEAN_DEFAULT_BLAST_INIT_DEPTH 1 +#endif +#ifndef LEAN_DEFAULT_BLAST_INC_DEPTH +#define LEAN_DEFAULT_BLAST_INC_DEPTH 5 +#endif + namespace lean { namespace blast { static name * g_prefix = nullptr; static name * g_tmp_prefix = nullptr; +/* Options */ +static name * g_blast_max_depth = nullptr; +static name * g_blast_init_depth = nullptr; +static name * g_blast_inc_depth = nullptr; + +unsigned get_blast_max_depth(options const & o) { + return o.get_unsigned(*g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH); +} +unsigned get_blast_init_depth(options const & o) { + return o.get_unsigned(*g_blast_init_depth, LEAN_DEFAULT_BLAST_INIT_DEPTH); +} +unsigned get_blast_inc_depth(options const & o) { + return o.get_unsigned(*g_blast_inc_depth, LEAN_DEFAULT_BLAST_INC_DEPTH); +} + class blastenv { friend class scope_assignment; typedef std::vector tmp_type_context_pool; @@ -46,12 +72,18 @@ class blastenv { name_predicate m_instance_pred; name_map m_projection_info; state m_curr_state; // current state + std::vector m_choice_points; tmp_type_context_pool m_tmp_ctx_pool; tmp_type_context_ptr m_tmp_ctx; // for app_builder and congr_lemma_manager app_builder m_app_builder; fun_info_manager m_fun_info_manager; congr_lemma_manager m_congr_lemma_manager; + /* options */ + unsigned m_max_depth; + unsigned m_init_depth; + unsigned m_inc_depth; + class tctx : public type_context { blastenv & m_benv; std::vector m_stack; @@ -378,6 +410,97 @@ class blastenv { m_initial_context = to_list(ctx); } + void set_options(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); + } + + bool next_choice_point() { + if (m_choice_points.empty()) + return false; + m_curr_state = m_choice_points.back(); + m_choice_points.pop_back(); + return true; + } + + enum status { NoAction, ClosedBranch, Continue }; + + optional activate_hypothesis() { + return m_curr_state.get_main_branch().activate_hypothesis(); + } + + pair next_action() { + if (activate_hypothesis()) { + // TODO(Leo): we should probably eagerly simplify the activated hypothesis. + return mk_pair(Continue, expr()); + } else { + // TODO(Leo): add more actions... + return mk_pair(NoAction, expr()); + } + } + + optional resolve(expr pr) { + while (m_curr_state.has_proof_steps()) { + proof_step s = m_curr_state.top_proof_step(); + if (auto new_pr = s.resolve(m_curr_state, pr)) { + pr = *new_pr; + m_curr_state.pop_proof_step(); + } else { + return none_expr(); // continue the search + } + } + return some_expr(pr); // closed all branches + } + + optional search_upto(unsigned depth) { + while (true) { + if (m_curr_state.get_depth() > depth) { + // maximum depth reached + if (!next_choice_point()) { + return none_expr(); + } + } + auto s = next_action(); + switch (s.first) { + case NoAction: + if (!next_choice_point()) + return none_expr(); + break; + case ClosedBranch: + if (auto pr = resolve(s.second)) + return pr; + break; + case Continue: + break; + } + } + } + + optional search() { + state s = m_curr_state; + unsigned d = m_init_depth; + while (d <= m_max_depth) { + if (auto r = search_upto(d)) + return r; + d += m_inc_depth; + m_curr_state = s; + m_choice_points.clear(); + } + return none_expr(); + } + + expr to_tactic_proof(expr const & pr) { + // TODO(Leo): when a proof is found we must + // 1- remove all occurrences of href's from pr + // 2- replace mrefs with their assignments, + // and convert unassigned meta-variables back into + // tactic meta-variables. + // 3- The external tactic meta-variables that have been instantiated + // by blast must also be communicated back to the tactic framework. + return pr; + } + public: blastenv(environment const & env, io_state const & ios, list const & ls, list const & ds): m_env(env), m_ios(ios), m_ngen(*g_prefix), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)), @@ -389,6 +512,7 @@ public: m_fun_info_manager(*m_tmp_ctx), m_congr_lemma_manager(m_app_builder, m_fun_info_manager), m_tctx(*this) { + set_options(m_ios.get_options()); } ~blastenv() { @@ -405,12 +529,11 @@ public: optional operator()(goal const & g) { init_state(g); - - // TODO(Leo): blast main loop - display("Blast tactic initial state\n"); - display_curr_state(); - - return none_expr(); + if (auto r = search()) { + return some_expr(to_tactic_proof(*r)); + } else { + return none_expr(); + } } environment const & get_env() const { return m_env; } @@ -695,8 +818,18 @@ optional blast_goal(environment const & env, io_state const & ios, list(hidx) + 1.0); +} + expr branch::add_hypothesis(name const & n, expr const & type, expr const & value) { hypothesis new_h; new_h.m_name = n; @@ -85,7 +90,8 @@ expr branch::add_hypothesis(name const & n, expr const & type, expr const & valu m_context.insert(new_hidx, new_h); if (new_h.is_assumption()) m_assumption.insert(new_hidx); - m_todo.insert(new_hidx); + double w = compute_weight(new_hidx, type); + m_todo_queue.insert(w, new_hidx); return blast::mk_href(new_hidx); } @@ -95,6 +101,22 @@ expr branch::add_hypothesis(expr const & type, expr const & value) { return add_hypothesis(name(*g_prefix, m_next), type, value); } +void branch::update_indices(unsigned /* hidx */) { + // TODO(Leo): we need to update the indexing data-structures and send + // the hypothesis if to the congruence closure module after it is implemented. +} + +optional branch::activate_hypothesis() { + if (m_todo_queue.empty()) { + return optional(); + } else { + unsigned hidx = m_todo_queue.erase_min(); + m_active.insert(hidx); + update_indices(hidx); + return optional(hidx); + } +} + bool branch::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const { if (auto s = m_forward_deps.find(hidx_provider)) { return s->contains(hidx_user); diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h index dbe944930..2e1bef5a3 100644 --- a/src/library/blast/branch.h +++ b/src/library/blast/branch.h @@ -19,6 +19,7 @@ using metavar_idx_map = typename lean::rb_map; class branch { typedef hypothesis_idx_map forward_deps; + typedef rb_map todo_queue; friend class state; unsigned m_next; context m_context; @@ -38,7 +39,7 @@ class branch { // We say a hypothesis is in the to-do set when the blast haven't process it yet. hypothesis_idx_set m_assumption; hypothesis_idx_set m_active; - hypothesis_idx_set m_todo; + todo_queue m_todo_queue; forward_deps m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h. expr m_target; @@ -48,6 +49,16 @@ class branch { void add_forward_dep(unsigned hidx_user, unsigned hidx_provider); void add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user); void add_deps(hypothesis & h_user, unsigned hidx_user); + + /** \brief Compute the weight of a hypothesis with the given type + We use this weight to update the todo_queue. */ + double compute_weight(unsigned hidx, expr const & type); + + /** \brief This method is invoked when a hypothesis move from todo to active. + + We will update indices and data-structures (e.g., congruence closure). */ + void update_indices(unsigned hidx); + public: branch():m_next(0) {} @@ -64,6 +75,9 @@ public: return get(href_index(h)); } void for_each_hypothesis(std::function const & fn) const { m_context.for_each(fn); } + /** \brief Activate the next hypothesis in the TODO queue, return none if the TODO queue is empty. */ + optional activate_hypothesis(); + /** \brief Store in \c r the hypotheses in this branch sorted by depth */ void get_sorted_hypotheses(hypothesis_idx_buffer & r) const; diff --git a/src/library/blast/state.h b/src/library/blast/state.h index b02cf1e29..3864fd457 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -32,11 +32,41 @@ public: hypothesis_idx_set get_assumptions() const { return m_assumptions; } }; +class proof_step_cell { + MK_LEAN_RC(); // Declare m_rc counter + void dealloc() { delete this; } +public: + virtual ~proof_step_cell() {} + /** \brief Every proof-step must provide a resolve method. + When the branch created by the proof-step is closed, + a proof pr is provided, and the proof-step can perform two operations + 1- setup the next branch and return none_expr + 2- finish and return a new proof */ + virtual optional resolve(state & s, expr const & pr) = 0; +}; + +class proof_step { + proof_step_cell * m_ptr; +public: + proof_step():m_ptr(nullptr) {} + proof_step(proof_step const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } + proof_step(proof_step && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + ~proof_step() { if (m_ptr) m_ptr->dec_ref(); } + proof_step & operator=(proof_step const & s) { LEAN_COPY_REF(s); } + proof_step & operator=(proof_step && s) { LEAN_MOVE_REF(s); } + + optional resolve(state & s, expr const & pr) { + lean_assert(m_ptr); + return m_ptr->resolve(s, pr); + } +}; + class state { typedef metavar_idx_map metavar_decls; typedef metavar_idx_map eassignment; typedef metavar_idx_map uassignment; typedef hypothesis_idx_map fixed_by; + typedef list proof_steps; unsigned m_next_uref_index; // index of the next universe metavariable uassignment m_uassignment; unsigned m_next_mref_index; // index of the next metavariable @@ -51,7 +81,9 @@ class state { // `B` contains an over-approximation of all meta-variables occuring in it (i.e., m_mvar_idxs). // If this check fails, then we should replace any assigned `m_i` with its value, if the intersection is still // non-empty, then we cannot clear `h`. - fixed_by m_fixed_by; + fixed_by m_fixed_by; + unsigned m_depth{0}; + proof_steps m_proof_steps; void add_fixed_by(unsigned hidx, unsigned midx); unsigned add_metavar_decl(metavar_decl const & decl); @@ -91,7 +123,7 @@ public: \pre ctx must be a subset of the hypotheses in the main branch. */ expr mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type); expr mk_metavar(hypothesis_idx_set const & ctx, expr const & type); -/** \brief Create a new metavariable using the given type. + /** \brief Create a new metavariable using the given type. The context of this metavariable will be all assumption hypotheses occurring in the main branch. */ expr mk_metavar(expr const & type); @@ -171,6 +203,27 @@ public: } }; + void push_proof_step(proof_step const & ps) { + m_depth++; + m_proof_steps = cons(ps, m_proof_steps); + } + + bool has_proof_steps() const { + return static_cast(m_proof_steps); + } + + proof_step top_proof_step() const { + return head(m_proof_steps); + } + + void pop_proof_step() { + lean_assert(m_proof_steps); + m_depth--; + m_proof_steps = tail(m_proof_steps); + } + + unsigned get_depth() const { return m_depth; } + #ifdef LEAN_DEBUG bool check_invariant() const; #endif