# HG changeset patch # User blanchet # Date 1306767638 -7200 # Node ID 8d6a4978cc65b706ca0d7a06ba25ac12acd8c24c # Parent d7075adac3bdf11623f4793bd1efd33a8207023a automatically minimize with Metis when this can be done within a few seconds diff -r d7075adac3bd -r 8d6a4978cc65 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 30 17:00:38 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 30 17:00:38 2011 +0200 @@ -397,9 +397,10 @@ NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) fun failed failure = - ({outcome = SOME failure, message = "", used_facts = [], - run_time_in_msecs = NONE}, ~1) - val ({outcome, message, used_facts, run_time_in_msecs} + ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE, + preplay = K Sledgehammer_ATP_Reconstruct.Failed_to_Play, + message = K ""}, ~1) + val ({outcome, used_facts, run_time_in_msecs, preplay, message} : Sledgehammer_Provers.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (fn () => let @@ -419,10 +420,11 @@ handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut | Fail "inappropriate" => failed ATP_Proof.Inappropriate val time_prover = run_time_in_msecs |> the_default ~1 + val msg = message (preplay ()) in case outcome of - NONE => (message, SH_OK (time_isa, time_prover, used_facts)) - | SOME _ => (message, SH_FAIL (time_isa, time_prover)) + NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) + | SOME _ => (msg, SH_FAIL (time_isa, time_prover)) end handle ERROR msg => ("error: " ^ msg, SH_ERROR) @@ -512,9 +514,11 @@ Sledgehammer_Minimize.minimize_facts prover_name params (SOME explicit_apply) true 1 (Sledgehammer_Util.subgoal_count st) val _ = log separator + val (used_facts, (preplay, message)) = minimize st (these (!named_thms)) + val msg = message (preplay ()) in - case minimize st (these (!named_thms)) of - (SOME named_thms', msg) => + case used_facts of + SOME named_thms' => (change_data id inc_min_succs; change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); if length named_thms' = n0 @@ -523,7 +527,7 @@ named_thms := SOME named_thms'; log (minimize_tag id ^ "succeeded:\n" ^ msg)) ) - | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg) + | NONE => log (minimize_tag id ^ "failed: " ^ msg) end diff -r d7075adac3bd -r 8d6a4978cc65 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 17:00:38 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 30 17:00:38 2011 +0200 @@ -8,13 +8,15 @@ signature SLEDGEHAMMER_MINIMIZE = sig type locality = Sledgehammer_Filter.locality + type play = Sledgehammer_ATP_Reconstruct.play type params = Sledgehammer_Provers.params val binary_min_facts : int Config.T val minimize_facts : string -> params -> bool option -> bool -> int -> int -> Proof.state -> ((string * locality) * thm list) list - -> ((string * locality) * thm list) list option * string + -> ((string * locality) * thm list) list option + * ((unit -> play) * (play -> string)) val run_minimize : params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit end; @@ -25,6 +27,7 @@ open ATP_Proof open Sledgehammer_Util open Sledgehammer_Filter +open Sledgehammer_ATP_Reconstruct open Sledgehammer_Provers (* wrapper for calling external prover *) @@ -171,7 +174,7 @@ Int.min (msecs, Time.toMilliseconds time + slack_msecs) |> Time.fromMilliseconds val facts = filter_used_facts used_facts facts - val (min_thms, {message, ...}) = + val (min_thms, {preplay, message, ...}) = if length facts >= Config.get ctxt binary_min_facts then binary_minimize (do_test new_timeout) facts else @@ -182,13 +185,16 @@ (case length (filter (curry (op =) Chained o snd o fst) min_thms) of 0 => "" | n => " (including " ^ string_of_int n ^ " chained)") ^ ".") - in (SOME min_thms, message) end - | {outcome = SOME TimedOut, ...} => - (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ - \option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ "\").") - | {message, ...} => (NONE, "Prover error: " ^ message)) - handle ERROR msg => (NONE, "Error: " ^ msg) + in (SOME min_thms, (preplay, message)) end + | {outcome = SOME TimedOut, preplay, ...} => + (NONE, + (preplay, + fn _ => "Timeout: You can increase the time limit using the \ + \\"timeout\" option (e.g., \"timeout = " ^ + string_of_int (10 + msecs div 1000) ^ "\").")) + | {preplay, message, ...} => + (NONE, (preplay, prefix "Prover error: " o message))) + handle ERROR msg => (NONE, (K Failed_to_Play, fn _ => "Error: " ^ msg)) end fun run_minimize (params as {provers, ...}) i refs state = @@ -207,7 +213,8 @@ | prover :: _ => (kill_provers (); minimize_facts prover params NONE false i n state facts - |> snd |> Output.urgent_message) + |> (fn (_, (preplay, message)) => + Output.urgent_message (message (preplay ())))) end end; diff -r d7075adac3bd -r 8d6a4978cc65 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 17:00:38 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 17:00:38 2011 +0200 @@ -13,6 +13,7 @@ type relevance_fudge = Sledgehammer_Filter.relevance_fudge type translated_formula = Sledgehammer_ATP_Translate.translated_formula type type_system = Sledgehammer_ATP_Translate.type_system + type play = Sledgehammer_ATP_Reconstruct.play type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command datatype mode = Auto_Try | Try | Normal | Minimize @@ -56,7 +57,8 @@ {outcome: failure option, used_facts: (string * locality) list, run_time_in_msecs: int option, - message: string} + preplay: unit -> play, + message: play -> string} type prover = params -> (string -> minimize_command) -> prover_problem -> prover_result @@ -315,9 +317,10 @@ type prover_result = {outcome: failure option, - message: string, used_facts: (string * locality) list, - run_time_in_msecs: int option} + run_time_in_msecs: int option, + preplay: unit -> play, + message: play -> string} type prover = params -> (string -> minimize_command) -> prover_problem -> prover_result @@ -388,13 +391,11 @@ |> Exn.release |> tap (after path) -fun proof_banner mode blocking name = +fun proof_banner mode name = case mode of Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" - | Normal => if blocking then quote name ^ " found a proof" - else "Try this" - | Minimize => "Try this" + | _ => "Try this" (* based on "Mirabelle.can_apply" and generalized *) fun timed_apply timeout tac state i = @@ -547,8 +548,8 @@ fun run_atp mode name ({exec, required_execs, arguments, proof_delims, known_failures, conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config) - ({debug, verbose, overlord, blocking, type_sys, max_relevant, - max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof, + ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters, + max_new_mono_instances, explicit_apply, isar_proof, isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params) minimize_command ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = @@ -772,50 +773,57 @@ extract_important_message output else "" - val (message, used_facts) = + val (used_facts, preplay, message) = case outcome of NONE => let val used_facts = used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof - val reconstructors = - if uses_typed_helpers typed_helpers atp_proof then [MetisFT, Metis] - else [Metis, MetisFT] - val used_ths = - facts |> map untranslated_fact - |> filter_used_facts used_facts - |> map snd - val preplay = - play_one_line_proof debug preplay_timeout used_ths state subgoal - reconstructors - val full_types = uses_typed_helpers typed_helpers atp_proof - val isar_params = - (debug, full_types, isar_shrink_factor, type_sys, pool, - conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, - goal) - val one_line_params = - (preplay, proof_banner mode blocking name, used_facts, - choose_minimize_command minimize_command name preplay, - subgoal, subgoal_count) in - (proof_text ctxt isar_proof isar_params one_line_params ^ - (if verbose then - "\nATP real CPU time: " ^ - string_from_time (Time.fromMilliseconds (the msecs)) ^ "." - else - "") ^ - (if important_message <> "" then - "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ - important_message - else - ""), - used_facts) + (used_facts, + fn () => + let + val used_ths = + facts |> map untranslated_fact |> filter_used_facts used_facts + |> map snd + val reconstructors = + [Metis, MetisFT] + |> uses_typed_helpers typed_helpers atp_proof ? rev + in + play_one_line_proof debug preplay_timeout used_ths state subgoal + reconstructors + end, + fn preplay => + let + val full_types = uses_typed_helpers typed_helpers atp_proof + val isar_params = + (debug, full_types, isar_shrink_factor, type_sys, pool, + conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, + goal) + val one_line_params = + (preplay, proof_banner mode name, used_facts, + choose_minimize_command minimize_command name preplay, + subgoal, subgoal_count) + in + proof_text ctxt isar_proof isar_params one_line_params ^ + (if verbose then + "\nATP real CPU time: " ^ + string_from_time (Time.fromMilliseconds (the msecs)) ^ "." + else + "") ^ + (if important_message <> "" then + "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ + important_message + else + "") + end) end - | SOME failure => (string_for_failure failure, []) + | SOME failure => + ([], K Failed_to_Play, fn _ => string_for_failure failure) in - {outcome = outcome, message = message, used_facts = used_facts, - run_time_in_msecs = msecs} + {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs, + preplay = preplay, message = message} end (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until @@ -956,8 +964,7 @@ end in do_slice timeout 1 NONE Time.zeroTime end -fun run_smt_solver mode name - (params as {debug, verbose, blocking, preplay_timeout, ...}) +fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command ({state, subgoal, subgoal_count, facts, smt_filter, ...} : prover_problem) = @@ -970,39 +977,43 @@ smt_filter_loop ctxt name params state subgoal smt_filter facts val (used_facts, used_ths) = used_facts |> ListPair.unzip val outcome = outcome |> Option.map failure_from_smt_failure - val message = + val (preplay, message) = case outcome of NONE => - let - fun smt_settings () = - if name = SMT_Solver.solver_name_of ctxt then "" - else "smt_solver = " ^ maybe_quote name - val preplay = - case play_one_line_proof debug preplay_timeout used_ths state - subgoal [Metis, MetisFT] of - p as Played _ => p - | _ => Trust_Playable (SMT (smt_settings ()), NONE) - val one_line_params = - (preplay, proof_banner mode blocking name, used_facts, - choose_minimize_command minimize_command name preplay, - subgoal, subgoal_count) - in - one_line_proof_text one_line_params ^ - (if verbose then - "\nSMT solver real CPU time: " ^ - string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^ - "." - else - "") - end - | SOME failure => string_for_failure failure + (fn () => + let + fun smt_settings () = + if name = SMT_Solver.solver_name_of ctxt then "" + else "smt_solver = " ^ maybe_quote name + in + case play_one_line_proof debug preplay_timeout used_ths state + subgoal [Metis, MetisFT] of + p as Played _ => p + | _ => Trust_Playable (SMT (smt_settings ()), NONE) + end, + fn preplay => + let + val one_line_params = + (preplay, proof_banner mode name, used_facts, + choose_minimize_command minimize_command name preplay, + subgoal, subgoal_count) + in + one_line_proof_text one_line_params ^ + (if verbose then + "\nSMT solver real CPU time: " ^ + string_from_time (Time.fromMilliseconds + (the run_time_in_msecs)) ^ "." + else + "") + end) + | SOME failure => (K Failed_to_Play, fn _ => string_for_failure failure) in {outcome = outcome, used_facts = used_facts, - run_time_in_msecs = run_time_in_msecs, message = message} + run_time_in_msecs = run_time_in_msecs, preplay = preplay, + message = message} end -fun run_metis mode name ({debug, blocking, timeout, ...} : params) - minimize_command +fun run_metis mode name ({debug, timeout, ...} : params) minimize_command ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = let val reconstructor = if name = Metis_Tactics.metisN then Metis @@ -1014,30 +1025,28 @@ case play_one_line_proof debug timeout used_ths state subgoal [reconstructor] of play as Played (_, time) => - let - val one_line_params = - (play, proof_banner mode blocking name, used_facts, - minimize_command name, subgoal, subgoal_count) - in - {outcome = NONE, used_facts = used_facts, - run_time_in_msecs = SOME (Time.toMilliseconds time), - message = one_line_proof_text one_line_params} + {outcome = NONE, used_facts = used_facts, + run_time_in_msecs = SOME (Time.toMilliseconds time), + preplay = K play, + message = fn play => + let + val one_line_params = + (play, proof_banner mode name, used_facts, + minimize_command name, subgoal, subgoal_count) + in one_line_proof_text one_line_params end} + | play => + let val failure = if play = Failed_to_Play then GaveUp else TimedOut in + {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE, + preplay = K play, message = fn _ => string_for_failure failure} end - | play => - {outcome = SOME (if play = Failed_to_Play then GaveUp else TimedOut), - used_facts = [], run_time_in_msecs = NONE, message = ""} end fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in - if is_metis_prover name then - run_metis mode name - else if is_atp thy name then - run_atp mode name (get_atp thy name) - else if is_smt_prover ctxt name then - run_smt_solver mode name - else - error ("No such prover: " ^ name ^ ".") + if is_metis_prover name then run_metis mode name + else if is_atp thy name then run_atp mode name (get_atp thy name) + else if is_smt_prover ctxt name then run_smt_solver mode name + else error ("No such prover: " ^ name ^ ".") end end; diff -r d7075adac3bd -r 8d6a4978cc65 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 30 17:00:38 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 30 17:00:38 2011 +0200 @@ -31,6 +31,7 @@ open Sledgehammer_Util open Sledgehammer_Filter open Sledgehammer_ATP_Translate +open Sledgehammer_ATP_Reconstruct open Sledgehammer_Provers open Sledgehammer_Minimize @@ -67,25 +68,45 @@ Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} (fn generic => Config.get_generic generic binary_min_facts) +val auto_minimize_max_seconds = + Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds} + (K 5.0) + fun get_minimizing_prover ctxt mode name (params as {debug, verbose, explicit_apply, ...}) minimize_command (problem as {state, subgoal, subgoal_count, facts, ...}) = get_prover ctxt mode name params minimize_command problem - |> (fn result as {outcome, used_facts, run_time_in_msecs, message} => + |> (fn result as {outcome, used_facts, run_time_in_msecs, preplay, message} => if is_some outcome then result else let - val (used_facts, message) = - if length used_facts - >= Config.get ctxt auto_minimize_min_facts then - minimize_facts name params (SOME explicit_apply) (not verbose) - subgoal subgoal_count state + val num_facts = length used_facts + val ((minimize, minimize_name), preplay) = + if mode = Normal then + if num_facts >= Config.get ctxt auto_minimize_min_facts then + ((true, name), preplay) + else + let val preplay = preplay () in + (case preplay of + Played (reconstructor, timeout) => + (0.001 * Real.fromInt ((num_facts + 2) + * Time.toMilliseconds timeout) + <= Config.get ctxt auto_minimize_max_seconds, + reconstructor_name reconstructor) + | _ => (false, name), K preplay) + end + else + ((false, name), preplay) + val (used_facts, (preplay, message)) = + if minimize then + minimize_facts minimize_name params (SOME explicit_apply) + (not verbose) subgoal subgoal_count state (filter_used_facts used_facts (map (apsnd single o untranslated_fact) facts)) |>> Option.map (map fst) else - (SOME used_facts, message) + (SOME used_facts, (preplay, message)) in case used_facts of SOME used_facts => @@ -103,7 +124,8 @@ else (); {outcome = NONE, used_facts = used_facts, - run_time_in_msecs = run_time_in_msecs, message = message}) + run_time_in_msecs = run_time_in_msecs, preplay = preplay, + message = message}) | NONE => result end) @@ -129,10 +151,10 @@ fun really_go () = problem |> get_minimizing_prover ctxt mode name params minimize_command - |> (fn {outcome, message, ...} => + |> (fn {outcome, preplay, message, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN - else someN, message)) + else someN, message o preplay)) fun go () = let val (outcome_code, message) = @@ -140,13 +162,13 @@ really_go () else (really_go () - handle ERROR message => (unknownN, "Error: " ^ message ^ "\n") + handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") | exn => if Exn.is_interrupt exn then reraise exn else - (unknownN, "Internal error:\n" ^ - ML_Compiler.exn_message exn ^ "\n")) + (unknownN, fn () => "Internal error:\n" ^ + ML_Compiler.exn_message exn ^ "\n")) val _ = (* The "expect" argument is deliberately ignored if the prover is missing so that the "Metis_Examples" can be processed on any @@ -167,15 +189,15 @@ |> outcome_code = someN ? Proof.goal_message (fn () => [Pretty.str "", - Pretty.mark Markup.hilite (Pretty.str message)] + Pretty.mark Markup.hilite (Pretty.str (message ()))] |> Pretty.chunks)) end else if blocking then let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () in - (if outcome_code = someN then message - else if mode = Normal then quote name ^ ": " ^ message + (if outcome_code = someN then message () + else if mode = Normal then quote name ^ ": " ^ message () else "") |> Async_Manager.break_into_chunks |> List.app Output.urgent_message; @@ -183,7 +205,8 @@ end else (Async_Manager.launch das_tool birth_time death_time (desc ()) - (apfst (curry (op =) someN) o go); + ((fn (outcome_code, message) => + (outcome_code = someN, message ())) o go); (unknownN, state)) end