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