# HG changeset patch # User blanchet # Date 1361289666 -3600 # Node ID c344cf148e8ff023f038c6a9a8567e8949dc873d # Parent c8721406511a0cfce1caeb16cf3c9398f629554c avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs diff -r c8721406511a -r c344cf148e8f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Feb 19 15:37:42 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Feb 19 17:01:06 2013 +0100 @@ -377,7 +377,7 @@ fun learn prover = Sledgehammer_MaSh.mash_learn_proof ctxt params prover (prop_of goal) all_facts in - Sledgehammer_Minimize.get_minimizing_isar_prover ctxt Sledgehammer_Provers.Normal + Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Provers.Normal learn name end @@ -605,7 +605,7 @@ true 1 (Sledgehammer_Util.subgoal_count st) val _ = log separator val (used_facts, (preplay, message, message_tail)) = - minimize st (these (!named_thms)) + minimize st NONE (these (!named_thms)) val msg = message (Lazy.force preplay) ^ message_tail in case used_facts of diff -r c8721406511a -r c344cf148e8f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Feb 19 15:37:42 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Feb 19 17:01:06 2013 +0100 @@ -558,8 +558,8 @@ {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, factss = [("", facts)]} in - get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) - problem + get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K ""))) + problem end val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] diff -r c8721406511a -r c344cf148e8f src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Feb 19 15:37:42 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Feb 19 17:01:06 2013 +0100 @@ -18,10 +18,11 @@ val auto_minimize_max_time : real Config.T val minimize_facts : (string -> thm list -> unit) -> string -> params -> bool -> int -> int - -> Proof.state -> ((string * stature) * thm list) list + -> Proof.state -> play Lazy.lazy option + -> ((string * stature) * thm list) list -> ((string * stature) * thm list) list option * (play Lazy.lazy * (play -> string) * string) - val get_minimizing_isar_prover : + val get_minimizing_prover : Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover val run_minimize : params -> (string -> thm list -> unit) -> int @@ -190,7 +191,7 @@ end fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent - i n state facts = + i n state preplay0 facts = let val ctxt = Proof.context_of state val prover = @@ -221,7 +222,12 @@ 0 => "" | n => "\n(including " ^ string_of_int n ^ " chained)") ^ "."); (if learn then do_learn prover_name (maps snd min_facts) else ()); - (SOME min_facts, (preplay, message, message_tail)) + (SOME min_facts, + (if is_some preplay0 andalso length min_facts = length facts then + the preplay0 + else + preplay, + message, message_tail)) end | {outcome = SOME TimedOut, preplay, ...} => (NONE, @@ -291,7 +297,7 @@ ((prover_fast_enough (), (name, params)), preplay) else (case Lazy.force preplay of - Played (reconstr, timeout) => + Played (reconstr as Metis _, timeout) => if can_min_fast_enough timeout then (true, extract_reconstructor params reconstr ||> (fn override_params => @@ -299,6 +305,10 @@ override_params params)) else (prover_fast_enough (), (name, params)) + | Played (SMT, timeout) => + (* Cheat: assume the original prover is as fast as "smt" for + the goal it proved itself *) + (can_min_fast_enough timeout, (name, params)) | _ => (prover_fast_enough (), (name, params)), preplay) end @@ -309,6 +319,7 @@ if minimize then minimize_facts do_learn minimize_name params (mode <> Normal orelse not verbose) subgoal subgoal_count state + (SOME preplay) (filter_used_facts true used_facts (map (apsnd single) used_from)) |>> Option.map (map fst) else @@ -325,8 +336,8 @@ (* TODO: implement *) fun maybe_regenerate_isar_proof result = result -fun get_minimizing_isar_prover ctxt mode do_learn name params minimize_command - problem = +fun get_minimizing_prover ctxt mode do_learn name params minimize_command + problem = get_prover ctxt mode name params minimize_command problem |> maybe_minimize ctxt mode do_learn name params problem |> maybe_regenerate_isar_proof @@ -347,7 +358,7 @@ [] => error "No prover is set." | prover :: _ => (kill_provers (); - minimize_facts do_learn prover params false i n state facts + minimize_facts do_learn prover params false i n state NONE facts |> (fn (_, (preplay, message, message_tail)) => message (Lazy.force preplay) ^ message_tail |> Output.urgent_message)) diff -r c8721406511a -r c344cf148e8f src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Feb 19 15:37:42 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Feb 19 17:01:06 2013 +0100 @@ -876,9 +876,15 @@ "" in one_line_proof ^ isar_proof end +fun isar_proof_would_be_a_good_idea preplay = + case preplay of + Played (reconstr, _) => reconstr = SMT + | Trust_Playable _ => false + | Failed_to_Play _ => true + fun proof_text ctxt isar_proofs isar_params num_chained (one_line_params as (preplay, _, _, _, _, _)) = - (if case preplay of Failed_to_Play _ => true | _ => isar_proofs then + (if isar_proofs orelse isar_proof_would_be_a_good_idea preplay then isar_proof_text ctxt isar_proofs isar_params else one_line_proof_text num_chained) one_line_params diff -r c8721406511a -r c344cf148e8f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Feb 19 15:37:42 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Feb 19 17:01:06 2013 +0100 @@ -98,7 +98,7 @@ |> Output.urgent_message fun really_go () = problem - |> get_minimizing_isar_prover ctxt mode learn name params minimize_command + |> get_minimizing_prover ctxt mode learn name params minimize_command |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => print_used_facts used_facts used_from