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