From c7390684bad504708e83181ca96f8f0f7dd2a47a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Dec 2015 08:45:54 -0800
Subject: [PATCH] feat(library/blast/strategies/portfolio): add 'unit' strategy
 for testing unit propagation

---
 src/library/blast/strategies/portfolio.cpp | 8 ++++++++
 tests/lean/run/blast_unit.lean             | 2 +-
 tests/lean/run/blast_unit_edges.lean       | 3 ++-
 3 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/library/blast/strategies/portfolio.cpp b/src/library/blast/strategies/portfolio.cpp
index ce80361b4..c2390743c 100644
--- a/src/library/blast/strategies/portfolio.cpp
+++ b/src/library/blast/strategies/portfolio.cpp
@@ -45,6 +45,12 @@ static optional<expr> apply_ematch() {
                                     ematch_action)();
 }
 
+static optional<expr> apply_unit() {
+    return mk_debug_action_strategy(unit_preprocess,
+                                    unit_propagate,
+                                    []() { return action_result::failed(); })();
+}
+
 optional<expr> apply_strategy() {
     std::string s_name(get_config().m_strategy);
     if (s_name == "preprocess") {
@@ -59,6 +65,8 @@ optional<expr> 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 84ea94f01..3c58c1ad2 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 97f867e2c..8de83de11 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}}