--- 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
--- 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 =