formal_lp/old/formal_interval/m_tests.hl

   1 flyspeck_needs "../formal_lp/formal_interval/m_verifier.hl";;
   2
   3
   4 let reset_all () =
   5   Arith_cache.reset_stat();
   6   Arith_cache.reset_cache();
   7   Arith_float.reset_stat();
   8   Arith_float.reset_cache();;
   9
  10
  11 (**************************)
  12 (* Examples *)
  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`;;
  27
  28
  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`;;
  36
  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]`;;
  47
  48
  49
  50 (****************)
  51 let delta_x_poly =
  52   let tm = (rand o concl o SPEC_ALL) Sphere.delta_x in
  53     expr_to_vector_fun tm;;
  54
  55 let delta_y_poly =
  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;;
  58
  59 let delta_x4_poly =
  60   let tm = (rand o concl o SPEC_ALL) Sphere.delta_x4 in
  61     expr_to_vector_fun tm;;
  62
  63
  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]`;;
  67
  68
  69
  70 (***********************************)
  71
  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
  88   let _ = report
  89     (sprintf "Total time: %f; Verification time: %f" (finish -. total_start) (finish -. start)) in
  90     result;;
  91
  92
  93 (******)
  94
  95 let pp = 5;;
  96
  97 let n = 2;;
  98 let poly_tm = expr_to_vector_fun `x1 pow 3 + x2`;;
  99
 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;;
 103
 104 let xx_float = map float_of_float_tm (dest_list xx1) and
 105     zz_float = map float_of_float_tm (dest_list zz1);;
 106
 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;;
 110 (* 5 *)
 111 result_size certificate;;
 112
 113 m_verify_list n pp eval_fs c1 xx1 zz1;;
 114
 115 let c0 = run_test0 tf xx_float zz_float false 0.0 false false false 0.0;;
 116 (* 7 *)
 117 result_size c0;;
 118 m_verify_raw0 n pp eval_fs c0 xx1 zz1;;
 119
 120 test_verify pp poly_tm true `-- &1` (xx,zz) 0.0;;
 121
 122
 123
 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;;
 128
 129 let eval_taylor =
 130   match eval_fs with (_, _, _, f) -> f;;
 131
 132 let taylor0 = eval_taylor domain0;;
 133 eval_m_taylor_upper_partial n pp 2 taylor0;;
 134
 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;;
 139
 140 let taylor12 = eval_taylor domain12;;
 141 eval_m_taylor_upper_bound n pp taylor12;;
 142
 143
 144
 145
 146 (****)
 147 (* delta_x4 *)
 148 let pp = 10;;
 149 let n = 6;;
 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;;
 154
 155 let xx_float = map float_of_float_tm (dest_list xx1) and
 156     zz_float = map float_of_float_tm (dest_list zz1);;
 157
 158
 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;;
 162 (* 1 *)
 163 result_size certificate;;
 164
 165 m_verify_list n pp eval_delta_x4 c1 xx1 zz1;;
 166 m_verify_raw0 n pp eval_delta_x4 certificate xx1 zz1;;
 167
 168
 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) *)
 171 result_size c0;;
 172 m_verify_raw0 n pp eval_delta_x4 c0 xx1 zz1;;
 173
 174 (* 1.076 *)
 175 test 10 (m_verify_raw0 n pp eval_delta_x4 certificate xx1) zz1;;
 176 (* 0.836 *)
 177 test 10 (m_verify_raw0 n pp eval_delta_x4 c0 xx1) zz1;;
 178
 179
 180
 181 (***)
 182 (* delta_x *)
 183
 184 let pp = 10;;
 185 let n = 6;;
 186 let xx = `[&4;&4;&4;&4;&4;&4]` and
 187     zz = `[#6.3504;#6.3504;#6.3504;#6.3504;#6.3504;#6.3504]`;;
 188
 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);;
 193
 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;;
 197 (* 1 *)
 198 length c1;;
 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;;
 203
 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) *)
 206 result_size c0;;
 207 m_verify_raw0 n pp eval_delta_x c0 xx1 zz1;;
 208
 209 (* 10: 65 *)
 210 test 1 (m_verify_raw_old n pp eval_delta_x certificate xx1) zz1;;
 211 (* 10: 38.642
 212  100 (cached): 0.384
 213 *)
 214 reset_all();;
 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) *)
 217 reset_all();;
 218 test 1 (m_verify_list n pp eval_delta_x c1 xx1) zz1;;
 219 (* 10: 1.860 *)
 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;;
 223
 224
 225
 226 (***)
 227 (* delta_y *)
 228 let pp = 10;;
 229 let n = 6;;
 230 let xx = `[&2;&2;&2;&2;&2;&2]` and
 231     zz = `[#2.52;#2.52;#2.52;#2.52;#2.52;#2.52]`;;
 232
 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);;
 239
 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;;
 244 (* 17 *)
 245 length c1;;
 246 (* 134 (true true false) 133 (128) (true true true) *)
 247 result_size certificate;;
 248
 249 m_verify_list n pp eval_delta_y c1 xx1 zz1;;
 250 (* 10: 494 *)
 251 test 1 (m_verify_raw n pp eval0_delta_y eval_delta_y certificate xx1) zz1;;
 252
 253 (* 10: 362; 165 (find_and_replace_all); 166.9 (mixed_partials) 300: 75
 254 *)
 255 reset_all();;
 256 test 1 (m_verify_list n pp eval_delta_y c1 xx1) zz1;;
 257
 258 (* 100:  *)
 259 reset_all();;
 260 test 1 (m_p_verify_list n pp eval_delta_y c1p xx1) zz1;;
 261
 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) *)
 264 result_size c00;;
 265 let c0 = transform_result xx_float zz_float c00;;
 266 (* 431 (460) *)
 267 length c0;;
 268
 269 (* 10: 406; 263 (find_and_replace_all) *)
 270 test 1 (m_verify_list n pp eval_delta_y c0 xx1) zz1;;
 271
 272
 273 (***)
 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;;
 277 (* 25 (27) *)
 278 result_size certificate;;
 279 let c1 = transform_result xx_float zz_float certificate;;
 280 (* 1 *)
 281 length c1;;
 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;;
 284
 285
 286 (***)
 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;;
 291
 292 let pp = 10;;
 293 let n = 6;;
 294
 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]`;;
 297
 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);;
 302
 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;;
 308 (* 30 *)
 309 length c1;;
 310
 311 m_verify_list n pp eval_ineq c1 xx1 zz1;;
 312
 313
 314
 315
 316
 317
 318 (***)
 319 (* schwefel *)
 320 let pp = 12;;
 321 let pp = 4;;
 322 let n = 3;;
 323 let xx = `[-- &10; -- &10; -- &10]` and
 324     zz = `[&10; &10; &10]`;;
 325
 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);;
 330
 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;;
 334
 335 let c1 = transform_result xx_float zz_float certificate;;
 336 (* 641 (661 after eps = 1e-10)*)
 337 length c1;;
 338 (* 1922 (true false false) 1423 (true false true) 1427 (true true true) *)
 339 result_size certificate;;
 340
 341 m_verify_list n pp eval_schwefel c1 xx1 zz1;;
 342
 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;;
 347
 348 let c0 = run_test0 tf_schwefel xx_float zz_float false 0.0 true false false 0.0;;
 349 (* 2152 (true false false) *)
 350 result_size c0;;
 351
 352
 353
 354 (***)
 355 (* rd *)
 356
 357 let pp = 12;;
 358 let n = 3;;
 359 let xx = `[-- &5; -- &5; -- &5]` and
 360     zz = `[&5; &5; &5]`;;
 361
 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);;
 366
 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;;
 369 (* 1 *)
 370 result_size certificate;;
 371 m_verify_raw0 n pp eval_rd certificate xx1 zz1;;
 372
 373 (***)
 374 (* caprasse *)
 375
 376 let pp = 8;;
 377 let n = 4;;
 378 let xx = `[-- #0.5; -- #0.5; -- #0.5; -- #0.5]` and
 379     zz = `[#0.5; #0.5; #0.5; #0.5]`;;
 380
 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);;
 385
 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)*)
 390 length c1;;
 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;;
 394
 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;;
 399
 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) *)
 402 result_size c00;;
 403 let c0 = transform_result xx_float zz_float c00;;
 404 (* 69 *)
 405 length c0;;
 406 m_verify_list n pp eval_caprasse c0 xx1 zz1;;
 407
 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;;
 410
 411
 412
 413 (***)
 414 (* lv *)
 415
 416 let pp = 5;;
 417 let n = 4;;
 418 let xx = `[-- &2; -- &2; -- &2; -- &2]` and
 419     zz = `[&2; &2; &2; &2]`;;
 420
 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);;
 425
 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;;
 429 (* 1 *)
 430 length c1;;
 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;;
 434
 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;;
 437
 438
 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) *)
 441 result_size c0;;
 442
 443 (* 0.06 (true true false) *)
 444 test 1 (m_verify_raw0 n pp eval_lv c0 xx1) zz1;;
 445
 446 (***)
 447 (* butcher *)
 448
 449 let pp = 5;;
 450 let n = 6;;
 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]`;;
 453
 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);;
 458
 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;;
 463
 464
 465 (***)
 466 (* magnetism *)
 467
 468 let pp = 8;;
 469 let n = 7;;
 470 let xx = `[-- &1; -- &1; -- &1; -- &1; -- &1; -- &1; -- &1]` and
 471     zz = `[&1; &1; &1; &1; &1; &1; &1]`;;
 472
 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);;
 477
 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;;
 482
 483 let c1 = transform_result xx_float zz_float certificate;;
 484 (* 76 *)
 485 length c1;;
 486 (* 8732 (true false false) 77 (true false/true true) *)
 487 result_size certificate;;
 488
 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;;
 492
 493
 494 let c00 = run_test0 tf_magnetism xx_float zz_float false 0.0 true false true 0.0;;
 495 (* 121 (true false true) *)
 496 result_size c00;;
 497 let c0 = transform_result xx_float zz_float c00;;
 498 (* 120 *)
 499 length c0;;
 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;;
 503
 504
 505
 506
 507
 508 (***)
 509 (* heart *)
 510
 511 let pp = 10;;
 512 let pp = 4;;
 513 let n = 8;;
 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]`;;
 516
 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);;
 521
 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;;
 526 (* 23 *)
 527 length c1;;
 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;;
 531
 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) *)
 534 result_size c00;;
 535 let c0 = transform_result xx_float zz_float c00;;
 536 (* 32 *)
 537 length c0;;
 538 m_verify_list n pp eval_heart c0 xx1 zz1;;
 539
 540
 541 (* 10: 109 *)
 542 test 1 (m_verify_raw_old n pp eval_heart certificate xx1) zz1;;
 543
 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;;
 546
 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;;
 549 (* 10: 4.048 *)
 550 test 1 (m_verify_raw0 n pp eval_heart c00 xx1) zz1;;
 551 (* 10: 4.248 *)
 552 test 1 (m_verify_list n pp eval_heart c0 xx1) zz1;;
 553
 554
 555
 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;;
 558
 559
 560
 561
 562 (************************************)
 563 (* full time tests *)
 564 (* Bernstein PVS time in parentheses *)
 565
 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;;
 569
 570 (* 10: 1.860; 0.024 (3.11; 0.17) *)
 571 test_verify 11 rd_poly true rd_min rd_dom 0.0;;
 572
 573 (* 10: 11.829; 4.856 (11.44; 1.2) *)
 574 reset_all();;
 575 test_verify 8 caprasse_poly true caprasse_min caprasse_dom 0.0;;
 576
 577 (* 10: 2.204; 0.048 (4.75; 0.23) *)
 578 test_verify 5 lv_poly true lv_min lv_dom 0.0;;
 579
 580 (* 10: 4.164; 0.024 (19.83; 0.47)*)
 581 test_verify 5 butcher_poly true butcher_min butcher_dom 0.0;;
 582
 583 (* 10: 11.965; 5.600 (160.44; 82.87) *)
 584 test_verify 8 magnetism_poly true magnetism_min magnetism_dom 0.0;;
 585
 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;;