# HG changeset patch
# User blanchet
# Date 1297268338 -3600
# Node ID 4b09f8b9e0122e931ab3d3453b98c77a6731b3e5
# Parent  2b896f7f232db499b69533c7459bb8c9cec46f8f
added "Z3 as an ATP" support to Sledgehammer locally

diff -r 2b896f7f232d -r 4b09f8b9e012 doc-src/Sledgehammer/sledgehammer.tex
--- 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
diff -r 2b896f7f232d -r 4b09f8b9e012 src/HOL/Tools/ATP/atp_systems.ML
--- 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;