src/HOL/TPTP/TPTP_Interpret_Test.thy
author sultana
Tue Apr 17 16:14:07 2012 +0100 (2012-04-17)
changeset 47516 9c29589c9b31
parent 47512 b381d428a725
child 47518 b2f209258621
permissions -rw-r--r--
improved tptp interpretation test thy
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@47516
    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@47512
    30
  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
sultana@47512
    31
*}
sultana@47512
    32
ML {*
sultana@47512
    33
  (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
sultana@47512
    34
  List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
sultana@47512
    35
*}
sultana@47516
    36
*)
sultana@47512
    37
sultana@47512
    38
subsection "Multiple tests"
sultana@47512
    39
sultana@47512
    40
ML {*
sultana@47516
    41
  fun interpret timeout file thy =
sultana@47516
    42
    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout))
sultana@47516
    43
     (TPTP_Interpret.interpret_file
sultana@47516
    44
       false
sultana@47516
    45
       (Path.dir tptp_probs_dir)
sultana@47516
    46
       file
sultana@47516
    47
       []
sultana@47516
    48
       []) thy
sultana@47516
    49
sultana@47516
    50
  fun interpret_timed timeout file thy =
sultana@47516
    51
    Timing.timing (interpret timeout file) thy
sultana@47516
    52
sultana@47516
    53
  (*default timeout is 10 mins*)
sultana@47512
    54
  fun interpretation_test timeout ctxt =
sultana@47512
    55
    test_fn ctxt
sultana@47516
    56
     (fn file => (*FIXME use "interpret" function above*)
sultana@47516
    57
       TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout))
sultana@47512
    58
        (TPTP_Interpret.interpret_file
sultana@47512
    59
          false
sultana@47512
    60
          (Path.dir tptp_probs_dir)
sultana@47512
    61
          file
sultana@47512
    62
          []
sultana@47512
    63
          [])
sultana@47516
    64
          @{theory}(*FIXME*))
sultana@47512
    65
     "interpreter"
sultana@47512
    66
     ()
sultana@47512
    67
sultana@47512
    68
  fun interpretation_tests timeout ctxt probs =
sultana@47512
    69
    List.app
sultana@47512
    70
     (interpretation_test timeout ctxt)
sultana@47512
    71
     (List.map situate probs)
sultana@47512
    72
*}
sultana@47512
    73
sultana@47512
    74
ML {*
sultana@47512
    75
  val some_probs =
sultana@47512
    76
    ["LCL/LCL825-1.p",
sultana@47512
    77
     "ALG/ALG001^5.p",
sultana@47512
    78
     "COM/COM003+2.p",
sultana@47512
    79
     "COM/COM003-1.p",
sultana@47512
    80
     "COM/COM024^5.p",
sultana@47512
    81
     "DAT/DAT017=1.p",
sultana@47512
    82
     "NUM/NUM021^1.p",
sultana@47512
    83
     "NUM/NUM858=1.p",
sultana@47512
    84
     "SYN/SYN000^2.p"]
sultana@47512
    85
sultana@47512
    86
  val take_too_long =
sultana@47512
    87
    ["NLP/NLP562+1.p",
sultana@47512
    88
     "SWV/SWV546-1.010.p",
sultana@47512
    89
     "SWV/SWV567-1.015.p",
sultana@47512
    90
     "LCL/LCL680+1.020.p"]
sultana@47512
    91
sultana@47516
    92
  val timeouts =
sultana@47516
    93
    ["NUM/NUM923^4.p",
sultana@47516
    94
    "NUM/NUM926^4.p",
sultana@47516
    95
    "NUM/NUM925^4.p",
sultana@47516
    96
    "NUM/NUM924^4.p",
sultana@47516
    97
    "CSR/CSR153^3.p",
sultana@47516
    98
    "CSR/CSR151^3.p",
sultana@47516
    99
    "CSR/CSR148^3.p",
sultana@47516
   100
    "CSR/CSR120^3.p",
sultana@47516
   101
    "CSR/CSR150^3.p",
sultana@47516
   102
    "CSR/CSR119^3.p",
sultana@47516
   103
    "CSR/CSR149^3.p"]
sultana@47516
   104
sultana@47512
   105
  val more_probs =
sultana@47512
   106
    ["GEG/GEG014^1.p",
sultana@47512
   107
     "GEG/GEG009^1.p",
sultana@47512
   108
     "GEG/GEG004^1.p",
sultana@47512
   109
     "GEG/GEG007^1.p",
sultana@47512
   110
     "GEG/GEG016^1.p",
sultana@47512
   111
     "GEG/GEG024=1.p",
sultana@47512
   112
     "GEG/GEG010^1.p",
sultana@47512
   113
     "GEG/GEG003^1.p",
sultana@47512
   114
     "GEG/GEG018^1.p",
sultana@47512
   115
     "SYN/SYN045^4.p",
sultana@47512
   116
     "SYN/SYN001^4.001.p",
sultana@47512
   117
     "SYN/SYN000^2.p",
sultana@47512
   118
     "SYN/SYN387^4.p",
sultana@47512
   119
     "SYN/SYN393^4.002.p",
sultana@47512
   120
     "SYN/SYN978^4.p",
sultana@47512
   121
     "SYN/SYN044^4.p",
sultana@47512
   122
     "SYN/SYN393^4.003.p",
sultana@47512
   123
     "SYN/SYN389^4.p"]
sultana@47512
   124
*}
sultana@47512
   125
sultana@47512
   126
ML {*
sultana@47516
   127
  interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
sultana@47512
   128
*}
sultana@47512
   129
sultana@47516
   130
ML {*
sultana@47516
   131
 interpretation_tests 5 @{context}
sultana@47516
   132
   (some_probs @ take_too_long @ timeouts @ more_probs)
sultana@47516
   133
*}
sultana@47516
   134
sultana@47516
   135
declare [[warning_out = ""]]
sultana@47512
   136
sultana@47512
   137
subsection "Test against whole TPTP"
sultana@47512
   138
sultana@47512
   139
text "Run interpretation over all problems. This works only for logics
sultana@47512
   140
 for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
sultana@47512
   141
ML {*
sultana@47512
   142
  report @{context} "Interpreting all problems.";
sultana@47512
   143
  (*val _ = S timed_test (interpretation_test 5) @{context}*)
sultana@47512
   144
*}
sultana@47512
   145
sultana@47516
   146
end