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

refactor(library/blast): move simple search strategy to separate module

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-10 11:44:18 -08:00
parent 6ac2bf9c6c
commit 6f01a7339a
4 changed files with 124 additions and 87 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/CMakeLists.txt
View file

@ -1,3 +1,3 @@
add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
init_module.cpp simplifier.cpp assumption.cpp intros.cpp proof_expr.cpp
options.cpp choice_point.cpp)
options.cpp choice_point.cpp simple_strategy.cpp)

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

@ -20,12 +20,9 @@ Author: Leonardo de Moura
#include "library/blast/expr.h"
#include "library/blast/state.h"
#include "library/blast/blast.h"
#include "library/blast/assumption.h"
#include "library/blast/intros.h"
#include "library/blast/proof_expr.h"
#include "library/blast/options.h"
#include "library/blast/choice_point.h"
#include "library/blast/blast_exception.h"
#include "library/blast/simple_strategy.h"
namespace lean {
namespace blast {
@ -57,11 +54,6 @@ class blastenv {
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::assignment_snapshot> m_stack;
@ -386,81 +378,6 @@ 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);
}
enum status { NoAction, ClosedBranch, Continue };
optional<unsigned> activate_hypothesis() {
return m_curr_state.activate_hypothesis();
}
pair<status, expr> next_action() {
if (intros_action()) {
return mk_pair(Continue, expr());
} else if (activate_hypothesis()) {
// TODO(Leo): we should probably eagerly simplify the activated hypothesis.
return mk_pair(Continue, expr());
} else if (auto pr = assumption_action()) {
return mk_pair(ClosedBranch, *pr);
} 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_proof_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;
clear_choice_points();
}
return none_expr();
}
expr to_tactic_proof(expr const & pr) {
// When a proof is found we must
@ -488,7 +405,6 @@ public:
m_congr_lemma_manager(m_app_builder, m_fun_info_manager),
m_tctx(*this) {
init_uref_mref_href_idxs();
set_options(m_ios.get_options());
}
~blastenv() {
@ -505,7 +421,7 @@ public:
optional<expr> operator()(goal const & g) {
init_state(g);
if (auto r = search()) {
if (auto r = apply_simple_strategy()) {
return some_expr(to_tactic_proof(*r));
} else {
return none_expr();

108
src/library/blast/simple_strategy.cpp Normal file
View file

@ -0,0 +1,108 @@
/*
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/blast.h"
#include "library/blast/options.h"
#include "library/blast/choice_point.h"
#include "library/blast/assumption.h"
#include "library/blast/intros.h"
namespace lean {
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 {
unsigned m_max_depth;
unsigned m_init_depth;
unsigned m_inc_depth;
enum status { NoAction, ClosedBranch, Continue };
optional<unsigned> activate_hypothesis() {
return curr_state().activate_hypothesis();
}
pair<status, expr> next_action() {
if (intros_action()) {
return mk_pair(Continue, expr());
} else if (activate_hypothesis()) {
// TODO(Leo): we should probably eagerly simplify the activated hypothesis.
return mk_pair(Continue, expr());
} else if (auto pr = assumption_action()) {
return mk_pair(ClosedBranch, *pr);
} else {
// TODO(Leo): add more actions...
return mk_pair(NoAction, expr());
}
}
optional<expr> resolve(expr pr) {
while (curr_state().has_proof_steps()) {
proof_step s = curr_state().top_proof_step();
if (auto new_pr = s.resolve(curr_state(), pr)) {
pr = *new_pr;
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 (curr_state().get_proof_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 = curr_state();
unsigned d = m_init_depth;
while (d <= m_max_depth) {
if (auto r = search_upto(d))
return r;
d += m_inc_depth;
curr_state() = s;
clear_choice_points();
}
return none_expr();
}
public:
simple_strategy() {
options o = ios().get_options();
m_max_depth = get_blast_max_depth(o);
m_init_depth = get_blast_init_depth(o);
m_inc_depth = get_blast_inc_depth(o);
}
optional<expr> operator()() {
return search();
}
};
optional<expr> apply_simple_strategy() {
return simple_strategy()();
}
}}

13
src/library/blast/simple_strategy.h Normal file
View file

@ -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_simple_strategy();
}}