# HG changeset patch # User blanchet # Date 1602172517 -7200 # Node ID 4a3169d8885cab657daa6a430bcd7fbd75e5fa8f # Parent 148e8332a8b16a89c7aff97a42ddc5cdafb41fd5 removed support for obsolete prover SNARK and underperforming prover E-Par diff -r 148e8332a8b1 -r 4a3169d8885c src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Oct 08 17:47:35 2020 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Oct 08 17:55:17 2020 +0200 @@ -102,23 +102,22 @@ \footnote{The distinction between ATPs and SMT solvers is convenient but mostly historical.} % -The supported ATPs are agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E +The supported ATPs include agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E \cite{schulz-2002}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III -\cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS -\cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, -Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}. The -ATPs are run either locally or remotely via the System\-On\-TPTP web service -\cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4 -\cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3 \cite{z3}. These are -always run locally. +\cite{leo3}, Satallax \cite{satallax}, SPASS \cite{weidenbach-et-al-2009}, +Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and +Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or remotely +via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT +solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT \cite{bouton-et-al-2009}, +and Z3 \cite{z3}. These are always run locally. 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 -not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed -proof typically relies on the general-purpose \textit{metis} proof method, which +The result of a successful proof search is some source text that typically +reconstructs the proof within Isabelle. For ATPs, the reconstructed proof +typically relies on the general-purpose \textit{metis} proof method, which integrates the Metis ATP in Isabelle/HOL with explicit inferences going through the kernel. Thus its results are correct by construction. @@ -149,7 +148,7 @@ Among the ATPs, agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and Zipperposition can be run locally; in addition, agsyHOL, -Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, Waldmeister, +Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, Vampire, Waldmeister, and Zipperposition are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers CVC3, CVC4, veriT, and Z3 can be run locally. @@ -765,14 +764,6 @@ install the prebuilt E package from \download. Sledgehammer has been tested with versions 1.6 to 1.8. -\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is an experimental metaprover -developed by Josef Urban that implements strategy scheduling on top of E. To use -E-Par, set the environment variable \texttt{E\_HOME} to the directory that -contains the \texttt{runepar.pl} script and the \texttt{eprover} and -\texttt{epclextract} executables, or use the prebuilt E package from \download. -Be aware that E-Par is experimental software. It has been known to generate -zombie processes. Use at your own risks. - \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. To use iProver, set the environment variable @@ -865,10 +856,6 @@ \item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. -\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order -resolution prover developed by Stickel et al.\ \cite{snark}. The remote -version of SNARK runs on Geoff Sutcliffe's Miami servers. - \item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of Vampire runs on Geoff Sutcliffe's Miami servers. diff -r 148e8332a8b1 -r 4a3169d8885c src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Oct 08 17:47:35 2020 +0200 +++ b/src/HOL/Sledgehammer.thy Thu Oct 08 17:55:17 2020 +0200 @@ -13,9 +13,6 @@ "sledgehammer_params" :: thy_decl begin -lemma size_ne_size_imp_ne: "size x \ size y \ x \ y" - by (erule contrapos_nn) (rule arg_cong) - ML_file \Tools/Sledgehammer/async_manager_legacy.ML\ ML_file \Tools/Sledgehammer/sledgehammer_util.ML\ ML_file \Tools/Sledgehammer/sledgehammer_fact.ML\ diff -r 148e8332a8b1 -r 4a3169d8885c src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Oct 08 17:47:35 2020 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Oct 08 17:55:17 2020 +0200 @@ -44,17 +44,14 @@ type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list - (* Named ATPs *) val agsyholN : string val alt_ergoN : string val eN : string - val e_parN : string val iproverN : string val leo2N : string val leo3N : string val pirateN : string val satallaxN : string - val snarkN : string val spassN : string val vampireN : string val waldmeisterN : string @@ -109,18 +106,14 @@ open ATP_Util open ATP_Problem -(* Named ATPs *) - val agsyholN = "agsyhol" val alt_ergoN = "alt_ergo" val eN = "e" -val e_parN = "e_par" val iproverN = "iprover" val leo2N = "leo2" val leo3N = "leo3" val pirateN = "pirate" val satallaxN = "satallax" -val snarkN = "snark" val spassN = "spass" val vampireN = "vampire" val waldmeisterN = "waldmeister" diff -r 148e8332a8b1 -r 4a3169d8885c src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Oct 08 17:47:35 2020 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Oct 08 17:55:17 2020 +0200 @@ -315,27 +315,6 @@ val e = (eN, fn () => e_config) -(* E-Par *) - -val e_par_config : atp_config = - {exec = K (["E_HOME"], ["runepar.pl"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => - string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^ " 2" (* proofs *), - proof_delims = tstp_proof_delims, - known_failures = #known_failures e_config, - prem_role = Conjecture, - best_slices = - (* FUDGE *) - K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")), - (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")), - (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")), - (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))], - best_max_mono_iters = default_max_mono_iters, - best_max_new_mono_instances = default_max_new_mono_instances} - -val e_par = (e_parN, fn () => e_par_config) - - (* iProver *) val iprover_config : atp_config = @@ -673,10 +652,6 @@ val remote_leo3 = remotify_atp leo3 "Leo-III" ["1.1"] (K (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) -val remote_snark = - remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"] - [("refutation.", "end_refutation.")] [] Hypothesis - (K (((100, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["THF-4.4"] (K (((400, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *)) @@ -719,9 +694,9 @@ end val atps = - [agsyhol, alt_ergo, e, e_par, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, - zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, - remote_leo3, remote_snark, remote_vampire, remote_waldmeister, remote_zipperposition] + [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, + remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, + remote_vampire, remote_waldmeister, remote_zipperposition] val _ = Theory.setup (fold add_atp atps)