From b044f9e8c103232a1d8506a3bdfc8b659a5110fd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Dec 2015 15:01:49 -0800 Subject: [PATCH] feat(library/blast/strategies): add "ematch" strategy for testing ematching --- .../strategies/debug_action_strategy.cpp | 21 +++++++++++++++++++ .../blast/strategies/debug_action_strategy.h | 3 +++ src/library/blast/strategies/portfolio.cpp | 14 +++++++++++++ tests/lean/run/blast_congr_bug.lean | 8 ++----- tests/lean/run/blast_ematch1.lean | 5 +---- tests/lean/run/blast_ematch10.lean | 3 +-- tests/lean/run/blast_ematch2.lean | 2 +- tests/lean/run/blast_ematch3.lean | 8 ++----- tests/lean/run/blast_ematch4.lean | 4 +--- tests/lean/run/blast_ematch5.lean | 8 +------ tests/lean/run/blast_ematch6.lean | 4 +--- tests/lean/run/blast_ematch7.lean | 10 ++------- tests/lean/run/blast_ematch8.lean | 4 +--- tests/lean/run/blast_ematch9.lean | 2 +- 14 files changed, 52 insertions(+), 44 deletions(-) diff --git a/src/library/blast/strategies/debug_action_strategy.cpp b/src/library/blast/strategies/debug_action_strategy.cpp index 1954383f60..46bdce69ac 100644 --- a/src/library/blast/strategies/debug_action_strategy.cpp +++ b/src/library/blast/strategies/debug_action_strategy.cpp @@ -61,6 +61,21 @@ public: m_action(a) {} }; +class xdebug_action_strategy_fn : public debug_action_strategy_core_fn { + std::function m_pre; + std::function m_post; + std::function m_next; + + virtual action_result pre(hypothesis_idx hidx) { return m_pre(hidx); } + virtual action_result post(hypothesis_idx hidx) { return m_post(hidx); } + virtual action_result next() { return m_next(); } +public: + xdebug_action_strategy_fn(std::function const & pre, + std::function const & post, + std::function const & next): + m_pre(pre), m_post(post), m_next(next) {} +}; + strategy mk_debug_action_strategy(std::function const & a) { return [=]() { return debug_action_strategy_fn(a)(); }; // NOLINT } @@ -72,4 +87,10 @@ strategy mk_debug_pre_action_strategy(std::function const & a) { return [=]() { return debug_post_action_strategy_fn(a)(); }; // NOLINT } + +strategy mk_debug_action_strategy(std::function const & pre, + std::function const & post, + std::function const & next) { + return [=]() { return xdebug_action_strategy_fn(pre, post, next)(); }; // NOLINT +} }} diff --git a/src/library/blast/strategies/debug_action_strategy.h b/src/library/blast/strategies/debug_action_strategy.h index 1da79bac2f..fc61330362 100644 --- a/src/library/blast/strategies/debug_action_strategy.h +++ b/src/library/blast/strategies/debug_action_strategy.h @@ -13,4 +13,7 @@ namespace blast { strategy mk_debug_action_strategy(std::function const & a); strategy mk_debug_pre_action_strategy(std::function const & a); strategy mk_debug_post_action_strategy(std::function const & a); +strategy mk_debug_action_strategy(std::function const & pre, + std::function const & post, + std::function const & next); }} diff --git a/src/library/blast/strategies/portfolio.cpp b/src/library/blast/strategies/portfolio.cpp index e21b89a542..ce80361b4e 100644 --- a/src/library/blast/strategies/portfolio.cpp +++ b/src/library/blast/strategies/portfolio.cpp @@ -7,6 +7,8 @@ Author: Leonardo de Moura #include #include "library/blast/actions/assert_cc_action.h" #include "library/blast/simplifier/simplifier_strategies.h" +#include "library/blast/unit/unit_actions.h" +#include "library/blast/forward/ematch.h" #include "library/blast/strategies/simple_strategy.h" #include "library/blast/strategies/preprocess_strategy.h" #include "library/blast/strategies/debug_action_strategy.h" @@ -18,10 +20,12 @@ static optional apply_preprocess() { } static optional apply_simp() { + flet set(get_config().m_simp, true); return mk_simplify_using_hypotheses_strategy()(); } static optional apply_simp_nohyps() { + flet set(get_config().m_simp, true); return mk_simplify_all_strategy()(); } @@ -30,9 +34,17 @@ static optional apply_simple() { } static optional apply_cc() { + flet set(get_config().m_cc, true); return mk_debug_pre_action_strategy(assert_cc_action)(); } +static optional apply_ematch() { + flet set(get_config().m_ematch, true); + return mk_debug_action_strategy([](hypothesis_idx hidx) { Try(unit_propagate(hidx)); TrySolve(assert_cc_action(hidx)); return action_result::new_branch(); }, + unit_propagate, + ematch_action)(); +} + optional apply_strategy() { std::string s_name(get_config().m_strategy); if (s_name == "preprocess") { @@ -45,6 +57,8 @@ optional apply_strategy() { return apply_simple(); } else if (s_name == "cc") { return apply_cc(); + } else if (s_name == "ematch") { + return apply_ematch(); } else { // TODO(Leo): add more builtin strategies return apply_simple(); diff --git a/tests/lean/run/blast_congr_bug.lean b/tests/lean/run/blast_congr_bug.lean index fda591fc58..0604421da1 100644 --- a/tests/lean/run/blast_congr_bug.lean +++ b/tests/lean/run/blast_congr_bug.lean @@ -4,17 +4,13 @@ attribute P_sub [instance] constant q : P → Prop section -set_option blast.simp true -set_option blast.cc false - example (h₁ h₂ : P) : q h₁ = q h₂ := -by blast +by simp end section -set_option blast.simp false -set_option blast.cc true +set_option blast.strategy "cc" example (h₁ h₂ : P) : q h₁ = q h₂ := by blast diff --git a/tests/lean/run/blast_ematch1.lean b/tests/lean/run/blast_ematch1.lean index e95ead910c..901de7d4e7 100644 --- a/tests/lean/run/blast_ematch1.lean +++ b/tests/lean/run/blast_ematch1.lean @@ -6,10 +6,7 @@ constant g : nat → nat definition lemma1 [forward] : ∀ x, (:g (f x):) = x := sorry -set_option blast.init_depth 10 -set_option blast.inc_depth 1000 -set_option blast.subst false -set_option blast.ematch true +set_option blast.strategy "ematch" example (a b c : nat) : a = f b → a = f c → g a ≠ b → false := by blast diff --git a/tests/lean/run/blast_ematch10.lean b/tests/lean/run/blast_ematch10.lean index 61890f1204..0fa71972ac 100644 --- a/tests/lean/run/blast_ematch10.lean +++ b/tests/lean/run/blast_ematch10.lean @@ -1,6 +1,5 @@ attribute iff [reducible] -set_option blast.subst false -set_option blast.simp false +set_option blast.strategy "ematch" definition lemma1 (p : nat → Prop) (a b c : nat) : p a → a = b → p b := by blast diff --git a/tests/lean/run/blast_ematch2.lean b/tests/lean/run/blast_ematch2.lean index 1888269e97..2ca111975b 100644 --- a/tests/lean/run/blast_ematch2.lean +++ b/tests/lean/run/blast_ematch2.lean @@ -6,7 +6,7 @@ constant g : nat → nat definition lemma1 [forward] : ∀ x, g (f x) = x := sorry -set_option blast.ematch true +set_option blast.strategy "ematch" example (a b : nat) : f a = f b → a = b := by blast diff --git a/tests/lean/run/blast_ematch3.lean b/tests/lean/run/blast_ematch3.lean index c337e523a5..8147b1eee1 100644 --- a/tests/lean/run/blast_ematch3.lean +++ b/tests/lean/run/blast_ematch3.lean @@ -10,9 +10,7 @@ include s attribute add.comm [forward] attribute add.assoc [forward] -set_option blast.simp false -set_option blast.subst false -set_option blast.ematch true +set_option blast.strategy "ematch" theorem add_comm_three (a b c : A) : a + b + c = c + b + a := by blast @@ -29,9 +27,7 @@ attribute mul.assoc [forward] attribute mul.left_inv [forward] attribute one_mul [forward] -set_option blast.simp false -set_option blast.subst false -set_option blast.ematch true +set_option blast.strategy "ematch" theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b := by blast diff --git a/tests/lean/run/blast_ematch4.lean b/tests/lean/run/blast_ematch4.lean index 7e39afb044..42d1ab5bfd 100644 --- a/tests/lean/run/blast_ematch4.lean +++ b/tests/lean/run/blast_ematch4.lean @@ -3,9 +3,7 @@ open algebra nat section open nat -set_option blast.simp false -set_option blast.subst false -set_option blast.ematch true +set_option blast.strategy "ematch" attribute add.comm [forward] attribute add.assoc [forward] diff --git a/tests/lean/run/blast_ematch5.lean b/tests/lean/run/blast_ematch5.lean index a5ab2f053e..5a8e8c45bc 100644 --- a/tests/lean/run/blast_ematch5.lean +++ b/tests/lean/run/blast_ematch5.lean @@ -3,13 +3,7 @@ constant subt : nat → nat → Prop lemma subt_trans [forward] {a b c : nat} : subt a b → subt b c → subt a c := sorry -set_option blast.init_depth 20 -set_option blast.inc_depth 100 -set_option blast.ematch true -set_option blast.simp false --- TODO(Leo): check if unit propagation is still buggy --- If I remove the following option, blast fails -set_option blast.backward true -- false +set_option blast.strategy "ematch" example (a b c d : nat) : subt a b → subt b c → subt c d → subt a d := by blast diff --git a/tests/lean/run/blast_ematch6.lean b/tests/lean/run/blast_ematch6.lean index d1bb16f7ac..d9bddeaee9 100644 --- a/tests/lean/run/blast_ematch6.lean +++ b/tests/lean/run/blast_ematch6.lean @@ -7,9 +7,7 @@ section variable [s : group A] include s -set_option blast.simp false -set_option blast.subst false -set_option blast.ematch true +set_option blast.strategy "ematch" attribute mul_one [forward] attribute mul.assoc [forward] diff --git a/tests/lean/run/blast_ematch7.lean b/tests/lean/run/blast_ematch7.lean index aff177afbb..30f01c3771 100644 --- a/tests/lean/run/blast_ematch7.lean +++ b/tests/lean/run/blast_ematch7.lean @@ -4,9 +4,8 @@ open algebra variables {A : Type} [s : ring A] (a b : A) include s -set_option blast.subst false -set_option blast.simp false -set_option blast.ematch true +set_option blast.strategy "ematch" + attribute zero_mul [forward] example : a = 0 → a * b = 0 := @@ -14,11 +13,6 @@ by blast open int --- Remark: int is a non-recursive datatype. So, the recursor action will --- destruct it. This is a dumb move, and we need to prove the same theorem 4 times because of that. --- It also demonstrates we need better heuristics for the recursor action and/or annotations. -set_option blast.recursor false - definition ex1 (a b : int) : a = 0 → a * b = 0 := by blast diff --git a/tests/lean/run/blast_ematch8.lean b/tests/lean/run/blast_ematch8.lean index a52a4c23e1..84f2053deb 100644 --- a/tests/lean/run/blast_ematch8.lean +++ b/tests/lean/run/blast_ematch8.lean @@ -5,9 +5,7 @@ variables {A : Type} variables [s : group A] include s namespace foo -set_option blast.ematch true -set_option blast.subst false -set_option blast.simp false +set_option blast.strategy "ematch" attribute inv_inv mul.left_inv mul.assoc one_mul mul_one [forward] theorem mul.right_inv (a : A) : a * a⁻¹ = 1 := diff --git a/tests/lean/run/blast_ematch9.lean b/tests/lean/run/blast_ematch9.lean index 450e2671ba..44963cb84a 100644 --- a/tests/lean/run/blast_ematch9.lean +++ b/tests/lean/run/blast_ematch9.lean @@ -2,7 +2,7 @@ constant P : nat → Prop definition h [reducible] (n : nat) := n definition foo [forward] : ∀ x, P (h x) := sorry -set_option blast.ematch true +set_option blast.strategy "ematch" example (n : nat) : P (h n) := by blast