# HG changeset patch # User blanchet # Date 1591797341 -7200 # Node ID 0c8a9c02830413a0c0d20bdfebb223eaa30fc355 # Parent 35a2ac83a262c2a9bc335223c39c12c0c6be5cd5 simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais) diff -r 35a2ac83a262 -r 0c8a9c028304 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Tue Jun 09 12:13:15 2020 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Wed Jun 10 15:55:41 2020 +0200 @@ -1234,11 +1234,9 @@ \textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs. The collection of methods is roughly the same as for the \textbf{try0} command. -\opsmart{smt\_proofs}{no\_smt\_proofs} +\optrue{smt\_proofs}{no\_smt\_proofs} Specifies whether the \textit{smt} proof method should be tried in addition to -Isabelle's other proof methods. If the option is set to \textit{smart} (the -default), the \textit{smt} method is used for one-line proofs but not in Isar -proofs. +Isabelle's built-in proof methods. \end{enum} diff -r 35a2ac83a262 -r 0c8a9c028304 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Jun 09 12:13:15 2020 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 10 15:55:41 2020 +0200 @@ -68,7 +68,7 @@ ("isar_proofs", "smart"), ("compress", "smart"), ("try0", "true"), - ("smt_proofs", "smart"), + ("smt_proofs", "true"), ("slice", "true"), ("minimize", "true"), ("preplay_timeout", "1")] @@ -267,7 +267,7 @@ val isar_proofs = lookup_option lookup_bool "isar_proofs" val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") val try0 = lookup_bool "try0" - val smt_proofs = lookup_option lookup_bool "smt_proofs" + val smt_proofs = lookup_bool "smt_proofs" val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = lookup_bool "minimize" val timeout = lookup_time "timeout" diff -r 35a2ac83a262 -r 0c8a9c028304 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jun 09 12:13:15 2020 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jun 10 15:55:41 2020 +0200 @@ -19,8 +19,8 @@ bool * (string option * string option) * Time.time * real option * bool * bool * (term, string) atp_step list * thm - val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) -> - int -> one_line_params -> string + val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int -> + one_line_params -> string end; structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = @@ -164,7 +164,7 @@ fun massage_methods (meths as meth :: _) = if not try0 then [meth] - else if smt_proofs = SOME true then SMT_Method :: meths + else if smt_proofs then SMT_Method :: meths else meths val (params, _, concl_t) = strip_subgoal goal subgoal ctxt @@ -461,16 +461,16 @@ (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else "")) end -fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = +fun isar_proof_would_be_a_good_idea (meth, play) = (case play of - Played _ => meth = SMT_Method andalso smt_proofs <> SOME true + Played _ => false | Play_Timed_Out time => time > Time.zeroTime | Play_Failed => true) fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained (one_line_params as ((_, preplay), _, _, _)) = (if isar_proofs = SOME true orelse - (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then + (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params else one_line_proof_text ctxt num_chained) one_line_params diff -r 35a2ac83a262 -r 0c8a9c028304 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Jun 09 12:13:15 2020 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jun 10 15:55:41 2020 +0200 @@ -36,7 +36,7 @@ isar_proofs : bool option, compress : real option, try0 : bool, - smt_proofs : bool option, + smt_proofs : bool, slice : bool, minimize : bool, timeout : Time.time, @@ -121,7 +121,7 @@ isar_proofs : bool option, compress : real option, try0 : bool, - smt_proofs : bool option, + smt_proofs : bool, slice : bool, minimize : bool, timeout : Time.time, @@ -155,7 +155,7 @@ | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" | _ => "Try this") -fun bunches_of_proof_methods try0 smt_method needs_full_types desperate_lam_trans = +fun bunches_of_proof_methods try0 smt_proofs needs_full_types desperate_lam_trans = (if try0 then [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method], [Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]] @@ -171,7 +171,7 @@ [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, SOME desperate_lam_trans), Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @ - (if smt_method then [[SMT_Method]] else []) + (if smt_proofs then [[SMT_Method]] else []) fun is_fact_chained ((_, (sc, _)), _) = sc = Chained diff -r 35a2ac83a262 -r 0c8a9c028304 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Jun 09 12:13:15 2020 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Jun 10 15:55:41 2020 +0200 @@ -362,8 +362,8 @@ val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof val preferred_methss = (Metis_Method (NONE, NONE), - bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types - (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)) + bunches_of_proof_methods try0 smt_proofs needs_full_types + (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)) in (used_facts, preferred_methss, fn preplay => diff -r 35a2ac83a262 -r 0c8a9c028304 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Tue Jun 09 12:13:15 2020 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Wed Jun 10 15:55:41 2020 +0200 @@ -200,10 +200,9 @@ NONE => let val _ = found_proof (); - val smt_method = smt_proofs <> SOME false val preferred_methss = - (if smt_method then SMT_Method else Metis_Method (NONE, NONE), - bunches_of_proof_methods try0 smt_method false liftingN) + (if smt_proofs then SMT_Method else Metis_Method (NONE, NONE), + bunches_of_proof_methods try0 smt_proofs false liftingN) in (preferred_methss, fn preplay => @@ -217,8 +216,7 @@ val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained - one_line_params + proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params end) end | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))