drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines
authorblanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 42748a37095d03074
parent 42747 f132d13fcf75
child 42749 47f283fcf2ae
drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -260,19 +260,10 @@
     1.4                    ::: Scan.repeat ($$ "," |-- parse_annotation)) []
     1.5     >> flat) x
     1.6  
     1.7 -(* Vampire proof lines sometimes contain needless information such as "(0:3)",
     1.8 -   which can be hard to disambiguate from function application in an LL(1)
     1.9 -   parser. As a workaround, we extend the TPTP term syntax with such detritus
    1.10 -   and ignore it. *)
    1.11 -fun parse_vampire_detritus x =
    1.12 -  (scan_general_id |-- $$ ":" --| scan_general_id >> K []) x
    1.13 -
    1.14  fun parse_term x =
    1.15    (scan_general_id
    1.16       --| Scan.option ($$ ":" -- scan_general_id) (* ignore TFF types for now *)
    1.17 -     -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
    1.18 -                       --| $$ ")") []
    1.19 -     --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
    1.20 +     -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
    1.21     >> ATerm) x
    1.22  and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
    1.23  
    1.24 @@ -348,22 +339,6 @@
    1.25               | _ => Inference (name, phi, map (rpair NONE) deps)
    1.26             end)) x
    1.27  
    1.28 -(**** PARSING OF VAMPIRE OUTPUT ****)
    1.29 -
    1.30 -val parse_vampire_braced_stuff =
    1.31 -  $$ "{" -- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) -- $$ "}"
    1.32 -fun parse_vampire_parenthesized_detritus x =
    1.33 -  ($$ "(" |-- parse_vampire_detritus --| $$ ")") x
    1.34 -
    1.35 -(* Syntax: <num>. <formula> <annotation> *)
    1.36 -fun parse_vampire_line x =
    1.37 -  (scan_general_id --| $$ "." -- parse_formula
    1.38 -     --| Scan.option parse_vampire_braced_stuff
    1.39 -     --| Scan.option parse_vampire_parenthesized_detritus
    1.40 -     -- parse_annotation
    1.41 -   >> (fn ((num, phi), deps) =>
    1.42 -          Inference ((num, NONE), phi, map (rpair NONE) deps))) x
    1.43 -
    1.44  (**** PARSING OF SPASS OUTPUT ****)
    1.45  
    1.46  (* SPASS returns clause references of the form "x.y". We ignore "y", whose role
    1.47 @@ -400,7 +375,7 @@
    1.48     >> (fn ((num, deps), u) =>
    1.49            Inference ((num, NONE), u, map (rpair NONE) deps))) x
    1.50  
    1.51 -fun parse_line x = (parse_tstp_line || parse_vampire_line || parse_spass_line) x
    1.52 +fun parse_line x = (parse_tstp_line || parse_spass_line) x
    1.53  fun parse_proof s =
    1.54    s |> strip_spaces_except_between_ident_chars
    1.55      |> raw_explode
     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu May 12 15:29:19 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 12 15:29:19 2011 +0200
     2.3 @@ -276,8 +276,7 @@
     2.4    {exec = ("VAMPIRE_HOME", "vampire"),
     2.5     required_execs = [],
     2.6     arguments = fn ctxt => fn slice => fn timeout => fn _ =>
     2.7 -     (* This would work too but it's less tested: "--proof tptp " ^ *)
     2.8 -     "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
     2.9 +     "--proof tptp --mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
    2.10       " --thanks \"Andrei and Krystof\" --input_file"
    2.11       |> (slice = 0 orelse Config.get ctxt vampire_force_sos)
    2.12          ? prefix "--sos on ",