1 needs "../formal_lp/formal_interval/m_taylor_arith2.hl";;
2 needs "../formal_lp/formal_interval/m_verifier.hl";;
3 needs "../formal_lp/arith/informal/informal_m_verifier.hl";;
8 Arith_cache.reset_stat();
9 Arith_cache.reset_cache();
10 Arith_float.reset_stat();
11 Arith_float.reset_cache();;
15 let f1, f2 = Informal_interval.dest_interval int in
16 Informal_float.dest_float f1, Informal_float.dest_float f2;;
18 let dest_f = Informal_float.dest_float;;
21 map dest_f dom.Informal_taylor.lo,
22 map dest_f dom.Informal_taylor.hi,
23 map dest_f dom.Informal_taylor.y,
24 map dest_f dom.Informal_taylor.w;;
27 dest_int ti.Informal_taylor.f,
28 map dest_int ti.Informal_taylor.df,
29 map (map dest_int) ti.Informal_taylor.ddf;;
33 (******************************)
37 let eval_d0 i pp t1 t2 = failwith "eval_d0";;
38 let eval_dd0 i j pp t1 t2 = failwith "eval_dd0";;
39 let eval_0 pp t1 t2 = failwith "eval_0";;
40 let eval_diff2 t1 t2 = failwith "eval_diff2";;
43 (******************************)
52 let tm = (rand o concl o SPEC_ALL o REWRITE_RULE[Sphere.delta_x]) Sphere.delta_y in
53 expr_to_vector_fun tm;;
57 let tm = (rand o concl o SPECL[`y1*y1`; `y2*y2`; `y3*y3`; `y4*y4`; `y5*y5`; `y6*y6`]) Sphere.delta_x4 in
58 expr_to_vector_fun tm;;
60 (* 4 * y1 * delta_y *)
61 let four_y1_delta_y_poly =
62 let x_var, tm = dest_abs delta_y_poly in
63 mk_abs (x_var, mk_binop mul_op_real `&4` (mk_binop mul_op_real `(x:real^6)$1 * x$1` tm));;
66 let neg_delta_y4_poly =
67 let x_var, tm = dest_abs delta_y4_poly in
68 mk_abs (x_var, mk_comb (neg_op_real, tm));;
71 let eval_neg_delta_y4, tf_neg_delta_y4, ti_neg_delta_y4 =
72 mk_verification_functions pp neg_delta_y4_poly false `&0`;;
74 let eval_4y1_delta_y, tf_4y1_delta_y, ti_4y1_delta_y =
75 mk_verification_functions pp four_y1_delta_y_poly false `&0`;;
77 let eval_pi2, tf_pi2, ti_pi2 =
78 mk_verification_functions pp `\x:real^6. pi / &2` false `&0`;;
81 let eval_pi2_plus, tf_pi2_plus, ti_pi2_plus =
82 mk_verification_functions pp `\x:real^6. pi / &2 - #1.893` false `&0`;;
89 let denom = Uni_compose (uinv, Uni_compose (usqrt, tf_4y1_delta_y)) in
90 Plus (tf_pi2_plus, Uni_compose (uatan, Product (tf_neg_delta_y4, denom)));;
92 let eval_dih_y_hi p_lin p_second th =
93 let inv, atn, sqrt, ( * ), ( + ) =
94 eval_m_taylor_inv2 n p_lin p_second, eval_m_taylor_atn2 n p_lin p_second,
95 eval_m_taylor_sqrt2 n p_lin p_second, eval_m_taylor_mul2 n p_lin p_second,
96 eval_m_taylor_add2 n p_lin p_second in
97 let poly1 = eval_4y1_delta_y.taylor p_lin p_second th and
98 poly2 = eval_neg_delta_y4.taylor p_lin p_second th and
99 pi2 = eval_pi2_plus.taylor p_lin p_second th in
100 pi2 + atn (poly2 * inv (sqrt (poly1)));;
103 let ti_dih_y_hi p_lin p_second th =
104 let inv, atn, sqrt, ( * ), ( + ) =
105 Informal_taylor.eval_m_taylor_inv p_lin p_second, Informal_taylor.eval_m_taylor_atn p_lin p_second,
106 Informal_taylor.eval_m_taylor_sqrt p_lin p_second, Informal_taylor.eval_m_taylor_mul p_lin p_second,
107 Informal_taylor.eval_m_taylor_add p_lin p_second in
108 let poly1 = ti_4y1_delta_y.Informal_verifier.taylor p_lin p_second th and
109 poly2 = ti_neg_delta_y4.Informal_verifier.taylor p_lin p_second th and
110 pi2 = ti_pi2_plus.Informal_verifier.taylor p_lin p_second th in
111 pi2 + atn (poly2 * inv (sqrt (poly1)));;
115 {taylor = eval_dih_y_hi; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;
118 {Informal_verifier.taylor = ti_dih_y_hi;
119 Informal_verifier.f = eval_0;
120 Informal_verifier.df = eval_d0;
121 Informal_verifier.ddf = eval_dd0};;
127 let xx_s = `[&2; &2; &2; &2; &2; &2]` and
128 zz_s = `[#2.1; #2.1; #2.1; #2.1; #2.1; #2.1]`;;
132 let xx1_s = convert_to_float_list pp true xx_s and
133 zz1_s = convert_to_float_list pp false zz_s in
134 mk_m_center_domain n pp xx1_s zz1_s;;
137 let xx2_s = Informal_taylor.convert_to_float_list pp true xx_s and
138 zz2_s = Informal_taylor.convert_to_float_list pp false zz_s in
139 Informal_taylor.mk_m_center_domain pp xx2_s zz2_s;;
143 (* 10: 9.121 (pp = 15) *)
144 (* 300: 5.5 (pp = 8) *)
145 (* 100 (cached, float_cached, pp = 8): 2.68 *)
146 (* 100 (optimization): 1.732 *)
147 (* 200 (m_taylor_arith2): 1.428 *)
149 test 1 (eval_dih_y_hi pp pp) domain_th;;
151 (* 200 (optimization): 0.580 *)
152 (* 200 (m_taylor_arith2): 0.328 *)
153 test 1 (eval_dih_y_hi pp pp) domain_th;;
156 test 1 (ti_dih_y_hi pp pp) dom;;
159 Arith_cache.print_stat();;
160 Arith_float.print_stat();;
164 let th1 = eval_4y1_delta_y.taylor pp pp domain_th;;
165 let th2 = eval_neg_delta_y4.taylor pp pp domain_th;;
166 let pi2_th = eval_pi2_plus.taylor pp pp domain_th;;
168 let r1 = eval_m_taylor_sqrt2 n pp pp th1;;
169 let r2 = eval_m_taylor_inv2 n pp pp r1;;
170 let r3 = eval_m_taylor_mul2 n pp pp th2 r2;;
171 let r4 = eval_m_taylor_atn2 n pp pp r3;;
172 let r5 = eval_m_taylor_add2 n pp pp pi2_th r4;;
176 (* 100: 0.264 (second: 0.084) *)
177 test 1 (eval_4y1_delta_y.taylor pp pp) domain_th;;
178 (* 100: 0.032 (second: 0.020) *)
179 test 1 (eval_neg_delta_y4.taylor pp pp) domain_th;;
180 (* 100: 0.000 (second: 0.000) *)
181 test 1 (eval_pi2_plus.taylor pp pp) domain_th;;
183 (* 100: 0.356 (second: 0.168); 0.300 (0.116) *)
184 test 1 (eval_m_taylor_sqrt n pp pp) th1;;
185 (* 200: 0.220 (second: 0.048) *)
186 test 1 (eval_m_taylor_sqrt2 n pp pp) th1;;
188 (* 100: 0.412 (second: 0.188); 0.316 (0.104) *)
189 test 1 (eval_m_taylor_inv n pp pp) r1;;
190 (* 200: 0.264 (second: 0.056) *)
191 test 1 (eval_m_taylor_inv2 n pp pp) r1;;
193 (* 100: 0.384 (second: 0.212); 0.316 (0.140) *)
194 test 1 (eval_m_taylor_mul n pp pp th2) r2;;
195 (* 200: 0.244 (second: 0.092) *)
196 test 1 (eval_m_taylor_mul2 n pp pp th2) r2;;
198 (* 100: 0.616 (second: 0.272); build2: 0.504 (0.132) *)
199 test 1 (eval_m_taylor_atn n pp pp) r3;;
200 (* 200: 0.436 (second: 0.060) *)
201 test 1 (eval_m_taylor_atn2 n pp pp) r3;;
203 (* 100: 0.096 (second: 0.072); 0.072 (0.052) *)
204 test 1 (eval_m_taylor_add n pp pp pi2_th) r4;;
205 (* 200: 0.032 (second: 0.024) *)
206 test 1 (eval_m_taylor_add2 n pp pp pi2_th) r4;;
211 let xx = `[&2; &2; &2; &2; &2; &2]` and
212 zz = `[#2.52; #2.52; #2.52; #2.52; #2.52; #2.52]`;;
214 let xx_s = `[&2; &2; &2; &2; &2; &2]` and
215 zz_s = `[#2.52; #2.1; #2.1; #2.1; #2.1; #2.1]`;;
217 let xx_s2 = `[&2; &2; &2; &2; &2; &2]` and
218 zz_s2 = `[#2.52; #2.2; #2.2; #2.2; #2.2; #2.2]`;;
223 let xx1 = convert_to_float_list pp0 true xx and
224 zz1 = convert_to_float_list pp0 false zz and
225 xx1_s = convert_to_float_list pp0 true xx_s and
226 zz1_s = convert_to_float_list pp0 false zz_s and
227 xx1_s2 = convert_to_float_list pp0 true xx_s2 and
228 zz1_s2 = convert_to_float_list pp0 false zz_s2;;
230 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
231 zz2 = Informal_taylor.convert_to_float_list pp0 false zz and
232 xx2_s = Informal_taylor.convert_to_float_list pp0 true xx_s and
233 zz2_s = Informal_taylor.convert_to_float_list pp0 false zz_s and
234 xx2_s2 = Informal_taylor.convert_to_float_list pp0 true xx_s2 and
235 zz2_s2 = Informal_taylor.convert_to_float_list pp0 false zz_s2;;
238 let xx_float, zz_float, xx_s_float, zz_s_float, xx_s2_float, zz_s2_float =
239 let pad = replicate 0.0 (8 - length (dest_list xx1)) in
240 map float_of_float_tm (dest_list xx1) @ pad,
241 map float_of_float_tm (dest_list zz1) @ pad,
242 map float_of_float_tm (dest_list xx1_s) @ pad,
243 map float_of_float_tm (dest_list zz1_s) @ pad,
244 map float_of_float_tm (dest_list xx1_s2) @ pad,
245 map float_of_float_tm (dest_list zz1_s2) @ pad;;
252 let c_dih_y_s = run_test tf_dih_y_hi xx_s_float zz_s_float false 0.0 true false true false 0.0;;
253 let c_dih_y_s2 = run_test tf_dih_y_hi xx_s2_float zz_s2_float false 0.0 true false true false 0.0;;
254 let c_dih_y0 = run_test tf_dih_y_hi xx_float zz_float false 0.0 true false false false 0.0;;
257 result_stat c_dih_y_s;;
259 result_stat c_dih_y_s2;;
260 (* pass = 4294, mono = 10 *)
261 result_stat c_dih_y0;;
267 let cp_s = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y_s xx2_s zz2_s;;
268 let cp_s2 = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y_s2 xx2_s2 zz2_s2;;
271 (*********************)
275 (* 10 (pp = 15): 38.418 *)
276 (* 300 (pp = 8): 22.289 *)
277 (* 100 (cached, float_cached, pp = 8): 12.229; 9.372 (MY_BETA_RULE); 8.028 (build2) *)
278 (* 200 (m_taylor_arith2) : 6.548 *)
280 let start = Sys.time() in
281 let result = m_verify_raw0 n pp eval_taylor c_dih_y_s xx1_s zz1_s in
282 let finish = Sys.time() in
284 (sprintf "Verification time: %f" (finish -. start)) in
287 Arith_cache.print_stat();;
288 Arith_float.print_stat();;
291 (* 100 (cached, float_cached, pp = 8): 8.025; 5.116 (MY_BETA_RULE); 3.700 (build2) *)
292 (* 200 (m_taylor_arith2): 2.496 *)
295 let start = Sys.time() in
296 let result = m_p_verify_raw0 n p_split eval_taylor cp_s xx1_s zz1_s in
297 let finish = Sys.time() in
299 (sprintf "Verification time: %f" (finish -. start)) in
303 result_p_stat false cp_s2;;
305 (* 100 (cached, float_cached, pp = adaptive): 129.788; 87.729 (MY_BETA_RULE); 64.884 (build2) *)
306 (* (pp = 8: 233.80) *)
307 (* 200: 63.984 (build2) *)
308 (* 200 (m_taylor_arith2): 43.927 *)
312 let start = Sys.time() in
313 let result = m_p_verify_raw0 n p_split eval_taylor cp_s2 xx1_s2 zz1_s2 in
314 let finish = Sys.time() in
316 (sprintf "Verification time: %f" (finish -. start)) in
320 let cp = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y0 xx2 zz2;;
321 result_p_stat false cp;;
323 (* 100: 9105 (was 15202)*)
324 (* 200 (build2): 4242 *)
325 (* 200 (m_taylor_arith2): 3121 *)
326 (* 200 (mixed_partials): 2880 *)
329 let start = Sys.time() in
330 let result = m_p_verify_raw0 n p_split eval_taylor cp xx1 zz1 in
331 let finish = Sys.time() in
333 (sprintf "Verification time: %f" (finish -. start)) in
340 (**************************************)
344 let denom = Uni_compose (uinv, Uni_compose (usqrt, tf_4y1_delta_y)) in
345 Plus (tf_pi2, Uni_compose (uatan, Product (tf_neg_delta_y4, denom)));;
347 let eval_dih_y p_lin p_second th =
348 let inv, atn, sqrt, ( * ), ( + ) =
349 eval_m_taylor_inv2 n p_lin p_second, eval_m_taylor_atn2 n p_lin p_second,
350 eval_m_taylor_sqrt2 n p_lin p_second, eval_m_taylor_mul2 n p_lin p_second,
351 eval_m_taylor_add2 n p_lin p_second in
352 let poly1 = eval_4y1_delta_y.taylor p_lin p_second th and
353 poly2 = eval_neg_delta_y4.taylor p_lin p_second th and
354 pi2 = eval_pi2.taylor p_lin p_second th in
355 pi2 + atn (poly2 * inv (sqrt (poly1)));;
358 let ti_dih_y p_lin p_second th =
359 let inv, atn, sqrt, ( * ), ( + ) =
360 Informal_taylor.eval_m_taylor_inv p_lin p_second, Informal_taylor.eval_m_taylor_atn p_lin p_second,
361 Informal_taylor.eval_m_taylor_sqrt p_lin p_second, Informal_taylor.eval_m_taylor_mul p_lin p_second,
362 Informal_taylor.eval_m_taylor_add p_lin p_second in
363 let poly1 = ti_4y1_delta_y.Informal_verifier.taylor p_lin p_second th and
364 poly2 = ti_neg_delta_y4.Informal_verifier.taylor p_lin p_second th and
365 pi2 = ti_pi2.Informal_verifier.taylor p_lin p_second th in
366 pi2 + atn (poly2 * inv (sqrt (poly1)));;
370 (#0.414 * (y2 + y3 + y5 + y6 - #8.0)) -
371 (#0.763 * (y4 - #2.52)) -
372 (#0.315 * (y1 - #2.0)) *)
373 let neg_poly3318 = expr_to_vector_fun `-- (-- #1.629 +
374 (#0.414 * (y2 + y3 + y5 + y6 - #8.0)) -
375 (#0.763 * (y4 - #2.52)) -
376 (#0.315 * (y1 - #2.0)))`;;
378 let eval_poly3318, tf_poly3318, ti_poly3318 =
379 mk_verification_functions pp neg_poly3318 false `&0`;;
383 let dih = tf_dih_y in
384 let poly = tf_poly3318 in
385 Plus (poly, Scale (dih, mk_interval (-1.0, -1.0)));;
388 let eval_3318 p_lin p_second th =
389 let ( - ) = eval_m_taylor_sub2 n p_lin p_second in
390 let dih = eval_dih_y p_lin p_second th and
391 poly = eval_poly3318.taylor p_lin p_second th in
394 let ti_3318 p_lin p_second th =
395 let ( - ) = Informal_taylor.eval_m_taylor_sub p_lin p_second in
396 let dih = ti_dih_y p_lin p_second th and
397 poly = ti_poly3318.Informal_verifier.taylor p_lin p_second th in
402 {taylor = eval_3318; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;
405 {Informal_verifier.taylor = ti_3318;
406 Informal_verifier.f = eval_0;
407 Informal_verifier.df = eval_d0;
408 Informal_verifier.ddf = eval_dd0};;
412 let xx = `[&2; &2; &2; #2.52; &2; &2]` and
413 zz = `[#2.52; #2.52; #2.52; sqrt(&8); #2.52; #2.52]`;;
415 let xx_s = `[&2; &2; &2; #2.52; &2; &2]` and
416 zz_s = `[#2.52; #2.1; #2.1; sqrt(&8); #2.1; #2.1]`;;
419 let xx1 = convert_to_float_list pp0 true xx and
420 zz1 = convert_to_float_list pp0 false zz and
421 xx1_s = convert_to_float_list pp0 true xx_s and
422 zz1_s = convert_to_float_list pp0 false zz_s;;
424 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
425 zz2 = Informal_taylor.convert_to_float_list pp0 false zz and
426 xx2_s = Informal_taylor.convert_to_float_list pp0 true xx_s and
427 zz2_s = Informal_taylor.convert_to_float_list pp0 false zz_s;;
429 let xx_float, zz_float, xx_s_float, zz_s_float =
430 let pad = replicate 0.0 (8 - length (dest_list xx1)) in
431 map float_of_float_tm (dest_list xx1) @ pad,
432 map float_of_float_tm (dest_list zz1) @ pad,
433 map float_of_float_tm (dest_list xx1_s) @ pad,
434 map float_of_float_tm (dest_list zz1_s) @ pad;;
439 let c_s = run_test tf_3318 xx_s_float zz_s_float false 0.0 true false false false 0.0;;
440 let c0 = run_test tf_3318 xx_float zz_float false 0.0 true false false false 0.0;;
441 let c_test = run_test tf_3318 xx_float zz_float false 0.0 true true true true 0.0;;
443 (* pass = 355, mono = 21 *)
445 (* pass = 16165, mono = 1036 *)
447 (* pass = 15924 (raw = 1), mono = 796, pass_mono = 240 *)
454 let cp_s = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_s xx2_s zz2_s;;
455 let cp0 = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c0 xx2 zz2;;
458 (*********************)
462 (* 200 (m_taylor_arith2): 282.7 *)
464 let start = Sys.time() in
465 let result = m_p_verify_raw0 n p_split eval_taylor cp_s xx1_s zz1_s in
466 let finish = Sys.time() in
468 (sprintf "Verification time: %f" (finish -. start)) in
474 (* 200 (m_taylor_arith2): 14175.2 *)
476 let start = Sys.time() in
477 let result = m_p_verify_raw0 n p_split eval_taylor cp0 xx1 zz1 in
478 let finish = Sys.time() in
480 (sprintf "Verification time: %f" (finish -. start)) in
484 (**************************************)
489 (#0.2213 * (y2 + y3 + y5 + y6 - #8.0)) +
490 (#0.913 * (y4 - #2.52)) +
491 (#0.728 * (y1 - #2.0)) *)
492 let neg_poly9922 = expr_to_vector_fun `-- (#1.6294 -
493 (#0.2213 * (y2 + y3 + y5 + y6 - #8.0)) +
494 (#0.913 * (y4 - #2.52)) +
495 (#0.728 * (y1 - #2.0)))`;;
497 let eval_poly9922, tf_poly9922, ti_poly9922 =
498 mk_verification_functions pp neg_poly9922 false `&0`;;
503 let dih = tf_dih_y in
504 let poly = tf_poly9922 in
508 let eval_9922 p_lin p_second th =
509 let ( + ) = eval_m_taylor_add2 n p_lin p_second in
510 let dih = eval_dih_y p_lin p_second th and
511 poly = eval_poly9922.taylor p_lin p_second th in
514 let ti_9922 p_lin p_second th =
515 let ( + ) = Informal_taylor.eval_m_taylor_add p_lin p_second in
516 let dih = ti_dih_y p_lin p_second th and
517 poly = ti_poly9922.Informal_verifier.taylor p_lin p_second th in
522 {taylor = eval_9922; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;
525 {Informal_verifier.taylor = ti_9922;
526 Informal_verifier.f = eval_0;
527 Informal_verifier.df = eval_d0;
528 Informal_verifier.ddf = eval_dd0};;
532 let xx = `[&2; &2; &2; #2.52; &2; &2]` and
533 zz = `[#2.52; #2.52; #2.52; sqrt(&8); #2.52; #2.52]`;;
535 let xx_s = `[&2; &2; &2; #2.52; &2; &2]` and
536 zz_s = `[#2.52; #2.1; #2.1; sqrt(&8); #2.1; #2.1]`;;
539 let xx1 = convert_to_float_list pp0 true xx and
540 zz1 = convert_to_float_list pp0 false zz and
541 xx1_s = convert_to_float_list pp0 true xx_s and
542 zz1_s = convert_to_float_list pp0 false zz_s;;
544 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
545 zz2 = Informal_taylor.convert_to_float_list pp0 false zz and
546 xx2_s = Informal_taylor.convert_to_float_list pp0 true xx_s and
547 zz2_s = Informal_taylor.convert_to_float_list pp0 false zz_s;;
549 let xx_float, zz_float, xx_s_float, zz_s_float =
550 let pad = replicate 0.0 (8 - length (dest_list xx1)) in
551 map float_of_float_tm (dest_list xx1) @ pad,
552 map float_of_float_tm (dest_list zz1) @ pad,
553 map float_of_float_tm (dest_list xx1_s) @ pad,
554 map float_of_float_tm (dest_list zz1_s) @ pad;;
559 let c_s = run_test tf_9922 xx_s_float zz_s_float false 0.0 true false false false 0.0;;
560 let c0 = run_test tf_9922 xx_float zz_float false 0.0 true false false false 0.0;;
561 let c_test = run_test tf_9922 xx_float zz_float false 0.0 true true true true 0.0;;
563 (* pass = 179, mono = 26 *)
565 (* pass = 6322, mono = 235 *)
567 (* pass = 6307 (raw = 5), mono = 220, pass_mono = 15 *)
574 let cp_s = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_s xx2_s zz2_s;;
575 let cp0 = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c0 xx2 zz2;;
578 (*********************)
582 (* 200 (m_taylor_arith2): 157.2 *)
584 let start = Sys.time() in
585 let result = m_p_verify_raw0 n p_split eval_taylor cp_s xx1_s zz1_s in
586 let finish = Sys.time() in
588 (sprintf "Verification time: %f" (finish -. start)) in
594 (* 200 (m_taylor_arith2): 5039.6 *)
596 let start = Sys.time() in
597 let result = m_p_verify_raw0 n p_split eval_taylor cp0 xx1 zz1 in
598 let finish = Sys.time() in
600 (sprintf "Verification time: %f" (finish -. start)) in