# HG changeset patch # User nipkow # Date 1402591647 -7200 # Node ID 5496011859eba73c073f4e0d141d7e2587cfdb12 # Parent 62746a41cc0c7003b2c77adca0d272b78395ff1a# Parent 8191ccf6a1bd0af5261411022d7a4ae9b489c374 merged diff -r 8191ccf6a1bd -r 5496011859eb NEWS --- 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: diff -r 8191ccf6a1bd -r 5496011859eb src/Doc/Nitpick/document/root.tex --- 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: diff -r 8191ccf6a1bd -r 5496011859eb src/Doc/Sledgehammer/document/root.tex --- 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} diff -r 8191ccf6a1bd -r 5496011859eb src/Doc/manual.bib --- 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 diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/List.thy --- 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 = diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Metis_Examples/Big_O.thy --- 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 "(\c\'a\linordered_idom. @@ -60,7 +60,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis F4) qed -sledgehammer_params [isar_proofs, compress_isar = 2] +sledgehammer_params [isar_proofs, compress = 2] lemma "(\c\'a\linordered_idom. @@ -83,7 +83,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis F2) qed -sledgehammer_params [isar_proofs, compress_isar = 3] +sledgehammer_params [isar_proofs, compress = 3] lemma "(\c\'a\linordered_idom. @@ -103,7 +103,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis A1 abs_ge_zero) qed -sledgehammer_params [isar_proofs, compress_isar = 4] +sledgehammer_params [isar_proofs, compress = 4] lemma "(\c\'a\linordered_idom. @@ -123,7 +123,7 @@ thus "\h x\ \ \c\ * \f x\" 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. \c. (0 < c \ (\x. abs (h x) <= c * abs (f x)))}" by (auto simp add: bigo_def bigo_pos_const) diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Metis_Examples/Sets.thy --- 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 \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by metis qed -sledgehammer_params [isar_proofs, compress_isar = 2] +sledgehammer_params [isar_proofs, compress = 2] lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" @@ -107,7 +107,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by metis qed -sledgehammer_params [isar_proofs, compress_isar = 3] +sledgehammer_params [isar_proofs, compress = 3] lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" @@ -124,7 +124,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ 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 \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" @@ -140,7 +140,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ 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 \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Metis_Examples/Trans_Closure.thy --- 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 "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b,c) \ R\<^sup>*\ \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" -(* sledgehammer [isar_proofs, compress_isar = 2] *) +(* sledgehammer [isar_proofs, compress = 2] *) proof - assume A1: "f c = Intg x" assume A2: "\y. f b = Intg y \ y \ x" diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Nitpick.thy --- 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 diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Random.thy --- 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 "\>" 60) diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/SMT2.thy --- 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 {* diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Sledgehammer.thy --- 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 diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/SMT2/smt2_solver.ML --- 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 diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/SMT2/smt2_systems.ML --- 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; diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/SMT2/smt2_translate.ML --- 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 diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/SMT2/smtlib2_interface.ML --- 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} diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/SMT2/z3_new_interface.ML --- 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 diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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 diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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)) diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- 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) diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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, diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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, diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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, ...}) diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- 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; diff -r 8191ccf6a1bd -r 5496011859eb src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- 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,