# HG changeset patch # User nipkow # Date 1252531594 -7200 # Node ID 338ccfd37f674ad3a5b87a36992f5092c9c9ac5b # Parent b4119bbb2b79ae63d2c83d8085b93c2100a48c92 minimization: comparing w/ and w/o. diff -r b4119bbb2b79 -r 338ccfd37f67 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 09 12:29:06 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 09 23:26:34 2009 +0200 @@ -1,5 +1,5 @@ (* Title: mirabelle_sledgehammer.ML - Author: Jasmin Blanchette and Sascha Boehme + Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow *) structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = @@ -8,7 +8,6 @@ val proverK = "prover" val prover_timeoutK = "prover_timeout" val keepK = "keep" -val metisK = "metis" val full_typesK = "full_types" val minimizeK = "minimize" val minimize_timeoutK = "minimize_timeout" @@ -20,69 +19,84 @@ val separator = "-----" -datatype data = Data of { - sh_calls: int, - sh_success: int, - sh_time_isa: int, - sh_time_atp: int, - sh_time_atp_fail: int, - metis_calls: int, - metis_success: int, - metis_time: int, - metis_timeout: int } +datatype sh_data = ShData of { + calls: int, + success: int, + time_isa: int, + time_atp: int, + time_atp_fail: int} + +datatype me_data = MeData of { + calls: int, + success: int, + time: int, + timeout: int } + -fun make_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, - metis_time, metis_timeout) = - Data {sh_calls=sh_calls, sh_success=sh_success, sh_time_isa=sh_time_isa, - sh_time_atp=sh_time_atp, sh_time_atp_fail=sh_time_atp_fail, - metis_calls=metis_calls, metis_success=metis_success, - metis_time=metis_time, metis_timeout=metis_timeout} +(* 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 + +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 map_data f (Data {sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, - metis_success, metis_time, metis_timeout}) = - make_data (f (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, - metis_time, metis_timeout)) +fun make_me_data (metis_calls, metis_success, metis_time, metis_timeout) = + MeData{calls=metis_calls, success=metis_success, + time=metis_time, timeout=metis_timeout} + +val empty_data = Data(make_sh_data (0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0), make_me_data(0, 0, 0, 0)) -val empty_data = make_data (0, 0, 0, 0, 0, 0, 0, 0, 0) +fun map_sh_data f + (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, meda)) = + Data (make_sh_data (f (calls, success, time_isa, time_atp, time_atp_fail)), + meda0, meda) -val inc_sh_calls = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, - metis_success, metis_time, metis_timeout) => (sh_calls + 1, sh_success, - sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout)) +fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout}, meda)) = + Data(shda, make_me_data(f (calls,success,time,timeout)), meda) -val inc_sh_success = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, - metis_success, metis_time, metis_timeout) => (sh_calls, sh_success + 1, - sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout)) +fun map_me_data f (Data (shda, meda0, MeData{calls,success,time,timeout})) = + Data(shda, meda0, make_me_data(f (calls,success,time,timeout))) -fun inc_sh_time_isa t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, - metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, - sh_time_isa + t, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout)) +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)) + +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)) -fun inc_sh_time_atp t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, - metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, - sh_time_isa, sh_time_atp + t, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout)) +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)) + +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)) -fun inc_sh_time_atp_fail t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, - metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, - sh_time_isa, sh_time_atp, sh_time_atp_fail + t, metis_calls, metis_success, metis_time, metis_timeout)) +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)) + +val inc_metis_calls = map_me_data (fn (metis_calls, metis_success, metis_time, metis_timeout) + => (metis_calls + 1, metis_success, metis_time, metis_timeout)) -val inc_metis_calls = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, - metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, - sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls + 1, metis_success, metis_time, metis_timeout)) +val inc_metis_success = map_me_data (fn (metis_calls, metis_success, metis_time, metis_timeout) + => (metis_calls, metis_success + 1, metis_time, metis_timeout)) -val inc_metis_success = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, - metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, - sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success + 1, metis_time, - metis_timeout)) +fun inc_metis_time t = map_me_data (fn (metis_calls, metis_success, metis_time, metis_timeout) + => (metis_calls, metis_success, metis_time + t, metis_timeout)) + +val inc_metis_timeout = map_me_data (fn (metis_calls, metis_success, metis_time, metis_timeout) + => (metis_calls, metis_success, metis_time, metis_timeout + 1)) -fun inc_metis_time t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, - metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, - sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time + t, - metis_timeout)) +val inc_metis_calls0 = map_me_data0 (fn (metis_calls, metis_success, metis_time, metis_timeout) + => (metis_calls + 1, metis_success, metis_time, metis_timeout)) + +val inc_metis_success0 = map_me_data0 (fn (metis_calls, metis_success, metis_time, metis_timeout) + => (metis_calls, metis_success + 1, metis_time, metis_timeout)) -val inc_metis_timeout = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, - metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, - sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time, - metis_timeout + 1)) +fun inc_metis_time0 t = map_me_data0 (fn (metis_calls, metis_success, metis_time, metis_timeout) + => (metis_calls, metis_success, metis_time + t, metis_timeout)) + +val inc_metis_timeout0 = map_me_data0 (fn (metis_calls, metis_success, metis_time, metis_timeout) + => (metis_calls, metis_success, metis_time, metis_timeout + 1)) local @@ -109,12 +123,12 @@ str3 (avg_time sh_time_atp_fail (sh_calls - sh_success))) ) -fun log_metis_data log sh_calls sh_success metis_calls metis_success metis_time +fun log_metis_data log tag 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: " ^ + (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls); + log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success); + log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout); + log ("Number of " ^ tag ^ "metis exceptions: " ^ str (sh_success - metis_success - metis_timeout)); log ("Success rate: " ^ percentage metis_success sh_calls ^ "%"); log ("Total time for successful metis calls: " ^ str3 (time metis_time)); @@ -123,15 +137,22 @@ in -fun log_data id log (Data {sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, - metis_success, metis_time, metis_timeout}) = +fun log_data id log (Data (ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa, 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}, MeData{calls=metis_calls, + success=metis_success, time=metis_time, timeout=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_isa sh_time_atp sh_time_atp_fail; log ""; - if metis_calls > 0 then log_metis_data log sh_calls sh_success metis_calls - metis_success metis_time metis_timeout else ()) + if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls + metis_success metis_time metis_timeout else (); + log ""; + if metis_calls0 > 0 + then log_metis_data log "unminimized " sh_calls sh_success metis_calls0 + metis_success0 metis_time0 metis_timeout0 + else () + ) else () end @@ -258,7 +279,7 @@ end -fun run_metis args named_thms id {pre=st, timeout, log, ...} = +fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout) args named_thms id {pre=st, timeout, log, ...} = let fun metis thms ctxt = MetisTools.metis_tac ctxt thms fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st @@ -279,9 +300,10 @@ |> log o prefix (metis_tag id) end - fun sledgehammer_action args id (st as {log, ...}) = let + val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout) + val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0, inc_metis_timeout0) val named_thms = ref (NONE : (string * thm list) list option) fun if_enabled k f = @@ -290,14 +312,17 @@ val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st val _ = if_enabled minimizeK - (Mirabelle.catch minimize_tag (run_minimize args named_thms)) - val _ = if_enabled metisK - (Mirabelle.catch metis_tag (run_metis args (these (!named_thms)))) + (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 is_some (!named_thms) + then Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st + else () in () end fun invoke args = let - val args = (metisK,"yes") :: args; (* always enable metis *) val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK) in Mirabelle.register (init, sledgehammer_action args, done) end