# HG changeset patch # User blanchet # Date 1402585323 -7200 # Node ID bc51864c2ac47f44c3f86ed9f3c72c2a4bf5f738 # Parent 2eb14982cd291f194527ed5b6a323b048bc0d93c took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale diff -r 2eb14982cd29 -r bc51864c2ac4 NEWS --- a/NEWS Thu Jun 12 17:02:02 2014 +0200 +++ b/NEWS Thu Jun 12 17:02:03 2014 +0200 @@ -382,7 +382,9 @@ * SMT module: * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g., 4.3). The new proof method is - called "smt2". + called "smt2". CVC3 is also supported as an oracle. Yices is no longer + supported, because no version of the solver can handle both SMT-LIB 2 and + quantifiers. * Sledgehammer: - New prover "z3_new" with support for Isar proofs diff -r 2eb14982cd29 -r bc51864c2ac4 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Jun 12 17:02:02 2014 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Jun 12 17:02:03 2014 +0200 @@ -110,9 +110,9 @@ \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, -a selection of the SMT solvers CVC3 \cite{cvc3}, Yices \cite{yices}, and Z3 -\cite{z3} are run by default; these are run either locally or (for CVC3 and Z3) -on a server at the TU M\"unchen. +a selection of the SMT solvers CVC3 \cite{cvc3} and Z3 \cite{z3} are run by +default; 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 @@ -157,8 +157,8 @@ be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, iProver, iProver-Eq, LEO-II, Satallax, SNARK, Vampire, and Waldmeister are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you -should at least install E and SPASS locally. The SMT solvers CVC3, Yices, and Z3 -can be run locally. +should at least install E and SPASS locally. The SMT solvers CVC3 and Z3 can be +run locally. There are three main ways to install automatic provers on your machine: @@ -166,8 +166,8 @@ \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.% -\footnote{Vampire's and Yices's licenses prevent us from doing the same for -these otherwise remarkable tools.} +\footnote{Vampire's license prevents us from doing the same for +this otherwise remarkable tool.} For Z3, you must additionally set the variable \texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a noncommercial user---either in the environment in which Isabelle is @@ -214,17 +214,13 @@ \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0''). Similarly, if you want to build CVC3, or found a -Yices or Z3 executable somewhere (e.g., -\url{http://yices.csl.sri.com/download.shtml} or -\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 CVC3 2.2 and 2.4.1, -Yices 1.0.28 and 1.0.33, and Z3 4.3.2. 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\_NEW\_VERSION} to the solver's version +Z3 executable somewhere (e.g., \url{http://z3.codeplex.com/}), +set the environment variable \texttt{CVC3\_\allowbreak SOLVER} +or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including +the file name}. Sledgehammer has been tested with CVC3 2.2 and 2.4.1 and Z3 +4.3.2. 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} or \texttt{Z3\_NEW\_VERSION} to the solver's version number (e.g., ``4.3.2''). \end{enum} \end{sloppy} @@ -570,12 +566,11 @@ that can be guessed from the number of facts in the original proof and the time it took to find or preplay it). -In addition, some provers (e.g., Yices) do not provide proofs or sometimes -produce incomplete proofs. The minimizer is then invoked to find out which facts -are actually needed from the (large) set of facts that was initially given to -the prover. Finally, if a prover returns a proof with lots of facts, the -minimizer is invoked automatically since Metis would be unlikely to re-find the -proof. +In addition, some provers do not provide proofs or sometimes produce incomplete +proofs. The minimizer is then invoked to find out which facts are actually needed +from the (large) set of facts that was initially given to the prover. Finally, +if a prover returns a proof with lots of facts, the minimizer is invoked +automatically since Metis would be unlikely to re-find the proof. % Automatic minimization can be forced or disabled using the \textit{minimize} option (\S\ref{mode-of-operation}). @@ -899,11 +894,6 @@ ``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0. Versions strictly above 1.8 support the TPTP typed first-order format (TFF0). -\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at -SRI \cite{yices}. To use Yices, set the environment variable -\texttt{YICES\_SOLVER} to the complete path of the executable, including the -file name. Sledgehammer has been tested with version 1.0.28. - \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at Microsoft Research \cite{z3}. To use Z3, set the environment variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable, including the file @@ -977,8 +967,8 @@ \end{enum} By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire, -Yices, and Z3 in parallel---either locally or remotely, depending on the number -of processor cores available. +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 diff -r 2eb14982cd29 -r bc51864c2ac4 src/HOL/SMT2.thy --- a/src/HOL/SMT2.thy Thu Jun 12 17:02:02 2014 +0200 +++ b/src/HOL/SMT2.thy Thu Jun 12 17:02:03 2014 +0200 @@ -162,9 +162,9 @@ solver. The possible values can be obtained from the @{text smt2_status} command. -Due to licensing restrictions, Yices and Z3 are not installed/enabled -by default. Z3 is free for non-commercial applications and can be enabled -by setting Isabelle system option @{text z3_non_commercial} to @{text yes}. +Due to licensing restrictions, Z3 is not enabled by default. Z3 is free +for non-commercial applications and can be enabled by setting Isabelle +system option @{text z3_non_commercial} to @{text yes}. *} declare [[smt2_solver = z3]] @@ -200,7 +200,6 @@ *} declare [[cvc3_new_options = ""]] -declare [[yices_new_options = ""]] declare [[z3_new_options = ""]] text {* diff -r 2eb14982cd29 -r bc51864c2ac4 src/HOL/Tools/SMT2/smt2_systems.ML --- a/src/HOL/Tools/SMT2/smt2_systems.ML Thu Jun 12 17:02:02 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML Thu Jun 12 17:02:03 2014 +0200 @@ -62,24 +62,6 @@ end -(* Yices *) - -val yices: SMT2_Solver.solver_config = { - name = "yices", - class = K SMTLIB2_Interface.smtlib2C, - avail = make_avail "YICES", - command = make_command "YICES", - options = (fn ctxt => [ - "--rand-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed), - "--timeout=" ^ - string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)), - "--smtlib"]), - default_max_relevant = 350 (* FUDGE *), - outcome = on_first_nontrivial_line (outcome_of "unsat" "sat" "unknown"), - parse_proof = NONE, - replay = NONE } - - (* Z3 *) datatype z3_non_commercial = @@ -152,7 +134,6 @@ val _ = Theory.setup ( SMT2_Solver.add_solver cvc3 #> - SMT2_Solver.add_solver yices #> SMT2_Solver.add_solver z3) end; diff -r 2eb14982cd29 -r bc51864c2ac4 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jun 12 17:02:02 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jun 12 17:02:03 2014 +0200 @@ -28,7 +28,6 @@ open Sledgehammer (* val cvc3N = "cvc3" *) -val yicesN = "yices" val z3N = "z3" val runN = "run" @@ -204,15 +203,13 @@ end fun remotify_prover_if_not_installed ctxt name = - if is_prover_supported ctxt name andalso is_prover_installed ctxt name then - SOME name - else - remotify_prover_if_supported_and_not_already_remote ctxt name + if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name + else remotify_prover_if_supported_and_not_already_remote ctxt name (* The first ATP of the list is used by Auto Sledgehammer. Because of the low timeout, it makes sense to put E first. *) fun default_provers_param_value mode ctxt = - [eN, spassN, z3N, e_sineN, vampireN, yicesN] + [eN, spassN, z3N, e_sineN, vampireN] |> 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))