# HG changeset patch # User blanchet # Date 1406897037 -7200 # Node ID e1b2442dc629825b1e0fabc1ce62859b6c96342c # Parent d99080b7f961373ba76bb9653e4a1d4cd4eb9b7c simplified minimization logic diff -r d99080b7f961 -r e1b2442dc629 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Aug 01 14:43:57 2014 +0200 @@ -318,8 +318,6 @@ (* Sledgehammer the given subgoal *) -val default_minimize_prover = metisN - fun is_raw_param_relevant_for_minimize (name, _) = not (member (op =) params_not_for_minimize name) fun string_of_raw_param (key, values) = @@ -338,7 +336,7 @@ more_override_params |> filter is_raw_param_relevant_for_minimize |> map nice_string_of_raw_param - |> (if prover_name = default_minimize_prover then I else cons prover_name) + |> cons prover_name |> space_implode ", " in sledgehammerN ^ " " ^ minN ^ (if params = "" then "" else enclose " [" "]" params) ^ @@ -365,8 +363,7 @@ let val ctxt = ctxt |> Config.put instantiate_inducts false val i = the_default 1 opt_i - val params = - get_params Minimize thy (("provers", [default_minimize_prover]) :: override_params) + val params = get_params Minimize thy override_params val goal = prop_of (#goal (Proof.goal state)) val facts = nearly_all_facts ctxt false fact_override Symtab.empty Termtab.empty [] [] goal val learn = mash_learn_proof ctxt params goal facts diff -r d99080b7f961 -r e1b2442dc629 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Aug 01 14:43:57 2014 +0200 @@ -12,6 +12,7 @@ type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step + val minimized_isar_step : Proof.context -> Time.time -> isar_step -> Time.time * isar_step val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref -> isar_step -> isar_step val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> diff -r d99080b7f961 -r e1b2442dc629 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200 @@ -68,11 +68,8 @@ val SledgehammerN : string val str_of_mode : mode -> string - val smtN : string val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string - val extract_proof_method : params -> proof_method -> string * (string * string list) list - val is_proof_method : string -> bool val is_atp : theory -> string -> bool val bunch_of_proof_methods : bool -> bool -> string -> proof_method list val is_fact_chained : (('a * stature) * 'b) -> bool @@ -80,9 +77,6 @@ ((''a * stature) * 'b) list val play_one_line_proof : mode -> Time.time -> ((string * 'a) * thm) list -> Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome - val isar_supported_prover_of : theory -> string -> string - val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) -> - string -> proof_method * play_outcome -> 'a val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> Proof.context @@ -120,11 +114,6 @@ | str_of_mode Auto_Minimize = "Auto_Minimize" | str_of_mode Minimize = "Minimize" -val smtN = "smt" - -val proof_method_names = [metisN, smtN] -val is_proof_method = member (op =) proof_method_names - val is_atp = member (op =) o supported_atps type params = @@ -197,17 +186,6 @@ Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @ (if smt_proofs then [SMT2_Method] else []) -fun extract_proof_method ({type_enc, lam_trans, ...} : params) - (Metis_Method (type_enc', lam_trans')) = - let - val override_params = - (if is_none type_enc' andalso is_none type_enc then [] - else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @ - (if is_none lam_trans' andalso is_none lam_trans then [] - else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])]) - in (metisN, override_params) end - | extract_proof_method _ SMT2_Method = (smtN, []) - fun preplay_methods timeout facts meths state i = let val {context = ctxt, facts = chained, goal} = Proof.goal state @@ -242,26 +220,6 @@ end end -val canonical_isar_supported_prover = eN -val z3N = "z3" - -fun isar_supported_prover_of thy name = - if is_atp thy name orelse name = z3N then name - else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover - else name - -(* FIXME: See the analogous logic in the function "maybe_minimize" in - "sledgehammer_prover_minimize.ML". *) -fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay = - let - val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy - val (min_name, override_params) = - (case preplay of - (meth as Metis_Method _, Played _) => - if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth - | _ => (maybe_isar_name, [])) - in minimize_command override_params min_name end - val max_fact_instances = 10 (* FUDGE *) fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = @@ -274,7 +232,6 @@ let val thy = Proof_Context.theory_of ctxt val (remote_provers, local_provers) = - proof_method_names @ sort_strings (supported_atps thy) @ sort_strings (SMT2_Config.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) diff -r d99080b7f961 -r e1b2442dc629 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200 @@ -132,9 +132,9 @@ val atp_important_message_keep_quotient = 25 fun run_atp mode name - (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, - fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, - smt_proofs, slice, minimize, timeout, preplay_timeout, ...}) + ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter, + max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, + slice, minimize, timeout, preplay_timeout, ...} : params) minimize_command ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let @@ -391,8 +391,7 @@ end val one_line_params = - (preplay, proof_banner mode name, used_facts, - choose_minimize_command thy params minimize_command name preplay, subgoal, + (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in diff -r d99080b7f961 -r e1b2442dc629 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Aug 01 14:43:57 2014 +0200 @@ -48,59 +48,17 @@ open Sledgehammer_Prover_ATP open Sledgehammer_Prover_SMT2 -fun run_proof_method mode name (params as {timeout, type_enc, lam_trans, ...}) - minimize_command - ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) = - let - val meth = - if name = metisN then Metis_Method (type_enc, lam_trans) - else if name = smtN then SMT2_Method - else raise Fail ("unknown proof_method: " ^ quote name) - val used_facts = facts |> map fst - in - (case play_one_line_proof (if mode = Minimize then Normal else mode) timeout facts state subgoal - meth [meth] of - play as (_, Played time) => - {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time, - preplay = Lazy.value play, - message = fn play => - let - val ctxt = Proof.context_of state - val (_, override_params) = extract_proof_method params meth - val one_line_params = - (play, proof_banner mode name, used_facts, minimize_command override_params name, - subgoal, subgoal_count) - val num_chained = length (#facts (Proof.goal state)) - in - one_line_proof_text ctxt num_chained one_line_params - end, - message_tail = ""} - | play => - let - val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut) - in - {outcome = SOME failure, used_facts = [], used_from = [], - run_time = Time.zeroTime, preplay = Lazy.value play, - message = fn _ => string_of_atp_failure failure, message_tail = ""} - end) - end - fun is_prover_supported ctxt = let val thy = Proof_Context.theory_of ctxt in - is_proof_method orf is_atp thy orf is_smt2_prover ctxt + is_atp thy orf is_smt2_prover ctxt end fun is_prover_installed ctxt = - is_proof_method orf is_smt2_prover ctxt orf - is_atp_installed (Proof_Context.theory_of ctxt) - -val proof_method_default_max_facts = 20 + is_smt2_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) fun default_max_facts_of_prover ctxt name = let val thy = Proof_Context.theory_of ctxt in - if is_proof_method name then - proof_method_default_max_facts - else if is_atp thy name then + if is_atp thy name then fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0 else if is_smt2_prover ctxt name then SMT2_Solver.default_max_relevant ctxt name @@ -110,8 +68,7 @@ fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in - if is_proof_method name then run_proof_method mode name - else if is_atp thy name then run_atp mode name + if is_atp thy name then run_atp mode name else if is_smt2_prover ctxt name then run_smt2_solver mode name else error ("No such prover: " ^ name ^ ".") end @@ -278,30 +235,7 @@ (NONE, (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, "")) end -fun adjust_proof_method_params override_params - ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans, - uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters, - max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, slice, minimize, timeout, - preplay_timeout, expect} : params) = - let - fun lookup_override name default_value = - (case AList.lookup (op =) override_params name of - SOME [s] => SOME s - | _ => default_value) - (* Only those options that proof_methods are interested in are considered here. *) - val type_enc = lookup_override "type_enc" type_enc - val lam_trans = lookup_override "lam_trans" lam_trans - in - {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking, - provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, - uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, - max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, - max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, - compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize, - timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} - end - -fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...}) +fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...}) ({state, goal, subgoal, subgoal_count, ...} : prover_problem) (result as {outcome, used_facts, used_from, run_time, preplay, message, message_tail} : prover_result) = @@ -309,26 +243,9 @@ result else let - val thy = Proof_Context.theory_of ctxt - - val (minimize_name, params) = - if mode = Normal then - (case Lazy.force preplay of - (meth as Metis_Method _, Played _) => - if isar_proofs = SOME true then - (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved - itself. *) - (isar_supported_prover_of thy name, params) - else - extract_proof_method params meth - ||> (fn override_params => adjust_proof_method_params override_params params) - | _ => (name, params)) - else - (name, params) - val (used_facts, (preplay, message, _)) = if minimize then - minimize_facts do_learn minimize_name params + minimize_facts do_learn name params (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state goal (SOME preplay) (filter_used_facts true used_facts (map (apsnd single) used_from)) |>> Option.map (map fst) @@ -344,7 +261,7 @@ fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem = get_prover ctxt mode name params minimize_command problem - |> maybe_minimize ctxt mode do_learn name params problem + |> maybe_minimize mode do_learn name params problem fun run_minimize (params as {provers, ...}) do_learn i refs state = let diff -r d99080b7f961 -r e1b2442dc629 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200 @@ -207,8 +207,7 @@ goal) val one_line_params = - (preplay, proof_banner mode name, used_facts, - choose_minimize_command thy params minimize_command name preplay, subgoal, + (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in