# HG changeset patch
# User blanchet
# Date 1280304366 -7200
# Node ID df99f022751df5e3be73f181121d457cb1c55d51
# Parent  54448f5d151f652e62cf9658da4842b2e8e49db9
support latest version of Vampire (1.0) locally

diff -r 54448f5d151f -r df99f022751d src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 28 00:53:24 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 28 10:06:06 2010 +0200
@@ -135,12 +135,13 @@
   {executable = ("VAMPIRE_HOME", "vampire"),
    required_executables = [],
    arguments = fn _ => fn timeout =>
-     "--output_syntax tptp --mode casc -t " ^
-     string_of_int (to_generous_secs timeout),
+     "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
+     " --input_file ",
    proof_delims =
      [("=========== Refutation ==========",
        "======= End of refutation ======="),
-      ("% SZS output start Refutation", "% SZS output end Refutation")],
+      ("% SZS output start Refutation", "% SZS output end Refutation"),
+      ("% SZS output start Proof", "% SZS output end Proof")],
    known_failures =
      [(Unprovable, "UNPROVABLE"),
       (IncompleteUnprovable, "CANNOT PROVE"),
diff -r 54448f5d151f -r df99f022751d src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 00:53:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 10:06:06 2010 +0200
@@ -522,12 +522,15 @@
 (* A list consisting of the first number in each line is returned. For TSTP,
    interesting lines have the form "fof(108, axiom, ...)", where the number
    (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
-   the first number (108) is extracted. *)
+   the first number (108) is extracted. For Vampire, we look for
+   "108. ... [input]". *)
 fun extract_formula_numbers_in_atp_proof atp_proof =
   let
     val tokens_of = String.tokens (not o Char.isAlphaNum)
     fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num
       | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
+      | extract_num (num :: rest) =
+        (case List.last rest of "input" => Int.fromString num | _ => NONE)
       | extract_num _ = NONE
   in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end