1(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML 2 Author: Philipp Meyer, TU Muenchen 3 Author: Jasmin Blanchette, TU Muenchen 4 5Minimization of fact list for Metis using external provers. 6*) 7 8signature SLEDGEHAMMER_PROVER_MINIMIZE = 9sig 10 type stature = ATP_Problem_Generate.stature 11 type proof_method = Sledgehammer_Proof_Methods.proof_method 12 type play_outcome = Sledgehammer_Proof_Methods.play_outcome 13 type mode = Sledgehammer_Prover.mode 14 type params = Sledgehammer_Prover.params 15 type prover = Sledgehammer_Prover.prover 16 17 val is_prover_supported : Proof.context -> string -> bool 18 val is_prover_installed : Proof.context -> string -> bool 19 val default_max_facts_of_prover : Proof.context -> string -> int 20 val get_prover : Proof.context -> mode -> string -> prover 21 22 val binary_min_facts : int Config.T 23 val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int -> 24 Proof.state -> thm -> ((string * stature) * thm list) list -> 25 ((string * stature) * thm list) list option 26 * ((unit -> (string * stature) list * (proof_method * play_outcome)) -> string) 27 val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover 28end; 29 30structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE = 31struct 32 33open ATP_Util 34open ATP_Proof 35open ATP_Problem_Generate 36open ATP_Proof_Reconstruct 37open ATP_Systems 38open Sledgehammer_Util 39open Sledgehammer_Fact 40open Sledgehammer_Proof_Methods 41open Sledgehammer_Isar 42open Sledgehammer_Prover 43open Sledgehammer_Prover_ATP 44open Sledgehammer_Prover_SMT 45 46fun is_prover_supported ctxt = 47 let val thy = Proof_Context.theory_of ctxt in 48 is_atp thy orf is_smt_prover ctxt 49 end 50 51fun is_prover_installed ctxt = 52 is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) 53 54fun default_max_facts_of_prover ctxt name = 55 let val thy = Proof_Context.theory_of ctxt in 56 if is_atp thy name then 57 fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0 58 else if is_smt_prover ctxt name then 59 SMT_Solver.default_max_relevant ctxt name 60 else 61 error ("No such prover: " ^ name) 62 end 63 64fun get_prover ctxt mode name = 65 let val thy = Proof_Context.theory_of ctxt in 66 if is_atp thy name then run_atp mode name 67 else if is_smt_prover ctxt name then run_smt_solver mode name 68 else error ("No such prover: " ^ name) 69 end 70 71(* wrapper for calling external prover *) 72 73fun n_facts names = 74 let val n = length names in 75 string_of_int n ^ " fact" ^ plural_s n ^ 76 (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "") 77 end 78 79fun print silent f = if silent then () else writeln (f ()) 80 81fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, 82 type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, 83 minimize, preplay_timeout, ...} : params) 84 silent (prover : prover) timeout i n state goal facts = 85 let 86 val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ 87 (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") 88 89 val facts = facts |> maps (fn (n, ths) => map (pair n) ths) 90 val params = 91 {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, 92 type_enc = type_enc, strict = strict, lam_trans = lam_trans, 93 uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, 94 max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), 95 max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, 96 isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, 97 slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, 98 expect = ""} 99 val problem = 100 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, 101 factss = [("", facts)], found_proof = I} 102 val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, 103 message} = 104 prover params problem 105 val result as {outcome, ...} = 106 if is_none outcome0 andalso 107 forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then 108 result0 109 else 110 {outcome = SOME MaybeUnprovable, used_facts = [], used_from = used_from, 111 preferred_methss = preferred_methss, run_time = run_time, message = message} 112 in 113 print silent (fn () => 114 (case outcome of 115 SOME failure => string_of_atp_failure failure 116 | NONE => 117 "Found proof" ^ 118 (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^ 119 " (" ^ string_of_time run_time ^ ")")); 120 result 121 end 122 123(* minimalization of facts *) 124 125(* Give the external prover some slack. The ATP gets further slack because the 126 Sledgehammer preprocessing time is included in the estimate below but isn't 127 part of the timeout. *) 128val slack_msecs = 200 129 130fun new_timeout timeout run_time = 131 Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs) 132 |> Time.fromMilliseconds 133 134(* The linear algorithm usually outperforms the binary algorithm when over 60% 135 of the facts are actually needed. The binary algorithm is much more 136 appropriate for provers that cannot return the list of used facts and hence 137 returns all facts as used. Since we cannot know in advance how many facts are 138 actually needed, we heuristically set the threshold to 10 facts. *) 139val binary_min_facts = 140 Attrib.setup_config_int \<^binding>\<open>sledgehammer_minimize_binary_min_facts\<close> (K 20) 141 142fun linear_minimize test timeout result xs = 143 let 144 fun min _ [] p = p 145 | min timeout (x :: xs) (seen, result) = 146 (case test timeout (xs @ seen) of 147 result as {outcome = NONE, used_facts, run_time, ...} : prover_result => 148 min (new_timeout timeout run_time) (filter_used_facts true used_facts xs) 149 (filter_used_facts false used_facts seen, result) 150 | _ => min timeout xs (x :: seen, result)) 151 in 152 min timeout xs ([], result) 153 end 154 155fun binary_minimize test timeout result xs = 156 let 157 fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) = 158 let 159 val (l0, r0) = chop (length xs div 2) xs 160(* 161 val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup)) 162 val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs)) 163 val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0)) 164 val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0)) 165*) 166 val depth = depth + 1 167 val timeout = new_timeout timeout run_time 168 in 169 (case test timeout (sup @ l0) of 170 result as {outcome = NONE, used_facts, ...} => 171 min depth result (filter_used_facts true used_facts sup) 172 (filter_used_facts true used_facts l0) 173 | _ => 174 (case test timeout (sup @ r0) of 175 result as {outcome = NONE, used_facts, ...} => 176 min depth result (filter_used_facts true used_facts sup) 177 (filter_used_facts true used_facts r0) 178 | _ => 179 let 180 val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 181 val (sup, r0) = (sup, r0) |> apply2 (filter_used_facts true (map fst sup_r0)) 182 val (sup_l, (r, result)) = min depth result (sup @ l) r0 183 val sup = sup |> filter_used_facts true (map fst sup_l) 184 in (sup, (l @ r, result)) end)) 185 end 186(* 187 |> tap (fn _ => warning (replicate_string depth " " ^ "}")) 188*) 189 | min _ result sup xs = (sup, (xs, result)) 190 in 191 (case snd (min 0 result [] xs) of 192 ([x], result as {run_time, ...}) => 193 (case test (new_timeout timeout run_time) [] of 194 result as {outcome = NONE, ...} => ([], result) 195 | _ => ([x], result)) 196 | p => p) 197 end 198 199fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal 200 facts = 201 let 202 val ctxt = Proof.context_of state 203 val prover = get_prover ctxt Minimize prover_name 204 val (chained, non_chained) = List.partition is_fact_chained facts 205 206 fun test timeout non_chained = 207 test_facts params silent prover timeout i n state goal (chained @ non_chained) 208 in 209 (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name); 210 (case test timeout non_chained of 211 result as {outcome = NONE, used_facts, run_time, ...} => 212 let 213 val non_chained = filter_used_facts true used_facts non_chained 214 val min = 215 if length non_chained >= Config.get ctxt binary_min_facts then binary_minimize 216 else linear_minimize 217 val (min_facts, {message, ...}) = 218 min test (new_timeout timeout run_time) result non_chained 219 val min_facts_and_chained = chained @ min_facts 220 in 221 print silent (fn () => cat_lines 222 ["Minimized to " ^ n_facts (map fst min_facts)] ^ 223 (case length chained of 224 0 => "" 225 | n => " (plus " ^ string_of_int n ^ " chained)")); 226 (if learn then do_learn (maps snd min_facts_and_chained) else ()); 227 (SOME min_facts_and_chained, message) 228 end 229 | {outcome = SOME TimedOut, ...} => 230 (NONE, fn _ => 231 "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ 232 \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")") 233 | {message, ...} => (NONE, (prefix "Prover error: " o message)))) 234 handle ERROR msg => (NONE, fn _ => "Error: " ^ msg) 235 end 236 237fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...}) 238 ({state, goal, subgoal, subgoal_count, ...} : prover_problem) 239 (result as {outcome, used_facts, used_from, preferred_methss, run_time, message} 240 : prover_result) = 241 if is_some outcome then 242 result 243 else 244 let 245 val (used_facts, message) = 246 if minimize then 247 minimize_facts do_learn name params 248 (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state 249 goal (filter_used_facts true used_facts (map (apsnd single) used_from)) 250 |>> Option.map (map fst) 251 else 252 (SOME used_facts, message) 253 in 254 (case used_facts of 255 SOME used_facts => 256 {outcome = NONE, used_facts = sort_by fst used_facts, used_from = used_from, 257 preferred_methss = preferred_methss, run_time = run_time, message = message} 258 | NONE => result) 259 end 260 261fun get_minimizing_prover ctxt mode do_learn name params problem = 262 get_prover ctxt mode name params problem 263 |> maybe_minimize mode do_learn name params problem 264 265end; 266