1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Jul 27 08:52:40 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Jul 27 08:52:40 2012 +0200
     1.3 @@ -52,7 +52,8 @@
     1.4      -> string * failure option
     1.5    val is_same_atp_step : step_name -> step_name -> bool
     1.6    val scan_general_id : string list -> string * string list
     1.7 -  val satallax_unsat_coreN : string
     1.8 +  val satallax_coreN : string
     1.9 +  val z3_tptp_coreN : string
    1.10    val parse_formula :
    1.11      string list
    1.12      -> (string, 'a, (string, 'a) ho_term, string) formula * string list
    1.13 @@ -154,7 +155,7 @@
    1.14  fun extract_delimited (begin_delim, end_delim) output =
    1.15    output |> first_field begin_delim |> the |> snd
    1.16           |> first_field end_delim |> the |> fst
    1.17 -         |> first_field "\n" |> the |> snd
    1.18 +         |> perhaps (try (first_field "\n" #> the #> snd))
    1.19    handle Option.Option => ""
    1.20  
    1.21  val tstp_important_message_delims =
    1.22 @@ -461,16 +462,23 @@
    1.23     >> (fn ((((num, rule), deps), u), names) =>
    1.24            Inference_Step ((num, these names), u, rule, map (rpair []) deps))) x
    1.25  
    1.26 -val satallax_unsat_coreN = "__satallax_unsat_core" (* arbitrary *)
    1.27 +val satallax_coreN = "__satallax_core" (* arbitrary *)
    1.28 +val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *)
    1.29 +
    1.30 +(* Syntax: core(<name>,[<name>,...,<name>]). *)
    1.31 +fun parse_z3_tptp_line x =
    1.32 +  (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
    1.33 +   >> (fn (name, names) =>
    1.34 +          Inference_Step (("", name :: names), dummy_phi, z3_tptp_coreN, []))) x
    1.35  
    1.36  (* Syntax: <name> *)
    1.37  fun parse_satallax_line x =
    1.38    (scan_general_id --| Scan.option ($$ " ")
    1.39 -   >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_unsat_coreN, [])))
    1.40 -      x
    1.41 +   >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_coreN, []))) x
    1.42  
    1.43  fun parse_line problem =
    1.44 -  parse_tstp_line problem || parse_spass_line || parse_satallax_line
    1.45 +  parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
    1.46 +  || parse_satallax_line
    1.47  fun parse_proof problem tstp =
    1.48    tstp |> strip_spaces_except_between_idents
    1.49         |> raw_explode

     2.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Jul 27 08:52:40 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Jul 27 08:52:40 2012 +0200
     2.3 @@ -216,7 +216,7 @@
     2.4           dependencies in the TSTP proof. Remove the next line once this is
     2.5           fixed. *)
     2.6         add_non_rec_defs fact_names
     2.7 -     else if rule = satallax_unsat_coreN then
     2.8 +     else if rule = satallax_coreN then
     2.9         (fn [] =>
    2.10             (* Satallax doesn't include definitions in its unsatisfiable cores,
    2.11                so we assume the worst and include them all here. *)

     3.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 27 08:52:40 2012 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 27 08:52:40 2012 +0200
     3.3 @@ -481,8 +481,9 @@
     3.4  val z3_tptp_config : atp_config =
     3.5    {exec = (["Z3_HOME"], ["z3"]),
     3.6     arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
     3.7 -     "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
     3.8 -   proof_delims = [],
     3.9 +     "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
    3.10 +     string_of_int (to_secs 1 timeout),
    3.11 +   proof_delims = [("\ncore(", ").")],
    3.12     known_failures = known_szs_status_failures,
    3.13     prem_role = Hypothesis,
    3.14     best_slices =