refactor(library/blast/simple_strategy): eliminate duplicated code

This commit is contained in:
Leonardo de Moura 2015-11-15 14:30:24 -08:00
parent 2549e49e72
commit ffd0c2b09a

View file

@ -22,8 +22,30 @@ namespace blast {
/** \brief Implement a simple proof strategy for blast. /** \brief Implement a simple proof strategy for blast.
We use it mainly for testing new actions and the whole blast infra-structure. */ We use it mainly for testing new actions and the whole blast infra-structure. */
class simple_strategy : public strategy { class simple_strategy : public strategy {
optional<hypothesis_idx> activate_hypothesis() {
return curr_state().activate_hypothesis(); action_result activate_hypothesis(bool preprocess) {
auto hidx = curr_state().activate_hypothesis();
if (!hidx) return action_result::failed();
if (!preprocess) display_action("activate");
if (auto pr = assumption_contradiction_actions(*hidx)) {
if (!preprocess) display_action("assumption-contradiction");
return action_result::solved(*pr);
}
if (subst_action(*hidx)) {
if (!preprocess) display_action("subst");
return action_result::new_branch();
}
action_result r = no_confusion_action(*hidx);
if (!failed(r)) {
if (!preprocess) display_action("no_confusion");
return r;
}
return action_result::new_branch();
} }
/* \brief Preprocess state /* \brief Preprocess state
@ -34,18 +56,9 @@ class simple_strategy : public strategy {
while (true) { while (true) {
if (intros_action()) if (intros_action())
continue; continue;
if (auto hidx = activate_hypothesis()) { auto r = activate_hypothesis(true);
if (auto pr = assumption_contradiction_actions(*hidx)) { if (solved(r)) return r.to_opt_expr();
return pr; if (failed(r)) break;
}
if (subst_action(*hidx))
continue;
action_result r = no_confusion_action(*hidx);
if (solved(r))
return r.to_opt_expr();
continue;
}
break;
} }
if (auto pr = assumption_action()) if (auto pr = assumption_action())
return pr; return pr;
@ -58,23 +71,8 @@ class simple_strategy : public strategy {
return action_result::new_branch(); return action_result::new_branch();
} }
if (auto hidx = activate_hypothesis()) { action_result r = activate_hypothesis(false);
display_action("activate"); if (!failed(r)) return r;
if (auto pr = assumption_contradiction_actions(*hidx)) {
display_action("assumption-contradiction");
return action_result::solved(*pr);
}
if (subst_action(*hidx)) {
display_action("subst");
return action_result::new_branch();
}
action_result r = no_confusion_action(*hidx);
if (!failed(r)) {
display_action("no_confusion");
return r;
}
return action_result::new_branch();
}
if (auto pr = trivial_action()) { if (auto pr = trivial_action()) {
display_action("trivial"); display_action("trivial");
@ -88,7 +86,7 @@ class simple_strategy : public strategy {
return action_result::solved(*pr); return action_result::solved(*pr);
} }
action_result r = constructor_action(); r = constructor_action();
if (!failed(r)) { if (!failed(r)) {
display_action("constructor"); display_action("constructor");
return r; return r;