# HG changeset patch # User wenzelm # Date 1396607877 -7200 # Node ID f0bd809b5d35f827fb8f3c22c8c00970b407b96d # Parent 6e08b45432f676ff99660752977bcc0037094ae1# Parent 386e4cb7ad68b695399e43c09fea544edb53fda6 merged diff -r 386e4cb7ad68 -r f0bd809b5d35 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Fri Apr 04 12:07:48 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Apr 04 12:37:57 2014 +0200 @@ -46,7 +46,6 @@ val spass_input_rule : string val spass_pre_skolemize_rule : string val spass_skolemize_rule : string - val z3_tptp_core_rule : string val short_output : bool -> string -> string val string_of_atp_failure : atp_failure -> string @@ -76,7 +75,6 @@ val spass_input_rule = "Inp" val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *) val spass_skolemize_rule = "__Sko" (* arbitrary *) -val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *) exception UNRECOGNIZED_ATP_PROOF of unit @@ -148,10 +146,18 @@ else ":\n" ^ s) fun extract_delimited (begin_delim, end_delim) output = - output |> first_field begin_delim |> the |> snd - |> first_field end_delim |> the |> fst - |> perhaps (try (first_field "\n" #> the #> snd)) - handle Option.Option => "" + (case first_field begin_delim output of + SOME (_, tail) => + (case first_field "\n" tail of + SOME (_, tail') => + if end_delim = "" then + tail' + else + (case first_field end_delim tail' of + SOME (body, _) => body + | NONE => "") + | NONE => "") + | NONE => "") val tstp_important_message_delims = ("% SZS start RequiredInformation", "% SZS end RequiredInformation") @@ -166,8 +172,7 @@ (* Splits by the first possible of a list of delimiters. *) fun extract_tstplike_proof delims output = - (case pairself (find_first (fn s => String.isSubstring s output)) - (ListPair.unzip delims) of + (case pairself (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of (SOME begin_delim, SOME end_delim) => extract_delimited (begin_delim, end_delim) output | _ => "") @@ -179,7 +184,7 @@ fun extract_tstplike_proof_and_outcome verbose proof_delims known_failures output = (case (extract_tstplike_proof proof_delims output, - extract_known_atp_failure known_failures output) of + extract_known_atp_failure known_failures output) of (_, SOME ProofIncomplete) => ("", NONE) | ("", SOME ProofMissing) => ("", NONE) | ("", NONE) => ("", SOME (UnknownError (short_output verbose output))) @@ -218,9 +223,9 @@ | skip n accum (ss as s :: ss') = if s = "," andalso n = 0 then (accum, ss) - else if member (op =) [")", "]", ">", "}"] s then + else if member (op =) [")", "]"] s then if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss' - else if member (op =) ["(", "[", "<", "{"] s then + else if member (op =) ["(", "["] s then skip (n + 1) (s :: accum) ss' else skip n (s :: accum) ss' @@ -240,7 +245,7 @@ (parse_inference_source >> snd || scan_general_id --| skip_term >> single) x and parse_dependencies x = - (parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency) >> flat) x + (Scan.repeat (Scan.option ($$ ",") |-- parse_dependency) >> flat) x and parse_file_source x = (Scan.this_string "file" |-- $$ "(" |-- scan_general_id -- Scan.option ($$ "," |-- scan_general_id) --| $$ ")") x @@ -277,7 +282,9 @@ -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") [] -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> ATerm) x -and parse_term x = (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x +and parse_term x = + (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) + --| Scan.option parse_type_signature >> list_app) x and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x fun parse_atom x = @@ -316,8 +323,7 @@ >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x val parse_tstp_extra_arguments = - Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) - dummy_inference + Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) dummy_inference val waldmeister_conjecture_name = "conjecture_1" @@ -488,18 +494,12 @@ fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, []) -(* Syntax: core(,[,...,]). *) -fun parse_z3_tptp_line x = - (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]" - >> (fn (name, names) => (("", name :: names), Unknown, dummy_phi, z3_tptp_core_rule, []))) x - (* Syntax: *) fun parse_satallax_line x = (scan_general_id --| Scan.option ($$ " ") >> core_inference satallax_core_rule) x fun parse_line problem = - parse_tstp_line problem || parse_spass_line || parse_spass_pirate_line || parse_z3_tptp_line - || parse_satallax_line + parse_tstp_line problem || parse_spass_line || parse_spass_pirate_line || parse_satallax_line fun parse_proof problem = strip_spaces_except_between_idents #> raw_explode @@ -540,13 +540,11 @@ | map_term (AAbs (((s, ty), tm), args)) = AAbs (((f s, map_type ty), map_term tm), map map_term args) - fun map_formula (AQuant (q, xs, phi)) = - AQuant (q, map (apfst f) xs, map_formula phi) + fun map_formula (AQuant (q, xs, phi)) = AQuant (q, map (apfst f) xs, map_formula phi) | map_formula (AConn (c, phis)) = AConn (c, map map_formula phis) | map_formula (AAtom t) = AAtom (map_term t) - fun map_step (name, role, phi, rule, deps) = - (name, role, map_formula phi, rule, deps) + fun map_step (name, role, phi, rule, deps) = (name, role, map_formula phi, rule, deps) in map map_step end diff -r 386e4cb7ad68 -r f0bd809b5d35 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Apr 04 12:07:48 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Apr 04 12:37:57 2014 +0200 @@ -621,7 +621,7 @@ {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name, - proof_delims = [], + proof_delims = [("SZS status Theorem", "")], known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices =