# HG changeset patch
# User blanchet
# Date 1344953385 -7200
# Node ID ffa31bf5c662f9dcec07f370b0d3d9934fc739f0
# Parent  b86e8cf3f4648a24cf744812198ffc287c64bc8d
tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0

diff -r b86e8cf3f464 -r ffa31bf5c662 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 14 15:26:45 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 14 16:09:45 2012 +0200
@@ -927,12 +927,6 @@
 name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
 noncommercial user. Sledgehammer has been tested with versions 3.0, 3.1, 3.2,
 and 4.0.
-
-\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
-an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
-formats (FOF and TFF0). It is included for experimental purposes. Sledgehammer
-requires version 4.0 or above. To use it, set the environment variable
-\texttt{Z3\_HOME} to the directory that contains the \texttt{z3} executable.
 \end{enum}
 \end{sloppy}
 
@@ -986,9 +980,6 @@
 \item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
 servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
 point).
-
-\item[\labelitemi] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
-with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
 By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
diff -r b86e8cf3f464 -r ffa31bf5c662 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 14 15:26:45 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 14 16:09:45 2012 +0200
@@ -528,7 +528,7 @@
 val vampire = (vampireN, fn () => vampire_config)
 
 
-(* Z3 with TPTP syntax *)
+(* Z3 with TPTP syntax (half experimental, half legacy) *)
 
 val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
 
@@ -665,9 +665,6 @@
 val remote_vampire =
   remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
       (K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
-val remote_z3_tptp =
-  remotify_atp z3_tptp "Z3" ["3.0"]
-      (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
       (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
@@ -728,7 +725,7 @@
   [alt_ergo, e, e_males, iprover, iprover_eq, leo2, satallax, spass, spass_poly,
    vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, remote_e_tofof,
    remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax,
-   remote_vampire, remote_z3_tptp, remote_snark, remote_waldmeister]
+   remote_vampire, remote_snark, remote_waldmeister]
 
 val setup = fold add_atp atps