better compliance with TPTP SZS standard
authorblanchet
Fri Oct 02 21:06:32 2015 +0200 (2015-10-02 ago)
changeset 613109a50ea544fd3
parent 61309 a2548e708f03
child 61311 150aa3015c47
better compliance with TPTP SZS standard
src/HOL/TPTP/atp_problem_import.ML
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Fri Oct 02 20:28:56 2015 +0200
     1.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Oct 02 21:06:32 2015 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4        (if s = "genuine" then
     1.5           if falsify then "CounterSatisfiable" else "Satisfiable"
     1.6         else
     1.7 -         "Unknown")
     1.8 +         "GaveUp")
     1.9        |> writeln
    1.10      val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
    1.11      val params =
    1.12 @@ -268,7 +268,7 @@
    1.13      (if success then
    1.14         if null conjs then "Unsatisfiable" else "Theorem"
    1.15       else
    1.16 -       "Unknown"))
    1.17 +       "GaveUp"))
    1.18  
    1.19  fun sledgehammer_tptp_file thy timeout file_name =
    1.20    let
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Oct 02 20:28:56 2015 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Oct 02 21:06:32 2015 +0200
     2.3 @@ -636,7 +636,7 @@
     2.4                 (if genuine then
     2.5                    if falsify then "CounterSatisfiable" else "Satisfiable"
     2.6                  else
     2.7 -                  "Unknown") ^ "\n" ^
     2.8 +                  "GaveUp") ^ "\n" ^
     2.9                 "% SZS output start FiniteModel")
    2.10          val (reconstructed_model, codatatypes_ok) =
    2.11            reconstruct_hol_model