merged
authornipkow
Thu, 12 Jun 2014 18:47:27 +0200
changeset 57248 5496011859eb
parent 57246 62746a41cc0c (diff)
parent 57247 8191ccf6a1bd (current diff)
child 57249 5c75baf68b77
merged
src/HOL/List.thy
--- a/NEWS	Thu Jun 12 18:47:16 2014 +0200
+++ b/NEWS	Thu Jun 12 18:47:27 2014 +0200
@@ -382,10 +382,12 @@
 * 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 and CVC4 are also supported as oracles. 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
+  - Z3 can now produce Isar proofs.
   - MaSh overhaul:
       - New SML-based learning engines eliminate the dependency on Python
         and increase performance and reliability.
@@ -397,8 +399,8 @@
   - New option:
       smt_proofs
   - Renamed options:
-      isar_compress ~> compress_isar
-      isar_try0 ~> try0_isar
+      isar_compress ~> compress
+      isar_try0 ~> try0
     INCOMPATIBILITY.
 
 * Metis:
--- a/src/Doc/Nitpick/document/root.tex	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/Doc/Nitpick/document/root.tex	Thu Jun 12 18:47:27 2014 +0200
@@ -1745,8 +1745,8 @@
 The options are categorized as follows:\ mode of operation
 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
 format (\S\ref{output-format}), automatic counterexample checks
-(\S\ref{authentication}), optimizations
-(\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
+(\S\ref{authentication}), regression testing (\S\ref{regression-testing}),
+optimizations (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
 
 If you use Isabelle/jEdit, Nitpick also provides an automatic mode that can
 be enabled via the ``Auto Nitpick'' option under ``Plugins > Plugin Options
@@ -2186,6 +2186,9 @@
 \nopagebreak
 {\small See also \textit{max\_genuine} (\S\ref{output-format}).}
 
+\subsection{Regression Testing}
+\label{regression-testing}
+
 \opnodefault{expect}{string}
 Specifies the expected outcome, which must be one of the following:
 
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jun 12 18:47:27 2014 +0200
@@ -109,13 +109,12 @@
 \cite{leo2}, Satallax \cite{satallax}, 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,
-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.
+the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT
+solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, and Z3 \cite{z3}. These are
+always run locally.
 
-The problem passed to the automatic provers consists of your current goal
-together with a heuristic selection of hundreds of facts (theorems) from the
+The problem passed to the external provers (or solvers) consists of your current
+goal together with a heuristic selection of hundreds of facts (theorems) from the
 current theory context, filtered by relevance.
 
 The result of a successful proof search is some source text that usually (but
@@ -157,7 +156,7 @@
 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
+should at least install E and SPASS locally. The SMT solvers CVC3, CVC4, and Z3
 can be run locally.
 
 There are three main ways to install automatic provers on your machine:
@@ -166,8 +165,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
@@ -213,19 +212,16 @@
 \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
 \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}),
+Similarly, if you want to build CVC3 or CVC4, or found a
+Z3 executable somewhere (e.g., \url{http://z3.codeplex.com/}),
 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
-number (e.g., ``4.3.2'').
+\texttt{CVC4\_\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, CVC4 1.2, and Z3 4.3.2. Since Z3's output format is
+somewhat unstable, other versions of the solver might not work well with
+Sledgehammer. Ideally, also set
+\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, or \texttt{Z3\_NEW\_VERSION} to
+the solver's version number (e.g., ``4.3.2'').
 \end{enum}
 \end{sloppy}
 
@@ -356,7 +352,7 @@
 \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
 that Isar proofs should be generated, in addition to one-line \textit{metis} or
 \textit{smt2} proofs. The length of the Isar proofs can be controlled by setting
-\textit{compress\_isar} (\S\ref{output-format}).
+\textit{compress} (\S\ref{output-format}).
 
 \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
@@ -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}).
@@ -775,8 +770,8 @@
 Sledgehammer's options are categorized as follows:\ mode of operation
 (\S\ref{mode-of-operation}), problem encoding (\S\ref{problem-encoding}),
 relevance filter (\S\ref{relevance-filter}), output format
-(\S\ref{output-format}), authentication (\S\ref{authentication}), and timeouts
-(\S\ref{timeouts}).
+(\S\ref{output-format}), regression testing (\S\ref{regression-testing}),
+and timeouts (\S\ref{timeouts}).
 
 The descriptions below refer to the following syntactic quantities:
 
@@ -829,7 +824,13 @@
 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
 executable, including the file name, or install the prebuilt CVC3 package from
-\download. Sledgehammer has been tested with version 2.2 and 2.4.1.
+\download. Sledgehammer has been tested with versions 2.2 and 2.4.1.
+
+\item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to
+CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the
+complete path of the executable, including the file name, or install the
+prebuilt CVC4 package from \download. Sledgehammer has been tested with version
+1.2.
 
 \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
 developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
@@ -899,11 +900,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 +973,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
@@ -1328,15 +1324,15 @@
 one-line proofs. If the option is set to \textit{smart} (the default), Isar
 proofs are only generated when no working one-line proof is available.
 
-\opdefault{compress\_isar}{int}{\upshape 10}
+\opdefault{compress}{int}{\upshape 10}
 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
 is explicitly enabled. A value of $n$ indicates that each Isar proof step should
 correspond to a group of up to $n$ consecutive proof steps in the ATP proof.
 
-\optrueonly{dont\_compress\_isar}
-Alias for ``\textit{compress\_isar} = 0''.
+\optrueonly{dont\_compress}
+Alias for ``\textit{compress} = 0''.
 
-\optrue{try0\_isar}{dont\_try0\_isar}
+\optrue{try0}{dont\_try0}
 Specifies whether standard proof methods such as \textit{auto} and
 \textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
 The collection of methods is roughly the same as for the \textbf{try0} command.
@@ -1348,8 +1344,8 @@
 proofs.
 \end{enum}
 
-\subsection{Authentication}
-\label{authentication}
+\subsection{Regression Testing}
+\label{regression-testing}
 
 \begin{enum}
 \opnodefault{expect}{string}
--- a/src/Doc/manual.bib	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/Doc/manual.bib	Thu Jun 12 18:47:27 2014 +0200
@@ -193,6 +193,26 @@
   year      = {2007}
 }
 
+@inproceedings{cvc4,
+  author    = {Clark Barrett and
+               Christopher L. Conway and
+               Morgan Deters and
+               Liana Hadarean and
+               Dejan Jovanovic and
+               Tim King and
+               Andrew Reynolds and
+               Cesare Tinelli},
+  title     = {{CVC4}},
+  booktitle = {CAV 2011},
+  pages     = {171--177},
+  editor    = {Ganesh Gopalakrishnan and
+               Shaz Qadeer},
+  publisher = {Springer},
+  series    = LNCS,
+  volume    = {6806},
+  year      = {2011}
+}
+
 @incollection{basin91,
   author	= {David Basin and Matt Kaufmann},
   title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
--- a/src/HOL/List.thy	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/List.thy	Thu Jun 12 18:47:27 2014 +0200
@@ -5,7 +5,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports Sledgehammer Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
+imports Sledgehammer Code_Numeral Lifting_Set Lifting_Option Lifting_Product
 begin
 
 datatype_new (set: 'a) list =
--- a/src/HOL/Metis_Examples/Big_O.thy	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Jun 12 18:47:27 2014 +0200
@@ -29,7 +29,7 @@
 
 (*** Now various verions with an increasing shrink factor ***)
 
-sledgehammer_params [isar_proofs, compress_isar = 1]
+sledgehammer_params [isar_proofs, compress = 1]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -60,7 +60,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 2]
+sledgehammer_params [isar_proofs, compress = 2]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -83,7 +83,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 3]
+sledgehammer_params [isar_proofs, compress = 3]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -103,7 +103,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 4]
+sledgehammer_params [isar_proofs, compress = 4]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -123,7 +123,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 1]
+sledgehammer_params [isar_proofs, compress = 1]
 
 lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
 by (auto simp add: bigo_def bigo_pos_const)
--- a/src/HOL/Metis_Examples/Sets.thy	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Metis_Examples/Sets.thy	Thu Jun 12 18:47:27 2014 +0200
@@ -21,7 +21,7 @@
 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
 by metis
 
-sledgehammer_params [isar_proofs, compress_isar = 1]
+sledgehammer_params [isar_proofs, compress = 1]
 
 (*multiple versions of this example*)
 lemma (*equal_union: *)
@@ -70,7 +70,7 @@
   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 2]
+sledgehammer_params [isar_proofs, compress = 2]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -107,7 +107,7 @@
   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 3]
+sledgehammer_params [isar_proofs, compress = 3]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -124,7 +124,7 @@
   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 4]
+sledgehammer_params [isar_proofs, compress = 4]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -140,7 +140,7 @@
   ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
 qed
 
-sledgehammer_params [isar_proofs, compress_isar = 1]
+sledgehammer_params [isar_proofs, compress = 1]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
--- a/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Jun 12 18:47:27 2014 +0200
@@ -44,7 +44,7 @@
 
 lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer [isar_proofs, compress_isar = 2] *)
+(* sledgehammer [isar_proofs, compress = 2] *)
 proof -
   assume A1: "f c = Intg x"
   assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
--- a/src/HOL/Nitpick.thy	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Nitpick.thy	Thu Jun 12 18:47:27 2014 +0200
@@ -8,7 +8,7 @@
 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
 
 theory Nitpick
-imports BNF_FP_Base Map Record
+imports Record
 keywords
   "nitpick" :: diag and
   "nitpick_params" :: thy_decl
--- a/src/HOL/Random.thy	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Random.thy	Thu Jun 12 18:47:27 2014 +0200
@@ -4,7 +4,7 @@
 header {* A HOL random engine *}
 
 theory Random
-imports Code_Numeral List
+imports List
 begin
 
 notation fcomp (infixl "\<circ>>" 60)
--- a/src/HOL/SMT2.thy	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/SMT2.thy	Thu Jun 12 18:47:27 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,7 @@
 *}
 
 declare [[cvc3_new_options = ""]]
-declare [[yices_new_options = ""]]
+declare [[cvc4_new_options = ""]]
 declare [[z3_new_options = ""]]
 
 text {*
--- a/src/HOL/Sledgehammer.thy	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Jun 12 18:47:27 2014 +0200
@@ -7,7 +7,7 @@
 header {* Sledgehammer: Isabelle--ATP Linkup *}
 
 theory Sledgehammer
-imports Presburger ATP SMT2
+imports Presburger SMT2
 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
 begin
 
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -20,6 +20,7 @@
      avail: unit -> bool,
      command: unit -> string list,
      options: Proof.context -> string list,
+     smt_options: (string * string) list,
      default_max_relevant: int,
      outcome: string -> string list -> outcome * string list,
      parse_proof: (Proof.context -> SMT2_Translate.replay_data ->
@@ -118,7 +119,7 @@
 
 in
 
-fun invoke name command ithms ctxt =
+fun invoke name command smt_options ithms ctxt =
   let
     val options = SMT2_Config.solver_options_of ctxt
     val comments = [space_implode " " options]
@@ -126,7 +127,7 @@
     val (str, replay_data as {context = ctxt', ...}) =
       ithms
       |> tap (trace_assms ctxt)
-      |> SMT2_Translate.translate ctxt comments
+      |> SMT2_Translate.translate ctxt smt_options comments
       ||> tap trace_replay_data
   in (run_solver ctxt' name (make_command command options) str, replay_data) end
 
@@ -148,6 +149,7 @@
    avail: unit -> bool,
    command: unit -> string list,
    options: Proof.context -> string list,
+   smt_options: (string * string) list,
    default_max_relevant: int,
    outcome: string -> string list -> outcome * string list,
    parse_proof: (Proof.context -> SMT2_Translate.replay_data ->
@@ -172,6 +174,7 @@
 
 type solver_info = {
   command: unit -> string list,
+  smt_options: (string * string) list,
   default_max_relevant: int,
   parse_proof: Proof.context -> SMT2_Translate.replay_data ->
     ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
@@ -207,11 +210,12 @@
   val cfalse = Thm.cterm_of @{theory} @{prop False}
 in
 
-fun add_solver ({name, class, avail, command, options, default_max_relevant, outcome,
+fun add_solver ({name, class, avail, command, options, smt_options, default_max_relevant, outcome,
     parse_proof = parse_proof0, replay = replay0} : solver_config) =
   let
     fun solver oracle = {
       command = command,
+      smt_options = smt_options,
       default_max_relevant = default_max_relevant,
       parse_proof = parse_proof (outcome name) parse_proof0,
       replay = replay (outcome name) replay0 oracle}
@@ -236,8 +240,9 @@
 fun apply_solver_and_replay ctxt thms0 =
   let
     val thms = map (check_topsort ctxt) thms0
-    val (name, {command, replay, ...}) = name_and_info_of ctxt
-    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt thms) ctxt
+    val (name, {command, smt_options, replay, ...}) = name_and_info_of ctxt
+    val (output, replay_data) =
+      invoke name command smt_options (SMT2_Normalize.normalize ctxt thms) ctxt
   in replay ctxt replay_data output end
 
 
@@ -259,8 +264,9 @@
     val thms = conjecture :: prems @ facts
     val thms' = map (check_topsort ctxt) thms
 
-    val (name, {command, parse_proof, ...}) = name_and_info_of ctxt
-    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt thms') ctxt
+    val (name, {command, smt_options, parse_proof, ...}) = name_and_info_of ctxt
+    val (output, replay_data) =
+      invoke name command smt_options (SMT2_Normalize.normalize ctxt thms') ctxt
   in
     parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output
   end
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -33,9 +33,8 @@
 
 fun on_first_line test_outcome solver_name lines =
   let
-    val empty_line = (fn "" => true | _ => false)
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
-    val (l, ls) = split_first (snd (take_prefix empty_line lines))
+    val (l, ls) = split_first (snd (take_prefix (curry (op =) "") lines))
   in (test_outcome solver_name l, ls) end
 
 
@@ -44,7 +43,7 @@
 local
   fun cvc3_options ctxt = [
     "-seed", string_of_int (Config.get ctxt SMT2_Config.random_seed),
-    "-lang", "smtlib", "-output-lang", "presentation",
+    "-lang", "smt2",
     "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]
 in
 
@@ -54,31 +53,38 @@
   avail = make_avail "CVC3",
   command = make_command "CVC3",
   options = cvc3_options,
+  smt_options = [],
   default_max_relevant = 400 (* FUDGE *),
-  outcome = on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   parse_proof = NONE,
   replay = NONE }
 
 end
 
 
-(* Yices *)
+(* CVC4 *)
 
-val yices: SMT2_Solver.solver_config = {
-  name = "yices",
+local
+  fun cvc4_options ctxt = [
+    "--random-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
+    "--lang=smt2",
+    "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT2_Config.timeout))]
+in
+
+val cvc4: SMT2_Solver.solver_config = {
+  name = "cvc4",
   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 *),
+  avail = make_avail "CVC4",
+  command = make_command "CVC4",
+  options = cvc4_options,
+  smt_options = [],
+  default_max_relevant = 400 (* FUDGE *),
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   parse_proof = NONE,
   replay = NONE }
 
+end
+
 
 (* Z3 *)
 
@@ -140,6 +146,7 @@
   avail = make_avail "Z3_NEW",
   command = z3_make_command "Z3_NEW",
   options = z3_options,
+  smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 350 (* FUDGE *),
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   parse_proof = SOME Z3_New_Replay.parse_proof,
@@ -152,7 +159,7 @@
 
 val _ = Theory.setup (
   SMT2_Solver.add_solver cvc3 #>
-  SMT2_Solver.add_solver yices #>
+  SMT2_Solver.add_solver cvc4 #>
   SMT2_Solver.add_solver z3)
 
 end;
--- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -17,14 +17,14 @@
 
   (*translation configuration*)
   type sign = {
-    header: string,
+    logic: string,
     sorts: string list,
     dtyps: (string * (string * (string * string) list) list) list list,
     funcs: (string * (string list * string)) list }
   type config = {
-    header: term list -> string,
+    logic: term list -> string,
     has_datatypes: bool,
-    serialize: string list -> sign -> sterm list -> string }
+    serialize: (string * string) list -> string list -> sign -> sterm list -> string }
   type replay_data = {
     context: Proof.context,
     typs: typ Symtab.table,
@@ -34,7 +34,8 @@
 
   (*translation*)
   val add_config: SMT2_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
-  val translate: Proof.context -> string list -> (int * thm) list -> string * replay_data
+  val translate: Proof.context -> (string * string) list -> string list -> (int * thm) list ->
+    string * replay_data
 end;
 
 structure SMT2_Translate: SMT2_TRANSLATE =
@@ -57,15 +58,15 @@
 (* translation configuration *)
 
 type sign = {
-  header: string,
+  logic: string,
   sorts: string list,
   dtyps: (string * (string * (string * string) list) list) list list,
   funcs: (string * (string list * string)) list }
 
 type config = {
-  header: term list -> string,
+  logic: term list -> string,
   has_datatypes: bool,
-  serialize: string list -> sign -> sterm list -> string }
+  serialize: (string * string) list -> string list -> sign -> sterm list -> string }
 
 type replay_data = {
   context: Proof.context,
@@ -111,8 +112,8 @@
         val terms' = Termtab.update (t, (name, sort)) terms
       in (name, (names', typs, terms')) end)
 
-fun sign_of header dtyps (_, typs, terms) = {
-  header = header,
+fun sign_of logic dtyps (_, typs, terms) = {
+  logic = logic,
   sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
   dtyps = dtyps,
   funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []}
@@ -411,7 +412,7 @@
 
 (** translation from Isabelle terms into SMT intermediate terms **)
 
-fun intermediate header dtyps builtin ctxt ts trx =
+fun intermediate logic dtyps builtin ctxt ts trx =
   let
     fun transT (T as TFree _) = add_typ T true
       | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
@@ -448,7 +449,7 @@
       end
 
     val (us, trx') = fold_map trans ts trx
-  in ((sign_of (header ts) dtyps trx', us), trx') end
+  in ((sign_of (logic ts) dtyps trx', us), trx') end
 
 
 (* translation *)
@@ -472,9 +473,9 @@
         "for solver class " ^ quote (SMT2_Util.string_of_class cs)))
   end
 
-fun translate ctxt comments ithms =
+fun translate ctxt smt_options comments ithms =
   let
-    val {header, has_datatypes, serialize} = get_config ctxt
+    val {logic, has_datatypes, serialize} = get_config ctxt
 
     fun no_dtyps (tr_context, ctxt) ts =
       ((Termtab.empty, [], tr_context, ctxt), ts)
@@ -512,8 +513,8 @@
       |>> apfst (cons fun_app_eq)
   in
     (ts4, tr_context)
-    |-> intermediate header dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2
-    |>> uncurry (serialize comments)
+    |-> intermediate logic dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2
+    |>> uncurry (serialize smt_options comments)
     ||> replay_data_of ctxt2 rewrite_rules ithms
   end
 
--- a/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -59,7 +59,7 @@
 
 (* serialization *)
 
-(** header **)
+(** logic **)
 
 fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
 
@@ -128,11 +128,11 @@
 fun assert_name_of_index i = assert_prefix ^ string_of_int i
 fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s))
 
-fun serialize comments {header, sorts, dtyps, funcs} ts =
+fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
   Buffer.empty
   |> fold (Buffer.add o enclose "; " "\n") comments
-  |> Buffer.add "(set-option :produce-proofs true)\n"
-  |> Buffer.add header
+  |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options
+  |> Buffer.add logic
   |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
   |> (if null dtyps then I
     else Buffer.add (enclose "(declare-datatypes () (" "))\n"
@@ -148,7 +148,7 @@
 (* interface *)
 
 fun translate_config ctxt = {
-  header = choose_logic ctxt,
+  logic = choose_logic ctxt,
   has_datatypes = false,
   serialize = serialize}
 
--- a/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -31,11 +31,8 @@
 
 local
   fun translate_config ctxt =
-    let
-      val {serialize, ...} = SMTLIB2_Interface.translate_config ctxt
-    in
-      {header=K "", serialize=serialize, has_datatypes=true}
-    end
+    {logic = K "", has_datatypes = true,
+     serialize = #serialize (SMTLIB2_Interface.translate_config ctxt)}
 
   fun is_div_mod @{const div (int)} = true
     | is_div_mod @{const mod (int)} = true
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -28,7 +28,6 @@
 open Sledgehammer
 
 (* val cvc3N = "cvc3" *)
-val yicesN = "yices"
 val z3N = "z3"
 
 val runN = "run"
@@ -95,8 +94,8 @@
    ("max_mono_iters", "smart"),
    ("max_new_mono_instances", "smart"),
    ("isar_proofs", "smart"),
-   ("compress_isar", "10"),
-   ("try0_isar", "true"),
+   ("compress", "10"),
+   ("try0", "true"),
    ("smt_proofs", "smart"),
    ("slice", "true"),
    ("minimize", "smart"),
@@ -105,7 +104,7 @@
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)
    ("dont_preplay", ("preplay_timeout", ["0"])),
-   ("dont_compress_isar", ("compress_isar", ["0"])),
+   ("dont_compress", ("compress", ["0"])),
    ("isar_proof", ("isar_proofs", [])) (* legacy *)]
 val negated_alias_params =
   [("no_debug", "debug"),
@@ -119,7 +118,7 @@
    ("no_isar_proofs", "isar_proofs"),
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize"),
-   ("dont_try0_isar", "try0_isar"),
+   ("dont_try0", "try0"),
    ("no_smt_proofs", "smt_proofs")]
 
 val params_not_for_minimize =
@@ -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))
@@ -302,8 +299,8 @@
     val max_new_mono_instances =
       lookup_option lookup_int "max_new_mono_instances"
     val isar_proofs = lookup_option lookup_bool "isar_proofs"
-    val compress_isar = Real.max (1.0, lookup_real "compress_isar")
-    val try0_isar = lookup_bool "try0_isar"
+    val compress = Real.max (1.0, lookup_real "compress")
+    val try0 = lookup_bool "try0"
     val smt_proofs = lookup_option lookup_bool "smt_proofs"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -316,8 +313,8 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
-     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
+     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params mode
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -123,13 +123,13 @@
 
     fun isar_proof_of () =
       let
-        val (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
-          atp_proof, goal) = isar_params ()
+        val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof, goal) =
+          isar_params ()
 
         val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0
 
         fun massage_methods (meths as meth :: _) =
-          if not try0_isar then [meth]
+          if not try0 then [meth]
           else if smt_proofs = SOME true then SMT2_Method :: meths
           else meths
 
@@ -138,7 +138,7 @@
         val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
 
         val do_preplay = preplay_timeout <> Time.zeroTime
-        val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
+        val compress = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress
 
         val is_fixed = Variable.is_declared ctxt orf Name.is_skolem
         fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
@@ -311,17 +311,17 @@
         val (play_outcome, isar_proof) =
           canonical_isar_proof
           |> tap (trace_isar_proof "Original")
-          |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
+          |> compress_isar_proof ctxt compress preplay_timeout preplay_data
           |> tap (trace_isar_proof "Compressed")
           |> postprocess_isar_proof_remove_unreferenced_steps
                (keep_fastest_method_of_isar_step (!preplay_data)
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
-          (* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an
+          (* It's not clear whether this is worth the trouble (and if so, "compress" has an
              unnatural semantics): *)
 (*
           |> minimize
-               ? (compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
+               ? (compress_isar_proof ctxt compress preplay_timeout preplay_data
                   #> tap (trace_isar_proof "Compressed again"))
 *)
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -109,15 +109,15 @@
 val compress_degree = 2
 
 (* Precondition: The proof must be labeled canonically. *)
-fun compress_isar_proof ctxt compress_isar preplay_timeout preplay_data proof =
-  if compress_isar <= 1.0 then
+fun compress_isar_proof ctxt compress preplay_timeout preplay_data proof =
+  if compress <= 1.0 then
     proof
   else
     let
       val (compress_further, decrement_step_count) =
         let
           val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0
-          val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
+          val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress)
           val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
         in
           (fn () => !delta > 0, fn () => delta := !delta - 1)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -36,8 +36,8 @@
      max_mono_iters : int option,
      max_new_mono_instances : int option,
      isar_proofs : bool option,
-     compress_isar : real,
-     try0_isar : bool,
+     compress : real,
+     try0 : bool,
      smt_proofs : bool option,
      slice : bool,
      minimize : bool option,
@@ -143,8 +143,8 @@
    max_mono_iters : int option,
    max_new_mono_instances : int option,
    isar_proofs : bool option,
-   compress_isar : real,
-   try0_isar : bool,
+   compress : real,
+   try0 : bool,
    smt_proofs : bool option,
    slice : bool,
    minimize : bool option,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -131,8 +131,8 @@
 
 fun run_atp mode name
     (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
-       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
-       try0_isar, smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
+       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0,
+       smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
     minimize_command
     ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
@@ -371,8 +371,8 @@
                       |> introduce_spass_skolem
                       |> factify_atp_proof fact_names hyp_ts concl_t
                   in
-                    (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
-                     try0_isar, minimize <> SOME false, atp_proof, goal)
+                    (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
+                     minimize <> SOME false, atp_proof, goal)
                   end
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -129,8 +129,8 @@
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
-      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
-      smt_proofs, preplay_timeout, ...} : params)
+      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
+      preplay_timeout, ...} : params)
     silent (prover : prover) timeout i n state goal facts =
   let
     val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
@@ -143,9 +143,9 @@
        uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
        max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
        max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
-       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
-       smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout,
-       preplay_timeout = preplay_timeout, expect = ""}
+       isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
+       slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
+       expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)]}
@@ -288,8 +288,8 @@
 fun adjust_proof_method_params override_params
     ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
       uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
-      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt_proofs, slice, minimize,
-      timeout, preplay_timeout, expect} : params) =
+      max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, slice, minimize, timeout,
+      preplay_timeout, expect} : params) =
   let
     fun lookup_override name default_value =
       (case AList.lookup (op =) override_params name of
@@ -304,8 +304,8 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
-     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
+     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Jun 12 18:47:16 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
-    Author:     Fabian Immler, TU Muenchen
-    Author:     Makarius
-    Author:     Jasmin Blanchette, TU Muenchen
-
-SMT solvers as Sledgehammer provers.
-*)
-
-signature SLEDGEHAMMER_PROVER_SMT =
-sig
-  type stature = ATP_Problem_Generate.stature
-  type mode = Sledgehammer_Prover.mode
-  type prover = Sledgehammer_Prover.prover
-
-  val smt_builtins : bool Config.T
-  val smt_triggers : bool Config.T
-  val smt_weights : bool Config.T
-  val smt_weight_min_facts : int Config.T
-  val smt_min_weight : int Config.T
-  val smt_max_weight : int Config.T
-  val smt_max_weight_index : int Config.T
-  val smt_weight_curve : (int -> int) Unsynchronized.ref
-  val smt_max_slices : int Config.T
-  val smt_slice_fact_frac : real Config.T
-  val smt_slice_time_frac : real Config.T
-  val smt_slice_min_secs : int Config.T
-
-  val is_smt_prover : Proof.context -> string -> bool
-  val run_smt_solver : mode -> string -> prover
-end;
-
-structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
-struct
-
-open ATP_Util
-open ATP_Proof
-open ATP_Systems
-open ATP_Problem_Generate
-open ATP_Proof_Reconstruct
-open Sledgehammer_Util
-open Sledgehammer_Proof_Methods
-open Sledgehammer_Prover
-
-val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
-val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
-val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
-val smt_weight_min_facts =
-  Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
-
-fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
-
-(* FUDGE *)
-val smt_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
-val smt_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
-val smt_max_weight_index =
-  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
-val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
-
-fun smt_fact_weight ctxt j num_facts =
-  if Config.get ctxt smt_weights andalso num_facts >= Config.get ctxt smt_weight_min_facts then
-    let
-      val min = Config.get ctxt smt_min_weight
-      val max = Config.get ctxt smt_max_weight
-      val max_index = Config.get ctxt smt_max_weight_index
-      val curve = !smt_weight_curve
-    in
-      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
-    end
-  else
-    NONE
-
-fun weight_smt_fact ctxt num_facts ((info, th), j) =
-  let val thy = Proof_Context.theory_of ctxt in
-    (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
-  end
-
-(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
-   properly in the SMT module, we must interpret these here. *)
-val z3_failures =
-  [(101, OutOfResources),
-   (103, MalformedInput),
-   (110, MalformedInput),
-   (112, TimedOut)]
-val unix_failures =
-  [(138, Crashed),
-   (139, Crashed)]
-val smt_failures = z3_failures @ unix_failures
-
-fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
-    if is_real_cex then Unprovable else GaveUp
-  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
-  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
-    (case AList.lookup (op =) smt_failures code of
-      SOME failure => failure
-    | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
-  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
-  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
-
-(* FUDGE *)
-val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
-val smt_slice_fact_frac =
-  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667)
-val smt_slice_time_frac =
-  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
-val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
-
-val is_boring_builtin_typ =
-  not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
-
-fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
-      ...} : params) state goal i =
-  let
-    fun repair_context ctxt =
-      ctxt |> Context.proof_map (SMT_Config.select_solver name)
-           |> Config.put SMT_Config.verbose debug
-           |> (if overlord then
-                 Config.put SMT_Config.debug_files
-                   (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
-               else
-                 I)
-           |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
-           |> not (Config.get ctxt smt_builtins)
-              ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
-                 #> Config.put SMT_Config.datatypes false)
-           |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
-                default_max_new_mono_instances
-
-    val state = Proof.map_context (repair_context) state
-    val ctxt = Proof.context_of state
-    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
-
-    fun do_slice timeout slice outcome0 time_so_far
-        (weighted_factss as (fact_filter, weighted_facts) :: _) =
-      let
-        val timer = Timer.startRealTimer ()
-        val slice_timeout =
-          if slice < max_slices then
-            let val ms = Time.toMilliseconds timeout in
-              Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs,
-                Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms)))
-              |> Time.fromMilliseconds
-            end
-          else
-            timeout
-        val num_facts = length weighted_facts
-        val _ =
-          if debug then
-            quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
-            " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
-            |> Output.urgent_message
-          else
-            ()
-        val birth = Timer.checkRealTimer timer
-
-        val (outcome, used_facts) =
-          SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
-          |> SMT_Solver.smt_filter_apply slice_timeout
-          |> (fn {outcome, used_facts} => (outcome, used_facts))
-          handle exn =>
-            if Exn.is_interrupt exn then reraise exn
-            else (Runtime.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
-
-        val death = Timer.checkRealTimer timer
-        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
-        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
-
-        val too_many_facts_perhaps =
-          (case outcome of
-            NONE => false
-          | SOME (SMT_Failure.Counterexample _) => false
-          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
-          | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
-          | SOME SMT_Failure.Out_Of_Memory => true
-          | SOME (SMT_Failure.Other_Failure _) => true)
-
-        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
-      in
-        if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
-           Time.> (timeout, Time.zeroTime) then
-          let
-            val new_num_facts =
-              Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
-            val weighted_factss as (new_fact_filter, _) :: _ =
-              weighted_factss
-              |> (fn (x :: xs) => xs @ [x])
-              |> app_hd (apsnd (take new_num_facts))
-            val show_filter = fact_filter <> new_fact_filter
-
-            fun num_of_facts fact_filter num_facts =
-              string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
-              " fact" ^ plural_s num_facts
-
-            val _ =
-              if debug then
-                quote name ^ " invoked with " ^
-                num_of_facts fact_filter num_facts ^ ": " ^
-                string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
-                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
-                "..."
-                |> Output.urgent_message
-              else
-                ()
-          in
-            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
-          end
-        else
-          {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
-           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
-      end
-  in
-    do_slice timeout 1 NONE Time.zeroTime
-  end
-
-fun run_smt_solver mode name (params as {verbose, smt_proofs, preplay_timeout, ...})
-    minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
-  let
-    val thy = Proof.theory_of state
-    val ctxt = Proof.context_of state
-
-    fun weight_facts facts =
-      let val num_facts = length facts in
-        map (weight_smt_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
-      end
-
-    val weighted_factss = factss |> map (apsnd weight_facts)
-    val {outcome, used_facts = used_pairs, used_from, run_time} =
-      smt_filter_loop name params state goal subgoal weighted_factss
-    val used_facts = used_pairs |> map fst
-    val outcome = outcome |> Option.map failure_of_smt_failure
-
-    val (preplay, message, message_tail) =
-      (case outcome of
-        NONE =>
-        (Lazy.lazy (fn () =>
-           play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal
-             SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
-         fn preplay =>
-            let
-              val one_line_params =
-                (preplay, proof_banner mode name, used_facts,
-                 choose_minimize_command thy params minimize_command name preplay, subgoal,
-                 subgoal_count)
-              val num_chained = length (#facts (Proof.goal state))
-            in
-              one_line_proof_text ctxt num_chained one_line_params
-            end,
-         if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
-      | SOME failure =>
-        (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
-         fn _ => string_of_atp_failure failure, ""))
-  in
-    {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
-     preplay = preplay, message = message, message_tail = message_tail}
-  end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Jun 12 18:47:16 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Jun 12 18:47:27 2014 +0200
@@ -177,13 +177,15 @@
     do_slice timeout 1 NONE Time.zeroTime
   end
 
-fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress_isar,
-      try0_isar, smt_proofs, minimize, preplay_timeout, ...})
+fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs,
+      minimize, preplay_timeout, ...})
     minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 
+    val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss
+
     val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
       smt2_filter_loop name params state goal subgoal factss
     val used_named_facts = map snd fact_ids
@@ -199,8 +201,8 @@
          fn preplay =>
             let
               fun isar_params () =
-                (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
-                 minimize <> SOME false, atp_proof (), goal)
+                (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize <> SOME false,
+                 atp_proof (), goal)
 
               val one_line_params =
                 (preplay, proof_banner mode name, used_facts,