# HG changeset patch # User desharna # Date 1603984061 -3600 # Node ID 4be6ae020fc4faf7b36eb597ec3cc9fdd7165c1d # Parent c2b643c9f2bfac85c41054933d949ee4ecf5d394 Added smt (verit) to Sledgehammer's proof preplay. Tuned preplay multithreading. diff -r c2b643c9f2bf -r 4be6ae020fc4 CONTRIBUTORS --- a/CONTRIBUTORS Thu Oct 29 18:23:29 2020 +0000 +++ b/CONTRIBUTORS Thu Oct 29 16:07:41 2020 +0100 @@ -6,6 +6,9 @@ Contributions to this Isabelle version -------------------------------------- +* October 2020: Jasmin Blanchette, Martin Desharnais, Mathias Fleury + Use veriT in proof preplay in Sledgehammer. + * October 2020: Mathias Fleury Updated proof reconstruction for the SMT solver veriT in the smt method. diff -r c2b643c9f2bf -r 4be6ae020fc4 NEWS --- a/NEWS Thu Oct 29 18:23:29 2020 +0000 +++ b/NEWS Thu Oct 29 16:07:41 2020 +0100 @@ -166,6 +166,10 @@ are in working order again, as opposed to outputting "GaveUp" on nearly all problems. +* Sledgehammer: + - Use veriT in proof preplay. + - Take adventage of more cores in proof preplay. + *** FOL *** diff -r c2b643c9f2bf -r 4be6ae020fc4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 29 18:23:29 2020 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 29 16:07:41 2020 +0100 @@ -160,7 +160,7 @@ fun massage_methods (meths as meth :: _) = if not try0 then [meth] - else if smt_proofs then SMT_Method :: meths + else if smt_proofs then SMT_Method SMT_Default :: meths else meths val (params, _, concl_t) = strip_subgoal goal subgoal ctxt diff -r c2b643c9f2bf -r 4be6ae020fc4 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Oct 29 18:23:29 2020 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Oct 29 16:07:41 2020 +0100 @@ -57,13 +57,15 @@ else let val y = f timeout x in (case get_time y of - SOME time => next_timeout := time + SOME time => next_timeout := time_min (time, !next_timeout) | _ => ()); SOME y end end in - map_filter I (Par_List.map apply_f xs) + chop_groups (Multithreading.max_threads ()) xs + |> map (map_filter I o Par_List.map apply_f) + |> flat end fun enrich_context_with_local_facts proof ctxt = diff -r c2b643c9f2bf -r 4be6ae020fc4 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Oct 29 18:23:29 2020 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Oct 29 16:07:41 2020 +0100 @@ -9,10 +9,14 @@ sig type stature = ATP_Problem_Generate.stature + datatype SMT_backend = + SMT_Default | + SMT_Verit of string + datatype proof_method = Metis_Method of string option * string option | Meson_Method | - SMT_Method | + SMT_Method of SMT_backend | SATx_Method | Blast_Method | Simp_Method | @@ -48,10 +52,14 @@ open ATP_Problem_Generate open ATP_Proof_Reconstruct +datatype SMT_backend = + SMT_Default | + SMT_Verit of string + datatype proof_method = Metis_Method of string option * string option | Meson_Method | - SMT_Method | + SMT_Method of SMT_backend | SATx_Method | Blast_Method | Simp_Method | @@ -73,7 +81,7 @@ fun is_proof_method_direct (Metis_Method _) = true | is_proof_method_direct Meson_Method = true - | is_proof_method_direct SMT_Method = true + | is_proof_method_direct (SMT_Method _) = true | is_proof_method_direct Simp_Method = true | is_proof_method_direct _ = false @@ -93,7 +101,9 @@ | Metis_Method (type_enc_opt, lam_trans_opt) => "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" | Meson_Method => "meson" - | SMT_Method => "smt" + | SMT_Method SMT_Default => "smt" + | SMT_Method (SMT_Verit strategy) => + "smt (" ^ commas ("verit" :: (if strategy = "default" then [] else [strategy])) ^ ")" | SATx_Method => "satx" | Blast_Method => "blast" | Simp_Method => if null ss then "simp" else "simp add:" @@ -109,34 +119,41 @@ end fun tac_of_proof_method ctxt (local_facts, global_facts) meth = - (case meth of - Metis_Method (type_enc_opt, lam_trans_opt) => - let - val ctxt = ctxt - |> Config.put Metis_Tactic.verbose false - |> Config.put Metis_Tactic.trace false - in - SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt), - global_facts) ctxt local_facts) - end - | SMT_Method => SMT_Solver.smt_tac ctxt (local_facts @ global_facts) - | _ => - Method.insert_tac ctxt local_facts THEN' + let + fun tac_of_metis (type_enc_opt, lam_trans_opt) = + let + val ctxt = ctxt + |> Config.put Metis_Tactic.verbose false + |> Config.put Metis_Tactic.trace false + in + SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt), + global_facts) ctxt local_facts) + end + + fun tac_of_smt SMT_Default = SMT_Solver.smt_tac + | tac_of_smt (SMT_Verit strategy) = Verit_Proof.verit_tac_stgy strategy + in (case meth of - Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts - | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) + Metis_Method options => tac_of_metis options + | SMT_Method backend => tac_of_smt backend ctxt (local_facts @ global_facts) | _ => - Method.insert_tac ctxt global_facts THEN' + Method.insert_tac ctxt local_facts THEN' (case meth of - SATx_Method => SAT.satx_tac ctxt - | Blast_Method => blast_tac ctxt - | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt) - | Fastforce_Method => Clasimp.fast_force_tac ctxt - | Force_Method => Clasimp.force_tac ctxt - | Moura_Method => moura_tac ctxt - | Linarith_Method => Lin_Arith.tac ctxt - | Presburger_Method => Cooper.tac true [] [] ctxt - | Algebra_Method => Groebner.algebra_tac [] [] ctxt))) + Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts + | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) + | _ => + Method.insert_tac ctxt global_facts THEN' + (case meth of + SATx_Method => SAT.satx_tac ctxt + | Blast_Method => blast_tac ctxt + | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt) + | Fastforce_Method => Clasimp.fast_force_tac ctxt + | Force_Method => Clasimp.force_tac ctxt + | Moura_Method => moura_tac ctxt + | Linarith_Method => Lin_Arith.tac ctxt + | Presburger_Method => Cooper.tac true [] [] ctxt + | Algebra_Method => Groebner.algebra_tac [] [] ctxt))) + end fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) | string_of_play_outcome (Play_Timed_Out time) = @@ -158,7 +175,7 @@ | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n (* FIXME *) -fun proof_method_command ctxt meth i n used_chaineds _(*num_chained*) extras = +fun proof_method_command meth i n used_chaineds _(*num_chained*) extras = let val (indirect_ss, direct_ss) = if is_proof_method_direct meth then @@ -177,11 +194,11 @@ (s |> s <> "" ? enclose " (" ")") end -fun one_line_proof_text ctxt num_chained +fun one_line_proof_text _ num_chained ((used_facts, (meth, play)), banner, subgoal, subgoal_count) = let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in map fst extra - |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained + |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained |> (if play = Play_Failed then prefix "One-line proof reconstruction failed: " else try_command_line banner play) end diff -r c2b643c9f2bf -r 4be6ae020fc4 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Oct 29 18:23:29 2020 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Oct 29 16:07:41 2020 +0100 @@ -67,7 +67,8 @@ val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string val is_atp : theory -> string -> bool - val bunches_of_proof_methods : bool -> bool -> bool -> string -> proof_method list list + val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string -> + proof_method list list val is_fact_chained : (('a * stature) * 'b) -> bool val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list @@ -155,23 +156,35 @@ | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" | _ => "Try this") -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]] - else - []) @ - [[Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE)], - (if needs_full_types then - [Metis_Method (NONE, NONE), - Metis_Method (SOME really_full_type_enc, NONE), - Metis_Method (SOME full_typesN, SOME desperate_lam_trans), - Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] - else - [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_proofs then [[SMT_Method]] else []) +fun bunches_of_proof_methods ctxt try0 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 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 smt_methodss = + if smt_proofs then + [SMT_Method SMT_Default :: + map (fn strategy => SMT_Method (SMT_Verit strategy)) + (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))] + else + [] + in + try0_methodss @ [metis_methods] @ smt_methodss + end fun is_fact_chained ((_, (sc, _)), _) = sc = Chained diff -r c2b643c9f2bf -r 4be6ae020fc4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Oct 29 18:23:29 2020 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Oct 29 16:07:41 2020 +0100 @@ -360,7 +360,7 @@ 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 needs_full_types + bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)) in (used_facts, preferred_methss, diff -r c2b643c9f2bf -r 4be6ae020fc4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Oct 29 18:23:29 2020 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Oct 29 16:07:41 2020 +0100 @@ -200,11 +200,14 @@ NONE => let val _ = found_proof (); - val preferred_methss = - (if smt_proofs then SMT_Method else Metis_Method (NONE, NONE), - bunches_of_proof_methods try0 smt_proofs false liftingN) + val preferred = + if smt_proofs then + SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Default) + else + Metis_Method (NONE, NONE); + val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN; in - (preferred_methss, + ((preferred, methss), fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () diff -r c2b643c9f2bf -r 4be6ae020fc4 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Oct 29 18:23:29 2020 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Oct 29 16:07:41 2020 +0100 @@ -14,6 +14,7 @@ val simplify_spaces : string -> string val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b val time_mult : real -> Time.time -> Time.time + val time_min : Time.time * Time.time -> Time.time val parse_bool_option : bool -> string -> string -> bool option val parse_time : string -> string -> Time.time val subgoal_count : Proof.state -> int @@ -49,6 +50,7 @@ |> Exn.release fun time_mult k t = Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t))) +fun time_min (x, y) = if x < y then x else y fun parse_bool_option option name s = (case s of