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
--- 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
--- 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}]
--- 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))
--- 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
--- 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