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
1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Feb 09 15:48:43 2011 +0100
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Feb 09 17:18:57 2011 +0100
1.3 @@ -455,13 +455,18 @@
1.4 developed by Stickel et al.\ \cite{snark}. The remote version of
1.5 SNARK runs on Geoff Sutcliffe's Miami servers.
1.6
1.7 +\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
1.8 +on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
1.9 +point).
1.10 +
1.11 \item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
1.12 servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
1.13 point).
1.14
1.15 -\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
1.16 -on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
1.17 -point).
1.18 +\item[$\bullet$] \textbf{\textit{remote\_z3\_atp}:} This version of Z3 pretends
1.19 +to be an ATP: It accepts the TPTP syntax and runs on Geoff Sutcliffe's Miami
1.20 +servers. For the moment, it cannot provide proofs and is included in
1.21 +Sledgehammer for experimental purposes.
1.22 \end{enum}
1.23
1.24 By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
2.1 --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Feb 09 15:48:43 2011 +0100
2.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Feb 09 17:18:57 2011 +0100
2.3 @@ -12,7 +12,7 @@
2.4 type 'a uniform_formula = 'a ATP_Problem.uniform_formula
2.5
2.6 datatype failure =
2.7 - Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
2.8 + Unprovable | IncompleteUnprovable | ProofMissing | CantConnect | TimedOut |
2.9 OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
2.10 NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
2.11 InternalError | UnknownError of string
2.12 @@ -47,10 +47,10 @@
2.13 open ATP_Problem
2.14
2.15 datatype failure =
2.16 - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
2.17 - SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | NoRealZ3 |
2.18 - MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError |
2.19 - UnknownError of string
2.20 + Unprovable | IncompleteUnprovable | ProofMissing | CantConnect | TimedOut |
2.21 + OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
2.22 + NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
2.23 + InternalError | UnknownError of string
2.24
2.25 fun strip_spaces_in_list _ [] = []
2.26 | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
2.27 @@ -90,6 +90,9 @@
2.28 "The " ^ prover ^ " problem is unprovable."
2.29 | string_for_failure prover IncompleteUnprovable =
2.30 "The " ^ prover ^ " cannot prove the problem."
2.31 + | string_for_failure prover ProofMissing =
2.32 + "The " ^ prover ^ " claims the conjecture is a theorem but did not provide \
2.33 + \a proof."
2.34 | string_for_failure _ CantConnect = "Cannot connect to remote server."
2.35 | string_for_failure _ TimedOut = "Timed out."
2.36 | string_for_failure prover OutOfResources =
2.37 @@ -117,8 +120,6 @@
2.38 \Isabelle developers."
2.39 | string_for_failure prover MalformedOutput =
2.40 "The " ^ prover ^ " output is malformed."
2.41 - | string_for_failure prover Interrupted =
2.42 - "The " ^ prover ^ " was interrupted."
2.43 | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
2.44 | string_for_failure prover InternalError =
2.45 "An internal " ^ prover ^ " error occurred."
2.46 @@ -163,7 +164,7 @@
2.47 case extract_known_failure known_failures output of
2.48 NONE => (case extract_tstplike_proof proof_delims output of
2.49 "" => ("", SOME (if res_code = 0 andalso output = "" then
2.50 - Interrupted
2.51 + ProofMissing
2.52 else
2.53 UnknownError (short_output verbose output)))
2.54 | tstplike_proof =>
3.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 09 15:48:43 2011 +0100
3.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 09 17:18:57 2011 +0100
3.3 @@ -36,7 +36,11 @@
3.4 val vampireN : string
3.5 val sine_eN : string
3.6 val snarkN : string
3.7 + val z3_atpN : string
3.8 val remote_prefix : string
3.9 + val remote_atp :
3.10 + string -> string -> string list -> (string * string) list
3.11 + -> (failure * string) list -> int -> bool -> string * atp_config
3.12 val add_atp : string * atp_config -> theory -> theory
3.13 val get_atp : theory -> string -> atp_config
3.14 val supported_atps : theory -> string list
3.15 @@ -75,6 +79,7 @@
3.16 val vampireN = "vampire"
3.17 val sine_eN = "sine_e"
3.18 val snarkN = "snark"
3.19 +val z3_atpN = "z3_atp"
3.20 val remote_prefix = "remote_"
3.21
3.22 structure Data = Theory_Data
3.23 @@ -296,6 +301,11 @@
3.24 val remote_snark =
3.25 remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] []
3.26 250 (* FUDGE *) true
3.27 +val remote_z3_atp =
3.28 + remote_atp z3_atpN "Z3---" ["2.18"] []
3.29 + [(IncompleteUnprovable, "SZS status Satisfiable"),
3.30 + (ProofMissing, "SZS status Unsatisfiable")]
3.31 + 250 (* FUDGE *) false
3.32
3.33 (* Setup *)
3.34
3.35 @@ -318,7 +328,7 @@
3.36 Synchronized.change systems (fn _ => get_systems ())
3.37
3.38 val atps = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
3.39 - remote_snark]
3.40 + remote_snark, remote_z3_atp]
3.41 val setup = fold add_atp atps
3.42
3.43 end;