# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID fcfd96a59625ca3db9c5b3526022a6d886adae23 # Parent 30ccc472d4866310790aa33c77ad45474f9f7c3f disable slicing within ATP module (in preparation for refactoring) diff -r 30ccc472d486 -r fcfd96a59625 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100 @@ -103,13 +103,6 @@ transform_elim_prop #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) -fun get_slices slice slices = - map_index I slices |> slice = Time.zeroTime ? (List.last #> single) - -(* For low values of "max_facts", this fudge value ensures that most slices are invoked with a - nontrivial amount of facts. *) -val max_fact_factor_fudge = 5 - val mono_max_privileged_facts = 10 fun suffix_of_mode Auto_Try = "_try" @@ -118,16 +111,13 @@ | suffix_of_mode MaSh = "" | suffix_of_mode Minimize = "_min" -(* Give the ATPs some slack before interrupting them the hard way. *) -val atp_timeout_slack = seconds 1.0 - (* Important messages are important but not so important that users want to see them each time. *) val atp_important_message_keep_quotient = 25 fun run_atp mode name ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_facts, - max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, slice, - minimize, timeout, preplay_timeout, spy, ...} : params) + max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, + slice, timeout, preplay_timeout, spy, ...} : params) ({comment, state, goal, subgoal, subgoal_count, facts, found_proof, ...} : prover_problem) = let val thy = Proof.theory_of state @@ -180,17 +170,9 @@ fun run () = let - (* If slicing is disabled, we expand the last slice to fill the entire time available. *) - val all_slices = best_slices ctxt - val actual_slices = get_slices slice all_slices - - fun max_facts_of_slices (slices : (real * (slice_spec * string)) list) = - fold (Integer.max o fst o #1 o fst o snd) slices 0 - - val num_actual_slices = length actual_slices - val max_fact_factor = - Real.fromInt (case max_facts of NONE => max_facts_of_slices all_slices | SOME max => max) - / Real.fromInt (max_facts_of_slices (map snd actual_slices)) + val (_, (((best_max_facts, _), format, best_type_enc, best_lam_trans, + best_uncurried_aliases), extra)) = + List.last (best_slices ctxt) fun monomorphize_facts facts = let @@ -213,139 +195,91 @@ |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end - val real_ms = Real.fromInt o Time.toMilliseconds - (* TODO: replace this seems-to-work per-slice overhead with actually-measured value *) - val slices_overhead_ms = Int.max (0, num_actual_slices * 25) - val slices_timeout_ms = real (Time.toMilliseconds timeout - slices_overhead_ms) - - fun run_slice time_left (cache_key, cache_value) (slice, (time_frac, - (key as ((best_max_facts, _ (* best_fact_filter *)), format, best_type_enc, - best_lam_trans, best_uncurried_aliases), - extra))) = + val facts = snd facts + val num_facts = + (case max_facts of + NONE => best_max_facts + | SOME max_facts => max_facts) + |> Integer.min (length facts) + val strictness = if strict then Strict else Non_Strict + val type_enc = type_enc |> choose_type_enc strictness best_type_enc format + val run_timeout = if slice = Time.zeroTime then timeout else slice + val generous_run_timeout = if mode = MaSh then one_day else run_timeout + val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => let - val facts = snd facts - val num_facts = - Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge - |> Integer.min (length facts) - val strictness = if strict then Strict else Non_Strict - val type_enc = type_enc |> choose_type_enc strictness best_type_enc format - val slice_timeout = - (real_ms time_left - |> (if slice < num_actual_slices - 1 then - curry Real.min (time_frac * slices_timeout_ms) - else - I)) - * 0.001 - |> seconds - val generous_slice_timeout = - if mode = MaSh then one_day else slice_timeout + atp_timeout_slack - val _ = - if debug then - quote name ^ " slice #" ^ string_of_int (slice + 1) ^ - " with " ^ string_of_int num_facts ^ " fact" ^ - plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..." - |> writeln - else - () - val ({elapsed, ...}, value as (atp_problem, _, _, _)) = Timing.timing (fn () => - if cache_key = SOME key then - cache_value - else - let - val sound = is_type_enc_sound type_enc - val generate_info = (case format of DFG _ => true | _ => false) - val readable_names = not (Config.get ctxt atp_full_names) - val lam_trans = lam_trans |> the_default best_lam_trans - val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases - in - facts - |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) - |> take num_facts - |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts - |> map (apsnd Thm.prop_of) - |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode - lam_trans uncurried_aliases readable_names true hyp_ts concl_t - end) () + val sound = is_type_enc_sound type_enc + val generate_info = (case format of DFG _ => true | _ => false) + val readable_names = not (Config.get ctxt atp_full_names) + val lam_trans = lam_trans |> the_default best_lam_trans + val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases + in + facts + |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) + |> take num_facts + |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts + |> map (apsnd Thm.prop_of) + |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode + lam_trans uncurried_aliases readable_names true hyp_ts concl_t + end) () - val () = spying spy (fn () => - (state, subgoal, name, "Slice #" ^ string_of_int (slice + 1) ^ - " generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) + val () = spying spy (fn () => + (state, subgoal, name, "Generating ATP problem in " ^ + string_of_int (Time.toMilliseconds elapsed) ^ " ms")) - fun sel_weights () = atp_problem_selection_weights atp_problem - fun ord_info () = atp_problem_term_order_info atp_problem + fun sel_weights () = atp_problem_selection_weights atp_problem + fun ord_info () = atp_problem_term_order_info atp_problem - val ord = effective_term_order ctxt name - val args = - arguments ctxt full_proofs extra slice_timeout prob_path (ord, ord_info, sel_weights) - val command = space_implode " " (File.bash_path executable :: args) + val ord = effective_term_order ctxt name + val args = arguments ctxt full_proofs extra run_timeout prob_path + (ord, ord_info, sel_weights) + val command = space_implode " " (File.bash_path executable :: args) - fun run_command () = - if exec = isabelle_scala_function then - let val {output, timing} = SystemOnTPTP.run_system_encoded args - in (output, timing) end - else - let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) - in (Process_Result.out res, Process_Result.timing_elapsed res) end - - val _ = - atp_problem - |> lines_of_atp_problem format ord ord_info - |> (exec <> isabelle_scala_function) ? - cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) - |> File.write_list prob_path + fun run_command () = + if exec = isabelle_scala_function then + let val {output, timing} = SystemOnTPTP.run_system_encoded args + in (output, timing) end + else + let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) + in (Process_Result.out res, Process_Result.timing_elapsed res) end - val ((output, run_time), (atp_proof, outcome)) = - Timeout.apply generous_slice_timeout run_command () - |>> overlord ? - (fn output => prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output) - |> (fn accum as (output, _) => - (accum, - extract_tstplike_proof_and_outcome verbose proof_delims known_failures output - |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) - atp_problem - handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable))) - handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut)) - | ERROR msg => (("", Time.zeroTime), ([], SOME (UnknownError msg))) - - val () = spying spy (fn () => - (state, subgoal, name, "Slice #" ^ string_of_int (slice + 1) ^ - " running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms")) + val _ = + atp_problem + |> lines_of_atp_problem format ord ord_info + |> (exec <> isabelle_scala_function) ? + cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) + |> File.write_list prob_path - val outcome = - (case outcome of - NONE => - (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of - SOME facts => - let - val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) - in - if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure - end - | NONE => (found_proof (); NONE)) - | _ => outcome) - in - ((SOME key, value), (output, run_time, facts, atp_proof, outcome), - SOME (format, type_enc)) - end + val ((output, run_time), (atp_proof, outcome)) = + Timeout.apply generous_run_timeout run_command () + |>> overlord ? + (fn output => prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output) + |> (fn accum as (output, _) => + (accum, + extract_tstplike_proof_and_outcome verbose proof_delims known_failures output + |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) + atp_problem + handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable))) + handle Timeout.TIMEOUT _ => (("", run_timeout), ([], SOME TimedOut)) + | ERROR msg => (("", Time.zeroTime), ([], SOME (UnknownError msg))) - val timer = Timer.startRealTimer () + val () = spying spy (fn () => + (state, subgoal, name, "Running command in " ^ + string_of_int (Time.toMilliseconds run_time) ^ " ms")) - fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) = - let val time_left = timeout - Timer.checkRealTimer timer in - if time_left <= Time.zeroTime then - result - else - run_slice time_left cache slice - |> (fn (cache, (output, run_time, used_from, atp_proof, outcome), - format_type_enc) => - (cache, (output, run_time0 + run_time, used_from, atp_proof, outcome), - format_type_enc)) - end - | maybe_run_slice _ result = result + val outcome = + (case outcome of + NONE => + (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of + SOME facts => + let + val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) + in + if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure + end + | NONE => (found_proof (); NONE)) + | _ => outcome) in - ((NONE, ([], Symtab.empty, [], Symtab.empty)), - ("", Time.zeroTime, [], [], SOME InternalError), NONE) - |> fold maybe_run_slice actual_slices + (atp_problem_data, (output, run_time, facts, atp_proof, outcome), (format, type_enc)) end (* If the problem file has not been exported, remove it; otherwise, export @@ -367,8 +301,8 @@ error ("No such directory: " ^ quote proof_dest_dir) end - val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome), - SOME (format, type_enc)) = + val ((_, pool, lifted, sym_tab), (output, run_time, used_from, atp_proof, outcome), + (format, type_enc)) = with_cleanup clean_up run () |> tap export val important_message =