blanchet@39232: (* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize.ML immler@31037: Author: Philipp Meyer, TU Muenchen blanchet@36370: Author: Jasmin Blanchette, TU Muenchen immler@31037: blanchet@41223: Minimization of fact list for Metis using external provers. immler@31037: *) immler@31037: blanchet@39232: signature SLEDGEHAMMER_MINIMIZE = boehmes@32525: sig blanchet@43926: type locality = ATP_Translate.locality blanchet@43926: type play = ATP_Reconstruct.play blanchet@41335: type params = Sledgehammer_Provers.params blanchet@35867: blanchet@43517: val binary_min_facts : int Config.T blanchet@40242: val minimize_facts : blanchet@43905: string -> params -> bool -> int -> int -> Proof.state blanchet@41339: -> ((string * locality) * thm list) list blanchet@43893: -> ((string * locality) * thm list) list option blanchet@44102: * ((unit -> play) * (play -> string) * string) blanchet@39240: val run_minimize : blanchet@39240: params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit blanchet@35866: end; boehmes@32525: blanchet@39232: structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = immler@31037: struct immler@31037: blanchet@43926: open ATP_Util blanchet@39736: open ATP_Proof blanchet@43926: open ATP_Translate blanchet@43926: open ATP_Reconstruct blanchet@36140: open Sledgehammer_Util blanchet@39232: open Sledgehammer_Filter blanchet@41335: open Sledgehammer_Provers nipkow@33492: blanchet@36370: (* wrapper for calling external prover *) wenzelm@31236: blanchet@40242: fun n_facts names = blanchet@38937: let val n = length names in blanchet@40242: string_of_int n ^ " fact" ^ plural_s n ^ blanchet@38338: (if n > 0 then blanchet@46227: ": " ^ (names |> map fst |> sort_distinct string_ord blanchet@46227: |> space_implode " ") blanchet@38338: else blanchet@38338: "") blanchet@38338: end blanchet@38338: blanchet@41339: fun print silent f = if silent then () else Output.urgent_message (f ()) blanchet@41339: blanchet@43589: fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, blanchet@46385: max_new_mono_instances, type_enc, lam_trans, isar_proof, blanchet@43856: isar_shrink_factor, preplay_timeout, ...} : params) blanchet@43905: silent (prover : prover) timeout i n state facts = wenzelm@31236: let blanchet@41525: val _ = blanchet@41525: print silent (fn () => blanchet@41525: "Testing " ^ n_facts (map fst facts) ^ blanchet@41525: (if verbose then " (timeout: " ^ string_from_time timeout ^ ")" blanchet@43926: else "") ^ "...") blanchet@42613: val {goal, ...} = Proof.goal state blanchet@45320: val facts = blanchet@45320: facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) blanchet@38346: val params = blanchet@42915: {debug = debug, verbose = verbose, overlord = overlord, blocking = true, blanchet@44493: provers = provers, type_enc = type_enc, sound = true, blanchet@46385: lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01), blanchet@46385: max_relevant = SOME (length facts), max_mono_iters = max_mono_iters, blanchet@43605: max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, blanchet@43605: isar_shrink_factor = isar_shrink_factor, slicing = false, blanchet@43856: timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} blanchet@40246: val problem = blanchet@40246: {state = state, goal = goal, subgoal = i, subgoal_count = n, blanchet@42612: facts = facts, smt_filter = NONE} blanchet@46231: val result as {outcome, used_facts, run_time, ...} = blanchet@43892: prover params (K (K "")) problem blanchet@36223: in blanchet@44100: print silent blanchet@44100: (fn () => blanchet@44100: case outcome of blanchet@44100: SOME failure => string_for_failure failure blanchet@44100: | NONE => blanchet@44100: "Found proof" ^ blanchet@44100: (if length used_facts = length facts then "" blanchet@46231: else " with " ^ n_facts used_facts) ^ blanchet@46231: " (" ^ string_from_time run_time ^ ")."); blanchet@38338: result blanchet@36223: end wenzelm@31236: blanchet@40445: (* minimalization of facts *) wenzelm@31236: blanchet@46233: (* Give the external prover some slack. The ATP gets further slack because the blanchet@46233: Sledgehammer preprocessing time is included in the estimate below but isn't blanchet@46233: part of the timeout. *) blanchet@46233: val slack_msecs = 200 blanchet@46233: blanchet@46233: fun new_timeout timeout run_time = blanchet@46233: Int.min (Time.toMilliseconds timeout, blanchet@46233: Time.toMilliseconds run_time + slack_msecs) blanchet@46233: |> Time.fromMilliseconds blanchet@46233: blanchet@46228: (* The linear algorithm usually outperforms the binary algorithm when over 60% blanchet@46228: of the facts are actually needed. The binary algorithm is much more blanchet@46228: appropriate for provers that cannot return the list of used facts and hence blanchet@46228: returns all facts as used. Since we cannot know in advance how many facts are blanchet@46228: actually needed, we heuristically set the threshold to 10 facts. *) blanchet@43517: val binary_min_facts = blanchet@43517: Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts} blanchet@46229: (K 20) blanchet@41223: blanchet@46229: fun linear_minimize test timeout result xs = blanchet@46229: let blanchet@46229: fun min _ [] p = p blanchet@46229: | min timeout (x :: xs) (seen, result) = blanchet@46229: case test timeout (xs @ seen) of blanchet@46233: result as {outcome = NONE, used_facts, run_time, ...} blanchet@46233: : prover_result => blanchet@46233: min (new_timeout timeout run_time) (filter_used_facts used_facts xs) blanchet@46233: (filter_used_facts used_facts seen, result) blanchet@46229: | _ => min timeout xs (x :: seen, result) blanchet@46229: in min timeout xs ([], result) end blanchet@38249: blanchet@46229: fun binary_minimize test timeout result xs = blanchet@41223: let blanchet@46233: fun min depth (result as {run_time, ...} : prover_result) sup blanchet@46233: (xs as _ :: _ :: _) = blanchet@42614: let blanchet@46228: val (l0, r0) = chop (length xs div 2) xs blanchet@42614: (* blanchet@46227: val _ = warning (replicate_string depth " " ^ "{ " ^ blanchet@46227: "sup: " ^ n_facts (map fst sup)) blanchet@46227: val _ = warning (replicate_string depth " " ^ " " ^ blanchet@46227: "xs: " ^ n_facts (map fst xs)) blanchet@46227: val _ = warning (replicate_string depth " " ^ " " ^ blanchet@46227: "l0: " ^ n_facts (map fst l0)) blanchet@46227: val _ = warning (replicate_string depth " " ^ " " ^ blanchet@46227: "r0: " ^ n_facts (map fst r0)) blanchet@42614: *) blanchet@46228: val depth = depth + 1 blanchet@46233: val timeout = new_timeout timeout run_time blanchet@42614: in blanchet@46229: case test timeout (sup @ l0) of blanchet@46233: result as {outcome = NONE, used_facts, ...} => blanchet@46228: min depth result (filter_used_facts used_facts sup) blanchet@46228: (filter_used_facts used_facts l0) blanchet@46228: | _ => blanchet@46229: case test timeout (sup @ r0) of blanchet@46228: result as {outcome = NONE, used_facts, ...} => blanchet@46228: min depth result (filter_used_facts used_facts sup) blanchet@46228: (filter_used_facts used_facts r0) blanchet@46228: | _ => blanchet@46228: let blanchet@46228: val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 blanchet@46228: val (sup, r0) = blanchet@46228: (sup, r0) |> pairself (filter_used_facts (map fst sup_r0)) blanchet@46228: val (sup_l, (r, result)) = min depth result (sup @ l) r0 blanchet@46228: val sup = sup |> filter_used_facts (map fst sup_l) blanchet@46228: in (sup, (l @ r, result)) end blanchet@41223: end blanchet@42614: (* blanchet@42614: |> tap (fn _ => warning (replicate_string depth " " ^ "}")) blanchet@42614: *) blanchet@46228: | min _ result sup xs = (sup, (xs, result)) blanchet@46228: in blanchet@46228: case snd (min 0 result [] xs) of blanchet@46233: ([x], result as {run_time, ...}) => blanchet@46233: (case test (new_timeout timeout run_time) [] of blanchet@46228: result as {outcome = NONE, ...} => ([], result) blanchet@46228: | _ => ([x], result)) blanchet@46228: | p => p blanchet@46228: end blanchet@41223: blanchet@43905: fun minimize_facts prover_name (params as {timeout, ...}) silent i n state blanchet@43905: facts = wenzelm@31236: let blanchet@41189: val ctxt = Proof.context_of state blanchet@43862: val prover = get_prover ctxt Minimize prover_name blanchet@43899: val _ = print silent (fn () => "Sledgehammer minimizer: " ^ blanchet@41223: quote prover_name ^ ".") blanchet@46229: fun test timeout = test_facts params silent prover timeout i n state wenzelm@31236: in blanchet@46229: (case test timeout facts of blanchet@46232: result as {outcome = NONE, used_facts, run_time, ...} => blanchet@38249: let blanchet@41223: val facts = filter_used_facts used_facts facts blanchet@46233: val min = blanchet@46229: if length facts >= Config.get ctxt binary_min_facts then blanchet@46229: binary_minimize blanchet@46229: else blanchet@46229: linear_minimize blanchet@44439: val (min_facts, {preplay, message, message_tail, ...}) = blanchet@46232: min test (new_timeout timeout run_time) result facts blanchet@41339: val _ = print silent (fn () => cat_lines blanchet@44497: ["Minimized to " ^ n_facts (map fst min_facts)] ^ blanchet@44439: (case length (filter (curry (op =) Chained o snd o fst) min_facts) of blanchet@38937: 0 => "" blanchet@44439: | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".") blanchet@44439: in (SOME min_facts, (preplay, message, message_tail)) end blanchet@43893: | {outcome = SOME TimedOut, preplay, ...} => blanchet@43893: (NONE, blanchet@43893: (preplay, blanchet@43893: fn _ => "Timeout: You can increase the time limit using the \ blanchet@43893: \\"timeout\" option (e.g., \"timeout = " ^ blanchet@46232: string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ blanchet@46232: "\").", blanchet@44102: "")) blanchet@43893: | {preplay, message, ...} => blanchet@44102: (NONE, (preplay, prefix "Prover error: " o message, ""))) blanchet@44007: handle ERROR msg => blanchet@44102: (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg, "")) immler@31037: end immler@31037: blanchet@41513: fun run_minimize (params as {provers, ...}) i refs state = blanchet@38291: let blanchet@38291: val ctxt = Proof.context_of state blanchet@38935: val reserved = reserved_isar_keyword_table () blanchet@43884: val chained_ths = normalize_chained_theorems (#facts (Proof.goal state)) blanchet@40445: val facts = blanchet@41339: refs blanchet@41339: |> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths) blanchet@38291: in blanchet@38291: case subgoal_count state of wenzelm@40392: 0 => Output.urgent_message "No subgoal!" blanchet@41513: | n => case provers of blanchet@41513: [] => error "No prover is set." blanchet@41513: | prover :: _ => blanchet@41513: (kill_provers (); blanchet@43905: minimize_facts prover params false i n state facts blanchet@44102: |> (fn (_, (preplay, message, message_tail)) => blanchet@44102: message (preplay ()) ^ message_tail blanchet@44102: |> Output.urgent_message)) blanchet@38291: end blanchet@38291: blanchet@35866: end;