# HG changeset patch
# User blanchet
# Date 1318880257 -7200
# Node ID 170dffc6df751ab258279572eaee3ddea7873e9c
# Parent  699848baf70b2346bdcf47bb46dbe7d4affdef06
parse Satallax unsat cores

diff -r 699848baf70b -r 170dffc6df75 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Oct 17 18:05:14 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Oct 17 21:37:37 2011 +0200
@@ -324,6 +324,8 @@
           (* We ignore TFF and THF types for now. *)
           AQuant (q, map (rpair NONE o ho_term_head) ts, phi))) x
 
+val dummy_phi = AAtom (ATerm ("", []))
+
 fun skip_formula ss =
   let
     fun skip _ [] = []
@@ -335,7 +337,7 @@
       | skip n ("]" :: ss) = skip (n - 1) ss
       | skip n (")" :: ss) = skip (n - 1) ss
       | skip n (_ :: ss) = skip n ss
-  in (AAtom (ATerm ("", [])), skip 0 ss) end
+  in (dummy_phi, skip 0 ss) end
 
 val parse_tstp_extra_arguments =
   Scan.optional ($$ "," |-- parse_annotation
@@ -456,17 +458,22 @@
                 NONE
   | NONE => NONE
 
-(* Syntax: <num>[0:<inference><annotations>]
-   <atoms> || <atoms> -> <atoms>. *)
-fun parse_spass_line spass_names x =
-  (scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-     -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
-   >> (fn ((num, deps), u) =>
-          Inference ((num, resolve_spass_num spass_names num), u,
-                     map (swap o `(resolve_spass_num spass_names)) deps))) x
+(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. *)
+fun parse_spass_line spass_names =
+  scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
+    -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
+  >> (fn ((num, deps), u) =>
+         Inference ((num, resolve_spass_num spass_names num), u,
+                    map (swap o `(resolve_spass_num spass_names)) deps))
+
+(* Syntax: <name> *)
+fun parse_satallax_line problem =
+  scan_general_id --| Scan.option ($$ " ")
+  >> (fn s => Inference ((s, SOME [s]), dummy_phi, []))
 
 fun parse_line problem spass_names =
   parse_tstp_line problem || parse_spass_line spass_names
+  || parse_satallax_line problem
 fun parse_proof problem spass_names tstp =
   tstp |> strip_spaces_except_between_idents
        |> raw_explode
diff -r 699848baf70b -r 170dffc6df75 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Oct 17 18:05:14 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Oct 17 21:37:37 2011 +0200
@@ -266,9 +266,10 @@
    required_execs = [],
    arguments =
      fn _ => fn _ => fn _ => fn timeout => fn _ =>
-        "-t " ^ string_of_int (to_secs 1 timeout),
-   proof_delims = tstp_proof_delims,
-   known_failures = [(ProofMissing, "SZS status Theorem")],
+        "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
+   proof_delims =
+     [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
+   known_failures = [],
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices =