# HG changeset patch
# User blanchet
# Date 1305793453 -7200
# Node ID f133c030856a2e066ef7a9c3534147595509b195
# Parent  0e594ba0b3249e84fc081aa37c7ec5f439620062
better error reporting: detect missing E proofs and remove Vampire native format error

diff -r 0e594ba0b324 -r f133c030856a src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed May 18 15:45:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu May 19 10:24:13 2011 +0200
@@ -195,22 +195,18 @@
 
 fun extract_tstplike_proof_and_outcome debug verbose complete res_code
                                        proof_delims known_failures output =
-  case extract_known_failure known_failures output of
-    NONE =>
-    (case extract_tstplike_proof proof_delims output of
-       "" =>
-       ("", SOME (if res_code = 0 andalso (not debug orelse output = "") then
-                    ProofMissing
+   case extract_tstplike_proof proof_delims output of
+     "" =>
+     ("", SOME (if res_code = 0 andalso (not debug orelse output = "") then
+                  ProofMissing
+                else case extract_known_failure known_failures output of
+                  SOME failure =>
+                  if failure = IncompleteUnprovable andalso complete then
+                    Unprovable
                   else
-                    UnknownError (short_output verbose output)))
-     | tstplike_proof =>
-       if res_code = 0 then (tstplike_proof, NONE)
-       else ("", SOME (UnknownError (short_output verbose output))))
-  | SOME failure =>
-    ("", SOME (if failure = IncompleteUnprovable andalso complete then
-                 Unprovable
-               else
-                 failure))
+                    failure
+                | NONE => UnknownError (short_output verbose output)))
+   | tstplike_proof => (tstplike_proof, NONE)
 
 fun mk_anot (AConn (ANot, [phi])) = phi
   | mk_anot phi = AConn (ANot, [phi])
diff -r 0e594ba0b324 -r f133c030856a src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 18 15:45:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 19 10:24:13 2011 +0200
@@ -209,6 +209,7 @@
    known_failures =
      [(Unprovable, "SZS status: CounterSatisfiable"),
       (Unprovable, "SZS status CounterSatisfiable"),
+      (ProofMissing, "SZS status Theorem"),
       (TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded"),
       (OutOfResources,
@@ -289,8 +290,7 @@
      [(Unprovable, "UNPROVABLE"),
       (IncompleteUnprovable, "CANNOT PROVE"),
       (IncompleteUnprovable, "SZS status GaveUp"),
-      (ProofMissing, "[predicate definition introduction]"),
-      (ProofMissing, "predicate_definition_introduction,[]"), (* TSTP *)
+      (ProofMissing, "predicate_definition_introduction,[]"),
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),