1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -106,10 +106,10 @@
     1.4  SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire
     1.5  \cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are
     1.6  run either locally or remotely via the System\-On\-TPTP web service
     1.7 -\cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is
     1.8 -used by default, and you can tell Sledgehammer to try Alt-Ergo \cite{alt-ergo},
     1.9 -CVC3 \cite{cvc3}, and Yices \cite{yices} as well; these are run either locally
    1.10 -or (for CVC3 and Z3) on a server at the TU M\"unchen.
    1.11 +\cite{sutcliffe-2000}. In addition to the ATPs, a selection of the SMT solvers
    1.12 +CVC3 \cite{cvc3}, Yices \cite{yices}, and Z3 \cite{z3} are run by default, and
    1.13 +you can tell Sledgehammer to try Alt-Ergo \cite{alt-ergo} as well; these are run
    1.14 +either locally or (for CVC3 and Z3) on a server at the TU M\"unchen.
    1.15  
    1.16  The problem passed to the automatic provers consists of your current goal
    1.17  together with a heuristic selection of hundreds of facts (theorems) from the
    1.18 @@ -161,11 +161,10 @@
    1.19  \cite{sutcliffe-2000}. If you want better performance, you should at least
    1.20  install E and SPASS locally.
    1.21  
    1.22 -Among the SMT solvers, Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and
    1.23 -CVC3 and Z3 can be run remotely on a TU M\"unchen server. If you want better
    1.24 -performance and get the ability to replay proofs that rely on the \emph{smt}
    1.25 -proof method without an Internet connection, you should at least install Z3
    1.26 -locally.
    1.27 +The SMT solvers Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and CVC3 and
    1.28 +Z3 can be run remotely on a TU M\"unchen server. If you want better performance
    1.29 +and get the ability to replay proofs that rely on the \emph{smt} proof method
    1.30 +without an Internet connection, you should at least have Z3 locally installed.
    1.31  
    1.32  There are three main ways to install automatic provers on your machine:
    1.33  
    1.34 @@ -220,12 +219,16 @@
    1.35  \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),
    1.36  set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
    1.37  \texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of
    1.38 -the executable, \emph{including the file name}. Sledgehammer has been tested
    1.39 -with Alt-Ergo 0.93, CVC3 2.2 and 2.4.1, Yices 1.0.28 and 1.0.33, and Z3 3.0,
    1.40 -3.1, 3.2, and 4.0. Since the SMT solvers' output formats are somewhat unstable,
    1.41 -other versions of the solvers might not work well with Sledgehammer. Ideally,
    1.42 -also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or
    1.43 -\texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.0'').
    1.44 +the executable, \emph{including the file name};
    1.45 +for Alt-Ergo, set the
    1.46 +environment variable \texttt{WHY3\_HOME} to the directory that contains the
    1.47 +\texttt{why3} executable.
    1.48 +Sledgehammer has been tested with Alt-Ergo 0.93 and 0.94, CVC3 2.2 and 2.4.1,
    1.49 +Yices 1.0.28 and 1.0.33, and Z3 3.0 to 4.0. Since the SMT solvers' output
    1.50 +formats are somewhat unstable, other versions of the solvers might not work well
    1.51 +with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION},
    1.52 +\texttt{YICES\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number
    1.53 +(e.g., ``4.0'').
    1.54  \end{enum}
    1.55  \end{sloppy}
    1.56  
    1.57 @@ -472,8 +475,8 @@
    1.58  Since the steps are fairly small, \textit{metis} is more likely to be able to
    1.59  replay them.
    1.60  
    1.61 -\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It
    1.62 -is usually stronger, but you need to either have Z3 available to replay the
    1.63 +\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}.
    1.64 +It is usually stronger, but you need to either have Z3 available to replay the
    1.65  proofs, trust the SMT solver, or use certificates. See the documentation in the
    1.66  \emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details.
    1.67  
    1.68 @@ -970,12 +973,11 @@
    1.69  with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
    1.70  \end{enum}
    1.71  
    1.72 -By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
    1.73 -the SMT module's \textit{smt\_solver} configuration option is set to), and (if
    1.74 -appropriate) Waldmeister in parallel---either locally or remotely, depending on
    1.75 -the number of processor cores available. For historical reasons, the default
    1.76 -value of this option can be overridden using the option ``Sledgehammer:
    1.77 -Provers'' in Proof General's ``Isabelle'' menu.
    1.78 +By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
    1.79 +Yices, Z3, and (if appropriate) Waldmeister in parallel---either locally or
    1.80 +remotely, depending on the number of processor cores available. For historical
    1.81 +reasons, the default value of this option can be overridden using the option
    1.82 +``Sledgehammer: Provers'' in Proof General's ``Isabelle'' menu.
    1.83  
    1.84  It is generally a good idea to run several provers in parallel. Running E,
    1.85  SPASS, and Vampire for 5~seconds yields a similar success rate to running the

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -29,6 +29,10 @@
     2.4  open Sledgehammer_MaSh
     2.5  open Sledgehammer_Run
     2.6  
     2.7 +val cvc3N = "cvc3"
     2.8 +val yicesN = "yices"
     2.9 +val z3N = "z3"
    2.10 +
    2.11  val runN = "run"
    2.12  val minN = "min"
    2.13  val messagesN = "messages"
    2.14 @@ -220,10 +224,9 @@
    2.15  val max_default_remote_threads = 4
    2.16  
    2.17  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    2.18 -   timeout, it makes sense to put SPASS first. *)
    2.19 +   timeout, it makes sense to put E first. *)
    2.20  fun default_provers_param_value ctxt =
    2.21 -  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN,
    2.22 -   waldmeisterN]
    2.23 +  [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N]
    2.24    |> map_filter (remotify_prover_if_not_installed ctxt)
    2.25    |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
    2.26                                    max_default_remote_threads)