took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
authorblanchet
Thu Jun 12 17:02:03 2014 +0200 (2014-06-12)
changeset 57237bc51864c2ac4
parent 57236 2eb14982cd29
child 57238 7e2658f2e77d
took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
NEWS
src/Doc/Sledgehammer/document/root.tex
src/HOL/SMT2.thy
src/HOL/Tools/SMT2/smt2_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
     1.1 --- a/NEWS	Thu Jun 12 17:02:02 2014 +0200
     1.2 +++ b/NEWS	Thu Jun 12 17:02:03 2014 +0200
     1.3 @@ -382,7 +382,9 @@
     1.4  * SMT module:
     1.5    * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
     1.6      and supports recent versions of Z3 (e.g., 4.3). The new proof method is
     1.7 -    called "smt2".
     1.8 +    called "smt2". CVC3 is also supported as an oracle. Yices is no longer
     1.9 +    supported, because no version of the solver can handle both SMT-LIB 2 and
    1.10 +    quantifiers.
    1.11  
    1.12  * Sledgehammer:
    1.13    - New prover "z3_new" with support for Isar proofs
     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Thu Jun 12 17:02:02 2014 +0200
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jun 12 17:02:03 2014 +0200
     2.3 @@ -110,9 +110,9 @@
     2.4  \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and
     2.5  Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via
     2.6  the System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs,
     2.7 -a selection of the SMT solvers CVC3 \cite{cvc3}, Yices \cite{yices}, and Z3
     2.8 -\cite{z3} are run by default; these are run either locally or (for CVC3 and Z3)
     2.9 -on a server at the TU M\"unchen.
    2.10 +a selection of the SMT solvers CVC3 \cite{cvc3} and Z3 \cite{z3} are run by
    2.11 +default; these are run either locally or (for CVC3 and Z3) on a server at the
    2.12 +TU M\"unchen.
    2.13  
    2.14  The problem passed to the automatic provers consists of your current goal
    2.15  together with a heuristic selection of hundreds of facts (theorems) from the
    2.16 @@ -157,8 +157,8 @@
    2.17  be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, iProver, iProver-Eq,
    2.18  LEO-II, Satallax, SNARK, Vampire, and Waldmeister are available remotely via
    2.19  System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you
    2.20 -should at least install E and SPASS locally. The SMT solvers CVC3, Yices, and Z3
    2.21 -can be run locally.
    2.22 +should at least install E and SPASS locally. The SMT solvers CVC3 and Z3 can be
    2.23 +run locally.
    2.24  
    2.25  There are three main ways to install automatic provers on your machine:
    2.26  
    2.27 @@ -166,8 +166,8 @@
    2.28  \begin{enum}
    2.29  \item[\labelitemi] If you installed an official Isabelle package, it should
    2.30  already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%
    2.31 -\footnote{Vampire's and Yices's licenses prevent us from doing the same for
    2.32 -these otherwise remarkable tools.}
    2.33 +\footnote{Vampire's license prevents us from doing the same for
    2.34 +this otherwise remarkable tool.}
    2.35  For Z3, you must additionally set the variable
    2.36  \texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
    2.37  noncommercial user---either in the environment in which Isabelle is
    2.38 @@ -214,17 +214,13 @@
    2.39  \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0'').
    2.40  
    2.41  Similarly, if you want to build CVC3, or found a
    2.42 -Yices or Z3 executable somewhere (e.g.,
    2.43 -\url{http://yices.csl.sri.com/download.shtml} or
    2.44 -\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),
    2.45 -set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
    2.46 -\texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of
    2.47 -the executable, \emph{including the file name}.
    2.48 -Sledgehammer has been tested with CVC3 2.2 and 2.4.1,
    2.49 -Yices 1.0.28 and 1.0.33, and Z3 4.3.2. Since the SMT solvers' output
    2.50 -formats are somewhat unstable, other versions of the solvers might not work well
    2.51 -with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION},
    2.52 -\texttt{YICES\_VERSION}, or \texttt{Z3\_NEW\_VERSION} to the solver's version
    2.53 +Z3 executable somewhere (e.g., \url{http://z3.codeplex.com/}),
    2.54 +set the environment variable \texttt{CVC3\_\allowbreak SOLVER}
    2.55 +or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including
    2.56 +the file name}. Sledgehammer has been tested with CVC3 2.2 and 2.4.1 and Z3
    2.57 +4.3.2. Since the SMT solvers' output formats are somewhat unstable, other
    2.58 +versions of the solvers might not work well with Sledgehammer. Ideally, also set
    2.59 +\texttt{CVC3\_VERSION} or \texttt{Z3\_NEW\_VERSION} to the solver's version
    2.60  number (e.g., ``4.3.2'').
    2.61  \end{enum}
    2.62  \end{sloppy}
    2.63 @@ -570,12 +566,11 @@
    2.64  that can be guessed from the number of facts in the original proof and the time
    2.65  it took to find or preplay it).
    2.66  
    2.67 -In addition, some provers (e.g., Yices) do not provide proofs or sometimes
    2.68 -produce incomplete proofs. The minimizer is then invoked to find out which facts
    2.69 -are actually needed from the (large) set of facts that was initially given to
    2.70 -the prover. Finally, if a prover returns a proof with lots of facts, the
    2.71 -minimizer is invoked automatically since Metis would be unlikely to re-find the
    2.72 -proof.
    2.73 +In addition, some provers do not provide proofs or sometimes produce incomplete
    2.74 +proofs. The minimizer is then invoked to find out which facts are actually needed
    2.75 +from the (large) set of facts that was initially given to the prover. Finally,
    2.76 +if a prover returns a proof with lots of facts, the minimizer is invoked
    2.77 +automatically since Metis would be unlikely to re-find the proof.
    2.78  %
    2.79  Automatic minimization can be forced or disabled using the \textit{minimize}
    2.80  option (\S\ref{mode-of-operation}).
    2.81 @@ -899,11 +894,6 @@
    2.82  ``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0.
    2.83  Versions strictly above 1.8 support the TPTP typed first-order format (TFF0).
    2.84  
    2.85 -\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
    2.86 -SRI \cite{yices}. To use Yices, set the environment variable
    2.87 -\texttt{YICES\_SOLVER} to the complete path of the executable, including the
    2.88 -file name. Sledgehammer has been tested with version 1.0.28.
    2.89 -
    2.90  \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
    2.91  Microsoft Research \cite{z3}. To use Z3, set the environment variable
    2.92  \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable, including the file
    2.93 @@ -977,8 +967,8 @@
    2.94  \end{enum}
    2.95  
    2.96  By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
    2.97 -Yices, and Z3 in parallel---either locally or remotely, depending on the number
    2.98 -of processor cores available.
    2.99 +and Z3 in parallel---either locally or remotely, depending on the number of
   2.100 +processor cores available.
   2.101  
   2.102  It is generally a good idea to run several provers in parallel. Running E,
   2.103  SPASS, and Vampire for 5~seconds yields a similar success rate to running the
     3.1 --- a/src/HOL/SMT2.thy	Thu Jun 12 17:02:02 2014 +0200
     3.2 +++ b/src/HOL/SMT2.thy	Thu Jun 12 17:02:03 2014 +0200
     3.3 @@ -162,9 +162,9 @@
     3.4  solver.  The possible values can be obtained from the @{text smt2_status}
     3.5  command.
     3.6  
     3.7 -Due to licensing restrictions, Yices and Z3 are not installed/enabled
     3.8 -by default.  Z3 is free for non-commercial applications and can be enabled
     3.9 -by setting Isabelle system option @{text z3_non_commercial} to @{text yes}.
    3.10 +Due to licensing restrictions, Z3 is not enabled by default.  Z3 is free
    3.11 +for non-commercial applications and can be enabled by setting Isabelle
    3.12 +system option @{text z3_non_commercial} to @{text yes}.
    3.13  *}
    3.14  
    3.15  declare [[smt2_solver = z3]]
    3.16 @@ -200,7 +200,6 @@
    3.17  *}
    3.18  
    3.19  declare [[cvc3_new_options = ""]]
    3.20 -declare [[yices_new_options = ""]]
    3.21  declare [[z3_new_options = ""]]
    3.22  
    3.23  text {*
     4.1 --- a/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 17:02:02 2014 +0200
     4.2 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 17:02:03 2014 +0200
     4.3 @@ -62,24 +62,6 @@
     4.4  end
     4.5  
     4.6  
     4.7 -(* Yices *)
     4.8 -
     4.9 -val yices: SMT2_Solver.solver_config = {
    4.10 -  name = "yices",
    4.11 -  class = K SMTLIB2_Interface.smtlib2C,
    4.12 -  avail = make_avail "YICES",
    4.13 -  command = make_command "YICES",
    4.14 -  options = (fn ctxt => [
    4.15 -    "--rand-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
    4.16 -    "--timeout=" ^
    4.17 -      string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
    4.18 -    "--smtlib"]),
    4.19 -  default_max_relevant = 350 (* FUDGE *),
    4.20 -  outcome = on_first_nontrivial_line (outcome_of "unsat" "sat" "unknown"),
    4.21 -  parse_proof = NONE,
    4.22 -  replay = NONE }
    4.23 -
    4.24 -
    4.25  (* Z3 *)
    4.26  
    4.27  datatype z3_non_commercial =
    4.28 @@ -152,7 +134,6 @@
    4.29  
    4.30  val _ = Theory.setup (
    4.31    SMT2_Solver.add_solver cvc3 #>
    4.32 -  SMT2_Solver.add_solver yices #>
    4.33    SMT2_Solver.add_solver z3)
    4.34  
    4.35  end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jun 12 17:02:02 2014 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jun 12 17:02:03 2014 +0200
     5.3 @@ -28,7 +28,6 @@
     5.4  open Sledgehammer
     5.5  
     5.6  (* val cvc3N = "cvc3" *)
     5.7 -val yicesN = "yices"
     5.8  val z3N = "z3"
     5.9  
    5.10  val runN = "run"
    5.11 @@ -204,15 +203,13 @@
    5.12      end
    5.13  
    5.14  fun remotify_prover_if_not_installed ctxt name =
    5.15 -  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
    5.16 -    SOME name
    5.17 -  else
    5.18 -    remotify_prover_if_supported_and_not_already_remote ctxt name
    5.19 +  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
    5.20 +  else remotify_prover_if_supported_and_not_already_remote ctxt name
    5.21  
    5.22  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    5.23     timeout, it makes sense to put E first. *)
    5.24  fun default_provers_param_value mode ctxt =
    5.25 -  [eN, spassN, z3N, e_sineN, vampireN, yicesN]
    5.26 +  [eN, spassN, z3N, e_sineN, vampireN]
    5.27    |> map_filter (remotify_prover_if_not_installed ctxt)
    5.28    (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
    5.29    |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))