112 "SYN/SYN393^4.003.p", |
112 "SYN/SYN393^4.003.p", |
113 "SYN/SYN389^4.p"] |
113 "SYN/SYN389^4.p"] |
114 *} |
114 *} |
115 |
115 |
116 ML {* |
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"); |
117 interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory} |
123 interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory} |
118 *} |
124 *} |
119 |
125 |
120 ML {* |
126 ML {* |
121 interpretation_tests (get_timeout @{context}) @{context} |
127 fun interp_gain timeout thy file = |
122 (some_probs @ take_too_long @ timeouts @ more_probs) |
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 |
123 *} |
147 *} |
124 |
148 |
125 |
149 |
126 subsection "Test against whole TPTP" |
150 subsection "Test against whole TPTP" |
127 |
151 |