# HG changeset patch # User boehmes # Date 1252180891 -7200 # Node ID ea322e847633bef68360a88c990690cdd39d491a # Parent 9f2784eae302b4bcc36600a56441dcd22010bacd added signature ATP_MINIMAL, fixed AtpMinimal.minimalize for the trivial case, Mirabelle: added an option to minimize a theorem set found by sledgehammer, use timeout of sledgehammer instead of additional timeLimit diff -r 9f2784eae302 -r ea322e847633 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Sep 05 17:35:05 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Sep 05 22:01:31 2009 +0200 @@ -9,10 +9,15 @@ val keepK = "keep" val metisK = "metis" val full_typesK = "full_types" +val minimizeK = "minimize" +val minimize_timeoutK = "minimize_timeout" fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " +fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): " +val separator = "-----" + datatype data = Data of { sh_calls: int, @@ -125,6 +130,11 @@ fun change_data id f = (change data (AList.map_entry (op =) id f); ()) +fun get_atp thy args = + AList.lookup (op =) args proverK + |> the_default (hd (space_explode " " (AtpManager.get_atps ()))) + |> (fn name => (name, the (AtpManager.get_prover name thy))) + local fun safe init done f x = @@ -144,51 +154,18 @@ fun done_sh path = AtpWrapper.destdir := path -fun run_sh prover_name timeout st _ = +fun run_sh (prover_name, prover) 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 atp = prover (Time.toSeconds timeout) NONE NONE prover_name 1 val ((success, (message, thm_names), atp_time, _, _, _), sh_time) = - TimeLimit.timeLimit timeout (Mirabelle.cpu_time atp) (Proof.get_goal st) + Mirabelle.cpu_time atp (Proof.get_goal st) in if success then (message, SOME (atp_time, sh_time, thm_names)) else (message, NONE) end handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, 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 - in - (case result of - 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 thm_names (K (SOME names)) - in - log (sh_tag id ^ "succeeded (" ^ string_of_int atp_time ^ "+" ^ - string_of_int sh_time ^ ") [" ^ prover_name ^ "]:\n" ^ msg) - end - | NONE => log (sh_tag id ^ "failed: " ^ msg)) - end - -end - - -local - fun thms_of_name ctxt name = let val lex = OuterKeyword.get_lexicons @@ -204,10 +181,54 @@ in -fun run_metis args thm_names id {pre=st, timeout, log, ...} = +fun run_sledgehammer args named_thms id {pre=st, timeout, log, ...} = let - fun get_thms ctxt = maps (thms_of_name ctxt) + val _ = change_data id inc_sh_calls + val atp as (prover_name, _) = get_atp (Proof.theory_of st) args + val dir = AList.lookup (op =) args keepK + val (msg, result) = safe init_sh done_sh (run_sh atp timeout st) dir + in + (case result of + 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)) + + fun get_thms name = (name, thms_of_name (Proof.context_of st) name) + val _ = named_thms := SOME (map get_thms names) + in + log (sh_tag id ^ "succeeded (" ^ string_of_int atp_time ^ "+" ^ + string_of_int sh_time ^ ") [" ^ prover_name ^ "]:\n" ^ msg) + end + | NONE => log (sh_tag id ^ "failed: " ^ msg)) + end + +end + +fun run_minimize args named_thms id {pre=st, log, ...} = + let + val (prover_name, prover) = get_atp (Proof.theory_of st) args + val minimize = AtpMinimal.minimalize prover prover_name + val timeout = + AList.lookup (op =) args minimize_timeoutK + |> Option.map (fst o read_int o explode) + |> 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)) + end + + +fun run_metis 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 @@ -219,27 +240,29 @@ handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout") | ERROR msg => "error: " ^ msg - val _ = log "-----" + val _ = log separator val _ = change_data id inc_metis_calls in - thm_names - |> get_thms (Proof.context_of st) + maps snd named_thms |> timed_metis |> log o prefix (metis_tag id) end -end - 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) 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 + val named_thms = ref (NONE : (string * thm list) list option) + + fun if_enabled k f = + if AList.defined (op =) args k andalso is_some (!named_thms) + then f id st else () + + 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)))) + in () end fun invoke args = let diff -r 9f2784eae302 -r ea322e847633 src/HOL/Mirabelle/doc/options.txt --- a/src/HOL/Mirabelle/doc/options.txt Sat Sep 05 17:35:05 2009 +0200 +++ b/src/HOL/Mirabelle/doc/options.txt Sat Sep 05 22:01:31 2009 +0200 @@ -2,5 +2,7 @@ * prover=NAME: name of the external prover to call * keep=PATH: path where to keep temporary files created by sledgehammer + * full_types: enable full-typed encoding + * minimize: enable minimization of theorem set found by sledgehammer + * minimize_timeout: timeout for each minimization step * metis: apply metis with the theorems found by sledgehammer - * full_types: turn on full-typed encoding diff -r 9f2784eae302 -r ea322e847633 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Sat Sep 05 17:35:05 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Sat Sep 05 22:01:31 2009 +0200 @@ -4,7 +4,13 @@ Minimalization of theorem list for metis by using an external automated theorem prover *) -structure AtpMinimal: sig end = +signature ATP_MINIMAL = +sig + val minimalize: AtpManager.prover -> string -> int -> Proof.state -> + (string * thm list) list -> (string * thm list) list option * string +end + +structure AtpMinimal: ATP_MINIMAL = struct (* output control *) @@ -103,8 +109,7 @@ fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs = let val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ") - val name_thm_pairs = - flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) ths) name_thms_pairs) + val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val _ = debug_fn (fn () => print_names name_thm_pairs) val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val (result, proof) = @@ -130,6 +135,7 @@ val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state fun test_thms filtered thms = case test_thms_fun filtered thms of (Success _, _) => true | _ => false + val answer' = pair and answer'' = pair NONE in (* try prove first to check result and get used theorems *) (case test_thms_fun NONE name_thms_pairs of @@ -141,25 +147,26 @@ filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs else name_thms_pairs - val min_thms = (minimal (test_thms (SOME filtered)) to_use) + val min_thms = if null to_use then [] + else minimal (test_thms (SOME filtered)) to_use val min_names = order_unique (map fst min_thms) val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems") val _ = debug_fn (fn () => print_names min_thms) in - answer ("Try this command: " ^ + answer' (SOME min_thms) ("Try this command: " ^ Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")")) end | (Timeout, _) => - answer ("Timeout: You may need to increase the time limit of " ^ + answer'' ("Timeout: You may need to increase the time limit of " ^ Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ") | (Error, msg) => - answer ("Error in prover: " ^ msg) + answer'' ("Error in prover: " ^ msg) | (Failure, _) => - answer "Failure: No proof with the theorems supplied") + answer'' "Failure: No proof with the theorems supplied") handle ResHolClause.TOO_TRIVIAL => - answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") + answer' (SOME []) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") | ERROR msg => - answer ("Error: " ^ msg) + answer'' ("Error: " ^ msg) end @@ -204,8 +211,9 @@ SOME prover => prover | NONE => error ("Unknown prover: " ^ quote prover_name) val name_thms_pairs = get_thms (Proof.context_of state) thm_names + fun print_answer (_, msg) = answer msg in - minimalize prover prover_name time_limit state name_thms_pairs + print_answer (minimalize prover prover_name time_limit state name_thms_pairs) end val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []