# HG changeset patch # User blanchet # Date 1678458438 -3600 # Node ID 7c25451ae2c13a9a616fc15d4876dd3b6cb1fbab # Parent d39027e1c8c52644c6da379c14f23f0e471a59b1 use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism diff -r d39027e1c8c5 -r 7c25451ae2c1 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Mar 10 11:56:52 2023 +0100 +++ b/src/HOL/Sledgehammer.thy Fri Mar 10 15:27:18 2023 +0100 @@ -35,4 +35,10 @@ ML_file \Tools/Sledgehammer/sledgehammer_commands.ML\ ML_file \Tools/Sledgehammer/sledgehammer_tactics.ML\ +(* +lemma "x - y + y = (x::nat)" + sledgehammer[e, abduce = 10] + oops +*) + end diff -r d39027e1c8c5 -r 7c25451ae2c1 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Mar 10 11:56:52 2023 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Mar 10 15:27:18 2023 +0100 @@ -64,6 +64,7 @@ int Symtab.table -> (string, string, (string, string atp_type) atp_term, string) atp_formula -> term val top_abduce_candidates : int -> term list -> term list + val sort_propositions_by_provability : Proof.context -> term list -> term list end; structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT = @@ -859,4 +860,25 @@ sort_top max_candidates (map_filter maybe_score candidates) end +fun provability_status ctxt t = + let + val res = Timeout.apply (seconds 0.1) + (Thm.term_of o Thm.rhs_of o Simplifier.full_rewrite ctxt) (Thm.cterm_of ctxt t) + in + if res aconv @{prop True} then SOME true + else if res aconv @{prop False} then SOME false + else NONE + end + handle Timeout.TIMEOUT _ => NONE + +(* Put propositions that simplify to "True" first, and filter out propositions + that simplify to "False". *) +fun sort_propositions_by_provability ctxt ts = + let + val statuses_ts = map (`(provability_status ctxt)) ts + in + maps (fn (SOME true, t) => [t] | _ => []) statuses_ts @ + maps (fn (NONE, t) => [t] | _ => []) statuses_ts + end + end; diff -r d39027e1c8c5 -r 7c25451ae2c1 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 10 11:56:52 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 10 15:27:18 2023 +0100 @@ -339,11 +339,14 @@ end | SOME failure => let + val max_abduce_candidates_factor = 3 (* FUDGE *) val max_abduce_candidates = the_default default_abduce_max_candidates abduce_max_candidates val abduce_candidates = atp_abduce_candidates |> map (termify_atp_abduce_candidate ctxt name format type_enc pool lifted sym_tab) - |> top_abduce_candidates max_abduce_candidates + |> top_abduce_candidates (max_abduce_candidates * max_abduce_candidates_factor) + |> sort_propositions_by_provability ctxt + |> take max_abduce_candidates in if null abduce_candidates then (SOME failure, [], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)