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

fix(library/blast/strategies/preprocess_strategy): do not show failure state again

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-07 19:31:34 -08:00
parent 6bfc22de11
commit be99d5f26f
3 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -24,6 +24,8 @@ class preprocess_strategy_fn : public strategy_fn {
bool m_simple;
bool m_done{false};
virtual bool show_failure() const override { return false; }
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
Try(assumption_contradiction_actions(hidx));
Try(simplify_hypothesis_action(hidx));
@ -55,10 +57,8 @@ 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");
{
scope_trace s(get_config().m_trace);
TryStrategy(m_main);
}
scope_trace s(get_config().m_trace);
if (optional<expr> pf = m_main()) { return action_result::solved(*pf); }
return action_result::failed();
}
public:

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

@ -46,6 +46,10 @@ action_result strategy_fn::next_branch(expr pr) {
return action_result::solved(pr);
}
bool strategy_fn::show_failure() const {
return get_config().m_show_failure;
}
optional<expr> strategy_fn::search() {
scope_choice_points scope1;
m_ps_check_point = curr_state().mk_proof_steps_check_point();
@ -71,7 +75,7 @@ optional<expr> strategy_fn::search() {
if (failed(r)) {
// all choice points failed...
trace(">>> proof not found, no choice points left <<<");
if (get_config().m_show_failure)
if (show_failure())
display_curr_state();
return none_expr();
}

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

@ -26,6 +26,7 @@ protected:
virtual action_result next_action() = 0;
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;
action_result activate_hypothesis();
unsigned get_initial_num_choice_points() const { return m_init_num_choices; }
action_result next_branch(expr pr);