formal_lp/old/formal_interval/interval_m/function_data.hl

   1 (* file combining all the function data *)
   2
   3 (*
   4
   5 This gives the verification of a sample inequality drawn from ineq.hl.
   6
   7 *)
   8
   9
  10 flyspeck_needs "../formal_lp/formal_interval/interval_m/recurse.hl";;
  11 flyspeck_needs "../formal_lp/formal_interval/interval_m/verifier.hl";;
  12
  13
  14 open Interval;;
  15 open Univariate;;
  16 open Line_interval;;
  17 open Taylor;;
  18 open Recurse;;
  19
  20 (********************************)
  21
  22 let delta_x_poly =
  23   let tm = (rand o concl o SPEC_ALL) Sphere.delta_x in
  24     expr_to_vector_fun tm;;
  25
  26 let delta_y_poly =
  27   let tm = (rand o concl o SPEC_ALL o REWRITE_RULE[Sphere.delta_x]) Sphere.delta_y in
  28     expr_to_vector_fun tm;;
  29
  30 let delta_x4_poly =
  31   let tm = (rand o concl o SPEC_ALL) Sphere.delta_x4 in
  32     expr_to_vector_fun tm;;
  33
  34 let delta_y4_poly =
  35   let tm = (rand o concl o SPECL[`y1*y1`; `y2*y2`; `y3*y3`; `y4*y4`; `y5*y5`; `y6*y6`]) Sphere.delta_x4 in
  36     expr_to_vector_fun tm;;
  37
  38
  39 let tf_delta_x = build_taylor pp delta_x_poly;;
  40 let tf_delta_y = build_taylor pp delta_y_poly;;
  41 let tf_delta_x4 = build_taylor pp delta_x4_poly;;
  42 let tf_delta_y4 = build_taylor pp delta_y4_poly;;
  43
  44 let x = replicate 1.0 8 and
  45     y = replicate 2.0 8 and
  46     z = replicate 3.0 8 and
  47     w = replicate 1.0 8;;
  48
  49 evalf4 tf_delta_x w x y z;;
  50 evalf4 tf_delta_y w x y z;;
  51 evalf4 tf_delta_x4 w x y z;;
  52
  53
  54 (************************************)
  55
  56
  57 let four_y1_delta_y_poly =
  58   let x_var, tm = dest_abs delta_y_poly in
  59     mk_abs (x_var, mk_binop mul_op_real `&4` (mk_binop mul_op_real `(x:real^6)$1 * x$1` tm));;
  60
  61 let neg_delta_y4_poly =
  62   let x_var, tm = dest_abs delta_y4_poly in
  63     mk_abs (x_var, mk_comb (neg_op_real, tm));;
  64
  65 let four_y1_delta_y = build_taylor pp four_y1_delta_y_poly;;
  66 let neg_delta_y4 = build_taylor pp neg_delta_y4_poly;;
  67 dih_y_taylor;;
  68
  69 let pi_taylor = build_taylor 10 `\x:real^1. pi`;;
  70 let neg_pi_taylor = build_taylor 10 `\x:real^1. --pi`;;
  71 let pi2_taylor = build_taylor 10 `\x:real^1. pi / &2`;;
  72
  73
  74 let f = tf_product x1 (tf_product x1 x3);;
  75 let f = Uni_compose (uinv, x2);;
  76 evalf0 f 0 x y;;
  77 evalf0 f 2 x y;;
  78
  79 (* dih_y *)
  80 let dih_y_taylor =
  81   let denom = Uni_compose (uinv, Uni_compose (usqrt, four_y1_delta_y)) in
  82     Plus (pi2_taylor, Uni_compose (uatan, tf_product neg_delta_y4 denom));;
  83
  84
  85 (* sol_y *)
  86
  87 Sphere.sol_y;;
  88 let sol_y_taylor =
  89   let dih1 = dih_y_taylor and
  90       dih2 = Composite (dih_y_taylor, x2, x3, x1, x5, x6, x4, unit, unit) and
  91       dih3 = Composite (dih_y_taylor, x3, x1, x2, x6, x4, x5, unit, unit) in
  92     Plus (dih1, Plus (dih2, Plus (dih3, neg_pi_taylor)));;
  93
  94
  95 let pi_val= 3.1415926535897932;;
  96 let sol0_val = 0.5512855984325308;;
  97 let const1_val = sol0_val /. pi_val;;
  98 let const1_plus1 = const1_val +. 1.0;;
  99
 100
 101 let ly_taylor = build_taylor pp `\x:real^1. #2.52 / #0.52 - x$1 * inv(#0.52)`;;
 102 let lnazim_y_taylor =
 103   tf_product ly_taylor dih_y_taylor;;
 104
 105 Sphere.taum;;
 106 let taum_taylor =
 107   let azim1 = lnazim_y_taylor and
 108       azim2 = Composite (lnazim_y_taylor, x2, x3, x1, x5, x6, x4, unit, unit) and
 109       azim3 = Composite (lnazim_y_taylor, x3, x1, x2, x6, x4, x5, unit, unit) in
 110   let f1 = Scale (sol_y_taylor, mk_interval (const1_plus1, const1_plus1)) and
 111       f2 = Plus (azim1, Plus (azim2, azim3)) in
 112     Plus (f1, Scale (f2, mk_interval (~-.const1_val, ~-.const1_val)));;
 113
 114
 115 (*********************)
 116
 117 let rec count_f0_flags r =
 118   match r with
 119     | Result_false _ -> failwith "False result"
 120     | Result_glue (_,_,_,r1,r2) -> count_f0_flags r1 + count_f0_flags r2
 121     | Result_pass (_,flag,_,_) -> if flag then 1 else 0
 122     | Result_pass_mono _ -> 0;;
 123
 124 let rec all_mono r =
 125   match r with
 126     | Result_false _ -> failwith "False result"
 127     | Result_glue (mono,_,_,r1,r2) -> List.concat mono @ all_mono r1 @ all_mono r2
 128     | Result_pass (mono,_,_,_) -> List.concat mono
 129     | Result_pass_mono _ -> [];;
 130
 131 let rec all_pass r =
 132   match r with
 133     | Result_false _ -> failwith "False result"
 134     | Result_glue (_,_,_,r1,r2) -> all_pass r1 @ all_pass r2
 135     | Result_pass (_,_,x,z) -> [x,z]
 136     | Result_pass_mono _ -> [];;
 137
 138
 139 let rec count_pass_mono r =
 140   match r with
 141     | Result_false _ -> failwith "False result"
 142     | Result_glue (_,_,_,r1,r2) -> count_pass_mono r1 + count_pass_mono r2
 143     | Result_pass (_,_,_,_) -> 0
 144     | Result_pass_mono _ -> 1;;
 145
 146 let rec count_convex r =
 147   match r with
 148     | Result_false _ -> failwith "False result"
 149     | Result_glue (_,_,flag,r1,r2) -> (if flag then 1 else 0) + count_convex r1 + count_convex r2
 150     | _ -> 0;;
 151
 152
 153
 154
 155
 156 (*********************)
 157
 158 let x = [2.0001; 2.0001; 2.0001; 2.0; 2.0; 2.0; 0.0; 0.0] and
 159     z = [2.52; 2.52; 2.52; 2.0; 2.0; 2.0; 0.0; 0.0];;
 160
 161 let taum_test1 = run_test taum_taylor x z true 0.0 true true true;;
 162 (* 79 *)
 163 result_size taum_test1;;
 164
 165 let taum_test1_0 = run_test0 taum_taylor x z true 0.0 true true true;;
 166 (* 57281 *)
 167 result_size taum_test1_0;;
 168
 169
 170 count_f0_flags taum_test1;;
 171 length (all_mono taum_test1);;
 172 count_pass_mono taum_test1;;
 173 count_convex taum_test1;;
 174
 175
 176
 177
 178 (***)
 179 let x = [2.0; 2.0; 2.0; 2.0; 2.0; 2.52; 0.0; 0.0] and
 180     z = [2.52; 2.52; 2.52; 2.0; 2.0; 2.52; 0.0; 0.0];;
 181
 182 (CONV_RULE (NUM_REDUCE_CONV THENC REAL_RAT_REDUCE_CONV) o SPECL[`2`; `1`]) Sphere.tame_table_d;;
 183
 184 let taum_test2 = run_test taum_taylor x z true 0.103 false;;
 185 result_size taum_test2;;
 186
 187 (***)
 188 let x = [2.0; 2.0; 2.0; 2.1771; 2.0; 2.0; 0.0; 0.0] and
 189     z = [2.52; 2.52; 2.52; 2.52; 2.52; 2.52; 0.0; 0.0];;
 190
 191 let taum_test3 = run_test taum_taylor x z true 0.04 false;;
 192 result_size taum_test3;;
 193
 194
 195
 196
 197 (***)
 198 let x, z =
 199   replicate 2.0 6 @ [0.;0.],
 200   replicate 2.52 6 @ [0.;0.];;
 201 let ineq = Plus (taum_taylor, Scale (dih_y_taylor, mk_interval (0.626, 0.626)));;
 202 let taum_test4 = run_test ineq x z true 0.77 true true true;;
 203 (* 52540 (48014) *)
 204 result_size taum_test4;;
 205
 206 count_f0_flags taum_test4;;
 207 length (all_mono taum_test4);;
 208 count_pass_mono taum_test4;;
 209 count_convex taum_test4;;
 210
 211
 212 let ineq = Plus (taum_taylor, Scale (dih_y_taylor, mk_interval (-0.259, -0.259)));;
 213 let taum_test5 = run_test ineq x z true (-0.32) false;;
 214 (* 37737 *)
 215 result_size taum_test5;;
 216
 217
 218
 219
 220 let x, z =
 221   replicate 2.0 6 @ [0.;0.],
 222   replicate 2.52 6 @ [0.;0.];;
 223
 224 let ineq1_test = run_test dih_y_taylor x z true 0.852 true true true;;
 225 (* 10298 (10142) *)
 226 result_size ineq1_test;;
 227
 228 let ineq1_test0 = run_test0 dih_y_taylor x z true 0.852 true true true;;
 229 (* 604796 (true false true) 308962 (true true true) *)
 230 result_size ineq1_test0;;
 231
 232
 233
 234 count_f0_flags ineq1_test;;
 235 all_mono ineq1_test;;
 236 count_pass_mono ineq1_test;;
 237 count_convex ineq1_test;;
 238
 239 let pp = 10;;
 240 let n = 6;;
 241 let xx = `[&2;&2;&2;&2;&2;&2]` and
 242     zz = `[#2.52;#2.52;#2.52;#2.52;#2.52;#2.52]`;;
 243 let xx1 = convert_to_float_list pp true xx and
 244     zz1 = convert_to_float_list pp false zz;;
 245
 246 m_verify_domain_test n pp eval_delta_x4 ineq1_test xx1 zz1;;
 247
 248 ineq1_test;;
 249
 250 let dd = (evalf dih_y_taylor x x).dd;;
 251 map (fun i -> mth (mth dd i) i) iter8;;
 252
 253
 254 let ineq2_test = run_test dih_y_taylor x z false 1.893 true true false;;
 255 (* 4905 (4886 with derivatives) *)
 256 result_size ineq2_test;;
 257
 258 let ineq2_test0 = run_test0 dih_y_taylor x z false 1.893 true true true;;
 259 (* 35842 (true false true) 35842 (true true true) *)
 260 result_size ineq2_test0;;
 261
 262 let all_p = all_pass ineq2_test;;
 263 let xx, zz = List.nth all_p 134;;
 264 let dd = (evalf dih_y_taylor xx zz).dd;;
 265 map (fun i -> mth (mth dd i) i) iter8;;
 266
 267
 268
 269 count_f0_flags ineq2_test;;
 270 all_mono ineq2_test;;
 271 count_pass_mono ineq2_test;;
 272 count_convex ineq2_test;;
 273
 274 count_f0_flags ineq2_test0;;
 275 length (all_mono ineq2_test0);;
 276 count_pass_mono ineq2_test0;;
 277 count_convex ineq2_test0;;
 278
 279
 280
 281 let rec pass_intervals r =
 282   match r with
 283     | Result_false _ -> failwith "False result"
 284     | Result_glue (_,r1,r2) -> pass_intervals r1 @ pass_intervals r2
 285     | Result_pass (x,z) -> [x,z];;
 286
 287
 288 let intersect_results r1 r2 =
 289   let i1 = pass_intervals r1 and
 290       i2 = pass_intervals r2 in
 291   let i = intersect i1 i2 in
 292     length i, i;;
 293
 294 (* 1683 *)
 295 let n1, i1 = intersect_results ineq1_test ineq2_test;;
 296 (* 583 *)
 297 let n2, i2 = intersect_results ineq1_test taum_test4;;
 298 (* 5 *)
 299 let n3, i3 = intersect_results ineq2_test taum_test4;;
 300
 301 (* 14486 *)
 302 let n4, i4 = intersect_results taum_test4 taum_test5;;
 303 maxl (map (maxl o filter (fun x -> x <> 0.) o snd o center_form) (pass_intervals taum_test4));;
 304
 305 let x = 2;;
 306
 307
 308 (*****************************)
 309
 310
 311 (*
 312 Sphere.dih_x;;
 313 Ineq.I_5735387903;;
 314 Ineq.dart_std3;;
 315
 316 Ineq.getexact "5735387903";;
 317 Ineq.getexact "5490182221";;
 318 Ineq.getexact "2570626711";;
 319 Ineq.getexact "3296257235";;
 320
 321 Ineq.getexact "8519146937";;
 322 Ineq.getexact "4667071578";;
 323 Ineq.getexact "1395142356";;
 324 Ineq.getexact "7394240696";;
 325 Ineq.getexact "7726998381";;
 326 Ineq.getexact "4047599236";;
 327
 328 Ineq.getexact "8248508703";;
 329 Ineq.getexact "7931207804";;
 330
 331 Ineq.getexact "4491491732";;
 332 *)
 333
 334
 335
 336 (**********************************)
 337
 338