# HG changeset patch
# User blanchet
# Date 1319034973 -7200
# Node ID e3c13fa443efe8e3b9f9ef790ca8fe53e8660c32
# Parent  62b8bcf2477364184932047785f0dfa48e602d4a
more uniform SZS status handling

diff -r 62b8bcf24773 -r e3c13fa443ef src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Oct 19 16:36:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Oct 19 16:36:13 2011 +0200
@@ -467,13 +467,12 @@
                     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_satallax_line x =
+  (scan_general_id --| Scan.option ($$ " ")
+   >> (fn s => Inference ((s, SOME [s]), dummy_phi, []))) x
 
 fun parse_line problem spass_names =
-  parse_tstp_line problem || parse_spass_line spass_names
-  || parse_satallax_line problem
+  parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line
 fun parse_proof problem spass_names tstp =
   tstp |> strip_spaces_except_between_idents
        |> raw_explode
diff -r 62b8bcf24773 -r e3c13fa443ef src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 19 16:36:13 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 19 16:36:13 2011 +0200
@@ -101,6 +101,24 @@
    (NoPerl, "env: perl"),
    (NoLibwwwPerl, "Can't locate HTTP")]
 
+fun known_szs_failures wrap =
+  [(Unprovable, wrap "CounterSatisfiable"),
+   (Unprovable, wrap "Satisfiable"),
+   (GaveUp, wrap "GaveUp"),
+   (GaveUp, wrap "Unknown"),
+   (GaveUp, wrap "Incomplete"),
+   (ProofMissing, wrap "Theorem"),
+   (ProofMissing, wrap "Unsatisfiable"),
+   (TimedOut, wrap "Timeout"),
+   (Inappropriate, wrap "Inappropriate"),
+   (OutOfResources, wrap "ResourceOut"),
+   (OutOfResources, wrap "MemoryOut"),
+   (Interrupted, wrap "Forced"),
+   (Interrupted, wrap "User")]
+
+val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
+val known_says_failures = known_szs_failures (prefix " says ")
+
 (* named ATPs *)
 
 val eN = "e"
@@ -208,14 +226,10 @@
         " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
-     [(Unprovable, "SZS status: CounterSatisfiable"),
-      (Unprovable, "SZS status CounterSatisfiable"),
-      (ProofMissing, "SZS status Theorem"),
-      (TimedOut, "Failure: Resource limit exceeded (time)"),
+     known_szs_status_failures @
+     [(TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded"),
-      (OutOfResources, "# Cannot determine problem status"),
-      (OutOfResources, "SZS status: ResourceOut"),
-      (OutOfResources, "SZS status ResourceOut")],
+      (OutOfResources, "# Cannot determine problem status")],
    conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
@@ -244,7 +258,7 @@
         "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
         |> sos = sosN ? prefix "--sos ",
    proof_delims = tstp_proof_delims,
-   known_failures = [],
+   known_failures = known_szs_status_failures,
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
@@ -269,7 +283,7 @@
         "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
    proof_delims =
      [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
-   known_failures = [],
+   known_failures = known_szs_status_failures,
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices =
@@ -337,10 +351,9 @@
       ("% SZS output start Refutation", "% SZS output end Refutation"),
       ("% SZS output start Proof", "% SZS output end Proof")],
    known_failures =
+     known_szs_status_failures @
      [(GaveUp, "UNPROVABLE"),
       (GaveUp, "CANNOT PROVE"),
-      (GaveUp, "SZS status GaveUp"),
-      (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option"),
@@ -373,13 +386,7 @@
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
      "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
    proof_delims = [],
-   known_failures =
-     [(GaveUp, "SZS status Satisfiable"),
-      (GaveUp, "SZS status CounterSatisfiable"),
-      (GaveUp, "SZS status GaveUp"),
-      (GaveUp, "SZS status Unknown"),
-      (ProofMissing, "SZS status Unsatisfiable"),
-      (ProofMissing, "SZS status Theorem")],
+   known_failures = known_szs_status_failures,
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =
@@ -399,7 +406,7 @@
    required_execs = [],
    arguments = K (K (K (K (K "")))),
    proof_delims = [],
-   known_failures = [(GaveUp, "SZS status Unknown")],
+   known_failures = known_szs_status_failures,
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
@@ -456,15 +463,7 @@
      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
      ^ " -s " ^ the_system system_name system_versions,
    proof_delims = union (op =) tstp_proof_delims proof_delims,
-   known_failures = known_failures @ known_perl_failures @
-     [(Unprovable, "says Satisfiable"),
-      (Unprovable, "says CounterSatisfiable"),
-      (GaveUp, "says Unknown"),
-      (GaveUp, "says GaveUp"),
-      (ProofMissing, "says Theorem"),
-      (ProofMissing, "says Unsatisfiable"),
-      (TimedOut, "says Timeout"),
-      (Inappropriate, "says Inappropriate")],
+   known_failures = known_failures @ known_perl_failures @ known_says_failures,
    conj_sym_kind = conj_sym_kind,
    prem_kind = prem_kind,
    best_slices = fn ctxt =>