# HG changeset patch # User blanchet # Date 1406897037 -7200 # Node ID 708347f9bfc63a055d2963f233d652d26a4b596a # Parent f453bbc289fa0057caa4be4cde971804a316b96a removed Mirabelle minimization code diff -r f453bbc289fa -r 708347f9bfc6 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Aug 01 14:43:57 2014 +0200 @@ -15,9 +15,6 @@ val proverK = "prover" (*=NAME: name of the external prover to call*) val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*) val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*) -val minimizeK = "minimize" (*: enable minimization of theorem set found by sledgehammer*) - (*refers to minimization attempted by Mirabelle*) -val minimize_timeoutK = "minimize_timeout" (*=TIME: timeout for each minimization step (seconds of*) val proof_methodK = "proof_method" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*) val metis_ftK = "metis_ft" (*: apply metis with fully-typed encoding to the theorems found by sledgehammer*) @@ -43,7 +40,6 @@ val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*) fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " -fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): " val separator = "-----" @@ -60,7 +56,6 @@ val slice_default = "true" val max_calls_default = "10000000" val trivial_default = "false" -val minimize_timeout_default = 5 (*If a key is present in args then augment a list with its pair*) (*This is used to avoid fixing default values at the Mirabelle level, and @@ -93,11 +88,6 @@ posns: (Position.T * bool) list } -datatype min_data = MinData of { - succs: int, - ab_ratios: int - } - fun make_sh_data (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, time_prover,time_prover_fail) = @@ -106,9 +96,6 @@ time_isa=time_isa, time_prover=time_prover, time_prover_fail=time_prover_fail} -fun make_min_data (succs, ab_ratios) = - MinData{succs=succs, ab_ratios=ab_ratios} - fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, timeout,lemmas,posns) = ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, @@ -116,7 +103,6 @@ timeout=timeout, lemmas=lemmas, posns=posns} val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) -val empty_min_data = make_min_data (0, 0) val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, @@ -124,55 +110,37 @@ time_prover, time_prover_fail}) = (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) -fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios) - fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns) -datatype proof_method_mode = - Unminimized | Minimized | UnminimizedFT | MinimizedFT +datatype proof_method_mode = Unminimized | UnminimizedFT datatype data = Data of { sh: sh_data, - min: min_data, re_u: re_data, (* proof method with unminimized set of lemmas *) - re_m: re_data, (* proof method with minimized set of lemmas *) - re_uft: re_data, (* proof method with unminimized set of lemmas and fully-typed *) - re_mft: re_data, (* proof method with minimized set of lemmas and fully-typed *) - mini: bool (* with minimization *) + re_uft: re_data (* proof method with unminimized set of lemmas and fully-typed *) } -fun make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) = - Data {sh=sh, min=min, re_u=re_u, re_m=re_m, re_uft=re_uft, re_mft=re_mft, - mini=mini} +fun make_data (sh, re_u, re_uft) = Data {sh=sh, re_u=re_u, re_uft=re_uft} -val empty_data = make_data (empty_sh_data, empty_min_data, - empty_re_data, empty_re_data, empty_re_data, empty_re_data, false) - -fun map_sh_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = - let val sh' = make_sh_data (f (tuple_of_sh_data sh)) - in make_data (sh', min, re_u, re_m, re_uft, re_mft, mini) end +val empty_data = make_data (empty_sh_data, empty_re_data, empty_re_data) -fun map_min_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = - let val min' = make_min_data (f (tuple_of_min_data min)) - in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end +fun map_sh_data f (Data {sh, re_u, re_uft}) = + let val sh' = make_sh_data (f (tuple_of_sh_data sh)) + in make_data (sh', re_u, re_uft) end -fun map_re_data f m (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = +fun map_re_data f m (Data {sh, re_u, re_uft}) = let - fun map_me g Unminimized (u, m, uft, mft) = (g u, m, uft, mft) - | map_me g Minimized (u, m, uft, mft) = (u, g m, uft, mft) - | map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft) - | map_me g MinimizedFT (u, m, uft, mft) = (u, m, uft, g mft) + fun map_me g Unminimized (u, uft) = (g u, uft) + | map_me g UnminimizedFT (u, uft) = (u, g uft) val f' = make_re_data o f o tuple_of_re_data - val (re_u', re_m', re_uft', re_mft') = - map_me f' m (re_u, re_m, re_uft, re_mft) - in make_data (sh, min, re_u', re_m', re_uft', re_mft', mini) end + val (re_u', re_uft') = map_me f' m (re_u, re_uft) + in make_data (sh, re_u', re_uft') end -fun set_mini mini (Data {sh, min, re_u, re_m, re_uft, re_mft, ...}) = - make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) +fun set_mini (Data {sh, re_u, re_uft, ...}) = make_data (sh, re_u, re_uft) fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); @@ -212,12 +180,6 @@ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) -val inc_min_succs = map_min_data - (fn (succs,ab_ratios) => (succs+1, ab_ratios)) - -fun inc_min_ab_ratios r = map_min_data - (fn (succs, ab_ratios) => (succs, ab_ratios+r)) - val inc_proof_method_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) @@ -311,14 +273,9 @@ else () ) -fun log_min_data log (succs, ab_ratios) = - (log ("Number of successful minimizations: " ^ string_of_int succs); - log ("After/before ratios: " ^ string_of_int ab_ratios) - ) - in -fun log_data id log (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = +fun log_data id log (Data {sh, re_u, re_uft}) = let val ShData {calls=sh_calls, ...} = sh @@ -333,15 +290,7 @@ (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); log_sh_data log (tuple_of_sh_data sh); log ""; - if not mini - then log_proof_method ("", re_u) ("fully-typed ", re_uft) - else - app_if re_u (fn () => - (log_proof_method ("unminimized ", re_u) ("unminimized fully-typed ", re_uft); - log ""; - app_if re_m (fn () => - (log_min_data log (tuple_of_min_data min); log ""; - log_proof_method ("", re_m) ("fully-typed ", re_mft)))))) + log_proof_method ("", re_u) ("fully-typed ", re_uft)) else () end @@ -573,60 +522,6 @@ end -fun run_minimize args meth named_thms id ({pre = st, log, ...} : Mirabelle.run_args) = - let - val thy = Proof.theory_of st - val {goal, ...} = Proof.goal st - val i = 1 - val preferred_methss = - (Sledgehammer_Proof_Methods.Auto_Method, [[Sledgehammer_Proof_Methods.Auto_Method]]) (* wrong *) - val n0 = length (these (!named_thms)) - val prover_name = get_prover_name thy args - val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default - val strict = AList.lookup (op =) args strictK |> the_default strict_default - val timeout = - AList.lookup (op =) args minimize_timeoutK - |> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *) - |> the_default minimize_timeout_default - val preplay_timeout = AList.lookup (op =) args preplay_timeoutK - |> the_default preplay_timeout_default - val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs" - val sh_minimizeLST = available_parameter args sh_minimizeK "minimize" - val max_new_mono_instancesLST = - available_parameter args max_new_mono_instancesK max_new_mono_instancesK - val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK - val params as {preplay_timeout, ...} = Sledgehammer_Commands.default_params thy - ([("provers", prover_name), - ("verbose", "true"), - ("type_enc", type_enc), - ("strict", strict), - ("timeout", string_of_int timeout), - ("preplay_timeout", preplay_timeout)] - |> isar_proofsLST - |> sh_minimizeLST (*don't confuse the two minimization flags*) - |> max_new_mono_instancesLST - |> max_mono_itersLST) - val minimize = - Sledgehammer_Prover_Minimize.minimize_facts (K ()) prover_name params true 1 - (Sledgehammer_Util.subgoal_count st) - val _ = log separator - val (used_facts, message) = minimize st goal (these (!named_thms)) - val msg = message (fn () => Sledgehammer.play_one_line_proof preplay_timeout - (map fst (these used_facts)) st i preferred_methss) - in - (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 - then log (minimize_tag id ^ "already minimal") - else (meth := proof_method_from_msg args msg; - named_thms := SOME named_thms'; - log (minimize_tag id ^ "succeeded:\n" ^ msg)) - ) - | NONE => log (minimize_tag id ^ "failed: " ^ msg)) - end - fun override_params prover type_enc timeout = [("provers", prover), ("max_facts", "0"), @@ -726,7 +621,6 @@ val meth = Unsynchronized.ref "" val named_thms = Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) - val minimize = AList.defined (op =) args minimizeK val metis_ft = AList.defined (op =) args metis_ftK val trivial = if AList.lookup (op =) args check_trivialK |> the_default trivial_default @@ -747,17 +641,9 @@ (Mirabelle.catch_result (proof_method_tag meth) false (run_proof_method trivial false m1 name meth (these (!named_thms))) id st; ()) in - change_data id (set_mini minimize); + change_data id set_mini; Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st; - if is_some (!named_thms) - then - (apply_method Unminimized UnminimizedFT; - if minimize andalso not (null (these (!named_thms))) - then - (Mirabelle.catch minimize_tag (run_minimize args meth named_thms) id st; - apply_method Minimized MinimizedFT) - else ()) - else () + if is_some (!named_thms) then apply_method Unminimized UnminimizedFT else () end end end