--- a/Admin/components/components.sha1 Tue Sep 28 20:57:57 2021 +0200
+++ b/Admin/components/components.sha1 Tue Sep 28 20:58:04 2021 +0200
@@ -438,3 +438,4 @@
aa20745f0b03e606b1a4149598e0c7572b63c657 z3-4.8.3.tar.gz
9dfeb39c87393af7b6a34118507637aa53aca05e zipperposition-2.0-1.tar.gz
b884c60653002a7811e3b652ae0515e825d98667 zipperposition-2.0.tar.gz
+5f53a77efb5cbe9d0c95d74a1588cc923bd711a7 zipperposition-2.1.tar.gz
--- a/src/Doc/Sledgehammer/document/root.tex Tue Sep 28 20:57:57 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Tue Sep 28 20:58:04 2021 +0200
@@ -235,13 +235,13 @@
%
``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms) \\
%
-``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms)
+``\textit{vampire\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms)
%
\postw
-Sledgehammer ran CVC4, E, SPASS, and Z3 in parallel. Depending on which
-provers are installed and how many processor cores are available, some of the
-provers might be missing or present with a \textit{remote\_} prefix.
+Sledgehammer ran CVC4, E, Vampire, and Z3 in parallel. This list may vary
+depending on which provers are installed and how many processor cores are
+available.
For each successful prover, Sledgehammer gives a one-line Isabelle proof. Rough
timings are shown in parentheses, indicating how fast the call is. You can
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Sep 28 20:57:57 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Sep 28 20:58:04 2021 +0200
@@ -177,7 +177,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value mode ctxt =
- [cvc4N, vampireN, z3N, eN, spassN, veritN]
+ [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN]
|> 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))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Sep 28 20:57:57 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Sep 28 20:58:04 2021 +0200
@@ -189,9 +189,8 @@
val smt_methodss =
if smt_proofs then
- [SMT_Method SMT_Z3 ::
- map (fn strategy => SMT_Method (SMT_Verit strategy))
- (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))]
+ [map (SMT_Method o SMT_Verit) (Verit_Proof.all_veriT_stgies (Context.Proof ctxt)),
+ [SMT_Method SMT_Z3]]
else
[]
in
--- a/src/Pure/Admin/build_zipperposition.scala Tue Sep 28 20:57:57 2021 +0200
+++ b/src/Pure/Admin/build_zipperposition.scala Tue Sep 28 20:58:04 2021 +0200
@@ -9,7 +9,7 @@
object Build_Zipperposition
{
- val default_version = "2.0"
+ val default_version = "2.1"
/* build Zipperposition */