--- 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}
--- 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;
--- 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>\<open>False\<close>)
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;
--- 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;
--- 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}
--- 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
--- 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;
--- 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
--- 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 =
--- 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}
--- 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. *)
--- 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