--- 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"),
--- 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