src/HOL/TPTP/TPTP_Interpret_Test.thy
author sultana
Wed Apr 18 17:33:11 2012 +0100 (2012-04-18)
changeset 47547 1a5dc8377b5c
parent 47518 b2f209258621
child 47548 60849d8c457d
permissions -rw-r--r--
more tptp testing support functions;
sultana@47512
     1
(*  Title:      HOL/TPTP/TPTP_Interpret_Test.thy
sultana@47512
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
sultana@47512
     3
sultana@47512
     4
Some tests for the TPTP interface. Some of the tests rely on the Isabelle
sultana@47512
     5
environment variable TPTP_PROBLEMS_PATH, which should point to the
sultana@47512
     6
TPTP-vX.Y.Z/Problems directory.
sultana@47512
     7
*)
sultana@47512
     8
sultana@47512
     9
theory TPTP_Interpret_Test
sultana@47512
    10
imports TPTP_Test TPTP_Interpret
sultana@47512
    11
begin
sultana@47512
    12
sultana@47512
    13
section "Interpreter tests"
sultana@47518
    14
sultana@47512
    15
text "Interpret a problem."
sultana@47512
    16
ML {*
sultana@47512
    17
  val (time, ((type_map, const_map, fmlas), thy)) =
sultana@47512
    18
    Timing.timing
sultana@47512
    19
      (TPTP_Interpret.interpret_file
sultana@47512
    20
       false
sultana@47512
    21
       (Path.dir tptp_probs_dir)
sultana@47512
    22
      (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
sultana@47512
    23
       []
sultana@47512
    24
       [])
sultana@47512
    25
      @{theory}
sultana@47512
    26
*}
sultana@47512
    27
sultana@47512
    28
text "... and display nicely."
sultana@47512
    29
ML {*
sultana@47518
    30
  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
sultana@47518
    31
sultana@47512
    32
  (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
sultana@47512
    33
  List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
sultana@47512
    34
*}
sultana@47512
    35
sultana@47512
    36
subsection "Multiple tests"
sultana@47512
    37
sultana@47512
    38
ML {*
sultana@47518
    39
  (*default timeout is 1 min*)
sultana@47516
    40
  fun interpret timeout file thy =
sultana@47518
    41
    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
sultana@47516
    42
     (TPTP_Interpret.interpret_file
sultana@47516
    43
       false
sultana@47516
    44
       (Path.dir tptp_probs_dir)
sultana@47516
    45
       file
sultana@47516
    46
       []
sultana@47516
    47
       []) thy
sultana@47516
    48
sultana@47516
    49
  fun interpret_timed timeout file thy =
sultana@47516
    50
    Timing.timing (interpret timeout file) thy
sultana@47516
    51
sultana@47512
    52
  fun interpretation_test timeout ctxt =
sultana@47512
    53
    test_fn ctxt
sultana@47518
    54
     (fn file => interpret timeout file (Proof_Context.theory_of ctxt))
sultana@47512
    55
     "interpreter"
sultana@47512
    56
     ()
sultana@47512
    57
sultana@47512
    58
  fun interpretation_tests timeout ctxt probs =
sultana@47512
    59
    List.app
sultana@47512
    60
     (interpretation_test timeout ctxt)
sultana@47512
    61
     (List.map situate probs)
sultana@47512
    62
*}
sultana@47512
    63
sultana@47512
    64
ML {*
sultana@47512
    65
  val some_probs =
sultana@47512
    66
    ["LCL/LCL825-1.p",
sultana@47512
    67
     "ALG/ALG001^5.p",
sultana@47512
    68
     "COM/COM003+2.p",
sultana@47512
    69
     "COM/COM003-1.p",
sultana@47512
    70
     "COM/COM024^5.p",
sultana@47512
    71
     "DAT/DAT017=1.p",
sultana@47512
    72
     "NUM/NUM021^1.p",
sultana@47512
    73
     "NUM/NUM858=1.p",
sultana@47512
    74
     "SYN/SYN000^2.p"]
sultana@47512
    75
sultana@47512
    76
  val take_too_long =
sultana@47512
    77
    ["NLP/NLP562+1.p",
sultana@47512
    78
     "SWV/SWV546-1.010.p",
sultana@47512
    79
     "SWV/SWV567-1.015.p",
sultana@47512
    80
     "LCL/LCL680+1.020.p"]
sultana@47512
    81
sultana@47516
    82
  val timeouts =
sultana@47516
    83
    ["NUM/NUM923^4.p",
sultana@47516
    84
    "NUM/NUM926^4.p",
sultana@47516
    85
    "NUM/NUM925^4.p",
sultana@47516
    86
    "NUM/NUM924^4.p",
sultana@47516
    87
    "CSR/CSR153^3.p",
sultana@47516
    88
    "CSR/CSR151^3.p",
sultana@47516
    89
    "CSR/CSR148^3.p",
sultana@47516
    90
    "CSR/CSR120^3.p",
sultana@47516
    91
    "CSR/CSR150^3.p",
sultana@47516
    92
    "CSR/CSR119^3.p",
sultana@47516
    93
    "CSR/CSR149^3.p"]
sultana@47516
    94
sultana@47512
    95
  val more_probs =
sultana@47512
    96
    ["GEG/GEG014^1.p",
sultana@47512
    97
     "GEG/GEG009^1.p",
sultana@47512
    98
     "GEG/GEG004^1.p",
sultana@47512
    99
     "GEG/GEG007^1.p",
sultana@47512
   100
     "GEG/GEG016^1.p",
sultana@47512
   101
     "GEG/GEG024=1.p",
sultana@47512
   102
     "GEG/GEG010^1.p",
sultana@47512
   103
     "GEG/GEG003^1.p",
sultana@47512
   104
     "GEG/GEG018^1.p",
sultana@47512
   105
     "SYN/SYN045^4.p",
sultana@47512
   106
     "SYN/SYN001^4.001.p",
sultana@47512
   107
     "SYN/SYN000^2.p",
sultana@47512
   108
     "SYN/SYN387^4.p",
sultana@47512
   109
     "SYN/SYN393^4.002.p",
sultana@47512
   110
     "SYN/SYN978^4.p",
sultana@47512
   111
     "SYN/SYN044^4.p",
sultana@47512
   112
     "SYN/SYN393^4.003.p",
sultana@47512
   113
     "SYN/SYN389^4.p"]
sultana@47512
   114
*}
sultana@47512
   115
sultana@47512
   116
ML {*
sultana@47547
   117
 interpretation_tests (get_timeout @{context}) @{context}
sultana@47547
   118
   (some_probs @ take_too_long @ timeouts @ more_probs)
sultana@47547
   119
*}
sultana@47547
   120
sultana@47547
   121
ML {*
sultana@47547
   122
  parse_timed (situate "NUM/NUM923^4.p");
sultana@47516
   123
  interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
sultana@47512
   124
*}
sultana@47512
   125
sultana@47516
   126
ML {*
sultana@47547
   127
  fun interp_gain timeout thy file =
sultana@47547
   128
    let
sultana@47547
   129
      val t1 = (parse_timed file |> fst)
sultana@47547
   130
      val t2 = (interpret_timed timeout file thy |> fst)
sultana@47547
   131
        handle exn => (*FIXME*)
sultana@47547
   132
          if Exn.is_interrupt exn then reraise exn
sultana@47547
   133
          else
sultana@47547
   134
            (warning (" test: file " ^ Path.print file ^
sultana@47547
   135
             " raised exception: " ^ ML_Compiler.exn_message exn);
sultana@47547
   136
             {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
sultana@47547
   137
      val to_real = Time.toReal
sultana@47547
   138
      val diff_elapsed =
sultana@47547
   139
        #elapsed t2 - #elapsed t1
sultana@47547
   140
        |> to_real
sultana@47547
   141
      val elapsed = to_real (#elapsed t2)
sultana@47547
   142
    in
sultana@47547
   143
      (Path.base file, diff_elapsed,
sultana@47547
   144
       diff_elapsed / elapsed,
sultana@47547
   145
       elapsed)
sultana@47547
   146
    end
sultana@47516
   147
*}
sultana@47516
   148
sultana@47512
   149
sultana@47512
   150
subsection "Test against whole TPTP"
sultana@47512
   151
sultana@47512
   152
text "Run interpretation over all problems. This works only for logics
sultana@47512
   153
 for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
sultana@47512
   154
ML {*
sultana@47518
   155
  if test_all @{context} then
sultana@47518
   156
    (report @{context} "Interpreting all problems";
sultana@47518
   157
     S timed_test (interpretation_test (get_timeout @{context})) @{context})
sultana@47518
   158
  else ()
sultana@47512
   159
*}
sultana@47512
   160
sultana@47518
   161
end