src/HOL/TPTP/TPTP_Interpret_Test.thy
author sultana
Tue Apr 17 16:14:07 2012 +0100 (2012-04-17)
changeset 47518 b2f209258621
parent 47516 9c29589c9b31
child 47547 1a5dc8377b5c
permissions -rw-r--r--
more cleaning of tptp tests;
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@47516
   117
  interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
sultana@47512
   118
*}
sultana@47512
   119
sultana@47516
   120
ML {*
sultana@47518
   121
 interpretation_tests (get_timeout @{context}) @{context}
sultana@47516
   122
   (some_probs @ take_too_long @ timeouts @ more_probs)
sultana@47516
   123
*}
sultana@47516
   124
sultana@47512
   125
sultana@47512
   126
subsection "Test against whole TPTP"
sultana@47512
   127
sultana@47512
   128
text "Run interpretation over all problems. This works only for logics
sultana@47512
   129
 for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
sultana@47512
   130
ML {*
sultana@47518
   131
  if test_all @{context} then
sultana@47518
   132
    (report @{context} "Interpreting all problems";
sultana@47518
   133
     S timed_test (interpretation_test (get_timeout @{context})) @{context})
sultana@47518
   134
  else ()
sultana@47512
   135
*}
sultana@47512
   136
sultana@47518
   137
end