author blanchet Wed, 18 Apr 2012 22:40:25 +0200 changeset 47562 a72239723ae8 parent 47561 92d88c89efff child 47563 01f687b84aff
tuned SZS status output
 src/HOL/TPTP/atp_problem_import.ML file | annotate | diff | comparison | revisions src/HOL/Tools/Nitpick/nitpick.ML file | annotate | diff | comparison | revisions
```--- 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

@@ -116,21 +117,21 @@
(_, 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"),
("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

```
```--- 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```