michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast): very basic search procedure and iterative deepening

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-08 17:29:47 -08:00
parent 1d39b6d5d4
commit 6340b1ae5b
5 changed files with 237 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

149
src/library/blast/blast.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <vector>
#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 *> tmp_type_context_pool;
@ -46,12 +72,18 @@ class blastenv {
name_predicate m_instance_pred;
name_map<projection_info> m_projection_info;
state m_curr_state; // current state
std::vector<state> 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<state> 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<unsigned> activate_hypothesis() {
return m_curr_state.get_main_branch().activate_hypothesis();
}
pair<status, expr> 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<expr> 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<expr> 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<expr> 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<name> const & ls, list<name> 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<expr> 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<expr> blast_goal(environment const & env, io_state const & ios, list<na
return b(g);
}
void initialize_blast() {
blast::g_prefix = new name(name::mk_internal_unique_name());
blast::g_tmp_prefix = new name(name::mk_internal_unique_name());
blast::g_prefix = new name(name::mk_internal_unique_name());
blast::g_tmp_prefix = new name(name::mk_internal_unique_name());
blast::g_blast_max_depth = new name{"blast", "max_depth"};
blast::g_blast_init_depth = new name{"blast", "init_depth"};
blast::g_blast_inc_depth = new name{"blast", "inc_depth"};
register_unsigned_option(*blast::g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH,
"(blast) max search depth for blast");
register_unsigned_option(*blast::g_blast_init_depth, LEAN_DEFAULT_BLAST_INIT_DEPTH,
"(blast) initial search depth for blast (remark: blast uses iteration deepening)");
register_unsigned_option(*blast::g_blast_inc_depth, LEAN_DEFAULT_BLAST_INC_DEPTH,
"(blast) search depth increment for blast (remark: blast uses iteration deepening)");
}
void finalize_blast() {
delete blast::g_prefix;

4
src/library/blast/blast.h
View file

@ -24,8 +24,10 @@ environment const & env();
io_state const & ios();
/** \brief Return reference to blast thread local app_builder */
app_builder & get_app_builder();
/** \brief Return the thread local current state begin processed by the blast tactic. */
/** \brief Return the thread local current state being processed by the blast tactic. */
state & curr_state();
/** brief Return the main branch of the current state being processed by the blast tactic. */
inline branch & main_branch() { return curr_state().get_main_branch(); }
/** \brief Return a thread local fresh local constant. */
expr mk_fresh_local(expr const & type, binder_info const & bi = binder_info());
/** \brief Return true iff the given constant name is marked as reducible in env() */

24
src/library/blast/branch.cpp
View file

@ -74,6 +74,11 @@ void branch::add_deps(hypothesis & h_user, unsigned hidx_user) {
}
}
double branch::compute_weight(unsigned hidx, expr const & /* type */) {
// TODO(Leo): use heuristics and machine learning for computing the weight of a new hypothesis
return 1.0 / (static_cast<double>(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<unsigned> branch::activate_hypothesis() {
if (m_todo_queue.empty()) {
return optional<unsigned>();
} else {
unsigned hidx = m_todo_queue.erase_min();
m_active.insert(hidx);
update_indices(hidx);
return optional<unsigned>(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);

16
src/library/blast/branch.h
View file

@ -19,6 +19,7 @@ using metavar_idx_map = typename lean::rb_map<unsigned, T, unsigned_cmp>;
class branch {
typedef hypothesis_idx_map<hypothesis_idx_set> forward_deps;
typedef rb_map<double, unsigned, double_cmp> 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<void(unsigned, hypothesis const &)> 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<unsigned> activate_hypothesis();
/** \brief Store in \c r the hypotheses in this branch sorted by depth */
void get_sorted_hypotheses(hypothesis_idx_buffer & r) const;

57
src/library/blast/state.h
View file

@ -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<expr> 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<expr> resolve(state & s, expr const & pr) {
lean_assert(m_ptr);
return m_ptr->resolve(s, pr);
}
};
class state {
typedef metavar_idx_map<metavar_decl> metavar_decls;
typedef metavar_idx_map<expr> eassignment;
typedef metavar_idx_map<level> uassignment;
typedef hypothesis_idx_map<metavar_idx_set> fixed_by;
typedef list<proof_step> 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<bool>(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