# HG changeset patch
# User blanchet
# Date 1343371960 -7200
# Node ID 0debf65972c7925637b59abc11fc7d931562f867
# Parent  726590131ca10c61d0fab1d38970b3d496e4472e
extract Z3 unsat cores (for "z3_tptp")

diff -r 726590131ca1 -r 0debf65972c7 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Jul 27 08:52:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Jul 27 08:52:40 2012 +0200
@@ -52,7 +52,8 @@
     -> string * failure option
   val is_same_atp_step : step_name -> step_name -> bool
   val scan_general_id : string list -> string * string list
-  val satallax_unsat_coreN : string
+  val satallax_coreN : string
+  val z3_tptp_coreN : string
   val parse_formula :
     string list
     -> (string, 'a, (string, 'a) ho_term, string) formula * string list
@@ -154,7 +155,7 @@
 fun extract_delimited (begin_delim, end_delim) output =
   output |> first_field begin_delim |> the |> snd
          |> first_field end_delim |> the |> fst
-         |> first_field "\n" |> the |> snd
+         |> perhaps (try (first_field "\n" #> the #> snd))
   handle Option.Option => ""
 
 val tstp_important_message_delims =
@@ -461,16 +462,23 @@
    >> (fn ((((num, rule), deps), u), names) =>
           Inference_Step ((num, these names), u, rule, map (rpair []) deps))) x
 
-val satallax_unsat_coreN = "__satallax_unsat_core" (* arbitrary *)
+val satallax_coreN = "__satallax_core" (* arbitrary *)
+val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *)
+
+(* Syntax: core(<name>,[<name>,...,<name>]). *)
+fun parse_z3_tptp_line x =
+  (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
+   >> (fn (name, names) =>
+          Inference_Step (("", name :: names), dummy_phi, z3_tptp_coreN, []))) x
 
 (* Syntax: <name> *)
 fun parse_satallax_line x =
   (scan_general_id --| Scan.option ($$ " ")
-   >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_unsat_coreN, [])))
-      x
+   >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_coreN, []))) x
 
 fun parse_line problem =
-  parse_tstp_line problem || parse_spass_line || parse_satallax_line
+  parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
+  || parse_satallax_line
 fun parse_proof problem tstp =
   tstp |> strip_spaces_except_between_idents
        |> raw_explode
diff -r 726590131ca1 -r 0debf65972c7 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Jul 27 08:52:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Jul 27 08:52:40 2012 +0200
@@ -216,7 +216,7 @@
          dependencies in the TSTP proof. Remove the next line once this is
          fixed. *)
        add_non_rec_defs fact_names
-     else if rule = satallax_unsat_coreN then
+     else if rule = satallax_coreN then
        (fn [] =>
            (* Satallax doesn't include definitions in its unsatisfiable cores,
               so we assume the worst and include them all here. *)
diff -r 726590131ca1 -r 0debf65972c7 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 27 08:52:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 27 08:52:40 2012 +0200
@@ -481,8 +481,9 @@
 val z3_tptp_config : atp_config =
   {exec = (["Z3_HOME"], ["z3"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
-     "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
-   proof_delims = [],
+     "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
+     string_of_int (to_secs 1 timeout),
+   proof_delims = [("\ncore(", ").")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =