--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Feb 09 17:18:57 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Feb 09 17:18:58 2011 +0100
@@ -425,21 +425,25 @@
that contains the \texttt{vampire} executable. Sledgehammer has been tested with
versions 11, 0.6, and 1.0.
-\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
-Microsoft Research \cite{z3}. To use Z3, set the environment variable
-\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
-name. Sledgehammer has been tested with 2.7 to 2.15.
+\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
+Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
+set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
+executable, including the file name. Sledgehammer has been tested with version
+2.2.
\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
SRI \cite{yices}. To use Yices, set the environment variable
\texttt{YICES\_SOLVER} to the complete path of the executable, including the
file name. Sledgehammer has been tested with version 1.0.
-\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
-Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
-set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
-executable, including the file name. Sledgehammer has been tested with version
-2.2.
+\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
+Microsoft Research \cite{z3}. To use Z3, set the environment variable
+\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
+name. Sledgehammer has been tested with versions 2.7 to 2.18.
+
+\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
+ATP, exploiting Z3's undocumented support for the TPTP format. It is included
+for experimental purposes. It requires versions 2.18 or above.
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
@@ -463,10 +467,8 @@
servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
point).
-\item[$\bullet$] \textbf{\textit{remote\_z3\_atp}:} This version of Z3 pretends
-to be an ATP: It accepts the TPTP syntax and runs on Geoff Sutcliffe's Miami
-servers. For the moment, it cannot provide proofs and is included in
-Sledgehammer for experimental purposes.
+\item[$\bullet$] \textbf{\textit{remote\_z3\_atp}:} The remote version of ``Z3
+as an ATP'' runs on Geoff Sutcliffe's Miami servers.
\end{enum}
By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 09 17:18:57 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 09 17:18:58 2011 +0100
@@ -77,9 +77,9 @@
val eN = "e"
val spassN = "spass"
val vampireN = "vampire"
+val z3_atpN = "z3_atp"
val sine_eN = "sine_e"
val snarkN = "snark"
-val z3_atpN = "z3_atp"
val remote_prefix = "remote_"
structure Data = Theory_Data
@@ -231,6 +231,26 @@
val vampire = (vampireN, vampire_config)
+(* Z3 with TPTP syntax *)
+
+val z3_atp_config : atp_config =
+ {exec = ("Z3_HOME", "z3"),
+ required_execs = [],
+ arguments = fn _ => fn timeout => fn _ =>
+ "MBQI=true /p /t:" ^
+ string_of_int (to_secs 0 timeout),
+ has_incomplete_mode = false,
+ proof_delims = [],
+ known_failures =
+ [(IncompleteUnprovable, "\nsat"),
+ (ProofMissing, "\nunsat")],
+ default_max_relevant = 250 (* FUDGE *),
+ explicit_forall = true,
+ use_conjecture_for_hypotheses = false}
+
+val z3_atp = (z3_atpN, z3_atp_config)
+
+
(* Remote ATP invocation via SystemOnTPTP *)
val systems = Synchronized.var "atp_systems" ([] : string list)
@@ -295,17 +315,17 @@
val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
-val remote_sine_e =
- remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
- 600 (* FUDGE *) true
-val remote_snark =
- remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] []
- 250 (* FUDGE *) true
val remote_z3_atp =
remote_atp z3_atpN "Z3---" ["2.18"] []
[(IncompleteUnprovable, "SZS status Satisfiable"),
(ProofMissing, "SZS status Unsatisfiable")]
250 (* FUDGE *) false
+val remote_sine_e =
+ remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
+ 600 (* FUDGE *) true
+val remote_snark =
+ remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] []
+ 250 (* FUDGE *) true
(* Setup *)
@@ -327,8 +347,8 @@
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())
-val atps = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
- remote_snark, remote_z3_atp]
+val atps = [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
+ remote_sine_e, remote_snark]
val setup = fold add_atp atps
end;