formal_lp/old/formal_interval/m_tests4.hl

   1 let mem_stat () =
   2   let stat = Gc.stat() in
   3   let word = float_of_int (Sys.word_size / 8) in
   4   let free = float_of_int stat.Gc.free_words *. word /. 1024.0 in
   5   let total = float_of_int stat.Gc.heap_words *. word /. 1024.0 in
   6   let allocated = total -. free in
   7   let str = sprintf "allocated = %f (free = %f; total_size = %f; %f)\n"
   8     allocated free total (free /. total) in
   9     print_string str;;
  10
  11
  12 (* allocated = 85862 *)
  13 mem_stat();;
  14
  15 Gc.set { (Gc.get()) with Gc.verbose = 0x05 };;
  16 Gc.compact();;
  17
  18 (* allocated = 60243 *)
  19 mem_stat();;
  20
  21
  22 needs "../formal_lp/formal_interval/m_taylor_arith.hl";;
  23 needs "../formal_lp/formal_interval/m_verifier.hl";;
  24
  25 let reset_all () =
  26   Arith_cache.reset_cache();
  27   Arith_cache.reset_stat();
  28   Arith_float.reset_cache();
  29   Arith_float.reset_stat();;
  30
  31 Arith_cache.print_stat();;
  32 Arith_float.print_stat();;
  33 reset_all();;
  34
  35
  36 (******************************)
  37
  38 (* dummy functions *)
  39
  40 let eval_d0 i t1 t2 = failwith "eval_d0";;
  41 let eval_dd0 i j t1 t2 = failwith "eval_dd0";;
  42 let eval_0 t1 t2 = failwith "eval_0";;
  43
  44
  45 (******************************)
  46 (* real tests *)
  47
  48 let n = 6;;
  49 let pp = 15;;
  50 let pp = 8;;
  51
  52 (* delta_y *)
  53 let delta_y_poly =
  54   let tm = (rand o concl o SPEC_ALL o REWRITE_RULE[Sphere.delta_x]) Sphere.delta_y in
  55     expr_to_vector_fun tm;;
  56
  57 (* delta_y4 *)
  58 let delta_y4_poly =
  59   let tm = (rand o concl o SPECL[`y1*y1`; `y2*y2`; `y3*y3`; `y4*y4`; `y5*y5`; `y6*y6`]) Sphere.delta_x4 in
  60     expr_to_vector_fun tm;;
  61
  62 (* 4 * y1 * delta_y *)
  63 let four_y1_delta_y_poly =
  64   let x_var, tm = dest_abs delta_y_poly in
  65     mk_abs (x_var, mk_binop mul_op_real `&4` (mk_binop mul_op_real `(x:real^6)$1 * x$1` tm));;
  66
  67 (* - delta_y4 *)
  68 let neg_delta_y4_poly =
  69   let x_var, tm = dest_abs delta_y4_poly in
  70     mk_abs (x_var, mk_comb (neg_op_real, tm));;
  71
  72
  73 let (_, _, _, eval_neg_delta_y4), tf_neg_delta_y4 =
  74   mk_verification_functions pp neg_delta_y4_poly false `&0`;;
  75
  76 let (_, _, _, eval_4y1_delta_y), tf_4y1_delta_y =
  77   mk_verification_functions pp four_y1_delta_y_poly false `&0`;;
  78
  79 let (_, _, _, eval_pi2), tf_pi2 =
  80   mk_verification_functions pp `\x:real^6. pi / &2` false `&0`;;
  81
  82
  83 let (_, _, _, eval_pi2_plus), tf_pi2_plus =
  84   mk_verification_functions pp `\x:real^6. pi / &2 - #1.893` false `&0`;;
  85
  86
  87 (* dih_y *)
  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 th =
  93   let inv, atn, sqrt, ( * ), ( + ) =
  94     eval_m_taylor_inv n pp, eval_m_taylor_atn n pp, eval_m_taylor_sqrt n pp,
  95     eval_m_taylor_mul n pp, eval_m_taylor_add n pp in
  96   let poly1 = eval_4y1_delta_y th and
  97       poly2 = eval_neg_delta_y4 th and
  98       pi2 = eval_pi2_plus th in
  99     pi2 + atn (poly2 * inv (sqrt (poly1)));;
 100
 101
 102
 103 (************)
 104
 105 let xx = `[&2; &2; &2; &2; &2; &2]` and
 106     zz = `[#2.52; #2.52; #2.52; #2.52; #2.52; #2.52]`;;
 107
 108 let xx1 = convert_to_float_list pp true xx and
 109     zz1 = convert_to_float_list pp false zz;;
 110
 111
 112 (* Small domain *)
 113 let xx_s = `[&2; &2; &2; &2; &2; &2]` and
 114     zz_s = `[#2.1; #2.1; #2.1; #2.1; #2.1; #2.1]`;;
 115
 116
 117 let domain_th =
 118   let xx1_s = convert_to_float_list pp true xx_s and
 119       zz1_s = convert_to_float_list pp false zz_s in
 120     mk_m_center_domain n pp xx1_s zz1_s;;
 121
 122 reset_all();;
 123
 124 (* 10: 9.121 (pp = 15) *)
 125 (* 300: 5.5 (pp = 8) *)
 126 (* 100 (cached, float_cached, pp = 8): 2.68 *)
 127 test 1 eval_dih_y_hi domain_th;;
 128
 129 Arith_cache.print_stat();;
 130 Arith_float.print_stat();;
 131
 132
 133 (***)
 134
 135 let xx_s = `[&2; &2; &2; &2; &2; &2]` and
 136     zz_s = `[#2.52; #2.1; #2.1; #2.1; #2.1; #2.1]`;;
 137
 138 let xx_s2 = `[&2; &2; &2; &2; &2; &2]` and
 139     zz_s2 = `[#2.52; #2.2; #2.2; #2.2; #2.2; #2.2]`;;
 140
 141
 142 let xx1_s = convert_to_float_list pp true xx_s and
 143     zz1_s = convert_to_float_list pp false zz_s;;
 144
 145 let xx1_s2 = convert_to_float_list pp true xx_s2 and
 146     zz1_s2 = convert_to_float_list pp false zz_s2;;
 147
 148
 149
 150 let xx_float, zz_float, xx_s_float, zz_s_float, xx_s2_float, zz_s2_float =
 151   let pad = replicate 0.0 (8 - length (dest_list xx1)) in
 152     map float_of_float_tm (dest_list xx1) @ pad,
 153     map float_of_float_tm (dest_list zz1) @ pad,
 154     map float_of_float_tm (dest_list xx1_s) @ pad,
 155     map float_of_float_tm (dest_list zz1_s) @ pad,
 156     map float_of_float_tm (dest_list xx1_s2) @ pad,
 157     map float_of_float_tm (dest_list zz1_s2) @ pad;;
 158
 159
 160
 161 (***)
 162
 163 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;;
 164 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;;
 165 let c_dih_y0 = run_test tf_dih_y_hi xx_float zz_float false 0.0 true false false false 0.0;;
 166
 167 (* pass = 4 *)
 168 result_stat c_dih_y_s;;
 169 (* pass = 63 *)
 170 result_stat c_dih_y_s2;;
 171 (* pass = 4294, mono = 10 *)
 172 result_stat c_dih_y0;;
 173
 174 reset_all();;
 175 Gc.compact();;
 176 (* 80642 *)
 177 mem_stat();;
 178
 179 (* 10 (pp = 15): 38.418 *)
 180 (* 300 (pp = 8): 22.289 *)
 181 (* 100 (cached, float_cached, pp = 8): 12.229 *)
 182 let _ =
 183   let start = Sys.time() in
 184   let result = m_verify_raw0 n pp (eval_d0, eval_dd0, eval_0, eval_dih_y_hi) c_dih_y_s xx1_s zz1_s in
 185   let finish = Sys.time() in
 186   let _ = report
 187     (sprintf "Verification time: %f" (finish -. start)) in
 188     result;;
 189
 190 Arith_cache.print_stat();;
 191 Arith_float.print_stat();;
 192
 193 (* 104321 *)
 194 mem_stat();;
 195 Gc.compact();;
 196 (* 84679 *)
 197 mem_stat();;
 198
 199 reset_all();;
 200 Gc.compact();;
 201 (* 80643 *)
 202 mem_stat();;
 203
 204 (* 100 (cached, float_cached, pp = 8): 233.80 *)
 205 let _ =
 206   let start = Sys.time() in
 207   let result = m_verify_raw0 n pp (eval_d0, eval_dd0, eval_0, eval_dih_y_hi) c_dih_y_s2 xx1_s2 zz1_s2 in
 208   let finish = Sys.time() in
 209   let _ = report
 210     (sprintf "Verification time: %f" (finish -. start)) in
 211     result;;
 212
 213 Arith_cache.print_stat();;
 214 Arith_float.print_stat();;
 215
 216 (* 135718 (after two runs)  *)
 217 mem_stat();;
 218 Gc.compact();;
 219 (* 101048  *)
 220 mem_stat();;
 221
 222 reset_all();;
 223 Gc.compact();;
 224 (* 81711  *)
 225 mem_stat();;
 226
 227
 228 (* 15202 *)
 229 let _ =
 230   let start = Sys.time() in
 231   let result = m_verify_raw0 n pp (eval_d0, eval_dd0, eval_0, eval_dih_y_hi) c_dih_y0 xx1 zz1 in
 232   let finish = Sys.time() in
 233   let _ = report
 234     (sprintf "Verification time: %f" (finish -. start)) in
 235     result;;