Add SZS output + several fixes

globals.ml

@@ -43,3 +43,5 @@ let end_comment() =
   if !output_dk then ";)"
   else if !output_lp then "*/"
   else "*)"
+
+let has_a_conjecture = ref true

globals.mli

@@ -36,3 +36,6 @@ val check_axiom : bool ref;;
 
 val begin_comment : unit -> string;;
 val end_comment : unit -> string;;
+
+(* Has a conjecture, useful for SZS output *)
+val has_a_conjecture : bool ref;;

main.ml

@@ -7,6 +7,53 @@ open Globals;;
 open Namespace;;
 open Expr;;
 
+(* part of SZS ontology, see
+   https://tptp.org/cgi-bin/SeeTPTP?Category=Documents&File=SZSOntology
+*)
+type szs_success =
+    Success
+  | Theorem
+  | Unsatisfiable
+
+type szs_error =
+    NoSuccess
+  | Unknown
+  | ResourceOut
+
+type szs_status =
+    Suc of szs_success
+  | Err of szs_error
+
+let szs_status out (status, file) =
+  fprintf out "%% SZS status %a for %s"
+    (fun out -> function
+      | Suc Success -> fprintf out "Success"
+      | Suc Theorem -> fprintf out "Theorem"
+      | Suc Unsatisfiable -> fprintf out "Unsatisfiable"
+      | Err NoSuccess -> fprintf out "NoSuccess"
+      | Err Unknown -> fprintf out "Unknown"
+      | Err ResourceOut -> fprintf out "ResourceOut"
+    )
+    status file
+
+let get_status found =
+  if found then
+    if !Globals.has_a_conjecture then
+      Suc Theorem
+    else
+      Suc Unsatisfiable
+  else
+    Err Unknown
+
+let print_status status file =
+  printf "%s %s\n%a\n%s\n"
+    (begin_comment ())
+    (match status with Suc _ -> " PROOF-FOUND "
+                     | Err _ ->  "NO-PROOF")
+    szs_status (status, file)
+    (end_comment())
+
+
 type proof_level =
   | Proof_none
   | Proof_h of int
@@ -457,14 +504,9 @@ let main () =
     if is_open then
         retcode := 12;
     if not !quiet_flag then begin
-      if is_open then
-        if !Globals.signature_name <> "" then ()
-        else printf "%s" (begin_comment() ^ " NO-PROOF " ^ end_comment() ^ "\n")
-      else
-        if !Globals.signature_name <> "" then ()
-        else printf "%s" (begin_comment() ^ " PROOF-FOUND " ^ end_comment() ^ "\n");
+      print_status (get_status @@ not is_open) file;
       flush stdout
-      end;
+    end;
     let llp = lazy (optim (Extension.postprocess
                              (Mltoll.translate th_name ppphrases proof)))
     in
@@ -504,10 +546,12 @@ let main () =
   with
   | Prove.NoProof ->
      retcode := 12;
-     if not !quiet_flag then (if !Globals.signature_name <> "" then () else printf "(* NO-PROOF *)\n");
+     if not !quiet_flag then
+       print_status (Err Unknown) file
   | Prove.LimitsExceeded ->
      retcode := 13;
-     if not !quiet_flag then (if !Globals.signature_name <> "" then () else printf "(* NO-PROOF *)\n");
+     if not !quiet_flag then
+       print_status (Err ResourceOut) file
   end;
   if !stats_flag then begin
     eprintf "nodes searched: %d\n" !Globals.inferences;

parsetptp.mly

@@ -93,7 +93,7 @@ let cnf_to_formula l =
 
 file:
   | EOF             { [] }
-  | phrase file     { $1 :: $2 }
+  | phrase file     { Globals.has_a_conjecture := false; $1 :: $2 }
 ;
 phrase:
   | INCLUDE OPEN LIDENT CLOSE DOT  { Phrase.Include ($3, None) }

tptp.ml

@@ -141,11 +141,12 @@ let rec translate_one dirs accu p =
   | Formula (name, ("lemma"|"theorem"), body, None) ->
       Hyp (name, body, 1) :: accu
   | Formula (name, "conjecture", body, None) ->
-      tptp_thm_name := name;
-      Hyp (goal_name, enot (body), 0) :: accu
+    tptp_thm_name := name;
+    Globals.has_a_conjecture := true;
+    Hyp (goal_name, enot (body), 0) :: accu
   | Formula (name, "negated_conjecture", body, None) ->
-      tptp_thm_name := "negation_of_" ^ name;
-      Hyp (name, body, 0) :: accu
+    tptp_thm_name := "negation_of_" ^ name;
+    Hyp (name, body, 0) :: accu
   (* TFF formulas *)
   | Formula (name, "tff_type", body, None) ->
       Hyp (name, body, 13) :: accu
@@ -162,10 +163,11 @@ let rec translate_one dirs accu p =
   | Formula (name, ("tff_lemma"|"tff_theorem"), body, None) ->
       Hyp (name, body, 11) :: accu
   | Formula (name, "tff_conjecture", body, None) ->
-      tptp_thm_name := name;
-      Hyp (goal_name, enot (body), 10) :: accu
+    tptp_thm_name := name;
+    Globals.has_a_conjecture := true;
+    Hyp (goal_name, enot (body), 10) :: accu
   | Formula (name, "tff_negated_conjecture", body, None) ->
-      Hyp (name, body, 10) :: accu
+    Hyp (name, body, 10) :: accu
   (* Fallback *)
   | Formula (name, k, body, _) ->
       Error.warn ("unknown formula kind: " ^ k);