formal_lp/old/arith/informal/tests3.hl

   1 needs "../formal_lp/formal_interval/m_taylor_arith.hl";;
   2 needs "../formal_lp/formal_interval/m_verifier.hl";;
   3 needs "../formal_lp/arith/informal/informal_m_verifier.hl";;
   4
   5
   6 let reset_all () =
   7   Arith_cache.reset_stat();
   8   Arith_cache.reset_cache();
   9   Arith_float.reset_stat();
  10   Arith_float.reset_cache();;
  11
  12
  13 let dest_int int =
  14   let f1, f2 = Informal_interval.dest_interval int in
  15     Informal_float.dest_float f1, Informal_float.dest_float f2;;
  16
  17 let dest_f = Informal_float.dest_float;;
  18
  19 let dest_dom dom =
  20   map dest_f dom.Informal_taylor.lo,
  21   map dest_f dom.Informal_taylor.hi,
  22   map dest_f dom.Informal_taylor.y,
  23   map dest_f dom.Informal_taylor.w;;
  24
  25 let dest_ti ti =
  26   dest_int ti.Informal_taylor.f,
  27   map dest_int ti.Informal_taylor.df,
  28   map (map dest_int) ti.Informal_taylor.ddf;;
  29
  30
  31
  32 (******************************)
  33
  34 (* dummy functions *)
  35
  36 let eval_d0 i pp t1 t2 = failwith "eval_d0";;
  37 let eval_dd0 i j pp t1 t2 = failwith "eval_dd0";;
  38 let eval_0 pp t1 t2 = failwith "eval_0";;
  39 let eval_diff2 t1 t2 = failwith "eval_diff2";;
  40
  41
  42 (********************************)
  43 (* ArcProperties.hl inequality *)
  44
  45 let n = 2;;
  46 let p_split = 8 and
  47     p_min = 1 and
  48     p_max = 10;;
  49
  50 let poly1 = `\x:real^2. x$1 * x$1 + x$2 * x$2 - &2 * &2`;;
  51 let poly2 = `\x:real^2. &2 * x$1 * x$2`;;
  52 let lm2_poly = `\x:real^2. (#2.52 - x$1 * inv(&2)) * inv(#2.52 - &1)`;;
  53
  54 let eval1, tf1, ti1 =
  55   mk_verification_functions p_split poly1 false `&0`;;
  56
  57 let eval2, tf2, ti2 =
  58   mk_verification_functions p_split poly2 false `&0`;;
  59
  60 let eval_lm2, tf_lm2, ti_lm2 =
  61   mk_verification_functions p_split lm2_poly false `&0`;;
  62
  63
  64 (* arc *)
  65 open Univariate;;
  66
  67 let tf_arc =
  68   let r = Product (tf1, Uni_compose (uinv, tf2)) in
  69     Uni_compose (uacos, r);;
  70
  71
  72 let eval_arc p_lin p_second th =
  73   let inv, acs, ( * ) =
  74     eval_m_taylor_inv n p_lin p_second, eval_m_taylor_acs n p_lin p_second,
  75     eval_m_taylor_mul n p_lin p_second in
  76   let r1 = eval1.taylor p_lin p_second th and
  77       r2 = eval2.taylor p_lin p_second th in
  78     acs (r1 * inv r2);;
  79
  80
  81 let ti_arc p_lin p_second dom =
  82   let inv, acs, ( * ) =
  83     Informal_taylor.eval_m_taylor_inv p_lin p_second, Informal_taylor.eval_m_taylor_acs p_lin p_second,
  84     Informal_taylor.eval_m_taylor_mul p_lin p_second in
  85   let r1 = ti1.Informal_verifier.taylor p_lin p_second dom and
  86       r2 = ti2.Informal_verifier.taylor p_lin p_second dom in
  87     acs (r1 * inv r2);;
  88
  89
  90 (*********************)
  91
  92 let eval_ineq p_lin p_second th =
  93   let arc = eval_arc p_lin p_second
  94
  95 Sphere.lmfun;;
  96
  97
  98 let eval_taylor =
  99   {taylor = eval_dih_y_hi; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;
 100
 101 let ti =
 102   {Informal_verifier.taylor = ti_dih_y_hi;
 103   Informal_verifier.f = eval_0;
 104   Informal_verifier.df = eval_d0;
 105   Informal_verifier.ddf = eval_dd0};;
 106
 107
 108
 109 (************)
 110 (* Small domain *)
 111 let xx_s = `[&2; &2; &2; &2; &2; &2]` and
 112     zz_s = `[#2.1; #2.1; #2.1; #2.1; #2.1; #2.1]`;;
 113
 114 let domain_th =
 115   let xx1_s = convert_to_float_list pp true xx_s and
 116       zz1_s = convert_to_float_list pp false zz_s in
 117     mk_m_center_domain n pp xx1_s zz1_s;;
 118
 119 let dom =
 120   let xx2_s = Informal_taylor.convert_to_float_list pp true xx_s and
 121       zz2_s = Informal_taylor.convert_to_float_list pp false zz_s in
 122     Informal_taylor.mk_m_center_domain pp xx2_s zz2_s;;
 123
 124
 125
 126 (* 10: 9.121 (pp = 15) *)
 127 (* 300: 5.5 (pp = 8) *)
 128 (* 100 (cached, float_cached, pp = 8): 2.68 *)
 129 reset_all();;
 130 test 1 (eval_dih_y_hi pp pp) domain_th;;
 131 (* 100: 1.668 *)
 132 test 1 (eval_dih_y_hi pp pp) domain_th;;
 133 (* 100: 0.088 *)
 134 test 1 (ti_dih_y_hi pp pp) dom;;
 135
 136
 137 Arith_cache.print_stat();;
 138 Arith_float.print_stat();;
 139
 140 (***)
 141
 142 let th1 = eval_4y1_delta_y.taylor pp pp domain_th;;
 143 let th2 = eval_neg_delta_y4.taylor pp pp domain_th;;
 144 let pi2_th = eval_pi2_plus.taylor pp pp domain_th;;
 145
 146 let r1 = eval_m_taylor_sqrt n pp th1;;
 147 let r2 = eval_m_taylor_inv n pp r1;;
 148 let r3 = eval_m_taylor_mul n pp th2 r2;;
 149 let r4 = eval_m_taylor_atn n pp r3;;
 150 let r5 = eval_m_taylor_add n pp pi2_th r4;;
 151
 152
 153 reset_all();;
 154 (* 100: 0.264 (second: 0.084) *)
 155 test 1 (eval_4y1_delta_y.taylor pp pp) domain_th;;
 156 (* 100: 0.032 (second: 0.020) *)
 157 test 1 (eval_neg_delta_y4.taylor pp pp) domain_th;;
 158 (* 100: 0.000 (second: 0.000) *)
 159 test 1 (eval_pi2_plus.taylor pp pp) domain_th;;
 160
 161 (* 100: 0.444 (second: 0.280) *)
 162 test 1 (eval_m_taylor_sqrt n pp) th1;;
 163 (* 100: 0.496 (second: 0.284) *)
 164 test 1 (eval_m_taylor_inv n pp) r1;;
 165 (* 100: 0.512 (second: 0.396) *)
 166 test 1 (eval_m_taylor_mul n pp th2) r2;;
 167 (* 100: 0.780 (second: 0.444) *)
 168 test 1 (eval_m_taylor_atn n pp) r3;;
 169 (* 100: 0.264 (second: 0.256) *)
 170 test 1 (eval_m_taylor_add n pp pi2_th) r4;;
 171
 172
 173
 174 (***)
 175 let xx = `[&2; &2; &2; &2; &2; &2]` and
 176     zz = `[#2.52; #2.52; #2.52; #2.52; #2.52; #2.52]`;;
 177
 178 let xx_s = `[&2; &2; &2; &2; &2; &2]` and
 179     zz_s = `[#2.52; #2.1; #2.1; #2.1; #2.1; #2.1]`;;
 180
 181 let xx_s2 = `[&2; &2; &2; &2; &2; &2]` and
 182     zz_s2 = `[#2.52; #2.2; #2.2; #2.2; #2.2; #2.2]`;;
 183
 184
 185 let pp0 = 3;;
 186 let xx1 = convert_to_float_list pp0 true xx and
 187     zz1 = convert_to_float_list pp0 false zz and
 188     xx1_s = convert_to_float_list pp0 true xx_s and
 189     zz1_s = convert_to_float_list pp0 false zz_s and
 190     xx1_s2 = convert_to_float_list pp0 true xx_s2 and
 191     zz1_s2 = convert_to_float_list pp0 false zz_s2;;
 192
 193 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
 194     zz2 = Informal_taylor.convert_to_float_list pp0 false zz and
 195     xx2_s = Informal_taylor.convert_to_float_list pp0 true xx_s and
 196     zz2_s = Informal_taylor.convert_to_float_list pp0 false zz_s and
 197     xx2_s2 = Informal_taylor.convert_to_float_list pp0 true xx_s2 and
 198     zz2_s2 = Informal_taylor.convert_to_float_list pp0 false zz_s2;;
 199
 200
 201 let xx_float, zz_float, xx_s_float, zz_s_float, xx_s2_float, zz_s2_float =
 202   let pad = replicate 0.0 (8 - length (dest_list xx1)) in
 203     map float_of_float_tm (dest_list xx1) @ pad,
 204     map float_of_float_tm (dest_list zz1) @ pad,
 205     map float_of_float_tm (dest_list xx1_s) @ pad,
 206     map float_of_float_tm (dest_list zz1_s) @ pad,
 207     map float_of_float_tm (dest_list xx1_s2) @ pad,
 208     map float_of_float_tm (dest_list zz1_s2) @ pad;;
 209
 210
 211
 212 (***)
 213
 214
 215 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;;
 216 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;;
 217 let c_dih_y0 = run_test tf_dih_y_hi xx_float zz_float false 0.0 true false false false 0.0;;
 218
 219 (* pass = 4 *)
 220 result_stat c_dih_y_s;;
 221 (* pass = 63 *)
 222 result_stat c_dih_y_s2;;
 223 (* pass = 4294, mono = 10 *)
 224 result_stat c_dih_y0;;
 225
 226 let p_split = pp and
 227     p_min = 1 and
 228     p_max = pp;;
 229
 230 let cp_s = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y_s xx2_s zz2_s;;
 231 let cp_s2 = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y_s2 xx2_s2 zz2_s2;;
 232
 233
 234 (*********************)
 235
 236 reset_all();;
 237
 238 (* 10 (pp = 15): 38.418 *)
 239 (* 300 (pp = 8): 22.289 *)
 240 (* 100 (cached, float_cached, pp = 8): 12.229 *)
 241 let _ =
 242   let start = Sys.time() in
 243   let result = m_verify_raw0 n pp eval_taylor c_dih_y_s xx1_s zz1_s in
 244   let finish = Sys.time() in
 245   let _ = report
 246     (sprintf "Verification time: %f" (finish -. start)) in
 247     result;;