# HG changeset patch # User blanchet # Date 1677654051 -3600 # Node ID a8458f0df4ee42fdc9b846c6422d6a6a910577f0 # Parent 9bd6c78b3b77a3f0b16cb7afa38a8fa331624fe6 implemented ad hoc abduction in Sledgehammer with E diff -r 9bd6c78b3b77 -r a8458f0df4ee src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Tue Feb 28 20:37:57 2023 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Wed Mar 01 08:00:51 2023 +0100 @@ -1199,6 +1199,7 @@ \item[\labelitemi] \textbf{\textit{some\_preplayed}:} Sledgehammer found a proof that was successfully preplayed. \item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof. \item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out. +\item[\labelitemi] \textbf{\textit{resources\_out}:} Sledgehammer ran out of resources. \item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some problem. \end{enum} diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Mar 01 08:00:51 2023 +0100 @@ -99,6 +99,8 @@ val atp_proof_of_tstplike_proof : bool -> string -> string atp_problem -> string -> string atp_proof + val atp_abduce_candidates_of_output : string -> string atp_problem -> string -> + (string, string, (string, string atp_type) atp_term, string) atp_formula list end; structure ATP_Proof : ATP_PROOF = @@ -724,4 +726,58 @@ |> parse_proof full local_prover problem |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1)))) +val e_symbol_prefixes = ["esk", "epred"] + +fun exists_name_in_term pred = + let + fun ex_name (ATerm ((s, _), tms)) = pred s orelse exists ex_name tms + | ex_name (AAbs ((_, tm), tms)) = exists ex_name (tm :: tms) + in ex_name end + +fun exists_name_in_formula pred phi = + formula_fold NONE (fn _ => fn tm => fn ex => ex orelse exists_name_in_term pred tm) phi false + +fun exists_symbol_in_formula prefixes = + exists_name_in_formula (fn s => exists (fn prefix => String.isPrefix prefix s) prefixes) + +fun atp_abduce_candidates_of_output local_prover problem output = + let + (* Truncate too large output to avoid memory issues. *) + val max_size = 1000000 + val output = + if String.size output > max_size then + String.substring (output, 0, max_size) + else + output + + fun fold_extract accum [] = accum + | fold_extract accum (line :: lines) = + if String.isSubstring "# info" line + andalso String.isSubstring "negated_conjecture" line then + if String.isSubstring ", 0, 0," line then + (* This pattern occurs in the "info()" comment of an E clause that directly emerges from + the conjecture. We don't want to tell the user that they can prove "P" by assuming + "P". *) + fold_extract accum lines + else + let + val clean_line = + (case space_explode "#" line of + [] => "" + | before_hash :: _ => before_hash) + in + (case try (parse_proof true local_prover problem) clean_line of + SOME [(_, _, phi, _, _)] => + if local_prover = eN andalso exists_symbol_in_formula e_symbol_prefixes phi then + fold_extract accum lines + else + fold_extract (phi :: accum) lines + | _ => fold_extract accum lines) + end + else + fold_extract accum lines + in + fold_extract [] (split_lines output) + end + end; diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Mar 01 08:00:51 2023 +0100 @@ -58,6 +58,11 @@ val introduce_spass_skolems : (term, string) atp_step list -> (term, string) atp_step list val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list -> (term, string) atp_step list + val termify_atp_abduce_candidate : Proof.context -> string -> ATP_Problem.atp_format -> + ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list -> + int Symtab.table -> (string, string, (string, string atp_type) atp_term, string) atp_formula -> + term + val top_abduce_candidates : int -> term list -> term list end; structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT = @@ -624,7 +629,7 @@ #> map_proof_terms (infer_formulas_types ctxt #> map HOLogic.mk_Trueprop) #> local_prover = waldmeisterN ? repair_waldmeister_endgame -fun unskolemize_term skos = +fun unskolemize_spass_term skos = let val is_skolem_name = member (op =) skos @@ -653,10 +658,10 @@ val safe_abstract_over = abstract_over o apsnd (incr_boundvars 1) - fun unskolem t = + fun unskolem_inner t = (case find_argless_skolem t of SOME (x as (s, T)) => - HOLogic.exists_const T $ Abs (s, T, unskolem (safe_abstract_over (Free x, t))) + HOLogic.exists_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Free x, t))) | NONE => (case find_skolem_arg t of SOME (v as ((s, _), T)) => @@ -667,16 +672,19 @@ |> apply2 (fn lits => fold (curry s_disj) lits \<^term>\False\) in s_disj (HOLogic.all_const T - $ Abs (s, T, unskolem (safe_abstract_over (Var v, kill_skolem_arg haves))), - unskolem have_nots) + $ Abs (s, T, unskolem_inner (safe_abstract_over (Var v, kill_skolem_arg haves))), + unskolem_inner have_nots) end | NONE => (case find_var t of SOME (v as ((s, _), T)) => - HOLogic.all_const T $ Abs (s, T, unskolem (safe_abstract_over (Var v, t))) + HOLogic.all_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Var v, t))) | NONE => t))) + + fun unskolem_outer (@{const Trueprop} $ t) = @{const Trueprop} $ unskolem_outer t + | unskolem_outer t = unskolem_inner t in - HOLogic.mk_Trueprop o unskolem o HOLogic.dest_Trueprop + unskolem_outer end fun rename_skolem_args t = @@ -740,7 +748,7 @@ fold (union (op =) o filter (String.isPrefix spass_skolem_prefix) o fst) skoXss_steps [] val deps = map (snd #> #1) skoXss_steps in - [(name0, Unknown, unskolemize_term skos t, spass_pre_skolemize_rule, deps), + [(name0, Unknown, unskolemize_spass_term skos t, spass_pre_skolemize_rule, deps), (name, Unknown, t, spass_skolemize_rule, [name0])] end @@ -782,4 +790,48 @@ map repair_deps atp_proof end +fun termify_atp_abduce_candidate ctxt local_prover format type_enc pool lifted sym_tab phi = + let + val proof = [(("", []), Conjecture, mk_anot phi, "", [])] + val new_proof = termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab proof + in + (case new_proof of + [(_, _, phi', _, _)] => phi' + | _ => error "Impossible case in termify_atp_abduce_candidate") + end + +fun sort_top n scored_items = + if n <= 0 orelse null scored_items then + [] + else + let + fun split_min seen [] (_, best_item) = (best_item, List.rev seen) + | split_min seen ((score, item) :: scored_items) (best_score, best_item) = + if score < best_score then + split_min ((best_score, best_item) :: seen) scored_items (score, item) + else + split_min ((score, item) :: seen) scored_items (best_score, best_item) + + val (min_item, other_scored_items) = split_min [] (tl scored_items) (hd scored_items) + in + min_item :: sort_top (n - 1) (filter_out (equal min_item o snd) other_scored_items) + end + +fun top_abduce_candidates max_candidates candidates = + let + fun score t = + size_of_term t + + (if exists_subterm (fn Bound _ => true | Var _ => true | _ => false) t then 50 else 0) + + (if exists_subterm (fn Free _ => true | _ => false) t then ~10 else 0) + + fun maybe_score t = + (case t of + @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Free _ $ _) => NONE + | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Free _) => NONE + | @{const Trueprop} $ (Const (@{const_name All}, _) $ _) => NONE + | _ => SOME (score t, t)) + in + sort_top max_candidates (map_filter maybe_score candidates) + end + end; diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Mar 01 08:00:51 2023 +0100 @@ -24,7 +24,8 @@ datatype sledgehammer_outcome = SH_Some of prover_result * preplay_result list | SH_Unknown - | SH_Timeout + | SH_TimeOut + | SH_ResourcesOut | SH_None val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string @@ -57,12 +58,14 @@ datatype sledgehammer_outcome = SH_Some of prover_result * preplay_result list | SH_Unknown -| SH_Timeout +| SH_TimeOut +| SH_ResourcesOut | SH_None fun short_string_of_sledgehammer_outcome (SH_Some _) = "some" | short_string_of_sledgehammer_outcome SH_Unknown = "unknown" - | short_string_of_sledgehammer_outcome SH_Timeout = "timeout" + | short_string_of_sledgehammer_outcome SH_TimeOut = "timeout" + | short_string_of_sledgehammer_outcome SH_ResourcesOut = "resources_out" | short_string_of_sledgehammer_outcome SH_None = "none" fun alternative f (SOME x) (SOME y) = SOME (f (x, y)) @@ -79,13 +82,15 @@ fun max_outcome outcomes = let val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes + val timeout = find_first (fn (SH_TimeOut, _) => true | _ => false) outcomes + val resources_out = find_first (fn (SH_ResourcesOut, _) => true | _ => false) outcomes val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes - val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes val none = find_first (fn (SH_None, _) => true | _ => false) outcomes in some |> alternative snd unknown |> alternative snd timeout + |> alternative snd resources_out |> alternative snd none |> the_default (SH_Unknown, "") end @@ -220,12 +225,14 @@ |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) end -fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal +fun preplay_prover_result ({minimize, preplay_timeout, ...} : params) state subgoal (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) = let val (output, chosen_preplay_outcome) = if outcome = SOME ATP_Proof.TimedOut then - (SH_Timeout, select_one_line_proof used_facts (fst preferred_methss) []) + (SH_TimeOut, select_one_line_proof used_facts (fst preferred_methss) []) + else if outcome = SOME ATP_Proof.OutOfResources then + (SH_ResourcesOut, select_one_line_proof used_facts (fst preferred_methss) []) else if is_some outcome then (SH_None, select_one_line_proof used_facts (fst preferred_methss) []) else @@ -245,7 +252,9 @@ fun analyze_prover_result_for_consistency (result as {outcome, used_facts, ...} : prover_result) = if outcome = SOME ATP_Proof.TimedOut then - (SH_Timeout, K "") + (SH_TimeOut, K "") + else if outcome = SOME ATP_Proof.OutOfResources then + (SH_ResourcesOut, K "") else if is_some outcome then (SH_None, K "") else @@ -275,14 +284,15 @@ else error ("Unexpected outcome: the external prover found a proof but preplay failed") | ("unknown", SH_Unknown) => () - | ("timeout", SH_Timeout) => () + | ("timeout", SH_TimeOut) => () + | ("resources_out", SH_ResourcesOut) => () | ("none", SH_None) => () | _ => error ("Unexpected outcome: " ^ quote outcome_code)) end -fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode found_something - writeln_result learn (problem as {state, subgoal, ...}) - (slice as ((_, _, check_consistent, _, _), _)) prover_name = +fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode + has_already_found_something found_something writeln_result learn + (problem as {state, subgoal, ...}) (slice as ((_, _, check_consistent, _, _), _)) prover_name = let val ctxt = Proof.context_of state val hard_timeout = Time.scale 5.0 timeout @@ -306,6 +316,7 @@ in {comment = comment, state = state, goal = Thm.trivial @{cprop False}, subgoal = 1, subgoal_count = 1, factss = map (apsnd (append new_facts)) factss, + has_already_found_something = has_already_found_something, found_something = found_something "an inconsistency"} end @@ -354,11 +365,10 @@ val default_slice_schedule = (* FUDGE (loosely inspired by Seventeen evaluation) *) - [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N, - zipperpositionN, cvc4N, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, - cvc4N, iproverN, zipperpositionN, spassN, vampireN, zipperpositionN, - vampireN, zipperpositionN, z3N, zipperpositionN, vampireN, iproverN, spassN, - zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N, cvc4N, + [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N, zipperpositionN, + cvc4N, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, eN, cvc4N, iproverN, zipperpositionN, + spassN, vampireN, zipperpositionN, vampireN, zipperpositionN, z3N, zipperpositionN, vampireN, + iproverN, spassN, zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N, zipperpositionN] fun schedule_of_provers provers num_slices = @@ -410,7 +420,10 @@ ((slice_size0, abduce0, check_consistent0, num_facts0, fact_filter0), extra) = let val slice_size = Int.min (max_slice_size, slice_size0) - val abduce = abduce |> the_default abduce0 + val abduce = + (case abduce of + NONE => abduce0 + | SOME max_candidates => max_candidates > 0) val check_consistent = check_consistent |> the_default check_consistent0 val fact_filter = fact_filter |> the_default fact_filter0 val max_facts = max_facts |> the_default num_facts0 @@ -460,6 +473,12 @@ val found_proofs_and_inconsistencies = Synchronized.var "found_proofs_and_inconsistencies" 0 + fun has_already_found_something () = + if mode = Normal then + Synchronized.value found_proofs_and_inconsistencies > 0 + else + false + fun found_something a_proof_or_inconsistency prover_name = if mode = Normal then (Synchronized.change found_proofs_and_inconsistencies (fn n => n + 1); @@ -521,9 +540,11 @@ val factss = get_factss provers val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, - factss = factss, found_something = found_something "a proof"} + factss = factss, has_already_found_something = has_already_found_something, + found_something = found_something "a proof"} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) - val launch = launch_prover_and_preplay params mode found_something writeln_result learn + val launch = launch_prover_and_preplay params mode has_already_found_something + found_something writeln_result learn val schedule = if mode = Auto_Try then provers @@ -552,25 +573,26 @@ prover_slices |> max_outcome) end + + fun normal_failure () = + (the_default writeln writeln_result + ("No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^ + " found"); + false) in (launch_provers () - handle Timeout.TIMEOUT _ => (SH_Timeout, "")) + handle Timeout.TIMEOUT _ => (SH_TimeOut, "")) |> `(fn (outcome, message) => (case outcome of SH_Some _ => (the_default writeln writeln_result "Done"; true) - | SH_Unknown => (the_default writeln writeln_result message; false) - | SH_Timeout => - (the_default writeln writeln_result - ("No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^ - " found"); - false) - | SH_None => (the_default writeln writeln_result - (if message = "" then - "No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^ - " found" - else - "Warning: " ^ message); - false))) + | SH_Unknown => + if message = "" then normal_failure () + else (the_default writeln writeln_result ("Warning: " ^ message); false) + | SH_TimeOut => normal_failure () + | SH_ResourcesOut => normal_failure () + | SH_None => + if message = "" then normal_failure () + else (the_default writeln writeln_result ("Warning: " ^ message); false))) end) end; diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Mar 01 08:00:51 2023 +0100 @@ -15,7 +15,7 @@ type atp_slice = atp_format * string * string * bool * string type atp_config = {exec : string list * string list, - arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> string list, + arguments : bool -> bool -> string -> Time.time -> Path.T -> string list, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, @@ -76,7 +76,7 @@ type atp_config = {exec : string list * string list, - arguments : Proof.context -> bool -> string -> Time.time -> Path.T -> string list, + arguments : bool -> bool -> string -> Time.time -> Path.T -> string list, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, @@ -176,10 +176,13 @@ val e_config : atp_config = {exec = (["E_HOME"], ["eprover-ho", "eprover"]), - arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => - ["--tstp-in --tstp-out --silent " ^ extra_options ^ - " --cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ - File.bash_path problem], + arguments = fn abduce => fn _ => fn extra_options => fn timeout => fn problem => + ["--tstp-in --tstp-out --silent " ^ + (if abduce then + "--auto --print-saturated=ieIE --print-sat-info --soft-cpu-limit=" + else + extra_options ^ " --cpu-limit=") ^ + string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ File.bash_path problem], proof_delims = [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ tstp_proof_delims, @@ -193,7 +196,8 @@ let val (format, type_enc, lam_trans, extra_options) = if string_ord (getenv "E_VERSION", "2.7") <> LESS then - (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true") + (* '$ite' support appears to be buggy *) + (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true") else if string_ord (getenv "E_VERSION", "2.6") <> LESS then (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule") else @@ -201,11 +205,11 @@ in (* FUDGE *) K [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)), + ((1, true, false, 128, mashN), (format, type_enc, combsN, false, extra_options)), ((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)), - ((1000 (* infinity *), false, false, 128, mepoN), (format, type_enc, lam_trans, false, extra_options)), + ((1000 (* infinity *), false, false, 64, mepoN), (format, type_enc, lam_trans, false, extra_options)), ((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)), - ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options)), - ((1000 (* infinity *), false, false, 64, mashN), (format, type_enc, combsN, false, extra_options))] + ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options))] end, good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Mar 01 08:00:51 2023 +0100 @@ -77,6 +77,7 @@ val alias_params = [("prover", ("provers", [])), (* undocumented *) + ("dont_abduce", ("abduce", ["0"])), ("dont_preplay", ("preplay_timeout", ["0"])), ("dont_compress", ("compress", ["1"])), ("dont_slice", ("slices", ["1"])), @@ -86,7 +87,6 @@ ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), - ("dont_abduce", "abduce"), ("dont_check_consistent", "check_consistent"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), @@ -232,16 +232,12 @@ val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd + val abduce = + if mode = Auto_Try then SOME 0 + else lookup_option lookup_int "abduce" val check_consistent = - if mode = Auto_Try then - SOME false - else - lookup_option lookup_bool "check_consistent" - val abduce = - if mode = Auto_Try then - SOME false - else - lookup_option lookup_bool "abduce" + if mode = Auto_Try then SOME false + else lookup_option lookup_bool "check_consistent" val type_enc = if mode = Auto_Try then NONE diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 01 08:00:51 2023 +0100 @@ -21,6 +21,7 @@ val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int -> one_line_params -> string + val abduce_text : Proof.context -> term list -> string end; structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = @@ -528,4 +529,8 @@ else one_line_proof_text ctxt num_chained) one_line_params +fun abduce_text ctxt tms = + "Candidate" ^ plural_s (length tms) ^ " for missing hypothesis:\n" ^ + cat_lines (map (Syntax.string_of_term ctxt) tms) + end; diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Mar 01 08:00:51 2023 +0100 @@ -868,7 +868,8 @@ let val problem = {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, - subgoal_count = 1, factss = [("", facts)], found_something = K ()} + subgoal_count = 1, factss = [("", facts)], has_already_found_something = K false, + found_something = K ()} val slice = hd (get_slices ctxt prover) in get_minimizing_prover ctxt MaSh (K ()) prover params problem slice diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Mar 01 08:00:51 2023 +0100 @@ -29,7 +29,7 @@ overlord : bool, spy : bool, provers : string list, - abduce : bool option, + abduce : int option, check_consistent : bool option, type_enc : string option, strict : bool, @@ -63,6 +63,7 @@ subgoal : int, subgoal_count : int, factss : (string * fact list) list, + has_already_found_something : unit -> bool, found_something : string -> unit} datatype prover_slice_extra = @@ -82,6 +83,7 @@ type prover = params -> prover_problem -> prover_slice -> prover_result val SledgehammerN : string + val default_abduce_max_candidates : int val str_of_mode : mode -> string val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string @@ -113,6 +115,8 @@ (* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *) val SledgehammerN = "Sledgehammer" +val default_abduce_max_candidates = 1 + datatype mode = Auto_Try | Try | Normal | Minimize | MaSh fun str_of_mode Auto_Try = "Auto Try" @@ -136,7 +140,7 @@ overlord : bool, spy : bool, provers : string list, - abduce : bool option, + abduce : int option, check_consistent : bool option, type_enc : string option, strict : bool, @@ -182,6 +186,7 @@ subgoal : int, subgoal_count : int, factss : (string * fact list) list, + has_already_found_something : unit -> bool, found_something : string -> unit} datatype prover_slice_extra = diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Mar 01 08:00:51 2023 +0100 @@ -99,15 +99,17 @@ | suffix_of_mode Minimize = "_min" (* Important messages are important but not so important that users want to see them each time. *) -val atp_important_message_keep_quotient = 25 +val important_message_keep_quotient = 25 fun run_atp mode name - ({debug, verbose, overlord, strict, max_mono_iters, max_new_mono_instances, isar_proofs, - compress, try0, smt_proofs, minimize, slices, timeout, preplay_timeout, spy, ...} : params) - ({comment, state, goal, subgoal, subgoal_count, factss, found_something} : prover_problem) + ({debug, verbose, overlord, abduce = abduce_max_candidates, strict, max_mono_iters, + max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout, + preplay_timeout, spy, ...} : params) + ({comment, state, goal, subgoal, subgoal_count, factss, has_already_found_something, + found_something} : prover_problem) slice = let - val (basic_slice as (slice_size, _, _, _, _), + val (basic_slice as (slice_size, abduce, _, _, _), ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) = slice val facts = facts_of_basic_slice basic_slice factss @@ -185,11 +187,12 @@ val strictness = if strict then Strict else Non_Strict val type_enc = choose_type_enc strictness good_format good_type_enc val run_timeout = slice_timeout slice_size slices timeout - val generous_run_timeout = if mode = MaSh then one_day else run_timeout + val generous_run_timeout = + if mode = MaSh then one_day + else if abduce then run_timeout + seconds 5.0 + else run_timeout val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => - let - val readable_names = not (Config.get ctxt atp_full_names) - in + let 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) @@ -203,7 +206,7 @@ (state, subgoal, name, "Generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) - val args = arguments ctxt full_proofs extra run_timeout prob_path + val args = arguments abduce full_proofs extra run_timeout prob_path val command = space_implode " " (File.bash_path executable :: args) fun run_command () = @@ -220,6 +223,8 @@ cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path + val local_name = name |> perhaps (try (unprefix remote_prefix)) + val ((output, run_time), ((atp_proof, tstplike_proof), outcome)) = Timeout.apply generous_run_timeout run_command () |>> overlord ? @@ -227,12 +232,17 @@ |> (fn accum as (output, _) => (accum, extract_tstplike_proof_and_outcome verbose proof_delims known_failures output - |>> `(atp_proof_of_tstplike_proof false (perhaps (try (unprefix remote_prefix)) name) - atp_problem) + |>> `(atp_proof_of_tstplike_proof false local_name atp_problem) handle UNRECOGNIZED_ATP_PROOF () => (([], ""), SOME ProofUnparsable))) handle Timeout.TIMEOUT _ => (("", run_timeout), (([], ""), SOME TimedOut)) | ERROR msg => (("", Time.zeroTime), (([], ""), SOME (UnknownError msg))) + val atp_abduce_candidates = + if abduce andalso outcome <> NONE andalso not (has_already_found_something ()) then + atp_abduce_candidates_of_output local_name atp_problem output + else + [] + val () = spying spy (fn () => (state, subgoal, name, "Running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms")) @@ -243,14 +253,15 @@ | _ => ()) in (atp_problem_data, - (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, outcome), + (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, atp_abduce_candidates, + outcome), (good_format, type_enc)) end - (* If the problem file has not been exported, remove it; otherwise, export - the proof file too. *) + (* If the problem file has not been exported, remove it; otherwise, export the proof file + too. *) fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () - fun export (_, (output, _, _, _, _, _, _), _) = + fun export (_, (output, _, _, _, _, _, _, _), _) = let val proof_dest_dir_path = Path.explode proof_dest_dir val make_export_file_name = @@ -259,7 +270,8 @@ #> swap #> uncurry Path.ext in - if proof_dest_dir = "" then Output.system_message "don't export proof" + if proof_dest_dir = "" then + Output.system_message "don't export proof" else if File.exists proof_dest_dir_path then File.write (proof_dest_dir_path + make_export_file_name problem_file_name) output else @@ -267,16 +279,17 @@ end val ((_, pool, lifted, sym_tab), - (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof, outcome), + (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof, + atp_abduce_candidates, outcome), (format, type_enc)) = with_cleanup clean_up run () |> tap export val important_message = - if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0 + if mode = Normal andalso Random.random_range 0 (important_message_keep_quotient - 1) = 0 then extract_important_message output else "" - val (used_facts, preferred_methss, message) = + val (outcome, used_facts, preferred_methss, message) = (case outcome of NONE => let @@ -291,7 +304,7 @@ else [[preferred]]) in - (used_facts, preferred_methss, + (NONE, used_facts, preferred_methss, fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () @@ -330,7 +343,19 @@ end) end | SOME failure => - ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) + let + val max_abduce_candidates = + the_default default_abduce_max_candidates abduce_max_candidates + val abduce_candidates = + map (termify_atp_abduce_candidate ctxt name format type_enc pool lifted sym_tab) + atp_abduce_candidates + in + if null abduce_candidates then + (SOME failure, [], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure) + else + (NONE, [], (Auto_Method (* dummy *), []), fn _ => + abduce_text ctxt (top_abduce_candidates max_abduce_candidates abduce_candidates)) + end) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Mar 01 08:00:51 2023 +0100 @@ -83,8 +83,8 @@ fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, induction_rules, ...} : params) - (slice as ((_, abduce, check_consistent, _, _), _)) silent (prover : prover) timeout i n state - goal facts = + (slice as ((_, _, check_consistent, _, fact_filter), slice_extra)) silent + (prover : prover) timeout i n state goal facts = let val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") @@ -92,8 +92,8 @@ val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, - type_enc = type_enc, abduce = SOME abduce, check_consistent = SOME check_consistent, - strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false, + type_enc = type_enc, abduce = SOME 0, check_consistent = SOME false, strict = strict, + lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, induction_rules = induction_rules, max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, max_proofs = 1, @@ -102,10 +102,10 @@ expect = ""} val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, - factss = [("", facts)], found_something = K ()} + factss = [("", facts)], has_already_found_something = K false, found_something = K ()} val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, message} = - prover params problem slice + prover params problem ((1, false, false, length facts, fact_filter), slice_extra) val result as {outcome, ...} = if is_none outcome0 andalso forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then @@ -124,8 +124,6 @@ result end -(* minimalization of facts *) - (* Give the external prover some slack. The ATP gets further slack because the Sledgehammer preprocessing time is included in the estimate below but isn't part of the timeout. *) diff -r 9bd6c78b3b77 -r a8458f0df4ee src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Tue Feb 28 20:37:57 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Wed Mar 01 08:00:51 2023 +0100 @@ -45,7 +45,7 @@ |> hd |> snd val problem = {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - factss = [("", facts)], found_something = K ()} + factss = [("", facts)], has_already_found_something = K false, found_something = K ()} val slice = hd (get_slices ctxt name) in (case prover params problem slice of