# HG changeset patch # User blanchet # Date 1306767638 -7200 # Node ID d7075adac3bdf11623f4793bd1efd33a8207023a # Parent 59284a13abc46efb01963b8f82c2197d3bab4c15 minimize with Metis if possible diff -r 59284a13abc4 -r d7075adac3bd 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 @@ -415,7 +415,7 @@ subgoal_count = Sledgehammer_Util.subgoal_count st, facts = facts |> map Sledgehammer_Provers.Untranslated_Fact, smt_filter = NONE} - in prover params (K "") problem end)) () + in prover params (K (K "")) problem end)) () handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut | Fail "inappropriate" => failed ATP_Proof.Inappropriate val time_prover = run_time_in_msecs |> the_default ~1 diff -r 59284a13abc4 -r d7075adac3bd src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 30 17:00:38 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 30 17:00:38 2011 +0200 @@ -40,6 +40,7 @@ Proof.context -> type_system -> int list list -> int -> (string * locality) list vector -> 'a proof -> string list option val uses_typed_helpers : int list -> 'a proof -> bool + val reconstructor_name : reconstructor -> string val one_line_proof_text : one_line_params -> string val isar_proof_text : Proof.context -> isar_params -> one_line_params -> string diff -r 59284a13abc4 -r d7075adac3bd src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 30 17:00:38 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 30 17:00:38 2011 +0200 @@ -309,16 +309,20 @@ (* Sledgehammer the given subgoal *) +val default_minimize_prover = Metis_Tactics.metisN + val is_raw_param_relevant_for_minimize = member (op =) params_for_minimize o fst o unalias_raw_param fun string_for_raw_param (key, values) = key ^ (case implode_param values of "" => "" | value => " = " ^ value) fun minimize_command override_params i prover_name fact_names = - sledgehammerN ^ " " ^ minN ^ " [" ^ prover_name ^ + sledgehammerN ^ " " ^ minN ^ + (if prover_name = default_minimize_prover then "" + else enclose "[" "]" prover_name) ^ (override_params |> filter is_raw_param_relevant_for_minimize |> implode o map (prefix ", " o string_for_raw_param)) ^ - "] (" ^ space_implode " " fact_names ^ ")" ^ + " (" ^ space_implode " " fact_names ^ ")" ^ (if i = 1 then "" else " " ^ string_of_int i) fun hammer_away override_params subcommand opt_i relevance_override state = @@ -335,7 +339,9 @@ |> K () end else if subcommand = minN then - run_minimize (get_params Minimize ctxt override_params) + run_minimize (get_params Minimize ctxt + (("provers", [default_minimize_prover]) :: + override_params)) (the_default 1 opt_i) (#add relevance_override) state else if subcommand = messagesN then messages opt_i diff -r 59284a13abc4 -r d7075adac3bd 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 @@ -76,7 +76,7 @@ {state = state, goal = goal, subgoal = i, subgoal_count = n, facts = facts, smt_filter = NONE} val result as {outcome, used_facts, run_time_in_msecs, ...} = - prover params (K "") problem + prover params (K (K "")) problem in print silent (fn () => case outcome of diff -r 59284a13abc4 -r d7075adac3bd 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 @@ -58,7 +58,8 @@ run_time_in_msecs: int option, message: string} - type prover = params -> minimize_command -> prover_problem -> prover_result + type prover = + params -> (string -> minimize_command) -> prover_problem -> prover_result val smt_triggers : bool Config.T val smt_weights : bool Config.T @@ -318,7 +319,8 @@ used_facts: (string * locality) list, run_time_in_msecs: int option} -type prover = params -> minimize_command -> prover_problem -> prover_result +type prover = + params -> (string -> minimize_command) -> prover_problem -> prover_result (* configuration attributes *) @@ -516,14 +518,26 @@ | _ => type_sys) | format => (format, type_sys)) -fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = +fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = adjust_dumb_type_sys formats type_sys - | determine_format_and_type_sys best_type_systems formats - (Smart_Type_Sys full_types) = + | choose_format_and_type_sys best_type_systems formats + (Smart_Type_Sys full_types) = map type_sys_from_string best_type_systems @ fallback_best_type_systems |> find_first (if full_types then is_type_sys_virtually_sound else K true) |> the |> adjust_dumb_type_sys formats +val metis_minimize_max_time = seconds 2.0 + +fun choose_minimize_command minimize_command name preplay = + (case preplay of + Played (reconstructor, time) => + if Time.<= (time, metis_minimize_max_time) then + reconstructor_name reconstructor + else + name + | _ => name) + |> minimize_command + fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances = Config.put SMT_Config.verbose debug #> Config.put SMT_Config.monomorph_full false @@ -605,8 +619,7 @@ length facts |> is_none max_relevant ? Integer.min best_max_relevant val (format, type_sys) = - determine_format_and_type_sys best_type_systems formats - type_sys + choose_format_and_type_sys best_type_systems formats type_sys val fairly_sound = is_type_sys_fairly_sound type_sys val facts = facts |> not fairly_sound @@ -783,7 +796,8 @@ goal) val one_line_params = (preplay, proof_banner mode blocking name, used_facts, - minimize_command, subgoal, subgoal_count) + choose_minimize_command minimize_command name preplay, + subgoal, subgoal_count) in (proof_text ctxt isar_proof isar_params one_line_params ^ (if verbose then @@ -970,7 +984,8 @@ | _ => Trust_Playable (SMT (smt_settings ()), NONE) val one_line_params = (preplay, proof_banner mode blocking name, used_facts, - minimize_command, subgoal, subgoal_count) + choose_minimize_command minimize_command name preplay, + subgoal, subgoal_count) in one_line_proof_text one_line_params ^ (if verbose then @@ -1002,7 +1017,7 @@ let val one_line_params = (play, proof_banner mode blocking name, used_facts, - minimize_command, subgoal, subgoal_count) + minimize_command name, subgoal, subgoal_count) in {outcome = NONE, used_facts = used_facts, run_time_in_msecs = SOME (Time.toMilliseconds time), diff -r 59284a13abc4 -r d7075adac3bd 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 @@ -128,7 +128,7 @@ smt_filter = smt_filter} fun really_go () = problem - |> get_minimizing_prover ctxt mode name params (minimize_command name) + |> get_minimizing_prover ctxt mode name params minimize_command |> (fn {outcome, message, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN diff -r 59284a13abc4 -r d7075adac3bd src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Mon May 30 17:00:38 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Mon May 30 17:00:38 2011 +0200 @@ -43,7 +43,7 @@ facts = map Sledgehammer_Provers.Untranslated_Fact facts, smt_filter = NONE} in - (case prover params (K "") problem of + (case prover params (K (K "")) problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME | _ => NONE) handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)