# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID 890b70f96fe4da0bd2b6fc06ef36043bfd5766ea # Parent b55d84e41d612ee30aaea75cc9cbdfee9f9b10cb further work on new Sledgehammer slicing diff -r b55d84e41d61 -r 890b70f96fe4 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100 @@ -36,9 +36,6 @@ ML_file \Tools/Sledgehammer/sledgehammer_tactics.ML\ (* -lemma "1 + 1 = 3" - sledgehammer[verbose] - lemma "1 + 1 = 2" sledgehammer [slices = 40, max_proofs = 40] diff -r b55d84e41d61 -r 890b70f96fe4 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100 @@ -259,16 +259,15 @@ (outcome, message) end -fun string_of_facts facts = - "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^ - (facts |> map (fst o fst) |> space_implode " ") +fun string_of_facts filter facts = + "Selected " ^ string_of_int (length facts) ^ " " ^ (if filter = "" then "" else filter ^ " ") ^ + "fact" ^ plural_s (length facts) ^ ": " ^ (space_implode " " (map (fst o fst) facts)) fun string_of_factss factss = if forall (null o snd) factss then "Found no relevant facts" else - cat_lines (map (fn (filter, facts) => - (if filter = "" then "" else filter ^ ": ") ^ string_of_facts facts) factss) + cat_lines (map (fn (filter, facts) => string_of_facts filter facts) factss) val default_slice_schedule = (* FUDGE (based on Seventeen evaluation) *) @@ -278,10 +277,12 @@ fun schedule_of_provers provers num_slices = let - val num_default_slices = length default_slice_schedule val (known_provers, unknown_provers) = List.partition (member (op =) default_slice_schedule) provers + val default_slice_schedule = filter (member (op =) known_provers) default_slice_schedule + val num_default_slices = length default_slice_schedule + fun round_robin _ [] = [] | round_robin 0 _ = [] | round_robin n (prover :: provers) = prover :: round_robin (n - 1) (provers @ [prover]) @@ -293,7 +294,7 @@ @ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers) end -fun prover_slices_of_schedule ctxt schedule = +fun prover_slices_of_schedule ctxt ({max_facts, fact_filter, ...} : params) schedule = let fun triplicate_slices original = let @@ -309,9 +310,21 @@ original @ shifted_once @ shifted_twice end + fun adjust_extra XXX = XXX (* ### FIXME *) + + fun adjust_slice ((num_facts0, fact_filter0), extra) = + ((case max_facts of + NONE => num_facts0 + | SOME max_facts => Int.min (num_facts0, max_facts), + the_default fact_filter0 fact_filter), + Option.map adjust_extra extra) + val provers = distinct (op =) schedule val prover_slices = - map (fn prover => (prover, triplicate_slices (get_slices ctxt prover))) provers + map (fn prover => (prover, + (is_none fact_filter ? triplicate_slices) + (map adjust_slice (get_slices ctxt prover)))) + provers fun translate _ [] = [] | translate prover_slices (prover :: schedule) = @@ -323,6 +336,7 @@ | _ => translate prover_slices schedule) in translate prover_slices schedule + |> distinct (op =) end fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, max_proofs, @@ -375,6 +389,7 @@ fold (fn prover => fold (fn ((n, _), _) => Integer.max n) (get_slices ctxt prover)) provers 0) + * 51 div 50 (* some slack to account for filtering of induction facts below *) val ({elapsed, ...}, factss) = Timing.timing (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t) @@ -406,7 +421,7 @@ provers else schedule_of_provers provers slices - val prover_slices = prover_slices_of_schedule ctxt schedule + val prover_slices = prover_slices_of_schedule ctxt params schedule in if mode = Auto_Try then (SH_Unknown, "") diff -r b55d84e41d61 -r 890b70f96fe4 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Jan 31 16:09:23 2022 +0100 @@ -299,8 +299,8 @@ (* FUDGE *) K [((512, meshN), (format, type_enc, lam_trans, false, e_fun_weightN)), ((1024, meshN), (format, type_enc, lam_trans, false, e_sym_offset_weightN)), - ((91, mepoN), (format, type_enc, lam_trans, false, e_autoN)), - ((1000, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)), + ((128, mepoN), (format, type_enc, lam_trans, false, e_autoN)), + ((724, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)), ((256, mepoN), (format, type_enc, liftingN, false, e_fun_weightN)), ((64, mashN), (format, type_enc, combsN, false, e_fun_weightN))] end, diff -r b55d84e41d61 -r 890b70f96fe4 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Jan 31 16:09:23 2022 +0100 @@ -183,7 +183,7 @@ fun try_command_line banner play command = let val s = string_of_play_outcome play in - banner ^ ": " ^ Active.sendback_markup_command command ^ + banner ^ Active.sendback_markup_command command ^ (s |> s <> "" ? enclose " (" ")") end diff -r b55d84e41d61 -r 890b70f96fe4 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100 @@ -160,8 +160,12 @@ filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false) fun slice_timeout slices timeout = - Time.toReal timeout * Real.fromInt (Multithreading.max_threads ()) / Real.fromInt slices - |> seconds + let + val max_threads = Multithreading.max_threads () + val batches = (slices + max_threads - 1) div max_threads + in + seconds (Time.toReal timeout / Real.fromInt batches) + end type prover_problem = {comment : string, @@ -188,9 +192,9 @@ fun proof_banner mode prover_name = (case mode of - Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof" - | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof" - | _ => "Try this") + Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof: " + | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof: " + | _ => "") fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans = let