# HG changeset patch
# User blanchet
# Date 1396619800 -7200
# Node ID 9cb137ec6ec8f6aa449436fc167752b0539e2e3e
# Parent  ae4f904c98b03cd78f62c57a956f21bd5ee0a8ee
use Z3 TPTP cores rather than proofs since the latter are somewhat broken

diff -r ae4f904c98b0 -r 9cb137ec6ec8 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Apr 04 14:44:51 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Apr 04 15:56:40 2014 +0200
@@ -46,6 +46,7 @@
   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
@@ -75,6 +76,7 @@
 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
 
@@ -211,11 +213,13 @@
 
 (**** PARSING OF TSTP FORMAT ****)
 
-(* Strings enclosed in single quotes (e.g., file names) *)
+(* Strings enclosed in single quotes (e.g., file names), identifiers possibly starting
+   with "$" and possibly with "!" in them (for "z3_tptp"). *)
 val scan_general_id =
   $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
-  || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
-     >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
+  || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o pairself implode))
+    -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o pairself implode)) ""
+    >> op ^
 
 val skip_term =
   let
@@ -416,14 +420,14 @@
               | Inference_Source (rule, deps) => (((num, []), phi), rule, deps))
             fun mk_step () = (name, role_of_tptp_string role, phi, rule, map (rpair []) deps)
           in
-            (case role_of_tptp_string role of
-              Definition =>
-              (case phi of
-                 AAtom (ATerm (("equal", _), _)) =>
-                 (* Vampire's equality proxy axiom *)
-                 (name, Definition, phi, rule, map (rpair []) deps)
-               | _ => mk_step ())
-            | _ => mk_step ())
+            [(case role_of_tptp_string role of
+               Definition =>
+               (case phi of
+                  AAtom (ATerm (("equal", _), _)) =>
+                  (* Vampire's equality proxy axiom *)
+                  (name, Definition, phi, rule, map (rpair []) deps)
+                | _ => mk_step ())
+             | _ => mk_step ())]
           end)
 
 (**** PARSING OF SPASS OUTPUT ****)
@@ -464,7 +468,7 @@
      -- Scan.option (Scan.this_string "derived from formulae "
                      |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
    >> (fn ((((num, rule), deps), u), names) =>
-          ((num, these names), Unknown, u, rule, map (rpair []) deps))) x
+          [((num, these names), Unknown, u, rule, map (rpair []) deps)])) x
 
 fun parse_spass_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
 fun parse_spass_pirate_dependencies x =
@@ -489,23 +493,28 @@
            File_Source (_, SOME s) => ([s], spass_input_rule, [])
          | Inference_Source (rule, deps) => ([], rule, deps))
      in
-       ((num, names), Unknown, u, rule, map (rpair []) deps)
+       [((num, names), Unknown, u, rule, map (rpair []) deps)]
      end)) x
 
 fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
 
 (* Syntax: <name> *)
-fun parse_satallax_line x =
-  (scan_general_id --| Scan.option ($$ " ") >> core_inference satallax_core_rule) x
+fun parse_satallax_core_line x =
+  (scan_general_id --| Scan.option ($$ " ") >> (single o core_inference satallax_core_rule)) x
+
+(* Syntax: SZS core <name> ... <name> *)
+fun parse_z3_tptp_core_line x =
+  (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id)
+   >> map (core_inference z3_tptp_core_rule)) x
 
 fun parse_line problem =
-  parse_tstp_line problem || parse_spass_line || parse_spass_pirate_line || parse_satallax_line
+  parse_tstp_line problem || parse_z3_tptp_core_line || parse_spass_line || parse_spass_pirate_line
+  || parse_satallax_core_line
 fun parse_proof problem =
   strip_spaces_except_between_idents
   #> raw_explode
   #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
-         (Scan.finite Symbol.stopper
-                         (Scan.repeat1 (parse_line problem))))
+       (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line problem) >> flat)))
   #> fst
 
 fun core_of_agsyhol_proof s =
diff -r ae4f904c98b0 -r 9cb137ec6ec8 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Apr 04 14:44:51 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Apr 04 15:56:40 2014 +0200
@@ -620,7 +620,7 @@
 val z3_tptp_config : atp_config =
   {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,
+     "-core -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
    proof_delims = [("SZS status Theorem", "")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,