diff --git a/src/library/blast/strategies/portfolio.cpp b/src/library/blast/strategies/portfolio.cpp index ce80361b4e..c2390743c5 100644 --- a/src/library/blast/strategies/portfolio.cpp +++ b/src/library/blast/strategies/portfolio.cpp @@ -45,6 +45,12 @@ static optional apply_ematch() { ematch_action)(); } +static optional apply_unit() { + return mk_debug_action_strategy(unit_preprocess, + unit_propagate, + []() { return action_result::failed(); })(); +} + optional apply_strategy() { std::string s_name(get_config().m_strategy); if (s_name == "preprocess") { @@ -59,6 +65,8 @@ optional apply_strategy() { return apply_cc(); } else if (s_name == "ematch") { return apply_ematch(); + } else if (s_name == "unit") { + return apply_unit(); } else { // TODO(Leo): add more builtin strategies return apply_simple(); diff --git a/tests/lean/run/blast_unit.lean b/tests/lean/run/blast_unit.lean index 84ea94f015..3c58c1ad2c 100644 --- a/tests/lean/run/blast_unit.lean +++ b/tests/lean/run/blast_unit.lean @@ -1,5 +1,5 @@ -- Testing all possible cases of [unit_action] -set_option blast.recursor false +set_option blast.strategy "unit" variables {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Prop} -- H first, all pos diff --git a/tests/lean/run/blast_unit_edges.lean b/tests/lean/run/blast_unit_edges.lean index 97f867e2cb..8de83de114 100644 --- a/tests/lean/run/blast_unit_edges.lean +++ b/tests/lean/run/blast_unit_edges.lean @@ -1,5 +1,6 @@ -- Testing all possible cases of [unit_action] -set_option blast.recursor false +set_option blast.strategy "unit" + universes l1 l2 variables {A B C : Prop} variables {X : Type.{l1}} {Y : Type.{l2}}