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

feat(library/blast): trace strategy name

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-09 17:13:28 -08:00
parent 725101c777
commit 1502248d30
8 changed files with 18 additions and 4 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

@ -50,6 +50,8 @@ static backward_branch_extension & get_extension() {
/** \brief Basic backwards chaining, inspired by Coq's [auto]. */
class backward_strategy_fn : public strategy_fn {
virtual char const * get_name() const override { return "backward"; }
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
Try(assumption_contradiction_actions(hidx));
Try(subst_action(hidx));

1
src/library/blast/grinder/grinder_strategy.h
View file

@ -13,6 +13,7 @@ namespace blast {
The methods pre/post/next can be redefined to extend the set of actions
applied by the grinder. This strategy applies the grinder intro/elim actions. */
class grinder_strategy_core_fn : public strategy_fn {
virtual char const * get_name() const override { return "grinder"; }
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override;
virtual action_result hypothesis_post_activation(hypothesis_idx hidx) override;
virtual action_result next_action() override;

2
src/library/blast/simplifier/simplifier_strategies.cpp
View file

@ -19,6 +19,8 @@ class simplifier_strategy_fn : public strategy_fn {
bool m_simp_hyps;
bool m_use_hyps;
virtual char const * get_name() const override { return "simp"; }
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
Try(assumption_contradiction_actions(hidx));
if (m_simp_hyps) {

2
src/library/blast/strategies/debug_action_strategy.cpp
View file

@ -15,6 +15,8 @@ class debug_action_strategy_core_fn : public strategy_fn {
virtual action_result post(hypothesis_idx) { return action_result::failed(); }
virtual action_result next() { return action_result::failed(); }
virtual char const * get_name() const override { return "debug-action"; }
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
Try(assumption_contradiction_actions(hidx));
Try(discard_action(hidx));

6
src/library/blast/strategies/preprocess_strategy.cpp
View file

@ -27,6 +27,8 @@ class preprocess_strategy_fn : public strategy_fn {
virtual bool show_failure() const override { return false; }
virtual char const * get_name() const override { return "preprocessor"; }
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
Try(assumption_contradiction_actions(hidx));
Try(simplify_hypothesis_action(hidx));
@ -58,7 +60,9 @@ class preprocess_strategy_fn : public strategy_fn {
}
if (get_num_choice_points() > get_initial_num_choice_points())
throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points");
if (optional<expr> pf = m_main()) { return action_result::solved(*pf); }
if (optional<expr> pf = m_main()) {
return action_result::solved(*pf);
}
return action_result::failed();
}
public:

2
src/library/blast/strategies/simple_strategy.cpp
View file

@ -29,6 +29,8 @@ 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_fn : public strategy_fn {
virtual char const * get_name() const override { return "simple"; }
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
Try(assumption_contradiction_actions(hidx));
Try(simplify_hypothesis_action(hidx));

6
src/library/blast/strategy.cpp
View file

@ -58,7 +58,7 @@ optional<expr> strategy_fn::search() {
m_init_num_choices = get_num_choice_points();
unsigned init_proof_depth = curr_state().get_proof_depth();
unsigned max_depth = get_config().m_max_depth;
lean_trace_search(tout() << "search upto depth " << max_depth << "\n";);
lean_trace_search(tout() << "begin '" << get_name() << "' strategy (max-depth: " << max_depth << ")\n";);
trace_curr_state();
trace_target();
action_result r = next_action();
@ -75,7 +75,7 @@ optional<expr> strategy_fn::search() {
r = next_choice_point(m_init_num_choices);
if (failed(r)) {
// all choice points failed...
trace_search(">>> proof not found, no choice points left <<<");
lean_trace_search(tout() << "strategy '" << get_name() << "' failed, no proof found\n";);
if (show_failure())
display_curr_state();
return none_expr();
@ -86,7 +86,7 @@ optional<expr> strategy_fn::search() {
r = next_branch(r.get_proof());
if (r.get_kind() == action_result::Solved) {
// all branches have been solved
trace_search("* found proof");
lean_trace_search(tout() << "strategy '" << get_name() << "' succeeded, proof found\n";);
return some_expr(unfold_hypotheses_ge(curr_state(), r.get_proof(), init_proof_depth));
}
trace_search("* next branch");

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

@ -27,6 +27,7 @@ protected:
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) = 0;
virtual action_result hypothesis_post_activation(hypothesis_idx hidx) = 0;
virtual bool show_failure() const;
virtual char const * get_name() const = 0;
action_result activate_hypothesis();
unsigned get_initial_num_choice_points() const { return m_init_num_choices; }
action_result next_branch(expr pr);