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

feat(library/blast/subst_action): add option for disabling subst action

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-20 10:53:02 -08:00
parent 028a2ab785
commit 1e3f549c39
3 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/blast/options.cpp
View file

@ -19,6 +19,9 @@ Author: Leonardo de Moura
#ifndef LEAN_DEFAULT_BLAST_TRACE
#define LEAN_DEFAULT_BLAST_TRACE false
#endif
#ifndef LEAN_DEFAULT_BLAST_SUBST
#define LEAN_DEFAULT_BLAST_SUBST true
#endif
namespace lean {
namespace blast {
@ -27,6 +30,7 @@ static name * g_blast_max_depth = nullptr;
static name * g_blast_init_depth = nullptr;
static name * g_blast_inc_depth = nullptr;
static name * g_blast_trace = nullptr;
static name * g_blast_subst = nullptr;
unsigned get_blast_max_depth(options const & o) {
return o.get_unsigned(*g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH);
@ -40,12 +44,16 @@ unsigned get_blast_inc_depth(options const & o) {
bool get_blast_trace(options const & o) {
return o.get_bool(*g_blast_trace, LEAN_DEFAULT_BLAST_TRACE);
}
bool get_blast_subst(options const & o) {
return o.get_bool(*g_blast_subst, LEAN_DEFAULT_BLAST_SUBST);
}
config::config(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);
m_trace = get_blast_trace(o);
m_subst = get_blast_subst(o);
}
LEAN_THREAD_PTR(config, g_config);
@ -70,6 +78,7 @@ void initialize_options() {
g_blast_init_depth = new name{"blast", "init_depth"};
g_blast_inc_depth = new name{"blast", "inc_depth"};
g_blast_trace = new name{"blast", "trace"};
g_blast_subst = new name{"blast", "subst"};
register_unsigned_option(*blast::g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH,
"(blast) max search depth for blast");
@ -79,11 +88,14 @@ void initialize_options() {
"(blast) search depth increment for blast (remark: blast uses iteration deepening)");
register_bool_option(*blast::g_blast_trace, LEAN_DEFAULT_BLAST_TRACE,
"(blast) trace");
register_bool_option(*blast::g_blast_subst, LEAN_DEFAULT_BLAST_SUBST,
"(blast) enable subst action");
}
void finalize_options() {
delete g_blast_max_depth;
delete g_blast_init_depth;
delete g_blast_inc_depth;
delete g_blast_trace;
delete g_blast_subst;
}
}}

1
src/library/blast/options.h
View file

@ -15,6 +15,7 @@ struct config {
unsigned m_init_depth;
unsigned m_inc_depth;
bool m_trace;
bool m_subst;
config(options const & o);
};

3
src/library/blast/subst_action.cpp
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "library/blast/intros_action.h"
#include "library/blast/blast.h"
#include "library/blast/trace.h"
#include "library/blast/options.h"
namespace lean {
namespace blast {
@ -86,6 +87,8 @@ bool subst_core(hypothesis_idx hidx) {
}
action_result subst_action(hypothesis_idx hidx) {
if (!get_config().m_subst)
return action_result::failed();
state & s = curr_state();
app_builder & b = get_app_builder();
hypothesis const & h = s.get_hypothesis_decl(hidx);