feat(library/blast/strategies): add 'blast.strategy "preprocess"'

src/library/blast/strategies/portfolio.cpp

@@ -4,16 +4,29 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
 #include "library/blast/strategies/simple_strategy.h"
 #include "library/blast/strategies/preprocess_strategy.h"
 
 namespace lean {
 namespace blast {
+static optional<expr> apply_preprocess() {
+    return preprocess_and_then([]() { return none_expr(); })();
+}
+
 static optional<expr> apply_simple() {
     return preprocess_and_then(mk_simple_strategy())();
 }
 
 optional<expr> apply_strategy() {
-    return apply_simple();
+    std::string s_name(get_config().m_strategy);
+    if (s_name == "preprocess") {
+        return apply_preprocess();
+    } else if (s_name == "simple") {
+        return apply_simple();
+    } else {
+        // TODO(Leo): add more builtin strategies
+        return apply_simple();
+    }
 }
 }}

tests/lean/run/blast1.lean

@@ -1,2 +1,4 @@
+set_option blast.strategy "preprocess"
+
 example (a b : Prop) (Ha : a) (Hb : b) : a :=
 by blast

tests/lean/run/blast2.lean

@@ -1,3 +1,5 @@
+set_option blast.strategy "preprocess"
+
 example (a b : Prop) : forall (Ha : a) (Hb : b), a :=
 by blast
 

tests/lean/run/blast3.lean

@@ -1,4 +1,5 @@
-set_option blast.init_depth 10
+-- TODO(Leo): use better strategy
+set_option blast.strategy "simple"
 set_option blast.cc false
 
 example (a b c : Prop) : b → c → b ∧ c :=

tests/lean/run/blast4.lean

@@ -1,3 +1,5 @@
+set_option blast.strategy "preprocess"
+
 lemma T1 (a b : Prop) : false → a :=
 by blast
 

tests/lean/run/blast5.lean

@@ -1,4 +1,4 @@
-set_option blast.init_depth 10
+set_option blast.strategy "preprocess"
 
 example (a b : nat) : a = b → b = a :=
 by blast

tests/lean/run/blast6.lean

@@ -1,4 +1,4 @@
-set_option blast.init_depth 10
+set_option blast.strategy "preprocess"
 
 lemma lemma1 (bv : nat → Type) (n m : nat) (H : n = m) (b1 : bv n) (b2 : bv m) (H2 : eq.rec_on H b1 = b2) : b1 = eq.rec_on (eq.symm H) b2 :=
 by blast

tests/lean/run/blast7.lean

@@ -1,4 +1,4 @@
-set_option blast.init_depth 10
+set_option blast.strategy "preprocess"
 
 lemma lemma1 (p : Prop) (a b : nat) : a = b → p → p :=
 by blast

tests/lean/run/blast8.lean

@@ -1,6 +1,5 @@
 open nat
-set_option blast.init_depth 10
+set_option blast.strategy "preprocess"
-set_option blast.max_depth 10
 
 lemma l1 (a : nat) : zero = succ a → a = a → false :=
 by blast

tests/lean/run/blast9.lean

@@ -1,5 +1,6 @@
 import data.list
 open list
+set_option blast.strategy "preprocess"
 
 example (p : Prop) (a b c : nat) : [a, b, c] = [] → p :=
 by blast