1 flyspeck_needs "../formal_lp/formal_interval/m_verifier.hl";;
5 Arith_cache.reset_stat();
6 Arith_cache.reset_cache();
7 Arith_float.reset_stat();
8 Arith_float.reset_cache();;
11 (**************************)
13 let schwefel_poly = expr_to_vector_fun `(x1 - x2 pow 2) pow 2 + (x2 - &1) pow 2 +
14 (x1 - x3 pow 2) pow 2 + (x3 - &1) pow 2`;;
15 let rd_poly = expr_to_vector_fun `-- x1 + &2 * x2 - x3 - #0.835634534 * x2 * (&1 + x2)`;;
16 let caprasse_poly = expr_to_vector_fun `-- x1 * x3 pow 3 + &4 * x2 * x3 pow 2 * x4 +
17 &4 * x1 * x3 * x4 pow 2 + &2 * x2 * x4 pow 3 + &4 * x1 * x3 + &4 * x3 pow 2 -
18 &10 * x2 * x4 - &10 * x4 pow 2 + &2`;;
19 let lv_poly = expr_to_vector_fun `x1 * x2 pow 2 + x1 * x3 pow 2 + x1 * x4 pow 2 - #1.1 * x1 + &1`;;
20 let butcher_poly = expr_to_vector_fun `x6 * x2 pow 2 + x5 * x3 pow 2 - x1 * x4 pow 2 + x4 pow 2 -
21 &1 / &3 * x1 + &4 / &3 * x4`;;
22 let magnetism_poly = expr_to_vector_fun `x1 pow 2 + &2 * x2 pow 2 + &2 * x3 pow 2 + &2 * x4 pow 2 +
23 &2 * x5 pow 2 + &2 * x6 pow 2 + &2 * x7 pow 2 - x1`;;
24 let heart_poly = expr_to_vector_fun `-- x1 * x6 pow 3 + &3 * x1 * x6 * x7 pow 2 - x3 * x7 pow 3 +
25 &3 * x3 * x7 * x6 pow 2 - x2 * x5 pow 3 + &3 * x2 * x5 * x8 pow 2 - x4 * x8 pow 3 +
26 &3 * x4 * x8 * x5 pow 2 - #0.9563453`;;
29 let schwefel_min = `-- #0.00000000058806` and
30 rd_min = `-- #36.7126907` and
31 caprasse_min = `-- #3.1801` and
32 lv_min = `-- #20.801` and
33 butcher_min = `-- #1.44` and
34 magnetism_min = `-- #0.25001` and
35 heart_min = `-- #1.7435`;;
37 let schwefel_dom = `[-- &10; -- &10; -- &10]`, `[&10; &10; &10]`;;
38 let rd_dom = `[-- &5; -- &5; -- &5]`, `[&5; &5; &5]`;;
39 let caprasse_dom = `[-- #0.5; -- #0.5; -- #0.5; -- #0.5]`, `[#0.5; #0.5; #0.5; #0.5]`;;
40 let lv_dom = `[-- &2; -- &2; -- &2; -- &2]`, `[&2; &2; &2; &2]`;;
41 let butcher_dom = `[-- &1; -- #0.1; -- #0.1; -- &1; -- #0.1; -- #0.1]`,
42 `[&0; #0.9; #0.5; -- #0.1; -- #0.05; -- #0.03]`;;
43 let magnetism_dom = `[-- &1; -- &1; -- &1; -- &1; -- &1; -- &1; -- &1]`,
44 `[&1; &1; &1; &1; &1; &1; &1]`;;
45 let heart_dom = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]`,
46 `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;
52 let tm = (rand o concl o SPEC_ALL) Sphere.delta_x in
53 expr_to_vector_fun tm;;
56 let tm = (rand o concl o SPEC_ALL o REWRITE_RULE[Sphere.delta_x]) Sphere.delta_y in
57 expr_to_vector_fun tm;;
60 let tm = (rand o concl o SPEC_ALL) Sphere.delta_x4 in
61 expr_to_vector_fun tm;;
64 let delta_x4_dom = `[&4;&4;&4;&4;&4;&8]`, `[#6.3504;#6.3504;#6.3504;#6.3504;#6.3504;#25.4016]`;;
65 let delta_x_dom = `[&4;&4;&4;&4;&4;&4]`, `[#6.3504;#6.3504;#6.3504;#6.3504;#6.3504;#6.3504]`;;
66 let delta_y_dom = `[&2;&2;&2;&2;&2;&2]`, `[#2.52;#2.52;#2.52;#2.52;#2.52;#2.52]`;;
70 (***********************************)
72 let test_verify pp poly_tm min_flag val_tm (xx,zz) eps =
73 let total_start = Sys.time() in
74 let n = (get_dim o fst o dest_abs) poly_tm in
75 let xx1 = convert_to_float_list pp true xx and
76 zz1 = convert_to_float_list pp false zz in
77 let xx2 = Informal_taylor.convert_to_float_list pp true xx and
78 zz2 = Informal_taylor.convert_to_float_list pp false zz in
79 let xx_float = map float_of_float_tm (dest_list xx1) and
80 zz_float = map float_of_float_tm (dest_list zz1) in
81 let eval_fs, tf, ti = mk_verification_functions pp poly_tm min_flag val_tm in
82 let certificate = run_test tf xx_float zz_float false 0.0 true true true true eps in
83 let c1 = transform_result xx_float zz_float certificate in
84 let c1p = Informal_verifier.m_verify_list pp 1 pp ti c1 xx2 zz2 in
85 let start = Sys.time() in
86 let result = m_p_verify_list n pp eval_fs c1p xx1 zz1 in
87 let finish = Sys.time() in
89 (sprintf "Total time: %f; Verification time: %f" (finish -. total_start) (finish -. start)) in
98 let poly_tm = expr_to_vector_fun `x1 pow 3 + x2`;;
100 let xx = `[-- &1; &0]` and zz = `[&1; &1]`;;
101 let xx1 = convert_to_float_list pp true xx and
102 zz1 = convert_to_float_list pp false zz;;
104 let xx_float = map float_of_float_tm (dest_list xx1) and
105 zz_float = map float_of_float_tm (dest_list zz1);;
107 let eval_fs, tf, ti = mk_verification_functions pp poly_tm true `-- #1.1`;;
108 let certificate = run_test tf xx_float zz_float false 0.0 true false false false 0.0;;
109 let c1 = transform_result xx_float zz_float certificate;;
111 result_size certificate;;
113 m_verify_list n pp eval_fs c1 xx1 zz1;;
115 let c0 = run_test0 tf xx_float zz_float false 0.0 false false false 0.0;;
118 m_verify_raw0 n pp eval_fs c0 xx1 zz1;;
120 test_verify pp poly_tm true `-- &1` (xx,zz) 0.0;;
124 let domain0 = mk_m_center_domain n pp xx1 zz1;;
125 let domain1, _ = restrict_domain n 2 true domain0;;
126 let domain11, domain12 = split_domain n pp 1 domain1;;
127 let domain111, domain112 = split_domain n pp 1 domain11;;
130 match eval_fs with (_, _, _, f) -> f;;
132 let taylor0 = eval_taylor domain0;;
133 eval_m_taylor_upper_partial n pp 2 taylor0;;
135 let taylor111 = eval_taylor domain111;;
136 eval_m_taylor_upper_bound n pp taylor111;;
137 let taylor112 = eval_taylor domain112;;
138 eval_m_taylor_upper_bound n pp taylor112;;
140 let taylor12 = eval_taylor domain12;;
141 eval_m_taylor_upper_bound n pp taylor12;;
150 let xx = `[&4;&4;&4;&4;&4;&8]` and
151 zz = `[#6.3504;#6.3504;#6.3504;#6.3504;#6.3504;#25.4016]`;;
152 let xx1 = convert_to_float_list pp true xx and
153 zz1 = convert_to_float_list pp false zz;;
155 let xx_float = map float_of_float_tm (dest_list xx1) and
156 zz_float = map float_of_float_tm (dest_list zz1);;
159 let eval_delta_x4, tf_delta_x4, ti = mk_verification_functions pp delta_x4_poly true `#6.02525`;;
160 let certificate = run_test tf_delta_x4 xx_float zz_float false 0.0 true true true false 0.0;;
161 let c1 = transform_result xx_float zz_float certificate;;
163 result_size certificate;;
165 m_verify_list n pp eval_delta_x4 c1 xx1 zz1;;
166 m_verify_raw0 n pp eval_delta_x4 certificate xx1 zz1;;
169 let c0 = run_test0 tf_delta_x4 xx_float zz_float false 0.0 true true false 0.0;;
170 (* 12 (true false false) 2 (true true false) *)
172 m_verify_raw0 n pp eval_delta_x4 c0 xx1 zz1;;
175 test 10 (m_verify_raw0 n pp eval_delta_x4 certificate xx1) zz1;;
177 test 10 (m_verify_raw0 n pp eval_delta_x4 c0 xx1) zz1;;
186 let xx = `[&4;&4;&4;&4;&4;&4]` and
187 zz = `[#6.3504;#6.3504;#6.3504;#6.3504;#6.3504;#6.3504]`;;
189 let xx1 = convert_to_float_list pp true xx and
190 zz1 = convert_to_float_list pp false zz;;
191 let xx_float = map float_of_float_tm (dest_list xx1) and
192 zz_float = map float_of_float_tm (dest_list zz1);;
194 let eval_delta_x, tf_delta_x, ti = mk_verification_functions pp delta_x_poly true `#127.999`;;
195 let certificate = run_test tf_delta_x xx_float zz_float false 0.0 true true true true 0.0;;
196 let c1 = transform_result xx_float zz_float certificate;;
199 (* 46 (true false false) 10 (true true false) 10 (true true true) *)
200 result_size certificate;;
201 m_verify_raw0 n pp eval_delta_x certificate xx1 zz1;;
202 m_verify_list n pp eval_delta_x c1 xx1 zz1;;
204 let c0 = run_test0 tf_delta_x xx_float zz_float false 0.0 true true true 0.0;;
205 (* 4873 (true false true) 32 (true true true) *)
207 m_verify_raw0 n pp eval_delta_x c0 xx1 zz1;;
210 test 1 (m_verify_raw_old n pp eval_delta_x certificate xx1) zz1;;
215 test 1 (m_verify_raw0 n pp eval_delta_x certificate xx1) zz1;;
216 (* 10: 40.187; 5.140 (convexity) 3.104 (find_and_replace_all); 3.028 (mixed_partials) *)
218 test 1 (m_verify_list n pp eval_delta_x c1 xx1) zz1;;
220 test 1 (m_verify_raw0 n pp eval_delta_x c0 xx1) zz1;;
221 (* 10: 4.228 (2.408, new restrict_domain) *)
222 test 1 (m_verify_domain_test n pp certificate xx1) zz1;;
230 let xx = `[&2;&2;&2;&2;&2;&2]` and
231 zz = `[#2.52;#2.52;#2.52;#2.52;#2.52;#2.52]`;;
233 let xx1 = convert_to_float_list pp true xx and
234 zz1 = convert_to_float_list 4 false zz;;
235 let xx2 = Informal_taylor.convert_to_float_list pp true xx and
236 zz2 = Informal_taylor.convert_to_float_list 4 false zz;;
237 let xx_float = map float_of_float_tm (dest_list xx1) and
238 zz_float = map float_of_float_tm (dest_list zz1);;
240 let eval_delta_y, tf_delta_y, ti_delta_y = mk_verification_functions pp delta_y_poly true `#127.999`;;
241 let certificate = run_test tf_delta_y xx_float zz_float false 0.0 true true true true 0.0;;
242 let c1 = transform_result xx_float zz_float certificate;;
243 let c1p = Informal_verifier.m_verify_list pp 1 pp ti_delta_y c1 xx2 zz2;;
246 (* 134 (true true false) 133 (128) (true true true) *)
247 result_size certificate;;
249 m_verify_list n pp eval_delta_y c1 xx1 zz1;;
251 test 1 (m_verify_raw n pp eval0_delta_y eval_delta_y certificate xx1) zz1;;
253 (* 10: 362; 165 (find_and_replace_all); 166.9 (mixed_partials) 300: 75
256 test 1 (m_verify_list n pp eval_delta_y c1 xx1) zz1;;
260 test 1 (m_p_verify_list n pp eval_delta_y c1p xx1) zz1;;
262 let c00 = run_test0 tf_delta_y xx_float zz_float false 0.0 true true true 0.0;;
263 (* 24671 (true false true) 1785 (1862) (true true true) *)
265 let c0 = transform_result xx_float zz_float c00;;
269 (* 10: 406; 263 (find_and_replace_all) *)
270 test 1 (m_verify_list n pp eval_delta_y c0 xx1) zz1;;
274 let eval_delta_y0, tf_delta_y0 = mk_verification_functions pp delta_y_poly true `&0`;;
275 let certificate = run_test tf_delta_y0 xx_float zz_float false 0.0 true true true true 0.0;;
276 result_stat certificate;;
278 result_size certificate;;
279 let c1 = transform_result xx_float zz_float certificate;;
282 m_verify_list n pp eval_delta_y0 c1 xx1 zz1;;
283 test 1 (m_verify_list n pp eval_delta_y0 c1 xx1) zz1;;
287 let poly1 = `x2 + x3 + x5 + x6 - #7.99 - #0.00385 * delta_y x1 x2 x3 x4 x5 x6 -
288 #2.75 * ((x1 + x4) * #0.5 - sqrt (&8))`;;
289 let poly_ineq = (expr_to_vector_fun o rand o concl o
290 REWRITE_CONV[Sphere.delta_y; Sphere.delta_x]) poly1;;
295 let xx = `[sqrt (&8); &2; &2; sqrt (&8); &2; &2]` and
296 zz = `[&3; #2.07; #2.07; &4 * #1.26; #2.07; #2.07]`;;
298 let xx1 = convert_to_float_list pp true xx and
299 zz1 = convert_to_float_list pp false zz;;
300 let xx_float = map float_of_float_tm (dest_list xx1) and
301 zz_float = map float_of_float_tm (dest_list zz1);;
303 let eval_ineq, tf_ineq = mk_verification_functions pp poly_ineq true `&0`;;
304 let certificate = run_test tf_ineq xx_float zz_float false 0.0 true true true true 0.0;;
305 (* 51 (true true true) 54 (true false/true false) 439 (false false false) *)
306 result_size certificate;;
307 let c1 = transform_result xx_float zz_float certificate;;
311 m_verify_list n pp eval_ineq c1 xx1 zz1;;
323 let xx = `[-- &10; -- &10; -- &10]` and
324 zz = `[&10; &10; &10]`;;
326 let xx1 = convert_to_float_list pp true xx and
327 zz1 = convert_to_float_list pp false zz;;
328 let xx_float = map float_of_float_tm (dest_list xx1) and
329 zz_float = map float_of_float_tm (dest_list zz1);;
331 let eval_schwefel,tf_schwefel, ti = mk_verification_functions pp schwefel_poly true schwefel_min;;
332 let certificate = run_test tf_schwefel xx_float zz_float false 0.0 true true true true 0.0;;
333 result_stat certificate;;
335 let c1 = transform_result xx_float zz_float certificate;;
336 (* 641 (661 after eps = 1e-10)*)
338 (* 1922 (true false false) 1423 (true false true) 1427 (true true true) *)
339 result_size certificate;;
341 m_verify_list n pp eval_schwefel c1 xx1 zz1;;
343 (* 10: 698 (f0_flag: 133) *)
344 test 1 (m_verify_raw0 n pp eval0_schwefel eval_schwefel certificate xx1) zz1;;
345 (* 10: 103 (diff2_f: 100) (find_and_replace_all: 91); (mixed_partials: 93); 300: 54 *)
346 test 1 (m_verify_list n pp eval_schwefel c1 xx1) zz1;;
348 let c0 = run_test0 tf_schwefel xx_float zz_float false 0.0 true false false 0.0;;
349 (* 2152 (true false false) *)
359 let xx = `[-- &5; -- &5; -- &5]` and
360 zz = `[&5; &5; &5]`;;
362 let xx1 = convert_to_float_list pp true xx and
363 zz1 = convert_to_float_list pp false zz;;
364 let xx_float = map float_of_float_tm (dest_list xx1) and
365 zz_float = map float_of_float_tm (dest_list zz1);;
367 let eval_rd, tf_rd = mk_verification_functions pp rd_poly true rd_min;;
368 let certificate = run_test tf_rd xx_float zz_float false 0.0 true true true 0.0;;
370 result_size certificate;;
371 m_verify_raw0 n pp eval_rd certificate xx1 zz1;;
378 let xx = `[-- #0.5; -- #0.5; -- #0.5; -- #0.5]` and
379 zz = `[#0.5; #0.5; #0.5; #0.5]`;;
381 let xx1 = convert_to_float_list pp true xx and
382 zz1 = convert_to_float_list pp false zz;;
383 let xx_float = map float_of_float_tm (dest_list xx1) and
384 zz_float = map float_of_float_tm (dest_list zz1);;
386 let eval_caprasse,tf_caprasse,ti = mk_verification_functions pp caprasse_poly true caprasse_min;;
387 let certificate = run_test tf_caprasse xx_float zz_float false 0.0 true true true true 0.0;;
388 let c1 = transform_result xx_float zz_float certificate;;
389 (* 53 (true false true) 33 (true true true) (41, eps = 1e-10)*)
391 (* 48 (64, eps = 1e-10) (true true false/true) 80 (true false false) 80 (true false true) *)
392 result_size certificate;;
393 m_verify_list n pp eval_caprasse c1 xx1 zz1;;
395 (* 10: 30.826 (f0_flag: 16.497) (diff2_f: 10.1172, true false false) *)
396 test 1 (m_verify_raw0 n pp eval_caprasse certificate xx1) zz1;;
397 (* 10: 6.332 (8.912, eps = 1e-10); 4.848 (find_and_replace_all) *)
398 test 1 (m_verify_list n pp eval_caprasse c1 xx1) zz1;;
400 let c00 = run_test0 tf_caprasse xx_float zz_float false 0.0 true true true 0.0;;
401 (* 128 (true false false) 88 (true true false) *)
403 let c0 = transform_result xx_float zz_float c00;;
406 m_verify_list n pp eval_caprasse c0 xx1 zz1;;
408 (* 10: 6.652 (true true false) 4.632 (true true true) *)
409 test 1 (m_verify_list n pp eval_caprasse c0 xx1) zz1;;
418 let xx = `[-- &2; -- &2; -- &2; -- &2]` and
419 zz = `[&2; &2; &2; &2]`;;
421 let xx1 = convert_to_float_list pp true xx and
422 zz1 = convert_to_float_list pp false zz;;
423 let xx_float = map float_of_float_tm (dest_list xx1) and
424 zz_float = map float_of_float_tm (dest_list zz1);;
426 let eval_lv, tf_lv = mk_verification_functions pp lv_poly true lv_min;;
427 let certificate = run_test tf_lv xx_float zz_float false 0.0 true true true 0.0;;
428 let c1 = transform_result xx_float zz_float certificate;;
431 (* 3 (true true false/true) 11 (true false false) *)
432 result_size certificate;;
433 m_verify_list n pp eval_lv c1 xx1 zz1;;
435 (* 10: 2.688 (f0_flag: 1.216) (df0_flag: 0.564) 0.052 (true true true) *)
436 test 1 (m_verify_list n pp eval_lv c1 xx1) zz1;;
439 let c0 = run_test0 tf_lv xx_float zz_float false 0.0 true true false 0.0;;
440 (* 11 (true false false) 3 (true true false) *)
443 (* 0.06 (true true false) *)
444 test 1 (m_verify_raw0 n pp eval_lv c0 xx1) zz1;;
451 let xx = `[-- &1; -- #0.1; -- #0.1; -- &1; -- #0.1; -- #0.1]` and
452 zz = `[&0; #0.9; #0.5; -- #0.1; -- #0.05; -- #0.03]`;;
454 let xx1 = convert_to_float_list pp true xx and
455 zz1 = convert_to_float_list pp false zz;;
456 let xx_float = map float_of_float_tm (dest_list xx1) and
457 zz_float = map float_of_float_tm (dest_list zz1);;
459 let eval_butcher, tf_butcher = mk_verification_functions pp butcher_poly true butcher_min;;
460 let certificate = run_test tf_butcher xx_float zz_float false 0.0 true true false 0.0;;
461 result_size certificate;;
462 m_verify_raw0 n pp eval_butcher certificate xx1 zz1;;
470 let xx = `[-- &1; -- &1; -- &1; -- &1; -- &1; -- &1; -- &1]` and
471 zz = `[&1; &1; &1; &1; &1; &1; &1]`;;
473 let xx1 = convert_to_float_list pp true xx and
474 zz1 = convert_to_float_list pp false zz;;
475 let xx_float = map float_of_float_tm (dest_list xx1) and
476 zz_float = map float_of_float_tm (dest_list zz1);;
478 let eval_magnetism, tf_magnetism, ti =
479 mk_verification_functions pp magnetism_poly true magnetism_min;;
480 let certificate = run_test tf_magnetism xx_float zz_float false 0.0 true true true true 0.0;;
481 result_stat certificate;;
483 let c1 = transform_result xx_float zz_float certificate;;
486 (* 8732 (true false false) 77 (true false/true true) *)
487 result_size certificate;;
489 m_verify_list n pp eval_magnetism c1 xx1 zz1;;
490 (* 10: 7.86 (diff2_f: 5.788) *)
491 test 1 (m_verify_list n pp eval_magnetism c1 xx1) zz1;;
494 let c00 = run_test0 tf_magnetism xx_float zz_float false 0.0 true false true 0.0;;
495 (* 121 (true false true) *)
497 let c0 = transform_result xx_float zz_float c00;;
500 m_verify_list n pp eval_magnetism c0 xx1 zz1;;
501 (* 10: 13.772 (diff2_f: 9.517) *)
502 test 1 (m_verify_list n pp eval_magnetism c0 xx1) zz1;;
514 let xx = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]` and
515 zz = `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;
517 let xx1 = convert_to_float_list pp true xx and
518 zz1 = convert_to_float_list pp false zz;;
519 let xx_float = map float_of_float_tm (dest_list xx1) and
520 zz_float = map float_of_float_tm (dest_list zz1);;
522 let eval_heart, tf_heart, ti = mk_verification_functions pp heart_poly true heart_min;;
523 let certificate = run_test tf_heart xx_float zz_float false 0.0 true true true true 1e-10;;
524 result_stat certificate;;
525 let c1 = transform_result xx_float zz_float certificate;;
528 (* 42 (true true false) 50 (true false false) 48 (true false true) 37 (true true true) *)
529 result_size certificate;;
530 m_verify_list n pp eval_heart c1 xx1 zz1;;
532 let c00 = run_test0 tf_heart xx_float zz_float false 0.0 true true true 1e-10;;
533 (* 46 (true true false) 61 (true false false) 45 (true true true) *)
535 let c0 = transform_result xx_float zz_float c00;;
538 m_verify_list n pp eval_heart c0 xx1 zz1;;
542 test 1 (m_verify_raw_old n pp eval_heart certificate xx1) zz1;;
544 (* 10: 94 (f0_flag: 22.929) (df0_flag: 13.229) *)
545 test 1 (m_verify_raw0 n pp eval0_heart eval_heart certificate xx1) zz1;;
547 (* 10: 13.689 (diff2_f: 7.080 (true false true)) 4.868 (true true true) 4.448 (find_and_replace_all) *)
548 test 1 (m_verify_list n pp eval_heart c1 xx1) zz1;;
550 test 1 (m_verify_raw0 n pp eval_heart c00 xx1) zz1;;
552 test 1 (m_verify_list n pp eval_heart c0 xx1) zz1;;
556 (* 10: 13 (10.625, new restrict_domain) (f0_flag: 5.3) (df0_flag: 2.264) *)
557 test 1 (m_verify_domain_test n pp certificate xx1) zz1;;
562 (************************************)
563 (* full time tests *)
564 (* Bernstein PVS time in parentheses *)
566 (* 10: 93.717; 89.042 (10.23; 3.18) *)
567 (* 10 (adaptive p): 93.602; 83.853 *)
568 test_verify 12 schwefel_poly true schwefel_min schwefel_dom 0.0;;
570 (* 10: 1.860; 0.024 (3.11; 0.17) *)
571 test_verify 11 rd_poly true rd_min rd_dom 0.0;;
573 (* 10: 11.829; 4.856 (11.44; 1.2) *)
575 test_verify 8 caprasse_poly true caprasse_min caprasse_dom 0.0;;
577 (* 10: 2.204; 0.048 (4.75; 0.23) *)
578 test_verify 5 lv_poly true lv_min lv_dom 0.0;;
580 (* 10: 4.164; 0.024 (19.83; 0.47)*)
581 test_verify 5 butcher_poly true butcher_min butcher_dom 0.0;;
583 (* 10: 11.965; 5.600 (160.44; 82.87) *)
584 test_verify 8 magnetism_poly true magnetism_min magnetism_dom 0.0;;
586 (* 10: 23.205; 4.376 (79.68; 26.14) *)
587 (* 10 (adaptive p): 20.145; 4.288 *)
588 test_verify 10 heart_poly true heart_min heart_dom 1e-10;;