formal_lp/old/arith/informal/tests2.hl

   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";;
   4
   5
   6
   7 let reset_all () =
   8   Arith_cache.reset_stat();
   9   Arith_cache.reset_cache();
  10   Arith_float.reset_stat();
  11   Arith_float.reset_cache();;
  12
  13
  14 let dest_int int =
  15   let f1, f2 = Informal_interval.dest_interval int in
  16     Informal_float.dest_float f1, Informal_float.dest_float f2;;
  17
  18 let dest_f = Informal_float.dest_float;;
  19
  20 let dest_dom dom =
  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;;
  25
  26 let dest_ti ti =
  27   dest_int ti.Informal_taylor.f,
  28   map dest_int ti.Informal_taylor.df,
  29   map (map dest_int) ti.Informal_taylor.ddf;;
  30
  31
  32
  33 (******************************)
  34
  35 (* dummy functions *)
  36
  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";;
  41
  42
  43 (******************************)
  44 (* real tests *)
  45
  46 let n = 6;;
  47 let pp = 15;;
  48 let pp = 8;;
  49
  50 (* delta_y *)
  51 let delta_y_poly =
  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;;
  54
  55 (* delta_y4 *)
  56 let delta_y4_poly =
  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;;
  59
  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));;
  64
  65 (* - delta_y4 *)
  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));;
  69
  70
  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`;;
  73
  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`;;
  76
  77 let eval_pi2, tf_pi2, ti_pi2 =
  78   mk_verification_functions pp `\x:real^6. pi / &2` false `&0`;;
  79
  80
  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`;;
  83
  84
  85 (* dih_y *)
  86 open Univariate;;
  87
  88 let tf_dih_y_hi =
  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)));;
  91
  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)));;
 101
 102
 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)));;
 112
 113
 114 let eval_taylor =
 115   {taylor = eval_dih_y_hi; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;
 116
 117 let ti =
 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};;
 122
 123
 124
 125 (************)
 126 (* Small domain *)
 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]`;;
 129
 130 (* domain *)
 131 let domain_th =
 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;;
 135
 136 let dom =
 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;;
 140
 141
 142
 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 *)
 148 reset_all();;
 149 test 1 (eval_dih_y_hi pp pp) domain_th;;
 150 (* 100: 1.668 *)
 151 (* 200 (optimization): 0.580 *)
 152 (* 200 (m_taylor_arith2): 0.328 *)
 153 test 1 (eval_dih_y_hi pp pp) domain_th;;
 154 (* 100: 0.088 *)
 155
 156 test 1 (ti_dih_y_hi pp pp) dom;;
 157
 158
 159 Arith_cache.print_stat();;
 160 Arith_float.print_stat();;
 161
 162 (***)
 163
 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;;
 167
 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;;
 173
 174 reset_all();;
 175
 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;;
 182
 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;;
 187
 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;;
 192
 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;;
 197
 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;;
 202
 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;;
 207
 208
 209
 210 (***)
 211 let xx = `[&2; &2; &2; &2; &2; &2]` and
 212     zz = `[#2.52; #2.52; #2.52; #2.52; #2.52; #2.52]`;;
 213
 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]`;;
 216
 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]`;;
 219
 220
 221 let pp0 = 3;;
 222 let pp0 = 5;;
 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;;
 229
 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;;
 236
 237
 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;;
 246
 247
 248
 249 (***)
 250
 251
 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;;
 255
 256 (* pass = 4 *)
 257 result_stat c_dih_y_s;;
 258 (* pass = 63 *)
 259 result_stat c_dih_y_s2;;
 260 (* pass = 4294, mono = 10 *)
 261 result_stat c_dih_y0;;
 262
 263 let p_split = pp and
 264     p_min = 1 and
 265     p_max = pp;;
 266
 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;;
 269
 270
 271 (*********************)
 272
 273 reset_all();;
 274
 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 *)
 279 let _ =
 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
 283   let _ = report
 284     (sprintf "Verification time: %f" (finish -. start)) in
 285     result;;
 286
 287 Arith_cache.print_stat();;
 288 Arith_float.print_stat();;
 289
 290
 291 (* 100 (cached, float_cached, pp = 8): 8.025; 5.116 (MY_BETA_RULE); 3.700 (build2) *)
 292 (* 200 (m_taylor_arith2): 2.496 *)
 293 reset_all();;
 294 let _ =
 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
 298   let _ = report
 299     (sprintf "Verification time: %f" (finish -. start)) in
 300     result;;
 301
 302 (* stats *)
 303 result_p_stat false cp_s2;;
 304
 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 *)
 309 reset_all();;
 310
 311 let _ =
 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
 315   let _ = report
 316     (sprintf "Verification time: %f" (finish -. start)) in
 317     result;;
 318
 319 (*****************)
 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;;
 322
 323 (* 100: 9105 (was 15202)*)
 324 (* 200 (build2): 4242 *)
 325 (* 200 (m_taylor_arith2): 3121 *)
 326 (* 200 (mixed_partials): 2880 *)
 327 reset_all();;
 328 let _ =
 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
 332   let _ = report
 333     (sprintf "Verification time: %f" (finish -. start)) in
 334     result;;
 335
 336
 337
 338
 339
 340 (**************************************)
 341 (* 3318775219 *)
 342
 343 let tf_dih_y =
 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)));;
 346
 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)));;
 356
 357
 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)));;
 367
 368
 369 (* - #1.629 +
 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)))`;;
 377
 378 let eval_poly3318, tf_poly3318, ti_poly3318 =
 379   mk_verification_functions pp neg_poly3318 false `&0`;;
 380
 381
 382 let tf_3318 =
 383   let dih = tf_dih_y in
 384   let poly = tf_poly3318 in
 385     Plus (poly, Scale (dih, mk_interval (-1.0, -1.0)));;
 386
 387
 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
 392     poly - dih;;
 393
 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
 398     poly - dih;;
 399
 400
 401 let eval_taylor =
 402   {taylor = eval_3318; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;
 403
 404 let ti =
 405   {Informal_verifier.taylor = ti_3318;
 406   Informal_verifier.f = eval_0;
 407   Informal_verifier.df = eval_d0;
 408   Informal_verifier.ddf = eval_dd0};;
 409
 410
 411 (* domain *)
 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]`;;
 414
 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]`;;
 417
 418 let pp0 = 3;;
 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;;
 423
 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;;
 428
 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;;
 435
 436
 437 (* certificates *)
 438
 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;;
 442
 443 (* pass = 355, mono = 21 *)
 444 result_stat c_s;;
 445 (* pass = 16165, mono = 1036 *)
 446 result_stat c0;;
 447 (* pass = 15924 (raw = 1), mono = 796, pass_mono = 240 *)
 448 result_stat c_test;;
 449
 450 let p_split = pp and
 451     p_min = 1 and
 452     p_max = pp;;
 453
 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;;
 456
 457
 458 (*********************)
 459
 460 reset_all();;
 461
 462 (* 200 (m_taylor_arith2): 282.7 *)
 463 let _ =
 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
 467   let _ = report
 468     (sprintf "Verification time: %f" (finish -. start)) in
 469     result;;
 470
 471
 472 reset_all();;
 473
 474 (* 200 (m_taylor_arith2): 14175.2 *)
 475 let _ =
 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
 479   let _ = report
 480     (sprintf "Verification time: %f" (finish -. start)) in
 481     result;;
 482
 483
 484 (**************************************)
 485 (* 9922699028 *)
 486
 487
 488 (* #1.6294 -
 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)))`;;
 496
 497 let eval_poly9922, tf_poly9922, ti_poly9922 =
 498   mk_verification_functions pp neg_poly9922 false `&0`;;
 499
 500
 501
 502 let tf_9922 =
 503   let dih = tf_dih_y in
 504   let poly = tf_poly9922 in
 505     Plus (dih, poly);;
 506
 507
 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
 512     dih + poly;;
 513
 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
 518     dih + poly;;
 519
 520
 521 let eval_taylor =
 522   {taylor = eval_9922; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;
 523
 524 let ti =
 525   {Informal_verifier.taylor = ti_9922;
 526   Informal_verifier.f = eval_0;
 527   Informal_verifier.df = eval_d0;
 528   Informal_verifier.ddf = eval_dd0};;
 529
 530
 531 (* domain *)
 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]`;;
 534
 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]`;;
 537
 538 let pp0 = 3;;
 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;;
 543
 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;;
 548
 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;;
 555
 556
 557 (* certificates *)
 558
 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;;
 562
 563 (* pass = 179, mono = 26 *)
 564 result_stat c_s;;
 565 (* pass = 6322, mono = 235 *)
 566 result_stat c0;;
 567 (* pass = 6307 (raw = 5), mono = 220, pass_mono = 15 *)
 568 result_stat c_test;;
 569
 570 let p_split = pp and
 571     p_min = 1 and
 572     p_max = pp;;
 573
 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;;
 576
 577
 578 (*********************)
 579
 580 reset_all();;
 581
 582 (* 200 (m_taylor_arith2): 157.2 *)
 583 let _ =
 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
 587   let _ = report
 588     (sprintf "Verification time: %f" (finish -. start)) in
 589     result;;
 590
 591
 592 reset_all();;
 593
 594 (* 200 (m_taylor_arith2): 5039.6  *)
 595 let _ =
 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
 599   let _ = report
 600     (sprintf "Verification time: %f" (finish -. start)) in
 601     result;;