--- a/Admin/components/components.sha1 Wed Feb 11 15:03:21 2015 +0100
+++ b/Admin/components/components.sha1 Wed Feb 11 15:04:23 2015 +0100
@@ -1,5 +1,6 @@
70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz
2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz
+03aec2ec5757301c9df149f115d1f4f1d2cafd9e cvc4-1.5pre.tar.gz
842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz
cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
3b44cca04855016d5f8cfb5101b2e0579ab80197 cygwin-20130117.tar.gz
--- a/Admin/components/main Wed Feb 11 15:03:21 2015 +0100
+++ b/Admin/components/main Wed Feb 11 15:04:23 2015 +0100
@@ -1,6 +1,6 @@
#main components for everyday use, without big impact on overall build time
-cvc3-2.4.1
csdp-6.x
+cvc4-1.5pre
e-1.8
exec_process-1.0.3
Haskabelle-2014
--- a/NEWS Wed Feb 11 15:03:21 2015 +0100
+++ b/NEWS Wed Feb 11 15:04:23 2015 +0100
@@ -159,6 +159,8 @@
operations.
* Sledgehammer:
+ - CVC4 is now included with Isabelle instead of CVC3 and run by
+ default.
- Minimization is now always enabled by default.
Removed subcommand:
min
--- a/src/Doc/Sledgehammer/document/root.tex Wed Feb 11 15:03:21 2015 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Feb 11 15:04:23 2015 +0100
@@ -164,7 +164,7 @@
\begin{sloppy}
\begin{enum}
\item[\labelitemi] If you installed an official Isabelle package, it should
-already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%
+already include properly setup executables for CVC4, E, SPASS, and Z3, ready to use.%
\footnote{Vampire's license prevents us from doing the same for
this otherwise remarkable tool.}
For Z3, you must additionally set the variable
@@ -174,13 +174,14 @@
via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
> Isabelle > General'' in Isabelle/jEdit.
-\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
-SPASS, and Z3 binary packages from \download. Extract the archives, then add a
-line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
+\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3,
+CVC4, E, SPASS, and Z3 binary packages from \download. Extract the archives,
+then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash
+components}%
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
startup. Its value can be retrieved by executing \texttt{isabelle}
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
-file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the
+file with the absolute path to CVC3, CVC4, E, SPASS, or Z3. For example, if the
\texttt{components} file does not exist yet and you extracted SPASS to
\texttt{/usr/local/spass-3.8ds}, create it with the single line
@@ -942,13 +943,10 @@
runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
-and Z3 in parallel---either locally or remotely, depending on the number of
-processor cores available.
-
-It is generally a good idea to run several provers in parallel. Running E,
-SPASS, and Vampire for 5~seconds yields a similar success rate to running the
-most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
+By default, Sledgehammer runs a subset of CVC4, E, E-SInE, SPASS, Vampire,
+veriT, and Z3 in parallel---either locally or remotely, depending on the number
+of processor cores available and on which provers are actually installed.
+It is generally a good idea to run several provers in parallel.
\opnodefault{prover}{string}
Alias for \textit{provers}.
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Feb 11 15:03:21 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Feb 11 15:04:23 2015 +0100
@@ -27,7 +27,8 @@
open Sledgehammer_MaSh
open Sledgehammer
-(* val cvc3N = "cvc3" *)
+val cvc4N = "cvc4"
+val veritN = "verit"
val z3N = "z3"
val runN = "run"
@@ -180,7 +181,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value mode ctxt =
- [eN, spassN, z3N, vampireN, e_sineN]
+ [spassN, cvc4N, vampireN, eN, z3N, veritN, e_sineN]
|> 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_value () - (if mode = Try then 1 else 0))