tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
authorblanchet
Tue Aug 14 16:09:45 2012 +0200 (2012-08-14)
changeset 48803ffa31bf5c662
parent 48802 b86e8cf3f464
child 48806 559c1d80e129
tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
doc-src/Sledgehammer/sledgehammer.tex
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 14 15:26:45 2012 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 14 16:09:45 2012 +0200
     1.3 @@ -927,12 +927,6 @@
     1.4  name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
     1.5  noncommercial user. Sledgehammer has been tested with versions 3.0, 3.1, 3.2,
     1.6  and 4.0.
     1.7 -
     1.8 -\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
     1.9 -an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
    1.10 -formats (FOF and TFF0). It is included for experimental purposes. Sledgehammer
    1.11 -requires version 4.0 or above. To use it, set the environment variable
    1.12 -\texttt{Z3\_HOME} to the directory that contains the \texttt{z3} executable.
    1.13  \end{enum}
    1.14  \end{sloppy}
    1.15  
    1.16 @@ -986,9 +980,6 @@
    1.17  \item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
    1.18  servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
    1.19  point).
    1.20 -
    1.21 -\item[\labelitemi] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
    1.22 -with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
    1.23  \end{enum}
    1.24  
    1.25  By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 14 15:26:45 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 14 16:09:45 2012 +0200
     2.3 @@ -528,7 +528,7 @@
     2.4  val vampire = (vampireN, fn () => vampire_config)
     2.5  
     2.6  
     2.7 -(* Z3 with TPTP syntax *)
     2.8 +(* Z3 with TPTP syntax (half experimental, half legacy) *)
     2.9  
    2.10  val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
    2.11  
    2.12 @@ -665,9 +665,6 @@
    2.13  val remote_vampire =
    2.14    remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
    2.15        (K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
    2.16 -val remote_z3_tptp =
    2.17 -  remotify_atp z3_tptp "Z3" ["3.0"]
    2.18 -      (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
    2.19  val remote_e_sine =
    2.20    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
    2.21        (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
    2.22 @@ -728,7 +725,7 @@
    2.23    [alt_ergo, e, e_males, iprover, iprover_eq, leo2, satallax, spass, spass_poly,
    2.24     vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, remote_e_tofof,
    2.25     remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax,
    2.26 -   remote_vampire, remote_z3_tptp, remote_snark, remote_waldmeister]
    2.27 +   remote_vampire, remote_snark, remote_waldmeister]
    2.28  
    2.29  val setup = fold add_atp atps
    2.30