# HG changeset patch
# User Andreas Lochbihler
# Date 1423663463 -3600
# Node ID 67deb7bed6d3a57c17e178201d35e943e35314f8
# Parent  ef65605a7d9ca70fd3b877140a3758a4a908a9b8# Parent  860fb1c6555302106b6a7fe167beb9f9245c2d70
merged

diff -r 860fb1c65553 -r 67deb7bed6d3 Admin/components/components.sha1
--- 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
diff -r 860fb1c65553 -r 67deb7bed6d3 Admin/components/main
--- 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
diff -r 860fb1c65553 -r 67deb7bed6d3 NEWS
--- 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
diff -r 860fb1c65553 -r 67deb7bed6d3 src/Doc/Sledgehammer/document/root.tex
--- 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}.
diff -r 860fb1c65553 -r 67deb7bed6d3 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- 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))