fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
authorblanchet
Thu Dec 16 15:12:17 2010 +0100 (2010-12-16)
changeset 412031393514094d7
parent 41202 bf00e0a578e8
child 41204 bd57cf5944cb
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Dec 16 15:12:17 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Dec 16 15:12:17 2010 +0100
     1.3 @@ -100,11 +100,12 @@
     1.4    | string_for_failure prover NoLibwwwPerl =
     1.5      "The Perl module \"libwww-perl\"" ^ missing_message_tail prover
     1.6    | string_for_failure prover MalformedInput =
     1.7 -    "The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \
     1.8 -    \developers."
     1.9 +    "The " ^ prover ^ " problem is malformed. Please report this to the \
    1.10 +    \Isabelle developers."
    1.11    | string_for_failure prover MalformedOutput =
    1.12      "The " ^ prover ^ " output is malformed."
    1.13 -  | string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted."
    1.14 +  | string_for_failure prover Interrupted =
    1.15 +    "The " ^ prover ^ " was interrupted."
    1.16    | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
    1.17    | string_for_failure prover InternalError =
    1.18      "An internal " ^ prover ^ " error occurred."
    1.19 @@ -216,9 +217,9 @@
    1.20  
    1.21  fun parse_term x =
    1.22    (scan_general_id
    1.23 -    -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
    1.24 -                      --| $$ ")") []
    1.25 -    --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
    1.26 +     -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
    1.27 +                       --| $$ ")") []
    1.28 +     --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
    1.29     >> ATerm) x
    1.30  and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
    1.31  
    1.32 @@ -253,6 +254,8 @@
    1.33    Scan.optional ($$ "," |-- parse_annotation false
    1.34                   --| Scan.option ($$ "," |-- parse_annotations false)) []
    1.35  
    1.36 +val vampire_unknown_fact = "unknown"
    1.37 +
    1.38  (* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
    1.39     The <num> could be an identifier, but we assume integers. *)
    1.40  val parse_tstp_line =
    1.41 @@ -263,7 +266,8 @@
    1.42            let
    1.43              val (name, deps) =
    1.44                case deps of
    1.45 -                ["file", _, s] => ((num, SOME s), [])
    1.46 +                ["file", _, s] =>
    1.47 +                ((num, if s = vampire_unknown_fact then NONE else SOME s), [])
    1.48                | _ => ((num, NONE), deps)
    1.49            in
    1.50              case role of
    1.51 @@ -282,12 +286,15 @@
    1.52  
    1.53  val parse_vampire_braced_stuff =
    1.54    $$ "{" -- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) -- $$ "}"
    1.55 -  -- Scan.option ($$ "(" |-- parse_vampire_detritus --| $$ ")")
    1.56 +val parse_vampire_parenthesized_detritus =
    1.57 +  $$ "(" |-- parse_vampire_detritus --| $$ ")"
    1.58  
    1.59  (* Syntax: <num>. <formula> <annotation> *)
    1.60  val parse_vampire_line =
    1.61    scan_general_id --| $$ "." -- parse_formula
    1.62 -    --| Scan.option parse_vampire_braced_stuff -- parse_annotation true
    1.63 +    --| Scan.option parse_vampire_braced_stuff
    1.64 +    --| Scan.option parse_vampire_parenthesized_detritus
    1.65 +    -- parse_annotation true
    1.66    >> (fn ((num, phi), deps) =>
    1.67           Inference ((num, NONE), phi, map (rpair NONE) deps))
    1.68  
     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Dec 16 15:12:17 2010 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Dec 16 15:12:17 2010 +0100
     2.3 @@ -153,8 +153,9 @@
     2.4    {exec = ("VAMPIRE_HOME", "vampire"),
     2.5     required_execs = [],
     2.6     arguments = fn complete => fn timeout =>
     2.7 -     ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
     2.8 -      " --thanks Andrei --input_file")
     2.9 +     (* This would work too but it's less tested: "--proof tptp " ^ *)
    2.10 +     "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
    2.11 +     " --thanks \"Andrei and Krystof\" --input_file"
    2.12       |> not complete ? prefix "--sos on ",
    2.13     has_incomplete_mode = true,
    2.14     proof_delims =
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Dec 16 15:12:17 2010 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Dec 16 15:12:17 2010 +0100
     3.3 @@ -144,6 +144,8 @@
     3.4        "\nTo minimize the number of lemmas, try this: " ^
     3.5        Markup.markup Markup.sendback command ^ "."
     3.6  
     3.7 +val vampire_fact_prefix = "f" (* grrr... *)
     3.8 +
     3.9  fun resolve_fact fact_names ((_, SOME s)) =
    3.10      (case strip_prefix_and_unascii fact_prefix s of
    3.11         SOME s' => (case find_first_in_list_vector fact_names s' of
    3.12 @@ -151,7 +153,7 @@
    3.13                     | NONE => [])
    3.14       | NONE => [])
    3.15    | resolve_fact fact_names (num, NONE) =
    3.16 -    case Int.fromString num of
    3.17 +    case Int.fromString (perhaps (try (unprefix vampire_fact_prefix)) num) of
    3.18        SOME j =>
    3.19        if j > 0 andalso j <= Vector.length fact_names then
    3.20          Vector.sub (fact_names, j - 1)