# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID 873b581fd6908ad1a008550d7f462777706d2cae # Parent eaf22c0e9ddf5ddec4e68d45327d0d16800d4412 generalized the 'slice' option towards more flexible slicing diff -r eaf22c0e9ddf -r 873b581fd690 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 10:01:50 2022 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100 @@ -578,8 +578,7 @@ be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > Isabelle > General.'' For automatic runs, only the first prover set using \textit{provers} (\S\ref{mode-of-operation}) is considered (typically E), -\textit{slice} (\S\ref{mode-of-operation}) is disabled, -fewer facts are +\textit{slice} (\S\ref{timeouts}) is set to 0, fewer facts are passed to the prover, \textit{fact\_filter} (\S\ref{relevance-filter}) is set to \textit{mepo}, \textit{strict} (\S\ref{problem-encoding}) is enabled, \textit{verbose} (\S\ref{output-format}) and \textit{debug} @@ -806,20 +805,6 @@ \opnodefault{prover}{string} Alias for \textit{provers}. -\optrue{slice}{dont\_slice} -Specifies whether the time allocated to a prover should be sliced into several -segments, each of which has its own set of possibly prover-dependent options. -For SPASS and Vampire, the first slice tries the fast but incomplete -set-of-support (SOS) strategy, whereas the second slice runs without it. For E, -up to three slices are tried, with different weighted search strategies and -number of facts. For SMT solvers, several slices are tried with the same options -each time but fewer and fewer facts. According to benchmarks with a timeout of -30 seconds, slicing is a valuable optimization, and you should probably leave it -enabled unless you are conducting experiments. - -\nopagebreak -{\small See also \textit{verbose} (\S\ref{output-format}).} - \optrue{minimize}{dont\_minimize} Specifies whether the proof minimization tool should be invoked automatically after proof search. @@ -1215,6 +1200,20 @@ Specifies the maximum number of seconds that the automatic provers should spend searching for a proof. This excludes problem preparation and is a soft limit. +\opdefault{slice}{float}{\upshape 5} +Specifies the size of the time slices for each invocation of a prover. Each time +slice has its own set of options. For example, for SPASS, the first slice might +try the fast but incomplete set-of-support strategy, whereas other slices might +run without it. Slicing can be disable by setting \textit{slice} to 0. However, +slicing is a valuable optimization, and you should probably leave it enabled +unless you are conducting experiments. + +\nopagebreak +{\small See also \textit{verbose} (\S\ref{output-format}).} + +\optrueonly{dont\_slice} +Alias for ``\textit{slice} = 0''. + \opdefault{preplay\_timeout}{float}{\upshape 1} Specifies the maximum number of seconds that \textit{metis} or other proof methods should spend trying to ``preplay'' the found proof. If this option @@ -1289,10 +1288,11 @@ The following subsections assume that the environment variable \texttt{AFP} is defined and points to a release of the Archive of Formal Proofs. + \subsection{Example of Benchmarking Sledgehammer} \begin{verbatim} -isabelle mirabelle -d $AFP -O output \ +isabelle mirabelle -d '$AFP' -O output \ -A "sledgehammer[provers = e, timeout = 30]" \ VeriComp \end{verbatim} @@ -1302,7 +1302,7 @@ session VeriComp. The results are written to \texttt{output/mirabelle.log}. \begin{verbatim} -isabelle mirabelle -d $AFP -O output \ +isabelle mirabelle -d '$AFP' -O output \ -T Semantics -T Compiler \ -A "sledgehammer[provers = e, timeout = 30]" \ VeriComp @@ -1315,7 +1315,7 @@ \subsection{Example of Benchmarking Multiple Tools} \begin{verbatim} -isabelle mirabelle -d $AFP -O output -t 10 \ +isabelle mirabelle -d '$AFP' -O output -t 10 \ -A "try0" -A "metis" \ VeriComp \end{verbatim} @@ -1324,10 +1324,11 @@ commands, respectively, each with a timeout of 10 seconds. The results are written to \texttt{output/mirabelle.log}. + \subsection{Example of Generating TPTP Files} \begin{verbatim} -isabelle mirabelle -d $AFP -O output \ +isabelle mirabelle -d '$AFP' -O output \ -A "sledgehammer[provers = e, timeout = 5, keep_probs = true]" \ VeriComp \end{verbatim} diff -r eaf22c0e9ddf -r 873b581fd690 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jan 31 10:01:50 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jan 31 16:09:23 2022 +0100 @@ -71,14 +71,15 @@ ("compress", "smart"), ("try0", "true"), ("smt_proofs", "true"), - ("slice", "true"), ("minimize", "true"), + ("slice", "5"), ("preplay_timeout", "1")] val alias_params = [("prover", ("provers", [])), (* undocumented *) ("dont_preplay", ("preplay_timeout", ["0"])), ("dont_compress", ("compress", ["1"])), + ("dont_slice", ("slice", ["0"])), ("isar_proof", ("isar_proofs", [])) (* legacy *)] val negated_alias_params = [("no_debug", "debug"), @@ -89,7 +90,6 @@ ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), ("no_isar_proofs", "isar_proofs"), - ("dont_slice", "slice"), ("dont_minimize", "minimize"), ("dont_try0", "try0"), ("no_smt_proofs", "smt_proofs")] @@ -175,11 +175,9 @@ else remotify_prover_if_supported_and_not_already_remote ctxt name (* The first ATP of the list is used by Auto Sledgehammer. *) -fun default_provers_param_value mode ctxt = +fun default_provers_param_value ctxt = [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN] \ \see also \<^system_option>\sledgehammer_provers\\ |> map_filter (remotify_prover_if_not_installed ctxt) - (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) - |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0)) |> implode_param fun set_default_raw_param param thy = @@ -187,15 +185,15 @@ thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) end -fun default_raw_params mode thy = +fun default_raw_params thy = let val ctxt = Proof_Context.init_global thy in Data.get thy |> fold (AList.default (op =)) - [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]), - ("timeout", - let val timeout = Options.default_int \<^system_option>\sledgehammer_timeout\ in - [if timeout <= 0 then "none" else string_of_int timeout] - end)] + [("provers", [(case !provers of "" => default_provers_param_value ctxt | s => s)]), + ("timeout", + let val timeout = Options.default_int \<^system_option>\sledgehammer_timeout\ in + [if timeout <= 0 then "none" else string_of_int timeout] + end)] end fun extract_params mode default_params override_params = @@ -269,8 +267,8 @@ val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") val try0 = lookup_bool "try0" val smt_proofs = lookup_bool "smt_proofs" - val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = lookup_bool "minimize" + val slice = if mode = Auto_Try then Time.zeroTime else lookup_time "slice" val timeout = lookup_time "timeout" val preplay_timeout = lookup_time "preplay_timeout" val expect = lookup_string "expect" @@ -281,11 +279,11 @@ induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, - slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, + minimize = minimize, slice = slice, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end -fun get_params mode = extract_params mode o default_raw_params mode +fun get_params mode = extract_params mode o default_raw_params fun default_params thy = get_params Normal thy o map (apsnd single) val silence_state = @@ -301,8 +299,7 @@ give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs, verbose output, machine learning). However, if the fact is available by no other means (not even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice - but to insert it into the state as an additional hypothesis. - *) + but to insert it into the state as an additional hypothesis. *) val {facts = chained0, ...} = Proof.goal state0 val (inserts, keep_chained) = if null chained0 orelse #only fact_override then @@ -380,7 +377,7 @@ (parse_raw_params >> (fn params => Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Sledgehammer:\n" ^ - (case rev (default_raw_params Normal thy) of + (case rev (default_raw_params thy) of [] => "none" | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))))) diff -r eaf22c0e9ddf -r 873b581fd690 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 10:01:50 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100 @@ -42,8 +42,8 @@ compress : real option, try0 : bool, smt_proofs : bool, - slice : bool, minimize : bool, + slice : Time.time, timeout : Time.time, preplay_timeout : Time.time, expect : string} @@ -139,8 +139,8 @@ compress : real option, try0 : bool, smt_proofs : bool, - slice : bool, minimize : bool, + slice : Time.time, timeout : Time.time, preplay_timeout : Time.time, expect : string} @@ -173,8 +173,8 @@ compress = #compress params, try0 = #try0 params, smt_proofs = #smt_proofs params, + minimize = #minimize params, slice = #slice params, - minimize = #minimize params, timeout = #timeout params, preplay_timeout = #preplay_timeout params, expect = #expect params} diff -r eaf22c0e9ddf -r 873b581fd690 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 10:01:50 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100 @@ -103,7 +103,8 @@ 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 |> not slice ? (List.last #> single) +fun get_slices slice slices = + map_index I slices |> slice = Time.zeroTime ? (List.last #> single) fun get_facts_of_filter _ [(_, facts)] = facts | get_facts_of_filter fact_filter factss = diff -r eaf22c0e9ddf -r 873b581fd690 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 10:01:50 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100 @@ -94,8 +94,8 @@ 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, isar_proofs = isar_proofs, - compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = false, - minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} + compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize, + slice = Time.zeroTime, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)], found_proof = I} diff -r eaf22c0e9ddf -r 873b581fd690 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 10:01:50 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100 @@ -101,7 +101,7 @@ val state = Proof.map_context (repair_context) state val ctxt = Proof.context_of state - val max_slices = if slice then Config.get ctxt smt_max_slices else 1 + val max_slices = if slice = Time.zeroTime then 1 else Config.get ctxt smt_max_slices fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) = let