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

feat(library/blast): add blast.backward option for disabling/enabling backward chaining

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-30 10:56:52 -07:00
parent a8bb4ba109
commit 9260be01b2
3 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/backward/backward_strategy.cpp
View file

@ -76,6 +76,8 @@ class backward_strategy : public strategy {
};
optional<expr> apply_backward_strategy() {
if (!get_config().m_backward)
return none_expr();
flet<bool> disable_show_failure(get_config().m_show_failure, false);
return backward_strategy()();
}

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

@ -41,6 +41,9 @@ Author: Leonardo de Moura
#ifndef LEAN_DEFAULT_BLAST_EMATCH
#define LEAN_DEFAULT_BLAST_EMATCH false
#endif
#ifndef LEAN_DEFAULT_BLAST_BACKWARD
#define LEAN_DEFAULT_BLAST_BACKWARD true
#endif
namespace lean {
@ -56,6 +59,7 @@ static name * g_blast_cc = nullptr;
static name * g_blast_trace_cc = nullptr;
static name * g_blast_recursor = nullptr;
static name * g_blast_ematch = nullptr;
static name * g_blast_backward = nullptr;
static name * g_blast_show_failure = nullptr;
unsigned get_blast_max_depth(options const & o) {
@ -88,6 +92,9 @@ bool get_blast_recursor(options const & o) {
bool get_blast_ematch(options const & o) {
return o.get_bool(*g_blast_ematch, LEAN_DEFAULT_BLAST_EMATCH);
}
bool get_blast_backward(options const & o) {
return o.get_bool(*g_blast_backward, LEAN_DEFAULT_BLAST_BACKWARD);
}
bool get_blast_show_failure(options const & o) {
return o.get_bool(*g_blast_show_failure, LEAN_DEFAULT_BLAST_SHOW_FAILURE);
}
@ -103,6 +110,7 @@ config::config(options const & o) {
m_trace_cc = get_blast_trace_cc(o);
m_recursor = get_blast_recursor(o);
m_ematch = get_blast_ematch(o);
m_backward = get_blast_backward(o);
m_show_failure = get_blast_show_failure(o);
m_pattern_max_steps = get_pattern_max_steps(o);
}
@ -135,6 +143,7 @@ void initialize_options() {
g_blast_trace_cc = new name{"blast", "trace_cc"};
g_blast_recursor = new name{"blast", "recursor"};
g_blast_ematch = new name{"blast", "ematch"};
g_blast_backward = new name{"blast", "backward"};
g_blast_show_failure = new name{"blast", "show_failure"};
register_unsigned_option(*blast::g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH,
@ -157,6 +166,8 @@ void initialize_options() {
"(blast) enable recursor action");
register_bool_option(*blast::g_blast_ematch, LEAN_DEFAULT_BLAST_EMATCH,
"(blast) enable heuristic instantiation based on e-matching");
register_bool_option(*blast::g_blast_ematch, LEAN_DEFAULT_BLAST_BACKWARD,
"(blast) enable backward chaining");
register_bool_option(*blast::g_blast_show_failure, LEAN_DEFAULT_BLAST_SHOW_FAILURE,
"(blast) show failure state");
}
@ -171,6 +182,7 @@ void finalize_options() {
delete g_blast_trace_cc;
delete g_blast_recursor;
delete g_blast_ematch;
delete g_blast_backward;
delete g_blast_show_failure;
}
}}

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

@ -20,6 +20,7 @@ struct config {
bool m_recursor;
bool m_ematch;
bool m_cc;
bool m_backward;
bool m_trace_cc;
bool m_show_failure;
unsigned m_pattern_max_steps;