# HG changeset patch # User blanchet # Date 1342815586 -7200 # Node ID 7682bc885e8aab076df6edfc2b5cb238479dd80f # Parent 0a261b4aa093534a7dc05d0a9dfaf4cd5ac78122 use CVC3 and Yices by default if they are available and there are enough cores diff -r 0a261b4aa093 -r 7682bc885e8a doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Fri Jul 20 22:19:46 2012 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Jul 20 22:19:46 2012 +0200 @@ -106,10 +106,10 @@ SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via the System\-On\-TPTP web service -\cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is -used by default, and you can tell Sledgehammer to try Alt-Ergo \cite{alt-ergo}, -CVC3 \cite{cvc3}, and Yices \cite{yices} as well; these are run either locally -or (for CVC3 and Z3) on a server at the TU M\"unchen. +\cite{sutcliffe-2000}. In addition to the ATPs, a selection of the SMT solvers +CVC3 \cite{cvc3}, Yices \cite{yices}, and Z3 \cite{z3} are run by default, and +you can tell Sledgehammer to try Alt-Ergo \cite{alt-ergo} as well; these are run +either locally or (for CVC3 and Z3) on a server at the TU M\"unchen. The problem passed to the automatic provers consists of your current goal together with a heuristic selection of hundreds of facts (theorems) from the @@ -161,11 +161,10 @@ \cite{sutcliffe-2000}. If you want better performance, you should at least install E and SPASS locally. -Among the SMT solvers, Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and -CVC3 and Z3 can be run remotely on a TU M\"unchen server. If you want better -performance and get the ability to replay proofs that rely on the \emph{smt} -proof method without an Internet connection, you should at least install Z3 -locally. +The SMT solvers Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and CVC3 and +Z3 can be run remotely on a TU M\"unchen server. If you want better performance +and get the ability to replay proofs that rely on the \emph{smt} proof method +without an Internet connection, you should at least have Z3 locally installed. There are three main ways to install automatic provers on your machine: @@ -220,12 +219,16 @@ \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}), set the environment variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of -the executable, \emph{including the file name}. Sledgehammer has been tested -with Alt-Ergo 0.93, CVC3 2.2 and 2.4.1, Yices 1.0.28 and 1.0.33, and Z3 3.0, -3.1, 3.2, and 4.0. Since the SMT solvers' output formats are somewhat unstable, -other versions of the solvers might not work well with Sledgehammer. Ideally, -also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or -\texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.0''). +the executable, \emph{including the file name}; +for Alt-Ergo, set the +environment variable \texttt{WHY3\_HOME} to the directory that contains the +\texttt{why3} executable. +Sledgehammer has been tested with Alt-Ergo 0.93 and 0.94, CVC3 2.2 and 2.4.1, +Yices 1.0.28 and 1.0.33, and Z3 3.0 to 4.0. Since the SMT solvers' output +formats are somewhat unstable, other versions of the solvers might not work well +with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION}, +\texttt{YICES\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number +(e.g., ``4.0''). \end{enum} \end{sloppy} @@ -472,8 +475,8 @@ Since the steps are fairly small, \textit{metis} is more likely to be able to replay them. -\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It -is usually stronger, but you need to either have Z3 available to replay the +\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. +It is usually stronger, but you need to either have Z3 available to replay the proofs, trust the SMT solver, or use certificates. See the documentation in the \emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details. @@ -970,12 +973,11 @@ with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers. \end{enum} -By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever -the SMT module's \textit{smt\_solver} configuration option is set to), and (if -appropriate) Waldmeister in parallel---either locally or remotely, depending on -the number of processor cores available. For historical reasons, the default -value of this option can be overridden using the option ``Sledgehammer: -Provers'' in Proof General's ``Isabelle'' menu. +By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire, +Yices, Z3, and (if appropriate) Waldmeister in parallel---either locally or +remotely, depending on the number of processor cores available. For historical +reasons, the default value of this option can be overridden using the option +``Sledgehammer: Provers'' in Proof General's ``Isabelle'' menu. 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 diff -r 0a261b4aa093 -r 7682bc885e8a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200 @@ -29,6 +29,10 @@ open Sledgehammer_MaSh open Sledgehammer_Run +val cvc3N = "cvc3" +val yicesN = "yices" +val z3N = "z3" + val runN = "run" val minN = "min" val messagesN = "messages" @@ -220,10 +224,9 @@ val max_default_remote_threads = 4 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low - timeout, it makes sense to put SPASS first. *) + timeout, it makes sense to put E first. *) fun default_provers_param_value ctxt = - [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, - waldmeisterN] + [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N] |> map_filter (remotify_prover_if_not_installed ctxt) |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), max_default_remote_threads)