# HG changeset patch
# User blanchet
# Date 1396537039 -7200
# Node ID 8fb4515818f7d106b729f6a6c8a512a719abe8df
# Parent  a0c4a162bd130e0e007fdee27ecd5b058b90156d
updated Z3 TPTP to 4.3.1+

diff -r a0c4a162bd13 -r 8fb4515818f7 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Apr 03 13:29:58 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Apr 03 16:57:19 2014 +0200
@@ -919,12 +919,20 @@
 are treated as a different prover by Isabelle. To use these, set the environment
 variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable,
 including the file name. You also need to set \texttt{Z3\_NON\_COMMERCIAL} to
-``yes'', as described above. Sledgehammer has been tested with versions 4.3.0 and
-4.3.1.
+``yes'', as described above. Sledgehammer has been tested with versions 4.3.0
+and 4.3.1.
 \end{enum}
+
+\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. It requires
+version 4.3.1 of Z3 above. To use it, set the environment variable
+\texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp}
+executable.
+
 \end{sloppy}
 
-The following remote provers are supported:
+In addition to the local provers, the following remote provers are supported:
 
 \begin{enum}
 \item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
diff -r a0c4a162bd13 -r 8fb4515818f7 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 03 13:29:58 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 03 16:57:19 2014 +0200
@@ -619,11 +619,10 @@
 val z3_tff0 = TFF Monomorphic
 
 val z3_tptp_config : atp_config =
-  {exec = K (["Z3_HOME"], ["z3"]),
+  {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
-       "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
-       string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
-   proof_delims = [("\ncore(", ").")],
+     "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
+   proof_delims = [],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =