--- 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
--- 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
--- 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 {*
--- 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;
--- 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))