formal_lp/old/formal_interval/m_tests3.hl

   1 let mem_stat () =\r
   2   let stat = Gc.stat() in\r
   3   let word = float_of_int (Sys.word_size / 8) in\r
   4   let free = float_of_int stat.Gc.free_words *. word /. 1024.0 in\r
   5   let total = float_of_int stat.Gc.heap_words *. word /. 1024.0 in\r
   6   let allocated = total -. free in\r
   7   let str = sprintf "allocated = %f (free = %f; total_size = %f; %f)\n" \r
   8     allocated free total (free /. total) in\r
   9     print_string str;;\r
  10 \r
  11 \r
  12 (* allocated = 85862 *)\r
  13 mem_stat();;\r
  14 \r
  15 Gc.set { (Gc.get()) with Gc.verbose = 0x05 };;\r
  16 Gc.compact();;\r
  17 \r
  18 (* allocated = 60243 *)\r
  19 mem_stat();;\r
  20 \r
  21 \r
  22 \r
  23 \r
  24 flyspeck_needs "../formal_lp/formal_interval/m_verifier.hl";;\r
  25 \r
  26 (* allocated = 129006 *)\r
  27 mem_stat();;\r
  28 \r
  29 Gc.compact();;\r
  30 (* allocated = 80510 *)\r
  31 mem_stat();;\r
  32 \r
  33 Arith_cache.print_stat();;\r
  34 Arith_float.print_stat();;\r
  35 \r
  36 \r
  37 let reset_all () =\r
  38   Arith_cache.reset_cache();\r
  39   Arith_cache.reset_stat();\r
  40   Arith_float.reset_cache();\r
  41   Arith_float.reset_stat();;\r
  42 \r
  43 \r
  44 reset_all();;\r
  45 Gc.compact();;\r
  46 (* allocated = 79346 *)\r
  47 mem_stat();;\r
  48 \r
  49 \r
  50 (**************************)\r
  51 (* Examples *)\r
  52 let heart_poly = expr_to_vector_fun `-- x1 * x6 pow 3 + &3 * x1 * x6 * x7 pow 2 - x3 * x7 pow 3 +\r
  53   &3 * x3 * x7 * x6 pow 2 - x2 * x5 pow 3 + &3 * x2 * x5 * x8 pow 2 - x4 * x8 pow 3 + \r
  54   &3 * x4 * x8 * x5 pow 2 - #0.9563453`;;\r
  55 \r
  56 let poly1 = `x2 + x3 + x5 + x6 - #7.99 - #0.00385 * delta_y x1 x2 x3 x4 x5 x6 - \r
  57   #2.75 * ((x1 + x4) * #0.5 - sqrt (&8))`;;\r
  58 let poly_ineq = (expr_to_vector_fun o rand o concl o \r
  59                    REWRITE_CONV[Sphere.delta_y; Sphere.delta_x]) poly1;;\r
  60 \r
  61 let heart_min = `-- #1.7435` and\r
  62         poly_min = `&0`;;\r
  63 \r
  64 let heart_dom = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]`,\r
  65   `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;\r
  66 let poly_dom = `[sqrt (&8); &2; &2; sqrt (&8); &2; &2]`,\r
  67         `[&3; #2.07; #2.07; &4 * #1.26; #2.07; #2.07]`;;\r
  68 \r
  69 \r
  70 (***********************************)\r
  71 \r
  72 let test_verify pp poly_tm min_flag val_tm (xx,zz) eps =\r
  73   let total_start = Sys.time() in\r
  74   let n = (get_dim o fst o dest_abs) poly_tm in\r
  75   let xx1 = convert_to_float_list pp true xx and\r
  76       zz1 = convert_to_float_list pp false zz in\r
  77   let xx_float = map float_of_float_tm (dest_list xx1) and\r
  78       zz_float = map float_of_float_tm (dest_list zz1) in\r
  79   let eval_fs, tf = mk_verification_functions pp poly_tm min_flag val_tm in\r
  80   let certificate = run_test tf xx_float zz_float false 0.0 true true true true eps in\r
  81   let c1 = transform_result xx_float zz_float certificate in\r
  82   let start = Sys.time() in\r
  83   let result = m_verify_list n pp eval_fs c1 xx1 zz1 in\r
  84   let finish = Sys.time() in\r
  85   let _ = report \r
  86     (sprintf "Total time: %f; Verification time: %f" (finish -. total_start) (finish -. start)) in\r
  87     result;;\r
  88 \r
  89 \r
  90 (******)\r
  91 \r
  92 (* \r
  93    PVS: 79.68; 26.14\r
  94    8 (10): 27.937; 9.176\r
  95    64 (6): 24.249; 5.672\r
  96    512 (3): 23.113; 3.428\r
  97 \r
  98    Why is the base 10 much faster than 8?\r
  99    Possible explanation: the domain is described by decimal numbers,\r
 100    so computations with the base 10 are faster in general (the approximation is better:\r
 101    requires less digits).\r
 102    10 (10): 23.205; 4.376\r
 103    10 (10, cached, float_cached): 20.001; 1.548\r
 104    10 (10, float_cached): 19.769; 1.744\r
 105    100 (5): 21.733; 3.180\r
 106    100 (5, cached): 20.737; 2.196\r
 107 *)\r
 108 \r
 109 \r
 110 reset_all();;\r
 111 test_verify 10 heart_poly true heart_min heart_dom 1e-10;;\r
 112 \r
 113 Arith_cache.print_stat();;\r
 114 Arith_float.print_stat();;\r
 115 \r
 116 (* 117589 *)\r
 117 mem_stat();;\r
 118 \r
 119 Gc.compact();;\r
 120 (* 80340 *)\r
 121 mem_stat();;\r
 122 \r
 123 reset_all();;\r
 124 Gc.compact();;\r
 125 (* 79372 *)\r
 126 mem_stat();;\r
 127 \r
 128 (* \r
 129    8 (10): 215.953; 112.399\r
 130    64 (6): 162.754; 62.588\r
 131    64 (5): 150.573; 49.991\r
 132    512 (3): 137.967; 32.250\r
 133 \r
 134    10 (10): 185.211; 83.785\r
 135    100 (5): 139.821; 40.975\r
 136    100 (5, cached): 119.267; 20.009\r
 137 *)\r
 138 reset_all ();;\r
 139 (*\r
 140 test_verify 5 poly_ineq true poly_min poly_dom 0.0;;\r
 141 Arith_cache.print_stat();;\r
 142 *)\r
 143 \r
 144 (******)\r
 145 \r
 146 let pp = 10;;\r
 147 let n = (get_dim o fst o dest_abs) poly_ineq;;\r
 148 let xx, zz = poly_dom;;\r
 149 let xx1 = convert_to_float_list pp true xx and\r
 150     zz1 = convert_to_float_list pp false zz;;\r
 151 let xx_float = map float_of_float_tm (dest_list xx1) and\r
 152     zz_float = map float_of_float_tm (dest_list zz1);;\r
 153 \r
 154 Arith_cache.print_stat();;\r
 155 Arith_float.print_stat();;\r
 156 \r
 157 let eval_fs, tf = mk_verification_functions pp poly_ineq true poly_min;;\r
 158 \r
 159 Arith_cache.print_stat();;\r
 160 Arith_float.print_stat();;\r
 161 \r
 162 let certificate = run_test tf xx_float zz_float false 0.0 true true true true 0.0;;\r
 163 let c1 = transform_result xx_float zz_float certificate;;\r
 164 \r
 165 reset_all();;\r
 166 \r
 167 (* 10 (10, cached): 30.589 *)\r
 168 (* 10 (10, cached, float_cached): 16.137 *)\r
 169 (* 10 (10, float_cached): 17.001 *)\r
 170 (* 100 (5, cached): 20.101 *)\r
 171 (* 100 (5, cached, float_cached): 10.452 *)\r
 172 \r
 173 let _ =\r
 174   let start = Sys.time() in\r
 175   let result = m_verify_list n pp eval_fs c1 xx1 zz1 in\r
 176   let finish = Sys.time() in\r
 177   let _ = report \r
 178     (sprintf "Verification time: %f" (finish -. start)) in\r
 179     result;;\r
 180 \r
 181 Arith_cache.print_stat();;\r
 182 Arith_float.print_stat();;\r
 183 \r
 184 Gc.compact();;\r
 185 (* 89346 *)\r
 186 mem_stat();;\r
 187 \r
 188 reset_all();;\r
 189 Gc.compact();;\r
 190 (* 79973 *)\r
 191 mem_stat();;\r
 192 \r
 193 \r
 194 (* num *)\r
 195 \r
 196 let add_list = !Arith_cache.add_list and\r
 197     mul_list = !Arith_cache.mul_list and\r
 198     sub_le_list = !Arith_cache.sub_le_list;;\r
 199 \r
 200 (* 10: 24.621 *)\r
 201 (* 100: 7.612 *)\r
 202 test 1 (map Arith_hash.raw_add_conv_hash) add_list;;\r
 203 (* 100: 22.681 *)\r
 204 test 1 (map Arith_hash.raw_mul_conv_hash) mul_list;;\r
 205 (* 100: 9.917 *)\r
 206 test 1 (map (fun tm1, tm2 -> Arith_hash.raw_sub_and_le_hash_conv tm1 tm2)) sub_le_list;;\r
 207 \r
 208 Arith_cache.reset_cache();;\r
 209 \r
 210 (* 10: 6.064 *)\r
 211 (* 100: 1.884 *)\r
 212 test 1 (map raw_add_conv_hash) add_list;;\r
 213 (* 100: 2.396 *)\r
 214 test 1 (map raw_mul_conv_hash) mul_list;;\r
 215 (* 100: 2.384 *)\r
 216 test 1 (map (fun tm1, tm2 -> raw_sub_and_le_hash_conv tm1 tm2)) sub_le_list;;\r
 217 \r
 218 \r
 219 (****************)\r
 220 (* float *)\r
 221 \r
 222 let mul_lo_list = !Arith_float.mul_lo_list and\r
 223     mul_hi_list = !Arith_float.mul_hi_list and\r
 224     add_lo_list = !Arith_float.add_lo_list and\r
 225     add_hi_list = !Arith_float.add_hi_list;;\r
 226 \r
 227 (* 10: 10.308 *)\r
 228 reset_all();;\r
 229 test 1 (map (fun p,tm1,tm2 -> float_mul_lo p tm1 tm2)) mul_lo_list;;\r
 230 (* 10: 13.152 *)\r
 231 reset_all();;\r
 232 test 1 (map (fun p,tm1,tm2 -> float_mul_hi p tm1 tm2)) mul_hi_list;;\r
 233 \r
 234 (* 10: 2.688 *)\r
 235 reset_all();;\r
 236 test 1 (map (fun p,tm1,tm2 -> float_add_lo p tm1 tm2)) add_lo_list;;\r
 237 (* 10: 3.104 *)\r
 238 reset_all();;\r
 239 test 1 (map (fun p,tm1,tm2 -> float_add_hi p tm1 tm2)) add_hi_list;;\r
 240 \r
 241 (***********)\r
 242 \r
 243 let float_hash tm =\r
 244   let s, n_tm, e_tm = dest_float tm in\r
 245     s ^ (num_tm_hash n_tm) ^ "e" ^ (num_tm_hash e_tm);;\r
 246 \r
 247 \r
 248 let float_op_hash pp tm1 tm2 =\r
 249   string_of_int pp ^ float_hash tm1 ^ "x" ^ float_hash tm2;;\r
 250 \r
 251 let float_mul_table = Hashtbl.create 10000;;\r
 252 \r
 253 let float_mul_lo_cached pp tm1 tm2 =\r
 254   let hash = float_op_hash pp tm1 tm2 in\r
 255   try\r
 256     Hashtbl.find float_mul_table hash\r
 257   with Not_found ->\r
 258     let result = float_mul_lo pp tm1 tm2 in\r
 259     let _ = Hashtbl.add float_mul_table hash result in\r
 260       result;;\r
 261 \r
 262 reset_all();;  \r
 263 \r
 264 (* 10: 3.624 *)\r
 265 test 1 (map (fun p,tm1,tm2 -> float_mul_lo_cached p tm1 tm2)) mul_lo_list;;\r
 266 (* 2150 *)\r
 267 Hashtbl.length float_mul_table;;\r
 268 (* 24044 *)\r
 269 length mul_lo_list;;\r
 270 \r
 271 \r
 272 let x = 2;;\r
 273 \r
 274 \r
 275 \r
 276 (****************)\r
 277 \r
 278 Hashtbl.length Arith_cache.mul_table;;\r
 279 Hashtbl.length Arith_cache.sub_le_table;;\r
 280 Hashtbl.length Arith_cache.add_table;;\r
 281 \r
 282 \r
 283 (* 100: 0.148 *)\r
 284 test 1 (map Arith_hash.raw_suc_conv_hash) !Arith_cache.suc_list;;\r
 285 (* 100: 0.180 *)\r
 286 test 1 (map Arith_hash.raw_eq0_hash_conv) !Arith_cache.eq0_list;;\r
 287 (* 100: 0.532 *)\r
 288 test 1 (map Arith_hash.raw_div_hash_conv) !Arith_cache.div_list;;\r
 289 \r
 290 (* 100: 10.196 *)\r
 291 test 1 (map (fun tm1, tm2 -> Arith_hash.raw_sub_and_le_hash_conv tm1 tm2)) !Arith_cache.sub_le_list;;\r
 292 \r
 293 \r
 294 \r
 295 \r
 296 let mul_table = Hashtbl.create 100000;;\r
 297 \r
 298 let mul_cache1 tm =\r
 299   if Hashtbl.mem mul_table tm then\r
 300     Hashtbl.find mul_table tm\r
 301   else\r
 302     let result = Arith_hash.raw_mul_conv_hash tm in\r
 303     let _ = Hashtbl.add mul_table tm result in\r
 304       result;;\r
 305 \r
 306 \r
 307 (* 100: 25.882 *)\r
 308 Hashtbl.clear mul_table;;\r
 309 test 1 (map mul_cache1) !Arith_cache.mul_list;;\r
 310 (* 100: 44.398 *)\r
 311 test 1 (map mul_cache1) !Arith_cache.mul_list;;\r
 312 \r
 313 (* 100: 22.609 *)\r
 314 test 1 (map (Hashtbl.mem mul_table)) !Arith_cache.mul_list;;\r
 315 (* 100: 22.233 *)\r
 316 test 1 (map (Hashtbl.find mul_table)) !Arith_cache.mul_list;;\r
 317 (* 100: 0.044 *)\r
 318 test 1 (map Hashtbl.hash) !Arith_cache.mul_list;;\r
 319 \r
 320 let rec num_tm_hash tm =\r
 321   if is_comb tm then\r
 322     let b_tm, n_tm = dest_comb tm in\r
 323     let str = (fst o dest_const) b_tm in\r
 324       str ^ num_tm_hash n_tm\r
 325   else\r
 326     "";;\r
 327 \r
 328 \r
 329 let op_tm_hash tm =\r
 330   let lhs, tm2 = dest_comb tm in\r
 331   let tm1 = rand lhs in\r
 332     num_tm_hash tm1 ^ "x" ^ num_tm_hash tm2;;\r
 333 \r
 334 \r
 335 (* 0.340 *)\r
 336 test 1 (map op_tm_hash) !Arith_cache.mul_list;;\r
 337 (* 0.428 *)\r
 338 test 1 (map (Hashtbl.hash o op_tm_hash)) !Arith_cache.mul_list;;\r
 339 \r
 340 (******)\r
 341 \r
 342 let mul_table2 = Hashtbl.create 10000;;\r
 343 let add_table2 = Hashtbl.create 10000;;\r
 344 let div_table2 = Hashtbl.create 10000;;\r
 345 \r
 346 let mul_cache2 tm =\r
 347   let hash = op_tm_hash tm in\r
 348     try\r
 349       Hashtbl.find mul_table2 hash\r
 350     with Not_found ->\r
 351       let result = Arith_hash.raw_mul_conv_hash tm in\r
 352       let _ = Hashtbl.add mul_table2 hash result in\r
 353         result;;\r
 354 \r
 355 let add_cache2 tm =\r
 356   let hash = op_tm_hash tm in\r
 357     try\r
 358       Hashtbl.find add_table2 hash\r
 359     with Not_found ->\r
 360       let result = Arith_hash.raw_add_conv_hash tm in\r
 361       let _ = Hashtbl.add add_table2 hash result in\r
 362         result;;\r
 363 \r
 364 let div_cache2 tm =\r
 365   let hash = op_tm_hash tm in\r
 366     try\r
 367       Hashtbl.find div_table2 hash\r
 368     with Not_found ->\r
 369       let result = Arith_hash.raw_div_hash_conv tm in\r
 370       let _ = Hashtbl.add div_table2 hash result in\r
 371         result;;\r
 372 \r
 373 Hashtbl.clear div_table2;;\r
 374 (* 100: 0.016 *)\r
 375 test 1 (map div_cache2) !Arith_cache.div_list;;\r
 376 (* 12 *)\r
 377 Hashtbl.length div_table2;;\r
 378 (* 100: 0.016 *)\r
 379 test 1 (map div_cache2) !Arith_cache.div_list;;\r
 380 \r
 381 \r
 382 Hashtbl.clear mul_table2;;\r
 383 (* 100: 2.536 *)\r
 384 test 1 (map mul_cache2) !Arith_cache.mul_list;;\r
 385 (* 4687 *)\r
 386 Hashtbl.length mul_table2;;\r
 387 (* 100: 0.384 *)\r
 388 test 1 (map mul_cache2) !Arith_cache.mul_list;;\r
 389 \r
 390 Hashtbl.clear add_table2;;\r
 391 (* 100: 2.052 *)\r
 392 test 1 (map add_cache2) !Arith_cache.add_list;;\r
 393 (* 5184 *)\r
 394 Hashtbl.length add_table2;;\r
 395 (* 100: 1.548 *)\r
 396 test 1 (map add_cache2) !Arith_cache.add_list;;\r
 397 \r
 398 \r
 399 \r
 400 let op_sizes tm =\r
 401   let lhs, tm2 = dest_comb tm in\r
 402   let tm1 = rand lhs in\r
 403   let list1 = striplist dest_comb tm1 and\r
 404       list2 = striplist dest_comb tm2 in\r
 405     length list1, length list2;;\r
 406 \r
 407 let l0 = map op_sizes !Arith_cache.mul_list;;\r
 408 (* 172 *)\r
 409 length (List.filter (fun p -> fst p = 1) l0);;\r
 410 (* 514 *)\r
 411 length (List.filter (fun p -> fst p = 2) l0);;\r
 412 (* 345 *)\r
 413 length (List.filter (fun p -> fst p = 3) l0);;\r
 414 (* 6 *)\r
 415 length (List.filter (fun p -> fst p = 4) l0);;\r
 416 (* 106 *)\r
 417 length (List.filter (fun p -> fst p = 5) l0);;\r
 418 (* 2872 *)\r
 419 length (List.filter (fun p -> fst p = 6) l0);;\r
 420 (* 672 *)\r
 421 length (List.filter (fun p -> fst p = 7) l0);;\r
 422 \r
 423 (* 0 *)\r
 424 length (List.filter (fun p -> snd p = 1) l0);;\r
 425 (* 93 *)\r
 426 length (List.filter (fun p -> snd p = 2) l0);;\r
 427 (* 1 *)\r
 428 length (List.filter (fun p -> snd p = 3) l0);;\r
 429 (* 13 *)\r
 430 length (List.filter (fun p -> snd p = 4) l0);;\r
 431 (* 175 *)\r
 432 length (List.filter (fun p -> snd p = 5) l0);;\r
 433 (* 4187 *)\r
 434 length (List.filter (fun p -> snd p = 6) l0);;\r
 435 (* 218 *)\r
 436 length (List.filter (fun p -> snd p = 7) l0);;\r
 437 \r