--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 16 10:39:44 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 16 17:24:58 2022 +0200
@@ -110,7 +110,7 @@
comment = ""}
val ress' =
preplay_isar_step ctxt chained timeout [] (mk_step meths)
- |> map (fn result as (meth, play_outcome) =>
+ |> map (fn (meth, play_outcome) =>
(case (minimize, play_outcome) of
(true, Played time) =>
let
@@ -137,8 +137,11 @@
(* Select best method if preplay succeeded *)
(best_meth, best_outcome as Played _, best_used_facts) :: _ =>
(best_used_facts, (best_meth, best_outcome))
- (* Otherwise select preferred method with dummy timeout *)
- | _ => (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)))
+ (* Otherwise select preferred method *)
+ | (fst_meth, fst_outcome, _) :: _ =>
+ (used_facts, (preferred_meth,
+ if fst_meth = preferred_meth then fst_outcome else Play_Timed_Out Time.zeroTime))
+ | [] => (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)))
|> apfst (filter_out (fn (_, (sc, _)) => sc = Chained))
fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 16 10:39:44 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 16 17:24:58 2022 +0200
@@ -162,7 +162,7 @@
fun massage_methods (meths as meth :: _) =
if not try0 then [meth]
- else if smt_proofs then SMT_Method SMT_Z3 :: meths
+ else if smt_proofs then insert (op =) (SMT_Method SMT_Z3) meths
else meths
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Aug 16 10:39:44 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Aug 16 17:24:58 2022 +0200
@@ -84,8 +84,7 @@
val overlord_file_location_of_prover : string -> string * string
val proof_banner : mode -> string -> string
val is_atp : string -> bool
- val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string ->
- proof_method list list
+ val bunches_of_proof_methods : Proof.context -> bool -> bool -> string -> proof_method list list
val facts_of_filter : string -> (string * fact list) list -> fact list
val facts_of_basic_slice : base_slice -> (string * fact list) list -> fact list
val is_fact_chained : (('a * stature) * 'b) -> bool
@@ -205,24 +204,20 @@
| Try => "Sledgehammer (" ^ prover_name ^ ") found a proof: "
| _ => "Try this: ")
-fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans =
+fun bunches_of_proof_methods ctxt smt_proofs needs_full_types desperate_lam_trans =
let
- val try0_methodss =
- if try0 then
- [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
- Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]]
- else
- []
+ val misc_methodss =
+ [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
+ Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]]
- val metis_methods =
- (if try0 then [] else [Metis_Method (NONE, NONE)]) @
- Metis_Method (SOME full_typesN, NONE) ::
- Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) ::
- (if needs_full_types then
- [Metis_Method (SOME really_full_type_enc, NONE),
- Metis_Method (SOME full_typesN, SOME desperate_lam_trans)]
- else
- [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)])
+ val metis_methodss =
+ [Metis_Method (SOME full_typesN, NONE) ::
+ Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) ::
+ (if needs_full_types then
+ [Metis_Method (SOME really_full_type_enc, NONE),
+ Metis_Method (SOME full_typesN, SOME desperate_lam_trans)]
+ else
+ [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)])]
val smt_methodss =
if smt_proofs then
@@ -231,7 +226,7 @@
else
[]
in
- try0_methodss @ [metis_methods] @ smt_methodss
+ misc_methodss @ metis_methodss @ smt_methodss
end
fun facts_of_filter fact_filter factss =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Aug 16 10:39:44 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Aug 16 17:24:58 2022 +0200
@@ -291,10 +291,14 @@
let
val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof)
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
+ val preferred = Metis_Method (NONE, NONE)
val preferred_methss =
- (Metis_Method (NONE, NONE),
- bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types
- (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN))
+ (preferred,
+ if try0 then
+ bunches_of_proof_methods ctxt smt_proofs needs_full_types
+ (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN)
+ else
+ [[preferred]])
in
(used_facts, preferred_methss,
fn preplay =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Tue Aug 16 10:39:44 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Tue Aug 16 17:24:58 2022 +0200
@@ -145,7 +145,11 @@
SMT_Method (if name = "z3" then SMT_Z3 else SMT_Verit "default")
else
Metis_Method (NONE, NONE);
- val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN;
+ val methss =
+ if try0 then
+ bunches_of_proof_methods ctxt smt_proofs false liftingN
+ else
+ [[preferred]]
in
((preferred, methss),
fn preplay =>