# HG changeset patch # User blanchet # Date 1572007876 -7200 # Node ID 600da8ccbe5b2eff750fdcfacdaa84a2f643a0cd # Parent a35618d00d299129c1c5d9a242c820ac1df6b0c8 removed support for iProver-Eq diff -r a35618d00d29 -r 600da8ccbe5b src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 14:47:42 2019 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 14:51:16 2019 +0200 @@ -103,14 +103,13 @@ % The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver -\cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, 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{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. 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 @@ -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, E, E-SInE, E-ToFoF, -iProver, iProver-Eq, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are +iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers CVC3, CVC4, veriT, and Z3 can be run locally. @@ -789,13 +788,6 @@ executable. Sledgehammer has been tested with version 2.8. iProver depends on E to clausify problems, so make sure that E is installed as well. -\item[\labelitemi] \textbf{\textit{iprover\_eq}:} iProver-Eq is an -instantiation-based prover with native support for equality developed by -Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. To use -iProver-Eq, set the environment variable \texttt{IPROVER\_EQ\_HOME} to the -directory that contains the \texttt{iprover-eq} and \texttt{vclausify\_rel} -executables. Sledgehammer has been tested with version 0.8. - \item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, with support for the TPTP typed higher-order syntax (THF0). To use LEO-II, set @@ -880,10 +872,6 @@ remote version of iProver runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. -\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} The -remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers -\cite{sutcliffe-2000}. - \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. diff -r a35618d00d29 -r 600da8ccbe5b src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 25 14:47:42 2019 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 25 14:51:16 2019 +0200 @@ -56,7 +56,6 @@ val e_tofofN : string val ehohN : string val iproverN : string - val iprover_eqN : string val leo2N : string val leo3N : string val pirateN : string @@ -126,7 +125,6 @@ val e_tofofN = "e_tofof" val ehohN = "ehoh" val iproverN = "iprover" -val iprover_eqN = "iprover_eq" val leo2N = "leo2" val leo3N = "leo3" val pirateN = "pirate" diff -r a35618d00d29 -r 600da8ccbe5b src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:47:42 2019 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:51:16 2019 +0200 @@ -394,21 +394,6 @@ val iprover = (iproverN, fn () => iprover_config) -(* iProver-Eq *) - -val iprover_eq_config : atp_config = - {exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]), - arguments = #arguments iprover_config, - proof_delims = #proof_delims iprover_config, - known_failures = #known_failures iprover_config, - prem_role = #prem_role iprover_config, - best_slices = #best_slices iprover_config, - best_max_mono_iters = #best_max_mono_iters iprover_config, - best_max_new_mono_instances = #best_max_new_mono_instances iprover_config} - -val iprover_eq = (iprover_eqN, fn () => iprover_eq_config) - - (* LEO-II *) val leo2_config : atp_config = @@ -733,9 +718,6 @@ val remote_iprover = remotify_atp iprover "iProver" ["0.99"] (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) -val remote_iprover_eq = - remotify_atp iprover_eq "iProver-Eq" ["0.8"] - (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] (K (((40, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *)) @@ -791,10 +773,9 @@ end val atps = - [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, satallax, spass, - vampire, z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof, - remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, remote_vampire, remote_snark, - remote_pirate, remote_waldmeister] + [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, leo2, leo3, satallax, spass, vampire, + z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof, remote_iprover, + remote_leo2, remote_leo3, remote_vampire, remote_snark, remote_pirate, remote_waldmeister] val _ = Theory.setup (fold add_atp atps)