# HG changeset patch # User nipkow # Date 1252333472 -7200 # Node ID 9735013cec72ec591b379a0afc25f4a426be6170 # Parent e6996fb0a774c322e81d33940e1f82dbc6c46c34 tuned stats diff -r e6996fb0a774 -r 9735013cec72 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 07 08:32:22 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 07 16:24:32 2009 +0200 @@ -22,54 +22,60 @@ datatype data = Data of { sh_calls: int, sh_success: int, - sh_time: int, + sh_time_isa: int, + sh_time_atp: int, metis_calls: int, metis_success: int, metis_time: int, metis_timeout: int } -fun make_data (sh_calls, sh_success, sh_time, metis_calls, metis_success, +fun make_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout) = - Data {sh_calls=sh_calls, sh_success=sh_success, sh_time=sh_time, + Data {sh_calls=sh_calls, sh_success=sh_success, sh_time_isa=sh_time_isa, + sh_time_atp=sh_time_atp, metis_calls=metis_calls, metis_success=metis_success, metis_time=metis_time, metis_timeout=metis_timeout} -fun map_data f (Data {sh_calls, sh_success, sh_time, metis_calls, +fun map_data f (Data {sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout}) = - make_data (f (sh_calls, sh_success, sh_time, metis_calls, metis_success, + make_data (f (sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout)) -val empty_data = make_data (0, 0, 0, 0, 0, 0, 0) +val empty_data = make_data (0, 0, 0, 0, 0, 0, 0, 0) -val inc_sh_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, +val inc_sh_calls = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls + 1, sh_success, - sh_time, metis_calls, metis_success, metis_time, metis_timeout)) + sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout)) -val inc_sh_success = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, +val inc_sh_success = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, sh_success + 1, - sh_time, metis_calls, metis_success, metis_time, metis_timeout)) + sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout)) -fun inc_sh_time t = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, +fun inc_sh_time_isa t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, - sh_time + t, metis_calls, metis_success, metis_time, metis_timeout)) + sh_time_isa + t, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout)) -val inc_metis_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, +fun inc_sh_time_atp t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, - sh_time, metis_calls + 1, metis_success, metis_time, metis_timeout)) + sh_time_isa, sh_time_atp + t, metis_calls, metis_success, metis_time, metis_timeout)) -val inc_metis_success = map_data (fn (sh_calls, sh_success, sh_time, +val inc_metis_calls = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, + metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, + sh_time_isa, sh_time_atp, metis_calls + 1, metis_success, metis_time, metis_timeout)) + +val inc_metis_success = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, - sh_success, sh_time, metis_calls, metis_success + 1, metis_time, + sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success + 1, metis_time, metis_timeout)) -fun inc_metis_time t = map_data (fn (sh_calls, sh_success, sh_time, +fun inc_metis_time t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, - sh_success, sh_time, metis_calls, metis_success, metis_time + t, + sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time + t, metis_timeout)) -val inc_metis_timeout = map_data (fn (sh_calls, sh_success, sh_time, +val inc_metis_timeout = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, - sh_success, sh_time, metis_calls, metis_success, metis_time, + sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout + 1)) @@ -82,36 +88,40 @@ fun avg_time t n = if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 -fun log_sh_data log sh_calls sh_success sh_time = +fun log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp = (log ("Total number of sledgehammer calls: " ^ str sh_calls); log ("Number of successful sledgehammer calls: " ^ str sh_success); log ("Success rate: " ^ percentage sh_success sh_calls ^ "%"); - log ("Total time for successful sledgehammer calls: " ^ str3 (time sh_time)); - log ("Average time for successful sledgehammer calls: " ^ - str3 (avg_time sh_time sh_success))) + log ("Total time for successful sledgehammer calls (Isabelle): " ^ str3 (time sh_time_isa)); + log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time sh_time_atp)); + log ("Average time for successful sledgehammer calls (Isabelle): " ^ + str3 (avg_time sh_time_isa sh_success)); + log ("Average time for successful sledgehammer calls (ATP): " ^ + str3 (avg_time sh_time_atp sh_success)) + ) -fun log_metis_data log sh_success metis_calls metis_success metis_time +fun log_metis_data log sh_calls sh_success metis_calls metis_success metis_time metis_timeout = (log ("Total number of metis calls: " ^ str metis_calls); log ("Number of successful metis calls: " ^ str metis_success); log ("Number of metis timeouts: " ^ str metis_timeout); log ("Number of metis exceptions: " ^ str (sh_success - metis_success - metis_timeout)); - log ("Success rate: " ^ percentage metis_success sh_success ^ "%"); + log ("Success rate: " ^ percentage metis_success sh_calls ^ "%"); log ("Total time for successful metis calls: " ^ str3 (time metis_time)); log ("Average time for successful metis calls: " ^ str3 (avg_time metis_time metis_success))) in -fun log_data id log (Data {sh_calls, sh_success, sh_time, metis_calls, +fun log_data id log (Data {sh_calls, sh_success, sh_time_isa, sh_time_atp, metis_calls, metis_success, metis_time, metis_timeout}) = if sh_calls > 0 then (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); - log_sh_data log sh_calls sh_success sh_time; + log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp; log ""; - if metis_calls > 0 then log_metis_data log sh_success metis_calls + if metis_calls > 0 then log_metis_data log sh_calls sh_success metis_calls metis_success metis_time metis_timeout else ()) else () @@ -192,7 +202,8 @@ SOME (atp_time, sh_time, names) => let val _ = change_data id inc_sh_success - val _ = change_data id (inc_sh_time (atp_time + sh_time)) + val _ = change_data id (inc_sh_time_isa sh_time) + val _ = change_data id (inc_sh_time_atp atp_time) fun get_thms name = (name, thms_of_name (Proof.context_of st) name) val _ = named_thms := SOME (map get_thms names)