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