author blanchet Wed Apr 18 22:40:25 2012 +0200 (2012-04-18 ago) changeset 47562 a72239723ae8 parent 47561 92d88c89efff child 47563 01f687b84aff
tuned SZS status output
```     1.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 18 22:40:25 2012 +0200
1.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 18 22:40:25 2012 +0200
1.3 @@ -54,7 +54,8 @@
1.4     || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
1.5     || Scan.this_string "negated_conjecture") --| \$\$ "," -- parse_formula
1.6        --| \$\$ ")" --| \$\$ "."
1.7 -    >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
1.8 +    >> (fn ("conjecture", phi) => (true, AConn (ANot, [phi]))
1.9 +         | (_, phi) => (false, phi))
1.10    || Scan.this_string "thf" >> (fn _ => raise THF ())
1.11
1.12  val parse_problem =
1.13 @@ -108,7 +109,7 @@
1.14
1.15  fun mk_meta_not P = Logic.mk_implies (P, @{prop False})
1.16
1.17 -fun get_tptp_formula (_, role, _, P, _) =
1.18 +fun get_tptp_formula (_, role, P, _) =
1.19    P |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not
1.20
1.21  fun read_tptp_file thy file_name =
1.22 @@ -116,21 +117,21 @@
1.23      (case parse_tptp_problem (File.read path) of
1.24         (_, s :: ss) =>
1.25         raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
1.26 -     | (phis, []) =>
1.27 -       map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula) phis)
1.28 +     | (problem, []) =>
1.29 +       (exists fst problem,
1.30 +        map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula o snd)
1.31 +            problem))
1.32      handle THF () =>
1.33 -    TPTP_Interpret.interpret_file true (Path.explode "\$TPTP") path [] [] thy
1.34 -    |> fst |> #3 |> map get_tptp_formula
1.35 +    let
1.36 +      val problem =
1.37 +        TPTP_Interpret.interpret_file true (Path.explode "\$TPTP") path [] [] thy
1.38 +        |> fst |> #3
1.39 +    in
1.40 +      (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,
1.41 +       map get_tptp_formula problem)
1.42 +    end
1.43    end
1.44
1.45 -fun print_szs_from_outcome s =
1.46 -  "% SZS status " ^
1.47 -  (if s = Nitpick.genuineN then
1.48 -     "CounterSatisfiable"
1.49 -   else
1.50 -     "Unknown")
1.51 -  |> writeln
1.52 -
1.53  (** Isabelle (combination of provers) **)
1.54
1.55  fun isabelle_tptp_file file_name = ()
1.56 @@ -140,7 +141,7 @@
1.57
1.58  fun nitpick_tptp_file file_name =
1.59    let
1.60 -    val ts = read_tptp_file @{theory} file_name
1.61 +    val (falsify, ts) = read_tptp_file @{theory} file_name
1.62      val state = Proof.init @{context}
1.63      val params =
1.64        [("card", "1\<emdash>100"),
1.65 @@ -148,6 +149,7 @@
1.66         ("sat_solver", "smart"),
1.68         ("batch_size", "10"),
1.69 +       ("falsify", if falsify then "true" else "false"),
1.70         (* ("debug", "true"), *)
1.71         ("verbose", "true"),
1.72         (* ("overlord", "true"), *)
1.73 @@ -162,24 +164,31 @@
1.74      val step = 0
1.75      val subst = []
1.76    in
1.77 -    Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst ts
1.78 -        @{prop False}
1.79 -    |> fst |> print_szs_from_outcome
1.80 +    Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst ts
1.81 +        (if falsify then @{prop False} else @{prop True}); ()
1.82    end
1.83
1.84
1.85  (** Refute **)
1.86
1.87 +fun print_szs_from_outcome falsify s =
1.88 +  "% SZS status " ^
1.89 +  (if s = "genuine" then
1.90 +     if falsify then "CounterSatisfiable" else "Satisfiable"
1.91 +   else
1.92 +     "Unknown")
1.93 +  |> writeln
1.94 +
1.95  fun refute_tptp_file file_name =
1.96    let
1.97 -    val ts = read_tptp_file @{theory} file_name
1.98 +    val (falsify, ts) = read_tptp_file @{theory} file_name
1.99      val params =
1.100        [("maxtime", "10000"),
1.101         ("assms", "true"),
1.102         ("expect", Nitpick.genuineN)]
1.103    in
1.104      Refute.refute_term @{context} params ts @{prop False}
1.105 -    |> print_szs_from_outcome
1.106 +    |> print_szs_from_outcome falsify
1.107    end
1.108
1.109
```
```     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 18 22:40:25 2012 +0200
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 18 22:40:25 2012 +0200
2.3 @@ -680,7 +680,7 @@
2.4                  if falsify then "CounterSatisfiable" else "Satisfiable"
2.5                else
2.6                  "Unknown") ^ "\n" ^
2.7 -             "% SZS output start FiniteModel\n");
2.8 +             "% SZS output start FiniteModel");
2.9           pprint_a (Pretty.chunks
2.10               [Pretty.blk (0,
2.11                    (pstrs ((if mode = Auto_Try then "Auto " else "") ^
2.12 @@ -693,7 +693,7 @@
2.13                      | pretties => pstrs " for " @ pretties) @
2.14                     [Pretty.str ":\n"])),
2.15                Pretty.indent indent_size reconstructed_model]);
2.16 -         print_t (fn () => "% SZS output stop\n");
2.17 +         print_t (fn () => "% SZS output stop");
2.18           if genuine then
2.19             (if check_genuine andalso standard then
2.20                case prove_hol_model scope tac_timeout free_names sel_names
2.21 @@ -1005,7 +1005,7 @@
2.22            (print_nt (fn () => excipit "checked"); unknownN)
2.23          else if max_genuine = original_max_genuine then
2.24            if max_potential = original_max_potential then
2.25 -            (print_t (K "% SZS status Unknown\n");
2.26 +            (print_t (K "% SZS status Unknown");
2.27               print_nt (fn () =>
2.28                   "Nitpick found no " ^ das_wort_model ^ "." ^
2.29                   (if not standard andalso likely_in_struct_induct_step then
```