1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Time_Methods_Cmd_Test imports 8 Lib.Time_Methods_Cmd 9 Lib.Eisbach_Methods 10 "HOL-Library.Sublist" 11begin 12 13text \<open> 14 @{method time_methods} is a utility that runs several methods on the same 15 proof goal, printing the running time of each one. 16 17 Usage: 18 19 apply (time_methods [(no_check)] [(skip_fail)] 20 [name1:] \<open>method1\<close> 21 [name2:] \<open>method2\<close> 22 ...) 23 24 Options: 25 26 no_check: Don't check that the outputs of each method match. 27 28 skip_fail: Don't print anything for failed methods. 29\<close> 30 31experiment begin 32 section \<open>Basic examples\<close> 33 34 lemma 35 "A \<Longrightarrow> B \<Longrightarrow> A \<or> B" 36 apply (time_methods 37 \<open>erule disjI1\<close> 38 \<open>erule disjI2\<close>) 39 done 40 41 text \<open>Give labels to methods:\<close> 42 lemma 43 "A \<Longrightarrow> B \<Longrightarrow> A \<or> B" 44 apply (time_methods 45 label: \<open>erule disjI1\<close> 46 "another label": \<open>erule disjI2\<close>) 47 done 48 49 text \<open>no_check prevents failing even if the method results differ.\<close> 50 lemma 51 "A \<Longrightarrow> B \<Longrightarrow> A \<or> B" 52 apply (time_methods (no_check) 53 \<open>rule disjI1\<close> 54 \<open>rule disjI2\<close>) 55 apply assumption 56 done 57 58 text \<open> 59 Fast and slow list reversals. 60 \<close> 61 lemma list_eval_rev_append: 62 "rev xs = rev xs @ []" 63 "rev [] @ ys = ys" 64 "rev (x # xs) @ ys = rev xs @ (x # ys)" 65 by auto 66 67 lemma "rev [0..100] = map ((-) 100) [0..100]" 68 "rev [0..200] = map ((-) 200) [0..200]" 69 text \<open>evaluate everything but @{term rev}\<close> 70 apply (all \<open>match conclusion in "rev x = y" for x y \<Rightarrow> 71 \<open>rule subst[where t = x], simp add: upto.simps\<close>\<close>) 72 apply (all \<open>match conclusion in "rev x = y" for x y \<Rightarrow> 73 \<open>rule subst[where t = y], simp add: upto.simps\<close>\<close>) 74 75 text \<open>evaluate @{term rev}\<close> 76 apply (time_methods 77 naive100: \<open>simp\<close> 78 slow100: \<open>simp only: rev.simps append.simps\<close> 79 fast100: \<open>subst list_eval_rev_append(1), simp only: list_eval_rev_append(2-3)\<close> 80 ) 81 apply (time_methods 82 naive200: \<open>simp\<close> 83 slow200: \<open>simp only: rev.simps append.simps\<close> 84 fast200: \<open>subst list_eval_rev_append(1), simp only: list_eval_rev_append(2-3)\<close> 85 ) 86 done 87 88 text \<open> 89 Fast and slow subsequence testing. 90 \<close> 91 lemma 92 "subseq (map ((*) 2) [1 .. 5]) [1 .. 10]" 93 "subseq (map ((*) 2) [1 .. 6]) [1 .. 12]" 94 "subseq (map ((*) 2) [1 .. 7]) [1 .. 14]" 95 "subseq (map ((*) 2) [1 .. 8]) [1 .. 16]" 96 apply (all \<open>match conclusion in "subseq x y" for x y \<Rightarrow> 97 \<open>rule subst[where t = x], simp add: upto.simps, 98 rule subst[where t = y], simp add: upto.simps\<close>\<close>) 99 100 apply (time_methods 101 "HOL simp": \<open>simp\<close> 102 103 "l4v simp": \<open>simp cong: if_cong cong del: if_weak_cong\<close> 104 \<comment> \<open>exponential time!\<close> 105 )+ 106 done 107 108 text \<open> 109 Which method is a better SAT solver? 110 Instance 01 from the uf20-91 dataset at http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html 111 \<close> 112 lemma "\<exists>x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20. 113 (~x4 & x18 & ~x19) | (~x3 & ~x18 & x5) | (x5 & x8 & x15) | (x20 & ~x7 & x16) | 114 (~x10 & x13 & x7) | (x12 & x9 & ~x17) | (~x17 & ~x19 & ~x5) | (x16 & ~x9 & ~x15) | 115 (~x11 & x5 & x14) | (~x18 & x10 & ~x13) | (x3 & ~x11 & ~x12) | (x6 & x17 & x8) | 116 (x18 & ~x14 & ~x1) | (x19 & x15 & ~x10) | (~x12 & ~x18 & x19) | (x8 & ~x4 & ~x7) | 117 (x8 & x9 & ~x4) | (~x7 & ~x17 & x15) | (~x12 & x7 & x14) | (x10 & x11 & ~x8) | 118 (~x2 & x15 & x11) | (~x9 & ~x6 & ~x1) | (x11 & ~x20 & x17) | (~x9 & x15 & ~x13) | 119 (~x12 & x7 & x17) | (x18 & x2 & ~x20) | (~x20 & ~x12 & ~x4) | (~x19 & ~x11 & ~x14) | 120 (x16 & ~x18 & x4) | (x1 & x17 & x19) | (x13 & ~x15 & ~x10) | (x12 & x14 & x13) | 121 (~x12 & x14 & x7) | (x7 & ~x16 & ~x10) | (~x6 & ~x10 & ~x7) | (~x20 & ~x14 & x16) | 122 (x19 & ~x17 & ~x11) | (x7 & ~x1 & x20) | (x5 & ~x12 & ~x15) | (x4 & x9 & x13) | 123 (~x12 & x11 & x7) | (x5 & ~x19 & x8) | (~x1 & ~x16 & ~x17) | (~x20 & x14 & x15) | 124 (~x13 & x4 & ~x10) | (~x14 & ~x7 & ~x10) | (x5 & ~x9 & ~x20) | (~x10 & ~x1 & x19) | 125 (x16 & x15 & x1) | (~x16 & ~x3 & x11) | (x15 & x10 & ~x4) | (~x4 & x15 & x3) | 126 (x10 & x16 & ~x11) | (x8 & ~x12 & x5) | (~x14 & x6 & ~x12) | (~x1 & ~x6 & ~x11) | 127 (x13 & x5 & x1) | (x7 & x2 & ~x12) | (~x1 & x20 & ~x19) | (x2 & x13 & x8) | 128 (~x15 & ~x18 & ~x4) | (x11 & ~x14 & ~x9) | (x6 & x15 & x2) | (~x5 & x12 & x15) | 129 (x6 & ~x17 & ~x5) | (x13 & ~x5 & x19) | (~x20 & x1 & ~x14) | (~x9 & x17 & ~x15) | 130 (x5 & ~x19 & x18) | (x12 & ~x8 & x10) | (x18 & ~x14 & x4) | (~x15 & x9 & ~x13) | 131 (~x9 & x5 & x1) | (~x10 & x19 & x14) | (~x20 & ~x9 & ~x4) | (x9 & x2 & ~x19) | 132 (x5 & ~x13 & x17) | (~x2 & x10 & x18) | (x18 & ~x3 & ~x11) | (~x7 & x9 & ~x17) | 133 (x15 & x6 & x3) | (x2 & ~x3 & x13) | (~x12 & ~x3 & x2) | (x2 & x3 & ~x17) | 134 (~x20 & x15 & x16) | (x5 & x17 & x19) | (x20 & x18 & ~x11) | (x9 & ~x1 & x5) | 135 (x19 & ~x9 & ~x17) | (~x12 & x2 & ~x17)" 136 using [[meson_max_clauses=99]] 137 apply (time_methods 138 blast: \<open>blast\<close> 139 metis: \<open>metis\<close> 140 meson: \<open>meson\<close> 141 smt: \<open>smt\<close> 142 force: \<open>force\<close> 143 fastforce: \<open>fastforce intro: ex_bool_eq[THEN iffD2]\<close> 144 fastforce: \<open>fastforce simp: ex_bool_eq\<close> 145 presburger: \<open>use ex_bool_eq[simp] in presburger\<close> 146 ) 147 done 148 149 section \<open>Other tests\<close> 150 151 text \<open>Test ML interface\<close> 152 lemma "True" 153 apply (tactic \<open> 154 let val method = SIMPLE_METHOD (simp_tac @{context} 1) 155 fun dummy_callback _ _ = () 156 in (fn st => Time_Methods.time_methods false false dummy_callback [(NONE, method)] [] st 157 |> (fn ([timing], st') => (tracing (Timing.message timing); st'))) 158 |> NO_CONTEXT_TACTIC @{context} 159 end\<close>) 160 done 161 162 text \<open>Check that we fail when the methods give different results\<close> 163 lemma 164 "A \<or> B" 165 apply (tactic \<open> 166 let 167 fun skip_dummy_state tac = fn st => 168 case Thm.prop_of st of 169 Const ("Pure.prop", _) $ (Const ("Pure.term", _) $ Const ("Pure.dummy_pattern", _)) => 170 Seq.succeed st 171 | _ => tac st; 172 val methods = @{thms disjI1 disjI2} 173 |> map (fn rule => (NONE, SIMPLE_METHOD (resolve_tac @{context} [rule] 1))) 174 fun dummy_callback _ _ = () 175 in (fn st => Time_Methods.time_methods false false dummy_callback methods [] st 176 |> (fn (timing, st') => error "test failed: shouldn't reach here") 177 handle THM _ => Seq.succeed (Seq.Result st)) (* should reach here *) 178 |> NO_CONTEXT_TACTIC @{context} 179 |> skip_dummy_state 180 end\<close>) 181 oops 182 183 text \<open>Check that we propagate failures from the input methods\<close> 184 lemma "A" 185 apply (fails \<open>time_methods \<open>simp\<close>\<close>) 186 oops 187 188 text \<open>Check that we skip failing methods when skip_fail set\<close> 189 lemma "A \<and> B \<Longrightarrow> A" 190 apply ( 191 ( \<comment> \<open>roughly corresponds to "time_methods (skip_fail) \<open>fail\<close>", 192 but errors if it calls the output callback\<close> 193 tactic \<open> 194 let 195 fun timing_callback _ _ = error "test failed: shouldn't reach here" 196 val methods = [(NONE, SIMPLE_METHOD no_tac)] 197 in 198 (fn st => 199 #2 (Time_Methods.time_methods false true timing_callback methods [] st)) 200 |> NO_CONTEXT_TACTIC @{context} 201 end\<close>) 202 | time_methods (skip_fail) good_simp: \<open>simp\<close>) 203 done 204end 205 206end 207