--- 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}
--- 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] \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
|> 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>\<open>sledgehammer_timeout\<close> 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>\<open>sledgehammer_timeout\<close> 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))))))
--- 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}
--- 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 =
--- 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}
--- 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