# HG changeset patch # User nipkow # Date 1252949448 -7200 # Node ID d4bb776874b83f520b16b10f4ba89a81abf3cf28 # Parent 8df26038caa9d9a35ae5ab38d2d73fba7f3aff4a count number of iterations required for minimization (and fixed bug: minimization was always called) diff -r 8df26038caa9 -r d4bb776874b8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 14 12:25:02 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 14 19:30:48 2009 +0200 @@ -35,52 +35,72 @@ posns: Position.T list } +datatype min_data = MinData of { + calls: int, + ratios: int + } (* The first me_data component is only used if "minimize" is on. Then it records how metis behaves with un-minimized lemmas. *) -datatype data = Data of sh_data * me_data * me_data +datatype data = Data of sh_data * me_data * min_data * me_data fun make_sh_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) = ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa, time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail} +fun make_min_data (calls, ratios) = + MinData{calls=calls, ratios=ratios} + fun make_me_data (calls, success, time, timeout, lemmas, posns) = MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns} -val empty_data = Data(make_sh_data (0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0, 0, []), - make_me_data(0, 0, 0, 0, 0, [])) +val empty_data = + Data(make_sh_data (0, 0, 0, 0, 0), + make_me_data(0, 0, 0, 0, 0, []), + MinData{calls=0, ratios=0}, + make_me_data(0, 0, 0, 0, 0, [])) fun map_sh_data f - (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, meda)) = + (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) = Data (make_sh_data (f (calls, success, time_isa, time_atp, time_atp_fail)), - meda0, meda) + meda0, minda, meda) -fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, meda)) = - Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), meda) +fun map_min_data f + (Data(shda, meda0, MinData{calls,ratios}, meda)) = + Data(shda, meda0, make_min_data(f(calls,ratios)), meda) -fun map_me_data f (Data (shda, meda0, MeData{calls,success,time,timeout,lemmas,posns})) = - Data(shda, meda0, make_me_data(f (calls,success,time,timeout,lemmas,posns))) +fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) = + Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda) + +fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,time,timeout,lemmas,posns})) = + Data(shda, meda0, minda, make_me_data(f (calls,success,time,timeout,lemmas,posns))) val inc_sh_calls = - map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) - => (sh_calls + 1, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)) + map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail) + => (calls + 1, success, time_isa, time_atp, time_atp_fail)) val inc_sh_success = - map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) - => (sh_calls, sh_success + 1, sh_time_isa, sh_time_atp, sh_time_atp_fail)) + map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail) + => (calls, success + 1, time_isa, time_atp, time_atp_fail)) fun inc_sh_time_isa t = - map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) - => (sh_calls, sh_success, sh_time_isa + t, sh_time_atp, sh_time_atp_fail)) + map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail) + => (calls, success, time_isa + t, time_atp, time_atp_fail)) fun inc_sh_time_atp t = - map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) - => (sh_calls, sh_success, sh_time_isa, sh_time_atp + t, sh_time_atp_fail)) + map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail) + => (calls, success, time_isa, time_atp + t, time_atp_fail)) fun inc_sh_time_atp_fail t = - map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail) - => (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail + t)) + map_sh_data (fn (calls, success, time_isa, time_atp, time_atp_fail) + => (calls, success, time_isa, time_atp, time_atp_fail + t)) + +val inc_min_calls = + map_min_data (fn (calls, ratios) => (calls + 1, ratios)) + +fun inc_min_ratios n = + map_min_data (fn (calls, ratios) => (calls, ratios + n)) val inc_metis_calls = map_me_data (fn (calls, success, time, timeout, lemmas,posns) @@ -175,6 +195,12 @@ then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns)) else () ) + +fun log_min_data log calls ratios = + (log ("Number of minimizations: " ^ string_of_int calls); + log ("Minimization ratios: " ^ string_of_int ratios) + ) + in fun log_data id log (Data @@ -182,7 +208,9 @@ time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}, MeData{calls=metis_calls0, success=metis_success0, time=metis_time0, timeout=metis_timeout0, - lemmas=metis_lemmas0,posns=metis_posns0}, MeData{calls=metis_calls, + lemmas=metis_lemmas0,posns=metis_posns0}, + MinData{calls=min_calls, ratios=min_ratios}, + MeData{calls=metis_calls, success=metis_success, time=metis_time, timeout=metis_timeout, lemmas=metis_lemmas,posns=metis_posns})) = if sh_calls > 0 @@ -194,8 +222,9 @@ metis_success metis_time metis_timeout metis_lemmas metis_posns else (); log ""; if metis_calls0 > 0 - then log_metis_data log "unminimized " sh_calls sh_success metis_calls0 - metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0 + then (log_min_data log min_calls min_ratios; log ""; + log_metis_data log "unminimized " sh_calls sh_success metis_calls0 + metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0) else () ) else () @@ -305,6 +334,7 @@ fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = let + val n0 = length (these (!named_thms)) val (prover_name, prover) = get_atp (Proof.theory_of st) args val minimize = AtpMinimal.minimalize prover prover_name val timeout = @@ -313,14 +343,16 @@ |> the_default 5 val _ = log separator in - (case minimize timeout st (these (!named_thms)) of - (SOME named_thms', msg) => - if length named_thms' = length (these (!named_thms)) - then log (minimize_tag id ^ "already minimal") - else - (named_thms := SOME named_thms'; - log (minimize_tag id ^ "succeeded:\n" ^ msg)) - | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)) + case minimize timeout st (these (!named_thms)) of + (SOME (named_thms',its), msg) => + (change_data id inc_min_calls; + change_data id (inc_min_ratios ((100*its) div n0)); + if length named_thms' = n0 + then log (minimize_tag id ^ "already minimal") + else (named_thms := SOME named_thms'; + log (minimize_tag id ^ "succeeded:\n" ^ msg)) + ) + | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg) end @@ -364,9 +396,8 @@ val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st val _ = if_enabled minimizeK (Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms)))) - val _ = if is_some (!named_thms) - then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st - else () + val _ = if_enabled minimizeK + (Mirabelle.catch minimize_tag (run_minimize args named_thms)) val _ = if is_some (!named_thms) then Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st else () diff -r 8df26038caa9 -r d4bb776874b8 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Sep 14 12:25:02 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Sep 14 19:30:48 2009 +0200 @@ -7,7 +7,7 @@ signature ATP_MINIMAL = sig val minimalize: AtpManager.prover -> string -> int -> Proof.state -> - (string * thm list) list -> (string * thm list) list option * string + (string * thm list) list -> ((string * thm list) list * int) option * string end structure AtpMinimal: ATP_MINIMAL = @@ -69,9 +69,14 @@ forall e in v. ~p(v \ e) *) fun minimal p s = - case min p [] s of - [x] => if p [] then [] else [x] - | m => m + let val c = ref 0 + fun pc xs = (c := !c + 1; p xs) + in + (case min pc [] s of + [x] => if pc [] then [] else [x] + | m => m, + !c) + end end @@ -150,13 +155,14 @@ filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs else name_thms_pairs - val min_thms = if null to_use then [] + val (min_thms, n) = if null to_use then ([], 0) else minimal (test_thms (SOME filtered)) to_use val min_names = order_unique (map fst min_thms) + val _ = println ("Interations: " ^ string_of_int n) val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems") val _ = debug_fn (fn () => print_names min_thms) in - answer' (SOME min_thms) ("Try this command: " ^ + answer' (SOME(min_thms,n)) ("Try this command: " ^ Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")")) end | (Timeout, _) => @@ -167,7 +173,7 @@ | (Failure, _) => answer'' "Failure: No proof with the theorems supplied") handle ResHolClause.TOO_TRIVIAL => - answer' (SOME []) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") + answer' (SOME ([],0)) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") | ERROR msg => answer'' ("Error: " ^ msg) end