# HG changeset patch
# User blanchet
# Date 1334781625 -7200
# Node ID a72239723ae8d5799d9c9fab24b0864862f6fac9
# Parent  92d88c89efffe6cc583fe03fc12449371531cae9
tuned SZS status output

diff -r 92d88c89efff -r a72239723ae8 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 18 22:40:25 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 18 22:40:25 2012 +0200
@@ -54,7 +54,8 @@
    || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
    || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
       --| $$ ")" --| $$ "."
-    >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
+    >> (fn ("conjecture", phi) => (true, AConn (ANot, [phi]))
+         | (_, phi) => (false, phi))
   || Scan.this_string "thf" >> (fn _ => raise THF ())
 
 val parse_problem =
@@ -108,7 +109,7 @@
 
 fun mk_meta_not P = Logic.mk_implies (P, @{prop False})
 
-fun get_tptp_formula (_, role, _, P, _) =
+fun get_tptp_formula (_, role, P, _) =
   P |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not
 
 fun read_tptp_file thy file_name =
@@ -116,21 +117,21 @@
     (case parse_tptp_problem (File.read path) of
        (_, s :: ss) =>
        raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
-     | (phis, []) =>
-       map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula) phis)
+     | (problem, []) =>
+       (exists fst problem,
+        map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula o snd)
+            problem))
     handle THF () =>
-    TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
-    |> fst |> #3 |> map get_tptp_formula
+    let
+      val problem =
+        TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
+        |> fst |> #3
+    in
+      (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,
+       map get_tptp_formula problem)
+    end
   end
 
-fun print_szs_from_outcome s =
-  "% SZS status " ^
-  (if s = Nitpick.genuineN then
-     "CounterSatisfiable"
-   else
-     "Unknown")
-  |> writeln
-
 (** Isabelle (combination of provers) **)
 
 fun isabelle_tptp_file file_name = ()
@@ -140,7 +141,7 @@
 
 fun nitpick_tptp_file file_name =
   let
-    val ts = read_tptp_file @{theory} file_name
+    val (falsify, ts) = read_tptp_file @{theory} file_name
     val state = Proof.init @{context}
     val params =
       [("card", "1\<emdash>100"),
@@ -148,6 +149,7 @@
        ("sat_solver", "smart"),
        ("max_threads", "1"),
        ("batch_size", "10"),
+       ("falsify", if falsify then "true" else "false"),
        (* ("debug", "true"), *)
        ("verbose", "true"),
        (* ("overlord", "true"), *)
@@ -162,24 +164,31 @@
     val step = 0
     val subst = []
   in
-    Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst ts
-        @{prop False}
-    |> fst |> print_szs_from_outcome
+    Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst ts
+        (if falsify then @{prop False} else @{prop True}); ()
   end
 
 
 (** Refute **)
 
+fun print_szs_from_outcome falsify s =
+  "% SZS status " ^
+  (if s = "genuine" then
+     if falsify then "CounterSatisfiable" else "Satisfiable"
+   else
+     "Unknown")
+  |> writeln
+
 fun refute_tptp_file file_name =
   let
-    val ts = read_tptp_file @{theory} file_name
+    val (falsify, ts) = read_tptp_file @{theory} file_name
     val params =
       [("maxtime", "10000"),
        ("assms", "true"),
        ("expect", Nitpick.genuineN)]
   in
     Refute.refute_term @{context} params ts @{prop False}
-    |> print_szs_from_outcome
+    |> print_szs_from_outcome falsify
   end
 
 
diff -r 92d88c89efff -r a72239723ae8 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 18 22:40:25 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 18 22:40:25 2012 +0200
@@ -680,7 +680,7 @@
                 if falsify then "CounterSatisfiable" else "Satisfiable"
               else
                 "Unknown") ^ "\n" ^
-             "% SZS output start FiniteModel\n");
+             "% SZS output start FiniteModel");
          pprint_a (Pretty.chunks
              [Pretty.blk (0,
                   (pstrs ((if mode = Auto_Try then "Auto " else "") ^
@@ -693,7 +693,7 @@
                     | pretties => pstrs " for " @ pretties) @
                    [Pretty.str ":\n"])),
               Pretty.indent indent_size reconstructed_model]);
-         print_t (fn () => "% SZS output stop\n");
+         print_t (fn () => "% SZS output stop");
          if genuine then
            (if check_genuine andalso standard then
               case prove_hol_model scope tac_timeout free_names sel_names
@@ -1005,7 +1005,7 @@
           (print_nt (fn () => excipit "checked"); unknownN)
         else if max_genuine = original_max_genuine then
           if max_potential = original_max_potential then
-            (print_t (K "% SZS status Unknown\n");
+            (print_t (K "% SZS status Unknown");
              print_nt (fn () =>
                  "Nitpick found no " ^ das_wort_model ^ "." ^
                  (if not standard andalso likely_in_struct_induct_step then