# HG changeset patch # User desharna # Date 1644414725 -3600 # Node ID 455d886009b127b5d3ad9e8d48bdc6f9f695b535 # Parent c23aa0d177b4e8be9bef09c40f19dc1f3f584620 uniformized fact selection for ATP and SMT in Sledgehammer diff -r c23aa0d177b4 -r 455d886009b1 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Feb 09 13:02:59 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Feb 09 14:52:05 2022 +0100 @@ -87,6 +87,7 @@ val bunches_of_proof_methods : Proof.context -> bool -> 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 val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list @@ -238,6 +239,10 @@ SOME facts => facts | NONE => snd (hd factss)) +fun facts_of_basic_slice (num_facts, fact_filter) factss = + facts_of_filter fact_filter factss + |> take num_facts + fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = diff -r c23aa0d177b4 -r 455d886009b1 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Feb 09 13:02:59 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Feb 09 14:52:05 2022 +0100 @@ -107,12 +107,12 @@ ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem) slice = let + val (basic_slice, ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) = + slice + val facts = facts_of_basic_slice basic_slice factss val thy = Proof.theory_of state val ctxt = Proof.context_of state - val ((good_max_facts, good_fact_filter), ATP_Slice (good_format, good_type_enc, good_lam_trans, - good_uncurried_aliases, extra)) = slice - val {exec, arguments, proof_delims, known_failures, prem_role, good_max_mono_iters, good_max_new_mono_instances, ...} = get_atp thy name () @@ -185,16 +185,14 @@ val type_enc = choose_type_enc strictness good_format good_type_enc val run_timeout = slice_timeout slices timeout val generous_run_timeout = if mode = MaSh then one_day else run_timeout - val facts = facts_of_filter good_fact_filter factss - |> not (is_type_enc_sound type_enc) ? - filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) - |> take good_max_facts val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => let val generate_info = (case good_format of DFG _ => true | _ => false) val readable_names = not (Config.get ctxt atp_full_names) in facts + |> not (is_type_enc_sound type_enc) ? + filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) |> generate_atp_problem ctxt generate_info good_format prem_role type_enc atp_mode diff -r c23aa0d177b4 -r 455d886009b1 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Wed Feb 09 13:02:59 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Wed Feb 09 14:52:05 2022 +0100 @@ -119,13 +119,10 @@ ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) slice = let + val (basic_slice, SMT_Slice options) = slice + val facts = facts_of_basic_slice basic_slice factss val ctxt = Proof.context_of state - val ((good_max_facts, good_fact_filter), SMT_Slice options) = slice - - val facts = facts_of_filter good_fact_filter factss - |> take good_max_facts - val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = smt_filter name params state goal subgoal facts options val used_facts =