# HG changeset patch
# User blanchet
# Date 1297268337 -3600
# Node ID eb98c60a6cf0b984fbea8c20c4c7d99ad2acc24b
# Parent  1b225934c09d3441da5fad415bc44e36988b6ba3
added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation

diff -r 1b225934c09d -r eb98c60a6cf0 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Feb 09 15:48:43 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Feb 09 17:18:57 2011 +0100
@@ -455,13 +455,18 @@
 developed by Stickel et al.\ \cite{snark}. The remote version of
 SNARK runs on Geoff Sutcliffe's Miami servers.
 
+\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
+on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
+point).
+
 \item[$\bullet$] \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[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
-on 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.
 \end{enum}
 
 By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
diff -r 1b225934c09d -r eb98c60a6cf0 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 09 15:48:43 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 09 17:18:57 2011 +0100
@@ -12,7 +12,7 @@
   type 'a uniform_formula = 'a ATP_Problem.uniform_formula
 
   datatype failure =
-    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+    Unprovable | IncompleteUnprovable | ProofMissing | CantConnect | TimedOut |
     OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
     NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
     InternalError | UnknownError of string
@@ -47,10 +47,10 @@
 open ATP_Problem
 
 datatype failure =
-  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
-  SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | NoRealZ3 |
-  MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError |
-  UnknownError of string
+  Unprovable | IncompleteUnprovable | ProofMissing | CantConnect | TimedOut |
+  OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
+  NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
+  InternalError | UnknownError of string
 
 fun strip_spaces_in_list _ [] = []
   | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
@@ -90,6 +90,9 @@
     "The " ^ prover ^ " problem is unprovable."
   | string_for_failure prover IncompleteUnprovable =
     "The " ^ prover ^ " cannot prove the problem."
+  | string_for_failure prover ProofMissing =
+    "The " ^ prover ^ " claims the conjecture is a theorem but did not provide \
+    \a proof."
   | string_for_failure _ CantConnect = "Cannot connect to remote server."
   | string_for_failure _ TimedOut = "Timed out."
   | string_for_failure prover OutOfResources =
@@ -117,8 +120,6 @@
     \Isabelle developers."
   | string_for_failure prover MalformedOutput =
     "The " ^ prover ^ " output is malformed."
-  | string_for_failure prover Interrupted =
-    "The " ^ prover ^ " was interrupted."
   | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
   | string_for_failure prover InternalError =
     "An internal " ^ prover ^ " error occurred."
@@ -163,7 +164,7 @@
   case extract_known_failure known_failures output of
     NONE => (case extract_tstplike_proof proof_delims output of
              "" => ("", SOME (if res_code = 0 andalso output = "" then
-                                Interrupted
+                                ProofMissing
                               else
                                 UnknownError (short_output verbose output)))
            | tstplike_proof =>
diff -r 1b225934c09d -r eb98c60a6cf0 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 09 15:48:43 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 09 17:18:57 2011 +0100
@@ -36,7 +36,11 @@
   val vampireN : string
   val sine_eN : string
   val snarkN : string
+  val z3_atpN : string
   val remote_prefix : string
+  val remote_atp :
+    string -> string -> string list -> (string * string) list
+    -> (failure * string) list -> int -> bool -> string * atp_config
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val supported_atps : theory -> string list
@@ -75,6 +79,7 @@
 val vampireN = "vampire"
 val sine_eN = "sine_e"
 val snarkN = "snark"
+val z3_atpN = "z3_atp"
 val remote_prefix = "remote_"
 
 structure Data = Theory_Data
@@ -296,6 +301,11 @@
 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
 
 (* Setup *)
 
@@ -318,7 +328,7 @@
   Synchronized.change systems (fn _ => get_systems ())
 
 val atps = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
-            remote_snark]
+            remote_snark, remote_z3_atp]
 val setup = fold add_atp atps
 
 end;