tuned SZS status output
authorblanchet
Wed Apr 18 22:40:25 2012 +0200 (2012-04-18 ago)
changeset 47562a72239723ae8
parent 47561 92d88c89efff
child 47563 01f687b84aff
tuned SZS status output
src/HOL/TPTP/atp_problem_import.ML
src/HOL/Tools/Nitpick/nitpick.ML
     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.67         ("max_threads", "1"),
    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