formal_lp/old/arith/informal/tests1.hl

   1 (* Tests *)
   2 needs "../formal_lp/formal_interval/m_verifier.hl";;
   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 let dest_int int =
  11   let f1, f2 = Informal_interval.dest_interval int in
  12     Informal_float.dest_float f1, Informal_float.dest_float f2;;
  13
  14 let dest_f = Informal_float.dest_float;;
  15
  16 let dest_dom dom =
  17   map dest_f dom.Informal_taylor.lo,
  18   map dest_f dom.Informal_taylor.hi,
  19   map dest_f dom.Informal_taylor.y,
  20   map dest_f dom.Informal_taylor.w;;
  21
  22 let dest_ti ti =
  23   dest_int ti.Informal_taylor.f,
  24   map dest_int ti.Informal_taylor.df,
  25   map (map dest_int) ti.Informal_taylor.ddf;;
  26
  27
  28 needs "../formal_lp/formal_interval/m_examples_poly.hl";;
  29
  30
  31
  32 (***)
  33 (* delta_y *)
  34 let delta_y_poly =
  35   let tm = (rand o concl o SPEC_ALL o REWRITE_RULE[Sphere.delta_x]) Sphere.delta_y in
  36     expr_to_vector_fun tm;;
  37
  38
  39 let pp = 10;;
  40 let pp0 = 4;;
  41 let n = 6;;
  42 let xx = `[&2;&2;&2;&2;&2;&2]` and
  43     zz = `[#2.52;#2.52;#2.52;#2.52;#2.52;#2.52]`;;
  44
  45 let xx1 = convert_to_float_list pp0 true xx and
  46     zz1 = convert_to_float_list pp0 false zz;;
  47 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
  48     zz2 = Informal_taylor.convert_to_float_list pp0 false zz;;
  49 let xx_float = map float_of_float_tm (dest_list xx1) and
  50     zz_float = map float_of_float_tm (dest_list zz1);;
  51
  52 let eval_delta_y, tf_delta_y, ti_delta_y = mk_verification_functions pp delta_y_poly true `#127.999`;;
  53 let certificate = run_test tf_delta_y xx_float zz_float false 0.0 true true true true 0.0;;
  54 let c1 = transform_result xx_float zz_float certificate;;
  55
  56
  57 (* 10: 362; 165 (find_and_replace_all); 300: 75 *)
  58 (* 10 (cached, float_cached): 33.778 *)
  59 reset_all();;
  60 test 1 (m_verify_list n pp eval_delta_y c1 xx1) zz1;;
  61
  62 let p_min = 1 and
  63     p_max = pp and
  64     p_split = pp;;
  65
  66 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_delta_y c1 xx2 zz2;;
  67
  68 (* 10: 26.950 *)
  69 reset_all();;
  70 test 1 (m_p_verify_list n pp eval_delta_y cp1 xx1) zz1;;
  71
  72
  73
  74
  75 (************************)
  76 let poly1 = `x2 + x3 + x5 + x6 - #7.99 - #0.00385 * delta_y x1 x2 x3 x4 x5 x6 -
  77   #2.75 * ((x1 + x4) * #0.5 - sqrt (&8))`;;
  78 let poly_ineq = (expr_to_vector_fun o rand o concl o
  79                    REWRITE_CONV[Sphere.delta_y; Sphere.delta_x]) poly1;;
  80 let pp = 10;;
  81 let pp0 = 5;;
  82
  83 let n = 6;;
  84 let xx = `[sqrt (&8); &2; &2; sqrt (&8); &2; &2]` and
  85     zz = `[&3; #2.07; #2.07; &4 * #1.26; #2.07; #2.07]`;;
  86
  87 let xx1 = convert_to_float_list pp0 true xx and
  88     zz1 = convert_to_float_list pp0 false zz;;
  89 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
  90     zz2 = Informal_taylor.convert_to_float_list pp0 false zz;;
  91 let xx_float = map float_of_float_tm (dest_list xx1) and
  92     zz_float = map float_of_float_tm (dest_list zz1);;
  93
  94 let eval_ineq, tf_ineq, ti_ineq = mk_verification_functions pp poly_ineq true `&0`;;
  95 let certificate = run_test tf_ineq xx_float zz_float false 0.0 true true true true 0.0;;
  96 let c1 = transform_result xx_float zz_float certificate;;
  97
  98 let p_split = pp and
  99     p_min = 1 and
 100     p_max = pp;;
 101 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_ineq c1 xx2 zz2;;
 102
 103
 104 (* 10: 14.665 *)
 105 reset_all();;
 106 test 1 (m_verify_list n pp eval_ineq c1 xx1) zz1;;
 107 (* 10: 4.788 *)
 108 test 1 (m_verify_list n pp eval_ineq c1 xx1) zz1;;
 109
 110
 111 (* 10: 12.465 *)
 112 reset_all();;
 113 test 1 (m_p_verify_list n p_split eval_ineq cp1 xx1) zz1;;
 114 (* 10: 4.520 *)
 115 test 1 (m_p_verify_list n p_split eval_ineq cp1 xx1) zz1;;
 116
 117
 118
 119
 120 (*******************************)
 121
 122 let get_m_cell_domain =
 123   let domain_hash = Hashtbl.create 20 in
 124   let mem, find, add = Hashtbl.mem domain_hash,
 125     Hashtbl.find domain_hash, Hashtbl.add domain_hash in
 126     fun n pp domain0 path ->
 127       let rec get_rec domain_th path hash =
 128         match path with
 129           | [] -> domain_th
 130           | (s, j) :: ps ->
 131               let hash' = hash^s^(string_of_int j) in
 132                 if mem hash' then
 133                   get_rec (find hash') ps hash'
 134                 else
 135                   if s = "l" or s = "r" then
 136                     let domain1_th, domain2_th = split_domain n pp j domain_th in
 137                     let hash1 = hash^"l"^(string_of_int j) and
 138                         hash2 = hash^"r"^(string_of_int j) in
 139                     let _ = add hash1 domain1_th; add hash2 domain2_th in
 140                       if s = "l" then
 141                         get_rec domain1_th ps hash'
 142                       else
 143                         get_rec domain2_th ps hash'
 144                   else
 145                     let l_flag = (s = "ml") in
 146                     let domain_th', _ = restrict_domain n j l_flag domain_th in
 147                     let _ = add hash' domain_th' in
 148                       get_rec domain_th' ps hash' in
 149         get_rec domain0 path "";;
 150
 151
 152 let m_p_verify_list0 n p_split fs certificate_list xx zz th_refs =
 153   let domain_th0 = mk_m_center_domain n p_split xx zz in
 154   let size = length certificate_list in
 155   let k = ref 0 in
 156   let rec rec_verify certificate_list th_list =
 157     match certificate_list with
 158       | [] -> th_list
 159       | (path, certificate) :: cs ->
 160           let _ = k := !k + 1; report (sprintf "List: %d/%d" !k size) in
 161           let domain_th = get_m_cell_domain n p_split domain_th0 path in
 162           let th = m_p_verify_raw n p_split fs certificate domain_th th_list in
 163             rec_verify cs (th_list @ [th]) in
 164     rec_verify certificate_list th_refs;;
 165
 166
 167 let i_get_m_cell_domain =
 168   let domain_hash = Hashtbl.create 20 in
 169   let mem, find, add = Hashtbl.mem domain_hash,
 170     Hashtbl.find domain_hash, Hashtbl.add domain_hash in
 171     fun pp domain0 path ->
 172       let rec get_rec domain_th path hash =
 173         match path with
 174           | [] -> domain_th
 175           | (s, j) :: ps ->
 176               let hash' = hash^s^(string_of_int j) in
 177                 if mem hash' then
 178                   get_rec (find hash') ps hash'
 179                 else
 180                   if s = "l" or s = "r" then
 181                     let domain1_th, domain2_th = Informal_verifier.split_domain pp j domain_th in
 182                     let hash1 = hash^"l"^(string_of_int j) and
 183                         hash2 = hash^"r"^(string_of_int j) in
 184                     let _ = add hash1 domain1_th; add hash2 domain2_th in
 185                       if s = "l" then
 186                         get_rec domain1_th ps hash'
 187                       else
 188                         get_rec domain2_th ps hash'
 189                   else
 190                     let l_flag = (s = "ml") in
 191                     let domain_th' = Informal_verifier.restrict_domain j l_flag domain_th in
 192                     let _ = add hash' domain_th' in
 193                       get_rec domain_th' ps hash' in
 194         get_rec domain0 path "";;
 195
 196
 197 let i_m_verify_list p_split p_min p_max fs certificate_list xx zz =
 198   let domain0 = Informal_taylor.mk_m_center_domain p_split xx zz in
 199   let size = length certificate_list in
 200   let k = ref 0 in
 201   let rec rec_verify certificate_list dom_list tree_list =
 202     match certificate_list with
 203       | [] -> rev tree_list, dom_list
 204       | (path, certificate) :: cs ->
 205           let _ = k := !k + 1; report (sprintf "List: %d/%d" !k size) in
 206           let domain = i_get_m_cell_domain p_split domain0 path in
 207           let tree = Informal_verifier.m_verify_raw p_split p_min p_max fs certificate domain dom_list in
 208             rec_verify cs (dom_list @ [domain]) ((path, tree) :: tree_list) in
 209     rec_verify certificate_list [] [];;
 210
 211
 212 (***********************)
 213
 214
 215 let l1, l2 = chop_list 26 cp1;;
 216 let ths1 = m_p_verify_list0 n p_split eval_ineq l1 xx1 zz1 [];;
 217 let path2, c2 = hd l2;;
 218 let dom2_th = get_m_cell_domain n p_split (mk_m_center_domain n p_split xx1 zz1) path2;;
 219 let dom2 = i_get_m_cell_domain p_split (Informal_taylor.mk_m_center_domain p_split xx2 zz2) path2;;
 220 dest_dom dom2;;
 221
 222
 223 m_p_verify_raw n p_split eval_ineq c2 dom2_th ths1;;
 224 c2;;
 225
 226 let d1_th, d2_th = split_domain n p_split (3 + 1) dom2_th;;
 227 let d1, d2 = Informal_verifier.split_domain p_split (3 + 1) dom2;;
 228
 229 let t2_th = eval_ineq.taylor 4 4 d2_th;;
 230 eval_m_taylor_upper_partial n 4 4 t2_th;;
 231
 232 let t2 = ti_ineq.Informal_verifier.taylor 4 d2;;
 233 dest_f (Informal_taylor.eval_m_taylor_upper_partial 4 4 t2);;
 234
 235 let f0, df0, ddf0 = dest_ti t2;;
 236 let _, _, _, _, f1, df1, ddf1 = dest_m_taylor (concl t2_th);;
 237
 238 df1;;
 239 df0;;
 240 (* partial 4, upper bound: -67 * 10^-2, (true, 671, 47) *)
 241
 242 let x_tm, body_tm = dest_abs poly_ineq;;
 243 let new_f = mk_abs (x_tm, mk_binop sub_op_real `&0` body_tm);;
 244 let partial4 = gen_partial_poly 4 new_f;;
 245
 246 let g1 = mk_eval_function_eq pp partial4;;
 247 let g0 = Informal_taylor.mk_eval_function pp (rand (concl partial4));;
 248
 249 let _, y1, _ = dest_m_cell_domain (concl d2_th);;
 250 let y0 = d2.Informal_taylor.y;;
 251
 252 g1 2 y1 y1;;
 253 dest_int (g0 2 y0 y0);;
 254
 255 float_interval_pow_simple 2 4 (mk_const_interval (mk_float 29 49));;
 256 let ff = Informal_float.mk_float (Int 29) 49;;
 257 dest_int (Informal_interval.pow_interval 2 4 (Informal_interval.mk_interval (ff, ff)));;
 258
 259 let g_test = `\x:real^2. (-- &77 / &10000) * x$2 * x$1 pow 4`;;
 260 let pp = 10;;
 261 let g1 = mk_eval_function_eq pp (REFL g_test);;
 262 let g0 = Informal_taylor.mk_eval_function pp g_test;;
 263
 264 let yy = `[#2.9; &3]`;;
 265 let y1' = mk_vector (convert_to_float_list pp true yy);;
 266 let y0' = Informal_taylor.convert_to_float_list pp true yy;;
 267
 268 g1 2 y1' y1';;
 269 dest_int (g0 2 y0' y0');;
 270
 271 partial4;;
 272
 273
 274 (***)
 275
 276 List.nth ddf0 5;;
 277 List.nth (dest_list ddf1) 5;;
 278
 279
 280
 281
 282 d2_th;;
 283 dest_dom d2;;
 284
 285
 286 m_p_verify_list0 n p_split eval_ineq l2 xx1 zz1 ths1;;
 287
 288 List.nth cp1 26;;
 289
 290
 291
 292
 293
 294
 295
 296
 297
 298 let x = 2;;
 299
 300
 301
 302
 303 (***)
 304 (* schwefel *)
 305 let pp = 12;;
 306 let n = 3;;
 307 let xx = `[-- &10; -- &10; -- &10]` and
 308     zz = `[&10; &10; &10]`;;
 309
 310 let xx1 = convert_to_float_list pp true xx and
 311     zz1 = convert_to_float_list pp false zz;;
 312 let xx2 = Informal_taylor.convert_to_float_list pp true xx and
 313     zz2 = Informal_taylor.convert_to_float_list pp false zz;;
 314 let xx_float = map float_of_float_tm (dest_list xx1) and
 315     zz_float = map float_of_float_tm (dest_list zz1);;
 316
 317 let eval_schwefel, tf_schwefel, i_schwefel = mk_verification_functions pp schwefel_poly true schwefel_min;;
 318 let c00 = run_test tf_schwefel xx_float zz_float false 0.0 true true false false 0.0;;
 319 let c0 = run_test tf_schwefel xx_float zz_float false 0.0 true true false true 0.0;;
 320 result_stat c0;;
 321 let c1' = run_test tf_schwefel xx_float zz_float false 0.0 true true true true 0.0;;
 322 let c1 = transform_result xx_float zz_float c1';;
 323
 324 let p_split = pp and
 325     p_min = 1 and p_max = pp;;
 326
 327 reset_all();;
 328 let cp0 = Informal_verifier.m_verify_raw0 p_split p_min p_max i_schwefel c0 xx2 zz2;;
 329
 330 (* 10: 27.006 *)
 331 reset_all();;
 332 test 1 (m_verify_raw0 n pp eval_schwefel c0 xx1) zz1;;
 333
 334 (* 10: 24.642 *)
 335 reset_all();;
 336 test 1 (m_p_verify_raw0 n p_split eval_schwefel cp0 xx1) zz1;;
 337
 338
 339 (* 10: 136.257 *)
 340 reset_all();;
 341 test 1 (m_verify_raw0 n pp eval_schwefel c00 xx1) zz1;;
 342
 343 let cp00 = Informal_verifier.m_verify_raw0 p_split p_min p_max i_schwefel c00 xx2 zz2;;
 344
 345 (* 10: 126.400 *)
 346 reset_all();;
 347 test 1 (m_p_verify_raw0 n p_split eval_schwefel cp00 xx1) zz1;;
 348
 349 (* 10: 23.297 *)
 350 reset_all();;
 351 test 1 (m_verify_list n pp eval_schwefel c1 xx1) zz1;;
 352
 353 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max i_schwefel c1 xx2 zz2;;
 354
 355 (* 10: 21.205 *)
 356 reset_all();;
 357 test 1 (m_p_verify_list n p_split eval_schwefel cp1 xx1) zz1;;
 358
 359
 360 (***)
 361 (* rd *)
 362
 363 let pp = 12;;
 364 let n = 3;;
 365 let xx = `[-- &5; -- &5; -- &5]` and
 366     zz = `[&5; &5; &5]`;;
 367
 368 let xx1 = convert_to_float_list pp true xx and
 369     zz1 = convert_to_float_list pp false zz;;
 370 let xx2 = Informal_taylor.convert_to_float_list pp true xx and
 371     zz2 = Informal_taylor.convert_to_float_list pp false zz;;
 372 let xx_float = map float_of_float_tm (dest_list xx1) and
 373     zz_float = map float_of_float_tm (dest_list zz1);;
 374
 375 let eval_rd, tf_rd, i_rd = mk_verification_functions pp rd_poly true rd_min;;
 376 let certificate = run_test tf_rd xx_float zz_float false 0.0 true true true false 0.0;;
 377 (* 1 *)
 378 result_size certificate;;
 379 m_verify_raw0 n pp eval_rd certificate xx1 zz1;;
 380
 381 let p_split = pp and
 382     p_min = 1 and
 383     p_max = pp;;
 384
 385 Informal_verifier.m_verify_raw0 p_split p_min p_max i_rd certificate xx2 zz2;;
 386
 387
 388 (***)
 389 (* caprasse *)
 390
 391 let pp = 8;;
 392 let n = 4;;
 393 let xx = `[-- #0.5; -- #0.5; -- #0.5; -- #0.5]` and
 394     zz = `[#0.5; #0.5; #0.5; #0.5]`;;
 395
 396 let xx1 = convert_to_float_list pp true xx and
 397     zz1 = convert_to_float_list pp false zz;;
 398 let xx2 = Informal_taylor.convert_to_float_list pp true xx and
 399     zz2 = Informal_taylor.convert_to_float_list pp false zz;;
 400 let xx_float = map float_of_float_tm (dest_list xx1) and
 401     zz_float = map float_of_float_tm (dest_list zz1);;
 402
 403 let eval_caprasse, tf_caprasse, ti_caprasse = mk_verification_functions pp caprasse_poly true caprasse_min;;
 404 let c0 = run_test tf_caprasse xx_float zz_float false 0.0 true true false true 0.0;;
 405 let certificate = run_test tf_caprasse xx_float zz_float false 0.0 true true true true 0.0;;
 406 let c1 = transform_result xx_float zz_float certificate;;
 407
 408 (* 10: 1.668 *)
 409 reset_all();;
 410 test 1 (m_verify_list n pp eval_caprasse c1 xx1) zz1;;
 411
 412 let p_split = pp and
 413     p_min = 1 and
 414     p_max = pp;;
 415
 416 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_caprasse c1 xx2 zz2;;
 417
 418 (* 10: 1.552 *)
 419 reset_all();;
 420 test 1 (m_p_verify_list n p_split eval_caprasse cp1 xx1) zz1;;
 421
 422
 423 (***)
 424 (* magnetism *)
 425
 426 let pp = 8;;
 427 let n = 7;;
 428 let xx = `[-- &1; -- &1; -- &1; -- &1; -- &1; -- &1; -- &1]` and
 429     zz = `[&1; &1; &1; &1; &1; &1; &1]`;;
 430
 431 let xx1 = convert_to_float_list pp true xx and
 432     zz1 = convert_to_float_list pp false zz;;
 433 let xx2 = Informal_taylor.convert_to_float_list pp true xx and
 434     zz2 = Informal_taylor.convert_to_float_list pp false zz;;
 435 let xx_float = map float_of_float_tm (dest_list xx1) and
 436     zz_float = map float_of_float_tm (dest_list zz1);;
 437
 438 let eval_magnetism, tf_magnetism, ti_magnetism =
 439   mk_verification_functions pp magnetism_poly true magnetism_min;;
 440 let certificate = run_test tf_magnetism xx_float zz_float false 0.0 true true true true 0.0;;
 441 result_stat certificate;;
 442
 443 let c1 = transform_result xx_float zz_float certificate;;
 444
 445 (* 10: 1.34 *)
 446 reset_all();;
 447 test 1 (m_verify_list n pp eval_magnetism c1 xx1) zz1;;
 448
 449 let p_split = pp and
 450     p_min = 1 and
 451     p_max = pp;;
 452
 453 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_magnetism c1 xx2 zz2;;
 454
 455 (* 10: 1.372 *)
 456 reset_all();;
 457 test 1 (m_p_verify_list n p_split eval_magnetism cp1 xx1) zz1;;
 458
 459
 460 (***)
 461 (* heart *)
 462
 463 let pp = 10;;
 464 let pp0 = 6;;
 465 let n = 8;;
 466 let xx = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]` and
 467     zz = `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;
 468
 469 let xx1 = convert_to_float_list pp0 true xx and
 470     zz1 = convert_to_float_list pp0 false zz;;
 471 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
 472     zz2 = Informal_taylor.convert_to_float_list pp0 false zz;;
 473 let xx_float = map float_of_float_tm (dest_list xx1) and
 474     zz_float = map float_of_float_tm (dest_list zz1);;
 475
 476 let eval_heart, tf_heart, ti_heart = mk_verification_functions pp heart_poly true heart_min;;
 477 let certificate = run_test tf_heart xx_float zz_float false 0.0 true true true true 1e-10;;
 478 let c1 = transform_result xx_float zz_float certificate;;
 479
 480 let p_split = pp and
 481     p_min = 1 and
 482     p_max = 10;;
 483
 484 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_heart c1 xx2 zz2;;
 485
 486 (* 10: 1.528 *)
 487 reset_all();;
 488 test 1 (m_verify_list n pp eval_heart c1 xx1) zz1;;
 489
 490 (* 10: 1.496 *)
 491 reset_all();;
 492 test 1 (m_p_verify_list n p_split eval_heart cp1 xx1) zz1;;
 493