# HG changeset patch # User boehmes # Date 1252143957 -7200 # Node ID f20cc66b2c7412e99da6def580fe8cadb51271db # Parent e3c4e337196c5bbd1d529a3a69c72689e0d1d616 added initialization and cleanup of actions, added option to suppress Isabelle output, sledgehammer action produces its own report (no need for additional perl script) diff -r e3c4e337196c -r f20cc66b2c74 src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Sep 04 13:57:56 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sat Sep 05 11:45:57 2009 +0200 @@ -12,8 +12,11 @@ val setup : theory -> theory (* core *) + type init_action + type done_action + type run_action type action - val catch : string -> action -> action + val catch : (int -> string) -> run_action -> run_action val register : action -> theory -> theory val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> unit @@ -47,12 +50,16 @@ (* Mirabelle core *) -type action = {pre: Proof.state, post: Toplevel.state option, + +type init_action = int -> theory -> theory +type done_action = int -> {last: Toplevel.state, log: string -> unit} -> unit +type run_action = int -> {pre: Proof.state, post: Toplevel.state option, timeout: Time.time, log: string -> unit} -> unit +type action = init_action * run_action * done_action structure Actions = TheoryDataFun ( - type T = action list + type T = (int * run_action * done_action) list val empty = [] val copy = I val extend = I @@ -63,11 +70,17 @@ fun app_with f g x = (g x; ()) handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ()) -fun catch tag f (st as {log, ...}) = - let fun log_exn e = log (tag ^ "exception:\n" ^ General.exnMessage e) - in app_with log_exn f st end +fun catch tag f id (st as {log, ...}) = + let fun log_exn e = log (tag id ^ "exception:\n" ^ General.exnMessage e) + in app_with log_exn (f id) st end -val register = Actions.map o cons +fun register (init, run, done) thy = + let val id = length (Actions.get thy) + 1 + in + thy + |> init id + |> Actions.map (cons (id, run, done)) + end local @@ -82,7 +95,7 @@ fun apply_actions thy info (pre, post, time) actions = let fun apply f = f {pre=pre, post=post, timeout=time, log=log thy} - fun run f = (apply f; log_sep thy) + fun run (id, run, _) = (apply (run id); log_sep thy) in (log thy info; log_sep thy; List.app run actions) end fun in_range _ _ NONE = true @@ -94,7 +107,7 @@ in -fun basic_hook tr pre post = +fun run_actions tr pre post = let val thy = Proof.theory_of pre val pos = Toplevel.pos_of tr @@ -108,6 +121,16 @@ only_within_range thy pos (apply_actions thy info st) (Actions.get thy) end +fun done_actions st = + let + val thy = Toplevel.theory_of st + val _ = log thy "\n\n"; + in + thy + |> Actions.get + |> List.app (fn (id, _, done) => done id {last=st, log=log thy}) + end + end val whitelist = ["apply", "by", "proof"] @@ -116,7 +139,9 @@ (* FIXME: might require wrapping into "interruptible" *) if can (Proof.assert_backward o Toplevel.proof_of) pre andalso member (op =) whitelist (Toplevel.name_of tr) - then basic_hook tr (Toplevel.proof_of pre) (SOME post) + then run_actions tr (Toplevel.proof_of pre) (SOME post) + else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post + then done_actions pre else () (* FIXME: add theory_hook here *) diff -r e3c4e337196c -r f20cc66b2c74 src/HOL/Mirabelle/Tools/mirabelle_arith.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Fri Sep 04 13:57:56 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Sat Sep 05 11:45:57 2009 +0200 @@ -5,12 +5,17 @@ structure Mirabelle_Arith : MIRABELLE_ACTION = struct -fun arith_action {pre, timeout, log, ...} = +fun arith_tag id = "#" ^ string_of_int id ^ " arith: " + +fun init _ = I +fun done _ _ = () + +fun run id {pre, timeout, log, ...} = if Mirabelle.can_apply timeout Arith_Data.arith_tac pre - then log "arith: succeeded" + then log (arith_tag id ^ "succeeded") else () - handle TimeLimit.TimeOut => log "arith: timeout" + handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout") -fun invoke _ = Mirabelle.register (Mirabelle.catch "arith: " arith_action) +fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done) end diff -r e3c4e337196c -r f20cc66b2c74 src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 04 13:57:56 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Sat Sep 05 11:45:57 2009 +0200 @@ -5,7 +5,12 @@ structure Mirabelle_Metis : MIRABELLE_ACTION = struct -fun metis_action {pre, post, timeout, log} = +fun metis_tag id = "#" ^ string_of_int id ^ " metis: " + +fun init _ = I +fun done _ _ = () + +fun run id {pre, post, timeout, log} = let val thms = Mirabelle.theorems_of_sucessful_proof post val names = map Thm.get_name thms @@ -16,12 +21,13 @@ fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts) in (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") - |> prefix "metis: " + |> prefix (metis_tag id) |> add_info |> log end - handle TimeLimit.TimeOut => log "metis: timeout" + handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout") + | ERROR msg => log (metis_tag id ^ "error: " ^ msg) -fun invoke _ = Mirabelle.register (Mirabelle.catch "metis: " metis_action) +fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done) end diff -r e3c4e337196c -r f20cc66b2c74 src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Fri Sep 04 13:57:56 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Sat Sep 05 11:45:57 2009 +0200 @@ -5,18 +5,24 @@ structure Mirabelle_Quickcheck : MIRABELLE_ACTION = struct -fun quickcheck_action args {pre, timeout, log, ...} = +fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: " + +fun init _ = I +fun done _ _ = () + +fun run args id {pre, timeout, log, ...} = let val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1 in (case TimeLimit.timeLimit timeout quickcheck pre of - NONE => log "quickcheck: no counterexample" - | SOME _ => log "quickcheck: counterexample found") + NONE => log (qc_tag id ^ "no counterexample") + | SOME _ => log (qc_tag id ^ "counterexample found")) end - handle TimeLimit.TimeOut => log "quickcheck: timeout" + handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout") + | ERROR msg => log (qc_tag id ^ "error: " ^ msg) fun invoke args = - Mirabelle.register (Mirabelle.catch "quickcheck: " (quickcheck_action args)) + Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done) end diff -r e3c4e337196c -r f20cc66b2c74 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Sep 04 13:57:56 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Sep 05 11:45:57 2009 +0200 @@ -5,6 +5,190 @@ structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = struct +val proverK = "prover" +val keepK = "keep" +val metisK = "metis" +val full_typesK = "full_types" + +fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " +fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): " + + +datatype data = Data of { + sh_calls: int, + sh_success: int, + sh_time: 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, + metis_time, metis_timeout) = + Data {sh_calls=sh_calls, sh_success=sh_success, sh_time=sh_time, + 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, + metis_success, metis_time, metis_timeout}) = + make_data (f (sh_calls, sh_success, sh_time, metis_calls, metis_success, + metis_time, metis_timeout)) + +val empty_data = make_data (0, 0, 0, 0, 0, 0, 0) + +val inc_sh_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, + metis_success, metis_time, metis_timeout) => (sh_calls + 1, sh_success, + sh_time, metis_calls, metis_success, metis_time, metis_timeout)) + +val inc_sh_success = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, + metis_success, metis_time, metis_timeout) => (sh_calls, sh_success + 1, + sh_time, metis_calls, metis_success, metis_time, metis_timeout)) + +fun inc_sh_time t = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, + metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, + sh_time + t, metis_calls, metis_success, metis_time, metis_timeout)) + +val inc_metis_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls, + metis_success, metis_time, metis_timeout) => (sh_calls, sh_success, + sh_time, metis_calls + 1, metis_success, metis_time, metis_timeout)) + +val inc_metis_success = map_data (fn (sh_calls, sh_success, sh_time, + metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, + sh_success, sh_time, metis_calls, metis_success + 1, metis_time, + metis_timeout)) + +fun inc_metis_time t = map_data (fn (sh_calls, sh_success, sh_time, + metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, + sh_success, sh_time, metis_calls, metis_success, metis_time + t, + metis_timeout)) + +val inc_metis_timeout = map_data (fn (sh_calls, sh_success, sh_time, + metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls, + sh_success, sh_time, metis_calls, metis_success, metis_time, + metis_timeout + 1)) + + +local + +val str = string_of_int +val str3 = Real.fmt (StringCvt.FIX (SOME 3)) +fun percentage a b = string_of_int (a * 100 div b) +fun time t = Real.fromInt t / 1000.0 +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 = + (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))) + +fun log_metis_data log 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 metis_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, + 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 ""; + if metis_calls > 0 then log_metis_data log sh_success metis_calls + metis_success metis_time metis_timeout else ()) + else () + +end + + +(* Warning: we implicitly assume single-threaded execution here! *) +val data = ref ([] : (int * data) list) + +fun init id thy = (change data (cons (id, empty_data)); thy) +fun done id {log, ...} = + AList.lookup (op =) (!data) id + |> Option.map (log_data id log) + |> K () + +fun change_data id f = (change data (AList.map_entry (op =) id f); ()) + + +local + +fun safe init done f x = + let + val y = init x + val z = Exn.capture f y + val _ = done y + in Exn.release z end + +fun init_sh NONE = !AtpWrapper.destdir + | init_sh (SOME path) = + let + (* Warning: we implicitly assume single-threaded execution here! *) + val old = !AtpWrapper.destdir + val _ = AtpWrapper.destdir := path + in old end + +fun done_sh path = AtpWrapper.destdir := path + +fun run_sh prover_name timeout st _ = + let + val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st)) + val atp_timeout = AtpManager.get_timeout () + val atp = prover atp_timeout NONE NONE prover_name 1 + val ((success, (message, thm_names), time, _, _, _), time') = + TimeLimit.timeLimit timeout (Mirabelle.cpu_time atp) (Proof.get_goal st) + in + if success then (message, SOME (time + time', thm_names)) + else (message, NONE) + end + handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, [])) + | TimeLimit.TimeOut => ("timeout", NONE) + | ERROR msg => ("error: " ^ msg, NONE) + +in + +fun run_sledgehammer args thm_names id {pre=st, timeout, log, ...} = + let + val _ = change_data id inc_sh_calls + val prover_name = + AList.lookup (op =) args proverK + |> the_default (hd (space_explode " " (AtpManager.get_atps ()))) + val dir = AList.lookup (op =) args keepK + val (msg, result) = + safe init_sh done_sh (run_sh prover_name timeout st) dir + val _ = + if is_some result + then + let + val time = fst (the result) + val _ = change_data id inc_sh_success + val _ = change_data id (inc_sh_time time) + in + log (sh_tag id ^ "succeeded (" ^ string_of_int time ^ ") [" ^ + prover_name ^ "]:\n" ^ msg) + end + else log (sh_tag id ^ "failed: " ^ msg) + in change thm_names (K (Option.map snd result)) end + +end + + +local + fun thms_of_name ctxt name = let val lex = OuterKeyword.get_lexicons @@ -18,100 +202,48 @@ |> Source.exhaust end -fun safe init done f x = - let - val y = init x - val z = Exn.capture f y - val _ = done y - in Exn.release z end - -val proverK = "prover" -val keepK = "keep" -val metisK = "metis" -val full_typesK = "full_types" - -val sh_tag = "sledgehammer: " -val metis_tag = "metis (sledgehammer): " - - -local - -fun init NONE = !AtpWrapper.destdir - | init (SOME path) = - let - (* Warning: we implicitly assume single-threaded execution here! *) - val old = !AtpWrapper.destdir - val _ = AtpWrapper.destdir := path - in old end - -fun done path = AtpWrapper.destdir := path - -fun run prover_name timeout st _ = - let - val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st)) - val atp_timeout = AtpManager.get_timeout () - val atp = prover atp_timeout NONE NONE prover_name 1 - val (success, (message, thm_names), time, _, _, _) = - TimeLimit.timeLimit timeout atp (Proof.get_goal st) - in if success then (message, SOME (time, thm_names)) else (message, NONE) end - handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, [])) - | TimeLimit.TimeOut => ("timeout", NONE) - | ERROR msg => ("error: " ^ msg, NONE) - in -fun run_sledgehammer args thm_names {pre=st, timeout, log, ...} = +fun run_metis args thm_names id {pre=st, timeout, log, ...} = let - val prover_name = - AList.lookup (op =) args proverK - |> the_default (hd (space_explode " " (AtpManager.get_atps ()))) - val dir = AList.lookup (op =) args keepK - val (msg, result) = safe init done (run prover_name timeout st) dir - val _ = - if is_some result - then log (sh_tag ^ "succeeded (" ^ string_of_int (fst (the result)) ^ - ") [" ^ prover_name ^ "]:\n" ^ msg) - else log (sh_tag ^ "failed: " ^ msg) - in change thm_names (K (Option.map snd result)) end + fun get_thms ctxt = maps (thms_of_name ctxt) + + fun metis thms ctxt = MetisTools.metis_tac ctxt thms + fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st + + fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" + | with_time (true, t) = (change_data id inc_metis_success; + change_data id (inc_metis_time t); + "succeeded (" ^ string_of_int t ^ ")") + fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms) + handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout") + | ERROR msg => "error: " ^ msg + + val _ = log "-----" + val _ = change_data id inc_metis_calls + in + thm_names + |> get_thms (Proof.context_of st) + |> timed_metis + |> log o prefix (metis_tag id) + end end -fun with_time true t = "succeeded (" ^ string_of_int t ^ ")" - | with_time false t = "failed (" ^ string_of_int t ^ ")" - -fun run_metis args thm_names {pre=st, timeout, log, ...} = - let - fun get_thms ctxt = maps (thms_of_name ctxt) - fun metis thms ctxt = MetisTools.metis_tac ctxt thms - fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st - fun timed_metis thms = - uncurry with_time (Mirabelle.cpu_time apply_metis thms) - handle TimeLimit.TimeOut => "timeout" - | ERROR msg => "error: " ^ msg - fun log_metis s = log (metis_tag ^ s) - in - if not (AList.defined (op =) args metisK) then () - else if is_none (!thm_names) then () - else - log "-----" - |> K (these (!thm_names)) - |> get_thms (Proof.context_of st) - |> timed_metis - |> log_metis - end - - -fun sledgehammer_action args (st as {log, ...}) = +fun sledgehammer_action args id (st as {log, ...}) = let val thm_names = ref (NONE : string list option) - val _ = Mirabelle.catch sh_tag (run_sledgehammer args thm_names) st - val _ = Mirabelle.catch metis_tag (run_metis args thm_names) st - in () end + val _ = Mirabelle.catch sh_tag (run_sledgehammer args thm_names) id st + in + if AList.defined (op =) args metisK andalso is_some (!thm_names) + then Mirabelle.catch metis_tag (run_metis args (these (!thm_names))) id st + else () + end fun invoke args = let val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK) - in Mirabelle.register (sledgehammer_action args) end + in Mirabelle.register (init, sledgehammer_action args, done) end end diff -r e3c4e337196c -r f20cc66b2c74 src/HOL/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Mirabelle/lib/Tools/mirabelle Fri Sep 04 13:57:56 2009 +0200 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Sat Sep 05 11:45:57 2009 +0200 @@ -26,6 +26,7 @@ echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" echo " -O DIR output directory for test data (default $out)" echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" + echo " -q be quiet (suppress output of Isabelle process)" echo echo " Apply the given actions (i.e., automated proof tools)" echo " at all proof steps in the given theory files." @@ -46,7 +47,7 @@ # options -while getopts "L:T:O:t:?" OPT +while getopts "L:T:O:t:q?" OPT do case "$OPT" in L) @@ -61,15 +62,20 @@ t) MIRABELLE_TIMEOUT="$OPTARG" ;; + q) + MIRABELLE_QUIET="true" + ;; \?) usage ;; esac done +export MIRABELLE_QUIET + shift $(($OPTIND - 1)) -ACTIONS="$1" +export MIRABELLE_ACTIONS="$1" shift @@ -83,6 +89,6 @@ for FILE in "$@" do - perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE" + perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" done diff -r e3c4e337196c -r f20cc66b2c74 src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Fri Sep 04 13:57:56 2009 +0200 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Sat Sep 05 11:45:57 2009 +0200 @@ -14,15 +14,15 @@ my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; +my $be_quiet = $ENV{'MIRABELLE_QUIET'}; +my $actions = $ENV{'MIRABELLE_ACTIONS'}; my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; # arguments -my $actions = $ARGV[0]; - -my $thy_file = $ARGV[1]; +my $thy_file = $ARGV[0]; my $start_line = "0"; my $end_line = "~1"; if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { @@ -122,15 +122,17 @@ } close(LOG_FILE); -my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " . - "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n"; - +my $quiet = ""; +if (defined $be_quiet and $be_quiet ne "") { + $quiet = " > /dev/null 2>&1"; +} -# produce report +print "Mirabelle: $thy_file\n" if ($quiet ne ""); -if ($result == 0) { - system "perl -w \"$mirabelle_home/lib/scripts/report.pl\" \"$log_file\""; -} +my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " . + "-e 'use \"$root_file\";' -q $mirabelle_logic" . $quiet; + +print "Finished: $thy_file\n" if ($quiet ne ""); # cleanup diff -r e3c4e337196c -r f20cc66b2c74 src/HOL/Mirabelle/lib/scripts/report.pl --- a/src/HOL/Mirabelle/lib/scripts/report.pl Fri Sep 04 13:57:56 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -# -# Author: Sascha Boehme -# -# Reports for Mirabelle -# - -my $log_file = $ARGV[0]; - -open(FILE, "<$log_file") || die "Cannot open file '$log_file'"; -my @lines = ; -close(FILE); - -my $unhandled = 0; - -my $sh_calls = 0; -my $sh_succeeded = 0; -my $sh_time = 0; - -my $metis_calls = 0; -my $metis_succeeded = 0; -my $metis_timeout = 0; -my $metis_time = 0; - -foreach (@lines) { - if (m/^unhandled exception/) { - $unhandled++; - } - if (m/^sledgehammer:/) { - $sh_calls++; - } - if (m/^sledgehammer: succeeded \(([0-9]+)\)/) { - $sh_succeeded++; - $sh_time += $1; - } - if (m/^metis \(sledgehammer\):/) { - $metis_calls++; - } - if (m/^metis \(sledgehammer\): succeeded \(([0-9]+)\)/) { - $metis_succeeded++; - $metis_time += $1; - } - if (m/^metis \(sledgehammer\): timeout/) { - $metis_timeout++; - } -} - -open(FILE, ">>$log_file") || die "Cannot open file '$log_file'"; - -print FILE "\n\n\n"; - -if ($unhandled > 0) { - print FILE "Number of unhandled exceptions: $unhandled\n\n"; -} - -if ($sh_calls > 0) { - my $percent = $sh_succeeded / $sh_calls * 100; - my $time = $sh_time / 1000; - my $avg_time = $time / $sh_succeeded; - print FILE "Total number of sledgehammer calls: $sh_calls\n"; - print FILE "Number of successful sledgehammer calls: $sh_succeeded\n"; - printf FILE "Success rate: %.0f%%\n", $percent; - printf FILE "Total time for successful sledgehammer calls: %.3f seconds\n", $time; - printf FILE "Average time for successful sledgehammer calls: %.3f seconds\n\n", $avg_time; -} - -if ($metis_calls > 0) { - my $percent = $metis_succeeded / $metis_calls * 100; - my $time = $metis_time / 1000; - my $avg_time = $time / $metis_succeeded; - my $metis_exc = $sh_succeeded - $metis_succeeded - $metis_timeout; - print FILE "Total number of metis calls: $metis_calls\n"; - print FILE "Number of successful metis calls: $metis_succeeded\n"; - print FILE "Number of metis timeouts: $metis_timeout\n"; - print FILE "Number of metis exceptions: $metis_exc\n"; - printf FILE "Success rate: %.0f%%\n", $percent; - printf FILE "Total time for successful metis calls: %.3f seconds\n", $time; - printf FILE "Average time for successful metis calls: %.3f seconds\n", $avg_time; -} - -close(FILE);