formal_lp/old/formal_interval/m_tests2.hl

   1 needs "../formal_lp/formal_interval/m_taylor_arith.hl";;
   2 needs "../formal_lp/formal_interval/m_verifier.hl";;
   3
   4
   5 let pp = 10;;
   6 let n = 2;;
   7
   8 let poly1 = expr_to_vector_fun `x1 * x2`;;
   9 let poly2 = expr_to_vector_fun `x2 + x1 * x2`;;
  10
  11 let (_, _, _, eval1), tf1 = mk_verification_functions pp poly1 false `&0` and
  12     (_, _, _, eval2), tf2 = mk_verification_functions pp poly2 false `&0`;;
  13
  14
  15 let xx = `[&1; &1]` and
  16     zz = `[&2; &2]`;;
  17
  18 let xx1 = convert_to_float_list pp true xx and
  19     zz1 = convert_to_float_list pp false zz;;
  20
  21 let xx_float, zz_float =
  22   let pad = replicate 0.0 (8 - length (dest_list xx1)) in
  23     map float_of_float_tm (dest_list xx1) @ pad,
  24     map float_of_float_tm (dest_list zz1) @ pad;;
  25
  26 let domain_th = mk_m_center_domain n pp xx1 zz1;;
  27
  28 evalf (Uni_compose (uatan, tf2)) xx_float zz_float;;
  29 eval_m_taylor_mul n pp (eval1 domain_th) (eval2 domain_th);;
  30 evalf (Product (tf1, tf2)) xx_float zz_float;;
  31
  32
  33
  34 (******************************)
  35
  36 (* dummy functions *)
  37
  38 let eval_d0 i t1 t2 = failwith "eval_d0";;
  39 let eval_dd0 i j t1 t2 = failwith "eval_dd0";;
  40 let eval_0 t1 t2 = failwith "eval_0";;
  41
  42
  43 (******************************)
  44
  45
  46 (* 1d test *)
  47
  48 let n = 1;;
  49 let pp = 5;;
  50
  51 let eval_x = eval_m_taylor_poly0 pp `\x:real^1. x$1`;;
  52
  53 let f_eval th =
  54   let x = eval_x th in
  55   let ( - ), ( * ), atn = eval_m_taylor_sub n pp, eval_m_taylor_mul n pp, eval_m_taylor_atn n pp in
  56     x * x - atn x;;
  57
  58 let tf = Plus (Product (x1, x1), Scale (Uni_compose (uatan, x1), ineg one));;
  59
  60
  61 let xx = `[#0.01]` and
  62     zz = `[#0.8]`;;
  63
  64 let xx1 = convert_to_float_list pp true xx and
  65     zz1 = convert_to_float_list pp false zz;;
  66
  67 let xx_float, zz_float =
  68   let pad = replicate 0.0 (8 - length (dest_list xx1)) in
  69     map float_of_float_tm (dest_list xx1) @ pad,
  70     map float_of_float_tm (dest_list zz1) @ pad;;
  71
  72 let domain_th = mk_m_center_domain n pp xx1 zz1;;
  73 f_eval domain_th;;
  74 evalf tf xx_float zz_float;;
  75
  76 let certificate = run_test tf xx_float zz_float false 0.0 true false true false 0.0;;
  77 let c1 = transform_result xx_float zz_float certificate;;
  78
  79 m_verify_list n pp (eval_d0, eval_dd0, eval_0, f_eval) c1 xx1 zz1;;
  80
  81
  82 (********************)
  83
  84 let n = 1;;
  85 let pp = 10;;
  86
  87 let atan_num = `let P00, P01, P02 = #4.26665376811246382, #3.291955407318148, #0.281939359003812 in
  88   let x1 = x * x in
  89   let x2 = x1 * x1 in
  90     x * (x1 * P01 + x2 * P02 + P00)`;;
  91
  92 let atan_denom = `let Q00, Q01 = #4.26665376811354027, #4.714173328637605 in
  93     let x1 = x * x in
  94     let x2 = x1 * x1 in
  95       x1 * Q01 + x2 + Q00`;;
  96
  97
  98 let num_poly = (expr_to_vector_fun o rand o concl o REPEATC let_CONV) atan_num;;
  99 let denom_poly = (expr_to_vector_fun o rand o concl o REPEATC let_CONV) atan_denom;;
 100
 101 let (_, _, _, eval_num), tf_num = mk_verification_functions pp num_poly false `&0`;;
 102 let (_, _, _, eval_denom), tf_denom = mk_verification_functions pp denom_poly false `&0`;;
 103
 104 let (_, _, _, eval_eps), tf_eps = mk_verification_functions pp `\x:real^1. #0.00000001` false `&0`;;
 105
 106
 107 let eval_approx_hi th =
 108   let x = eval_x th in
 109   let eps = eval_eps th in
 110   let atn, inv, ( * ), ( - ) = eval_m_taylor_atn n pp, eval_m_taylor_inv n pp,
 111     eval_m_taylor_mul n pp, eval_m_taylor_sub n pp in
 112     (eval_num th * inv (eval_denom th) - atn x) - eps;;
 113
 114 (***)
 115 let xx = `[#0.0000001]` and
 116     zz = `[#0.2]`;;
 117
 118 let xx1 = convert_to_float_list pp true xx and
 119     zz1 = convert_to_float_list pp false zz;;
 120
 121 let xx_float, zz_float =
 122   let pad = replicate 0.0 (8 - length (dest_list xx1)) in
 123     map float_of_float_tm (dest_list xx1) @ pad,
 124     map float_of_float_tm (dest_list zz1) @ pad;;
 125
 126 let domain_th = mk_m_center_domain n pp xx1 zz1;;
 127
 128
 129 eval_approx_hi domain_th;;
 130 (* 10: 0.800 (p = 15) *)
 131 test 1 eval_approx_hi domain_th;;
 132
 133
 134 (***)
 135 let tf_approx_hi = Plus (Plus (Product (tf_num, Uni_compose (uinv, tf_denom)),
 136                                Scale (Uni_compose (uatan, x1), ineg one)),
 137                          Scale (tf_eps, ineg one));;
 138
 139
 140 let certificate = run_test tf_approx_hi xx_float zz_float false 0.0 true false true false 0.0;;
 141 result_stat certificate;;
 142 let c1 = transform_result xx_float zz_float certificate;;
 143
 144 m_verify_list n pp (eval_d0, eval_dd0, eval_0, eval_approx_hi) c1 xx1 zz1;;
 145
 146
 147
 148
 149 (* 2d test *)
 150
 151 let n = 2;;
 152 let pp = 10;;
 153
 154 let eval_x = eval_m_taylor_poly0 pp `\x:real^2. x$1` and
 155     eval_y = eval_m_taylor_poly0 pp `\x:real^2. x$2`;;
 156
 157 let eval_xy = eval_m_taylor_poly0 pp `\x:real^2. x$1 * x$2`;;
 158
 159 let f_eval th =
 160   let x = eval_x th in
 161   let y = eval_y th in
 162   let ( - ), ( * ), atn = eval_m_taylor_sub n pp, eval_m_taylor_mul n pp, eval_m_taylor_atn n pp in
 163     atn (x * y) - x * y;;
 164
 165 let f_eval2 th =
 166   let xy = eval_xy th in
 167   let ( - ), ( * ), atn = eval_m_taylor_sub n pp, eval_m_taylor_mul n pp, eval_m_taylor_atn n pp in
 168     atn xy - xy;;
 169
 170
 171 let tf = Plus (Uni_compose (uatan, Product (x1, x2)), Scale (Product (x1, x2), ineg one));;
 172
 173
 174 let xx = `[#0.1; #0.1]` and
 175     zz = `[#0.6; #0.6]`;;
 176
 177 let xx1 = convert_to_float_list pp true xx and
 178     zz1 = convert_to_float_list pp false zz;;
 179
 180 let xx_float, zz_float =
 181   let pad = replicate 0.0 (8 - length (dest_list xx1)) in
 182     map float_of_float_tm (dest_list xx1) @ pad,
 183     map float_of_float_tm (dest_list zz1) @ pad;;
 184
 185 let domain_th = mk_m_center_domain n pp xx1 zz1;;
 186
 187 let certificate = run_test tf xx_float zz_float false 0.0 true false true false 0.0;;
 188 let c1 = transform_result xx_float zz_float certificate;;
 189
 190 (* 10: 33.926 *)
 191 test 1 (m_verify_list n pp (eval_d0, eval_dd0, eval_0, f_eval) c1 xx1) zz1;;
 192 (* 10: 25.089 *)
 193 test 1 (m_verify_list n pp (eval_d0, eval_dd0, eval_0, f_eval2) c1 xx1) zz1;;
 194
 195
 196
 197 (* 6d tests *)
 198
 199 let n = 6;;
 200 let pp = 10;;
 201
 202 let (_, _, _, eval_xy), tf0 =
 203   mk_verification_functions pp `\x:real^6. x$1 * x$2 + x$3 * x$4 + x$5 * x$6` false `&0`;;
 204
 205 let f_eval_sqrt th =
 206   let xy = eval_xy th in
 207   let ( - ), ( * ), sqrt = eval_m_taylor_sub n pp, eval_m_taylor_mul n pp, eval_m_taylor_sqrt n pp in
 208     xy - sqrt xy;;
 209
 210 let f_eval_atn th =
 211   let xy = eval_xy th in
 212   let ( - ), ( * ), atn = eval_m_taylor_sub n pp, eval_m_taylor_mul n pp, eval_m_taylor_atn n pp in
 213     atn xy - xy;;
 214
 215
 216 let tf_sqrt = Plus (tf0, Scale (Uni_compose (usqrt, tf0), ineg one));;
 217 let tf_atn = Plus (Uni_compose (uatan, tf0), Scale (tf0, ineg one));;
 218
 219
 220 let xx = `[#0.1; #0.1; #0.1; #0.1; #0.1; #0.1]` and
 221     zz = `[#0.2; #0.2; #0.2; #0.2; #0.2; #0.2]`;;
 222
 223 let xx1 = convert_to_float_list pp true xx and
 224     zz1 = convert_to_float_list pp false zz;;
 225
 226 let xx_float, zz_float =
 227   let pad = replicate 0.0 (8 - length (dest_list xx1)) in
 228     map float_of_float_tm (dest_list xx1) @ pad,
 229     map float_of_float_tm (dest_list zz1) @ pad;;
 230
 231
 232 let certificate_sqrt = run_test tf_sqrt xx_float zz_float false 0.0 true false true false 0.0;;
 233 let c1_sqrt = transform_result xx_float zz_float certificate_sqrt;;
 234
 235 let certificate_atn = run_test tf_atn xx_float zz_float false 0.0 true false true false 0.0;;
 236 let c1_atn = transform_result xx_float zz_float certificate_atn;;
 237
 238 m_verify_list n pp (eval_d0, eval_dd0, eval_0, f_eval_sqrt) c1_sqrt xx1 zz1;;
 239 m_verify_list n pp (eval_d0, eval_dd0, eval_0, f_eval_atn) c1_atn xx1 zz1;;
 240
 241
 242
 243 (*********************************)
 244
 245 (* real tests *)
 246
 247 let n = 6;;
 248 let pp = 15;;
 249 (* let pp = 8;; *)
 250
 251 (* delta_y *)
 252 let delta_y_poly =
 253   let tm = (rand o concl o SPEC_ALL o REWRITE_RULE[Sphere.delta_x]) Sphere.delta_y in
 254     expr_to_vector_fun tm;;
 255
 256 (* delta_y4 *)
 257 let delta_y4_poly =
 258   let tm = (rand o concl o SPECL[`y1*y1`; `y2*y2`; `y3*y3`; `y4*y4`; `y5*y5`; `y6*y6`]) Sphere.delta_x4 in
 259     expr_to_vector_fun tm;;
 260
 261 (* 4 * y1 * delta_y *)
 262 let four_y1_delta_y_poly =
 263   let x_var, tm = dest_abs delta_y_poly in
 264     mk_abs (x_var, mk_binop mul_op_real `&4` (mk_binop mul_op_real `(x:real^6)$1 * x$1` tm));;
 265
 266 (* - delta_y4 *)
 267 let neg_delta_y4_poly =
 268   let x_var, tm = dest_abs delta_y4_poly in
 269     mk_abs (x_var, mk_comb (neg_op_real, tm));;
 270
 271
 272 let (_, _, _, eval_neg_delta_y4), tf_neg_delta_y4 =
 273   mk_verification_functions pp neg_delta_y4_poly false `&0`;;
 274
 275 let (_, _, _, eval_4y1_delta_y), tf_4y1_delta_y =
 276   mk_verification_functions pp four_y1_delta_y_poly false `&0`;;
 277
 278 let (_, _, _, eval_pi2), tf_pi2 =
 279   mk_verification_functions pp `\x:real^6. pi / &2` false `&0`;;
 280
 281
 282 let (_, _, _, eval_pi2_plus), tf_pi2_plus =
 283   mk_verification_functions pp `\x:real^6. pi / &2 - #1.893` false `&0`;;
 284
 285
 286
 287 Sphere.dih_x;;
 288
 289 (* dih_y *)
 290 let tf_dih_y_hi =
 291   let denom = Uni_compose (uinv, Uni_compose (usqrt, tf_4y1_delta_y)) in
 292     Plus (tf_pi2_plus, Uni_compose (uatan, Product (tf_neg_delta_y4, denom)));;
 293
 294 let eval_dih_y_hi th =
 295   let inv, atn, sqrt, ( * ), ( + ) =
 296     eval_m_taylor_inv n pp, eval_m_taylor_atn n pp, eval_m_taylor_sqrt n pp,
 297     eval_m_taylor_mul n pp, eval_m_taylor_add n pp in
 298   let poly1 = eval_4y1_delta_y th and
 299       poly2 = eval_neg_delta_y4 th and
 300       pi2 = eval_pi2_plus th in
 301     pi2 + atn (poly2 * inv (sqrt (poly1)));;
 302
 303
 304
 305 (************)
 306
 307 let xx = `[&2; &2; &2; &2; &2; &2]` and
 308     zz = `[#2.52; #2.52; #2.52; #2.52; #2.52; #2.52]`;;
 309
 310 let xx1 = convert_to_float_list pp true xx and
 311     zz1 = convert_to_float_list pp false zz;;
 312
 313
 314 (* Small domain *)
 315 let xx_s = `[&2; &2; &2; &2; &2; &2]` and
 316     zz_s = `[#2.1; #2.1; #2.1; #2.1; #2.1; #2.1]`;;
 317
 318 let domain_th =
 319   let xx1_s = convert_to_float_list pp true xx_s and
 320       zz1_s = convert_to_float_list pp false zz_s in
 321     mk_m_center_domain n pp xx1_s zz1_s;;
 322
 323 (* 10: 9.121 (pp = 15); 300: 5.5 (pp = 8) *)
 324 test 1 eval_dih_y_hi domain_th;;
 325
 326
 327 (***)
 328
 329 let xx_s = `[&2; &2; &2; &2; &2; &2]` and
 330     zz_s = `[#2.52; #2.1; #2.1; #2.1; #2.1; #2.1]`;;
 331
 332 let xx1_s = convert_to_float_list pp true xx_s and
 333     zz1_s = convert_to_float_list pp false zz_s;;
 334
 335
 336 let xx_float, zz_float, xx_s_float, zz_s_float =
 337   let pad = replicate 0.0 (8 - length (dest_list xx1)) in
 338     map float_of_float_tm (dest_list xx1) @ pad,
 339     map float_of_float_tm (dest_list zz1) @ pad,
 340     map float_of_float_tm (dest_list xx1_s) @ pad,
 341     map float_of_float_tm (dest_list zz1_s) @ pad;;
 342
 343
 344
 345 (***)
 346
 347 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;;
 348 let c_dih_y = run_test tf_dih_y_hi xx_float zz_float false 0.0 true false true false 0.0;;
 349 let c_dih_y0 = run_test tf_dih_y_hi xx_float zz_float false 0.0 true false false false 0.0;;
 350 let c_dih_y_full = run_test tf_dih_y_hi xx_float zz_float false 0.0 true true true true 0.0;;
 351 let c_dih_y_min = run_test tf_dih_y_hi xx_float zz_float false 0.0 false false false false 0.0;;
 352
 353 (* pass = 4 *)
 354 result_stat c_dih_y_s;;
 355
 356 (* pass = 4292, mono = 8, pass_mono = 2 *)
 357 result_stat c_dih_y;;
 358 (* pass = 4294, mono = 10 *)
 359 result_stat c_dih_y0;;
 360 (* pass = 4292, mono = 8, pass_mono = 2 *)
 361 result_stat c_dih_y_full;;
 362 (* pass = 4317, mono = 0 *)
 363 result_stat c_dih_y_min;;
 364
 365 m_verify_raw0 n pp (eval_d0, eval_dd0, eval_0, eval_dih_y) c_dih_y_s xx1_s zz1_s;;
 366 (* 10: 38.418; 300: 22.289 (pp = 8)*)
 367 test 1 (m_verify_raw0 n pp (eval_d0, eval_dd0, eval_0, eval_dih_y) c_dih_y_s xx1_s) zz1_s;;
 368
 369
 370
 371 m_verify_raw0 n pp (eval_d0, eval_dd0, eval_0, eval_dih_y) c_dih_y0 xx1 zz1;;
 372 let c1_dih_y = transform_result xx_float zz_float c_dih_y;;
 373
 374
 375
 376 (*************************************)
 377 (* dih_y *)
 378 let tf_dih_y =
 379   let denom = Uni_compose (uinv, Uni_compose (usqrt, tf_4y1_delta_y)) in
 380     Plus (tf_pi2, Uni_compose (uatan, Product (tf_neg_delta_y4, denom)));;
 381
 382
 383 (* sol_y *)
 384
 385 let _, tf_neg_pi = mk_verification_functions 15 `\x:real^6. --pi` false `&0`;;
 386
 387 Sphere.sol_y;;
 388 let tf_sol_y =
 389   let dih1 = tf_dih_y and
 390       dih2 = Composite (tf_dih_y, x2, x3, x1, x5, x6, x4, unit, unit) and
 391       dih3 = Composite (tf_dih_y, x3, x1, x2, x6, x4, x5, unit, unit) in
 392     Plus (dih1, Plus (dih2, Plus (dih3, tf_neg_pi)));;
 393
 394 (* taum *)
 395
 396 let pi_val= 3.1415926535897932;;
 397 let sol0_val = 0.5512855984325308;;
 398 let const1_val = sol0_val /. pi_val;;
 399 let const1_plus1 = const1_val +. 1.0;;
 400
 401 let _, tf_ly = mk_verification_functions 15 `\x:real^1. #2.52 / #0.52 - x$1 * inv(#0.52)` false `&0`;;
 402 let tf_lnazim_y = Product (tf_ly, tf_dih_y);;
 403
 404 Sphere.taum;;
 405 let tf_taum =
 406   let azim1 = tf_lnazim_y and
 407       azim2 = Composite (tf_lnazim_y, x2, x3, x1, x5, x6, x4, unit, unit) and
 408       azim3 = Composite (tf_lnazim_y, x3, x1, x2, x6, x4, x5, unit, unit) in
 409   let f1 = Scale (tf_sol_y, mk_interval (const1_plus1, const1_plus1)) and
 410       f2 = Plus (azim1, Plus (azim2, azim3)) in
 411     Plus (f1, Scale (f2, mk_interval (~-.const1_val, ~-.const1_val)));;
 412
 413
 414
 415 (* dih_y < 1.893 *)
 416 let tf_test1 =
 417   Plus (tf_dih_y, Scale (unit, ineg (mk_interval (1.893, 1.893))));;
 418
 419
 420 (* dih_y > 0.852 *)
 421 let tf_test2 =
 422   Plus (Scale (unit, mk_interval (0.852, 0.852)), Scale (tf_dih_y, ineg one));;
 423
 424
 425 (* taum + 0.626 * dih_y - 0.77 > 0 *)
 426 let tf_test3 =
 427   let f = Plus (tf_taum, Scale (tf_dih_y, mk_interval (0.626, 0.626))) in
 428     Plus (Scale (unit, mk_interval (0.77, 0.77)), Scale (f, ineg one));;
 429
 430
 431 (* taum - 0.259 * dih_y + 0.32 > 0 *)
 432 let tf_test4 =
 433   let f = Plus (tf_taum, Scale (tf_dih_y, mk_interval (-0.259, -0.259))) in
 434     Plus (Scale (unit, mk_interval (-0.32, -0.32)), Scale (f, ineg one));;
 435
 436
 437 (* taum - 0.507 * dih_y + 0.724 > 0 *)
 438 let tf_test5 =
 439   let f = Plus (tf_taum, Scale (tf_dih_y, mk_interval (-0.507, -0.507))) in
 440     Plus (Scale (unit, mk_interval (-0.724, -0.724)), Scale (f, ineg one));;
 441
 442
 443 (* sol_y - 0.55125 - 0.196 * (y4 + y5 + y6 - 6) + 0.38 * (y1 + y2 + y3 - 6) > 0 *)
 444 let _, tf_poly = mk_verification_functions 15
 445   `\x:real^6. #0.55125 + #0.196 * (x$4 + x$5 + x$6 - &6) - #0.38 * (x$1 + x$2 + x$3 - &6)` false `&0`;;
 446
 447 let tf_test6 =
 448   Plus (tf_poly, Scale (tf_sol_y, ineg one));;
 449
 450
 451 (* dih_y - 1.2308 + 0.3639 * (y2 + y3 + y5 + y6 - 8) - 0.235 * (y1 - 2) - 0.685 * (y4 - 2) > 0 *)
 452 let _, tf_poly = mk_verification_functions 15
 453   `\x:real^6. #1.2308 - #0.3639 * (x$2 + x$3 + x$5 + x$6 - &8) + #0.235 * (x$1 - &2) + #0.685 * (x$4 - &2)`
 454   false `&0`;;
 455
 456 let tf_test7 =
 457   Plus (tf_poly, Scale (tf_dih_y, ineg one));;
 458
 459
 460
 461
 462 (****)
 463 let c1_1 = run_test tf_test1 xx_float zz_float false 0.0 true false true false 0.0;;
 464 let c1 = run_test tf_test1 xx_float zz_float false 0.0 false false false false 0.0;;
 465 result_stat c1_1;;
 466 (* pass = 4317 *)
 467 result_stat c1;;
 468
 469
 470 (****)
 471 let c2_1 = run_test tf_test2 xx_float zz_float false 0.0 true false true false 0.0;;
 472 let c2 = run_test tf_test2 xx_float zz_float false 0.0 false false false false 0.0;;
 473 (* pass = 8891, mono = 77, pass_mono = 2 *)
 474 result_stat c2_1;;
 475 (* pass = 9007 *)
 476 result_stat c2;;
 477
 478 (***)
 479 let c3 = run_test tf_test3 xx_float zz_float false 0.0 false false false false 0.0 and
 480     c4 = run_test tf_test4 xx_float zz_float false 0.0 false false false false 0.0 and
 481     c5 = run_test tf_test5 xx_float zz_float false 0.0 false false false false 0.0;;
 482
 483
 484 (* 48104 *)
 485 result_stat c3;;
 486 (* 34015 *)
 487 result_stat c4;;
 488 (* 25859 *)
 489 result_stat c5;;
 490
 491
 492
 493
 494 (****)
 495 let c6_1 = run_test tf_test6 xx_float zz_float false 0.0 true false true false 0.0;;
 496 let c6 = run_test tf_test6 xx_float zz_float false 0.0 false false false false 0.0;;
 497 (* pass = 67337, mono = 214, pass_mono = 33 *)
 498 result_stat c6_1;;
 499 (* pass = 9007 *)
 500 result_stat c2;;
 501
 502
 503 (****)
 504 let c7_1 = run_test tf_test7 xx_float zz_float false 0.0 true false true false 0.0;;
 505 let c7 = run_test tf_test7 xx_float zz_float false 0.0 false false false false 0.0;;
 506 let c7_full = run_test tf_test7 xx_float zz_float false 0.0 true true true true 0.0;;
 507 (* pass = 21104, mono = 1203, pass_mono = 58 *)
 508 result_stat c7_full;;
 509 (* pass = 21104, mono = 1203, pass_mono = 58 *)
 510 result_stat c7_1;;
 511 (* pass = 23251 *)
 512 result_stat c7;;
 513
 514
 515
 516 (****************)
 517
 518 let rec get_pass_intervals r =
 519   match r with
 520     | Result_pass (_, xx, zz) -> [xx, zz]
 521     | Result_glue (_, _, r1, r2) -> get_pass_intervals r1 @ get_pass_intervals r2
 522     | _ -> [];;
 523
 524 let sum_rs rs = itlist (+) (map result_size rs) 0;;
 525 let sum1_rs rs = itlist (+) (filter (fun s -> s = 1) (map result_size rs)) 0;;
 526
 527
 528 let c1_ints = get_pass_intervals c1;;
 529 let c2_ints = get_pass_intervals c2;;
 530 let c3_ints = get_pass_intervals c3;;
 531 let c4_ints = get_pass_intervals c4;;
 532 let c5_ints = get_pass_intervals c5;;
 533 let c6_ints = get_pass_intervals c6;;
 534 let c7_ints = get_pass_intervals c7;;
 535
 536 (***)
 537 let c2_1_rs = map (fun (xx, zz) ->
 538                    run_test tf_test2 xx zz false 0.0 false false false false 0.0) c1_ints;;
 539
 540 let c2_7_rs = map (fun (xx, zz) ->
 541                    run_test tf_test2 xx zz false 0.0 false false false false 0.0) c7_ints;;
 542
 543 (* 9121 vs 9007 *)
 544 sum_rs c2_1_rs;;
 545 (* 2146 *)
 546 sum1_rs c2_1_rs;;
 547
 548 (* 23922 *)
 549 sum_rs c2_7_rs;;
 550 (* 22762 *)
 551 sum1_rs c2_7_rs;;
 552
 553 (***)
 554 let c1_2_rs = map (fun (xx, zz) ->
 555                    run_test tf_test1 xx zz false 0.0 false false false false 0.0) c2_ints;;
 556
 557 let c1_7_rs = map (fun (xx, zz) ->
 558                    run_test tf_test1 xx zz false 0.0 false false false false 0.0) c7_ints;;
 559
 560
 561 (* 9121 vs 9007 *)
 562 sum_rs c1_2_rs;;
 563 (* 8933 *)
 564 sum1_rs c1_2_rs;;
 565
 566 (* 23268 *)
 567 sum_rs c1_7_rs;;
 568 (* 23247 *)
 569 sum1_rs c1_7_rs;;
 570
 571
 572 (***)
 573 let c7_2_rs = map (fun (xx, zz) ->
 574                    run_test tf_test7 xx zz false 0.0 false false false false 0.0) c2_ints;;
 575
 576
 577 (* 23922 vs 23251 *)
 578 sum_rs c7_2_rs;;
 579 (* 3918 *)
 580 sum1_rs c7_2_rs;;
 581
 582
 583 (*********)
 584 let c4_3_rs = map (fun (xx, zz) ->
 585                    run_test tf_test4 xx zz false 0.0 false false false false 0.0) c3_ints and
 586     c5_3_rs = map (fun (xx, zz) ->
 587                    run_test tf_test5 xx zz false 0.0 false false false false 0.0) c3_ints;;
 588
 589
 590 (* 54465 vs 34015 *)
 591 sum_rs c4_3_rs;;
 592 (* 43517 *)
 593 sum1_rs c4_3_rs;;
 594
 595
 596 (* 52093 vs 25859 *)
 597 sum_rs c5_3_rs;;
 598 (* 45488 *)
 599 sum1_rs c5_3_rs;;