47512
|
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_PROBLEMS_PATH, which should point to the
|
|
6 |
TPTP-vX.Y.Z/Problems directory.
|
|
7 |
*)
|
|
8 |
|
|
9 |
theory TPTP_Interpret_Test
|
|
10 |
imports TPTP_Test TPTP_Interpret
|
|
11 |
begin
|
|
12 |
|
|
13 |
section "Interpreter tests"
|
47518
|
14 |
|
47512
|
15 |
text "Interpret a problem."
|
|
16 |
ML {*
|
|
17 |
val (time, ((type_map, const_map, fmlas), thy)) =
|
|
18 |
Timing.timing
|
|
19 |
(TPTP_Interpret.interpret_file
|
|
20 |
false
|
|
21 |
(Path.dir tptp_probs_dir)
|
|
22 |
(Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
|
|
23 |
[]
|
|
24 |
[])
|
|
25 |
@{theory}
|
|
26 |
*}
|
|
27 |
|
|
28 |
text "... and display nicely."
|
|
29 |
ML {*
|
47518
|
30 |
List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
|
|
31 |
|
47512
|
32 |
(*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
|
|
33 |
List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
|
|
34 |
*}
|
|
35 |
|
|
36 |
subsection "Multiple tests"
|
|
37 |
|
|
38 |
ML {*
|
47518
|
39 |
(*default timeout is 1 min*)
|
47516
|
40 |
fun interpret timeout file thy =
|
47518
|
41 |
TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
|
47516
|
42 |
(TPTP_Interpret.interpret_file
|
|
43 |
false
|
|
44 |
(Path.dir tptp_probs_dir)
|
|
45 |
file
|
|
46 |
[]
|
|
47 |
[]) thy
|
|
48 |
|
|
49 |
fun interpret_timed timeout file thy =
|
|
50 |
Timing.timing (interpret timeout file) thy
|
|
51 |
|
47512
|
52 |
fun interpretation_test timeout ctxt =
|
|
53 |
test_fn ctxt
|
47518
|
54 |
(fn file => interpret timeout file (Proof_Context.theory_of ctxt))
|
47512
|
55 |
"interpreter"
|
|
56 |
()
|
|
57 |
|
|
58 |
fun interpretation_tests timeout ctxt probs =
|
|
59 |
List.app
|
|
60 |
(interpretation_test timeout ctxt)
|
|
61 |
(List.map situate probs)
|
|
62 |
*}
|
|
63 |
|
|
64 |
ML {*
|
|
65 |
val some_probs =
|
|
66 |
["LCL/LCL825-1.p",
|
|
67 |
"ALG/ALG001^5.p",
|
|
68 |
"COM/COM003+2.p",
|
|
69 |
"COM/COM003-1.p",
|
|
70 |
"COM/COM024^5.p",
|
|
71 |
"DAT/DAT017=1.p",
|
|
72 |
"NUM/NUM021^1.p",
|
|
73 |
"NUM/NUM858=1.p",
|
|
74 |
"SYN/SYN000^2.p"]
|
|
75 |
|
|
76 |
val take_too_long =
|
|
77 |
["NLP/NLP562+1.p",
|
|
78 |
"SWV/SWV546-1.010.p",
|
|
79 |
"SWV/SWV567-1.015.p",
|
|
80 |
"LCL/LCL680+1.020.p"]
|
|
81 |
|
47516
|
82 |
val timeouts =
|
|
83 |
["NUM/NUM923^4.p",
|
|
84 |
"NUM/NUM926^4.p",
|
|
85 |
"NUM/NUM925^4.p",
|
|
86 |
"NUM/NUM924^4.p",
|
|
87 |
"CSR/CSR153^3.p",
|
|
88 |
"CSR/CSR151^3.p",
|
|
89 |
"CSR/CSR148^3.p",
|
|
90 |
"CSR/CSR120^3.p",
|
|
91 |
"CSR/CSR150^3.p",
|
|
92 |
"CSR/CSR119^3.p",
|
|
93 |
"CSR/CSR149^3.p"]
|
|
94 |
|
47512
|
95 |
val more_probs =
|
|
96 |
["GEG/GEG014^1.p",
|
|
97 |
"GEG/GEG009^1.p",
|
|
98 |
"GEG/GEG004^1.p",
|
|
99 |
"GEG/GEG007^1.p",
|
|
100 |
"GEG/GEG016^1.p",
|
|
101 |
"GEG/GEG024=1.p",
|
|
102 |
"GEG/GEG010^1.p",
|
|
103 |
"GEG/GEG003^1.p",
|
|
104 |
"GEG/GEG018^1.p",
|
|
105 |
"SYN/SYN045^4.p",
|
|
106 |
"SYN/SYN001^4.001.p",
|
|
107 |
"SYN/SYN000^2.p",
|
|
108 |
"SYN/SYN387^4.p",
|
|
109 |
"SYN/SYN393^4.002.p",
|
|
110 |
"SYN/SYN978^4.p",
|
|
111 |
"SYN/SYN044^4.p",
|
|
112 |
"SYN/SYN393^4.003.p",
|
|
113 |
"SYN/SYN389^4.p"]
|
|
114 |
*}
|
|
115 |
|
|
116 |
ML {*
|
47516
|
117 |
interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
|
47512
|
118 |
*}
|
|
119 |
|
47516
|
120 |
ML {*
|
47518
|
121 |
interpretation_tests (get_timeout @{context}) @{context}
|
47516
|
122 |
(some_probs @ take_too_long @ timeouts @ more_probs)
|
|
123 |
*}
|
|
124 |
|
47512
|
125 |
|
|
126 |
subsection "Test against whole TPTP"
|
|
127 |
|
|
128 |
text "Run interpretation over all problems. This works only for logics
|
|
129 |
for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
|
|
130 |
ML {*
|
47518
|
131 |
if test_all @{context} then
|
|
132 |
(report @{context} "Interpreting all problems";
|
|
133 |
S timed_test (interpretation_test (get_timeout @{context})) @{context})
|
|
134 |
else ()
|
47512
|
135 |
*}
|
|
136 |
|
47518
|
137 |
end |