port_interval/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 "../port_interval/types.hl";;
  11 flyspeck_needs "../port_interval/report.hl";;
  12 flyspeck_needs "../port_interval/interval.hl";;
  13 flyspeck_needs "../port_interval/univariate.hl";;
  14 flyspeck_needs "../port_interval/line_interval.hl";;
  15 flyspeck_needs "../port_interval/taylor.hl";;
  16 flyspeck_needs "../port_interval/recurse.hl";;
  17
  18 module Function_data = struct
  19
  20 open Interval;;
  21 open Univariate;;
  22 open Line_interval;;
  23 open Taylor;;
  24 open Recurse;;
  25
  26
  27 (* This was found  in recurse.cc, but doesn't belong there. *)
  28
  29 let deltainf =
  30   let ( * ) =  downmul in
  31   let ( + ) = downadd  in
  32   let  ( - ) = downsub in
  33   let ( ~- ) = ( ~-. ) in
  34     fun x1 x2 x3 x4 x5 x6 ->
  35       (down();
  36          ((~- x2)*x3)*x4 +((~-  x1)*x3)*x5 +((~-  x1)*x2)*x6 +((~-  x4)*x5)*x6 +
  37    x3*(x1 + x2 + x4 + x5)*x6 +  (x3*(~- x3- x6))*x6 +
  38    x2*x5*(x1 + x3 + x4 + x6) + x2*(x5*(~- x2-x5)) +
  39         x1*x4*(x2 + x3 + x5 + x6)+ x1*(x4*(~- x1-x4)));;
  40
  41
  42 let tupl x = let n = List.nth x in (n 0,n 1,n 2,n 3,n 4,n 5);;
  43
  44 let delta_x4L =
  45   fun x ->
  46     let (x1,x2,x3,x4,x5,x6) = tupl x in
  47     let ( + ),( * ) = up(); (upadd,upmul) in
  48     let fhi,tdhi=
  49     ( (~-.  x2)*x3 +(~-.  x1)*x4 + x2*x5 + x3*x6 +(~-.  x5)*x6 +
  50                 x1*(~-. x1) + x1*(~-. x4) + x1*(x2 + x3 + x5 + x6),
  51         [ (~-. 2.0)* x1 + x2 + x3 + (~-.  2.0)* x4 + x5 + x6;
  52          x1 + (~-.  1.0) * x3 + x5;
  53          x1 + (~-.  1.0) * x2 + x6;
  54          (~-. 2.0) * x1;
  55          x1 + x2 + (~-. 1.0) * x6;
  56          x1 + x3 + (~-. 1.0)* x5;]) in
  57     let ( + ),( * ) = down(); (downadd,downmul) in
  58     let flo,tdlo =
  59          (~-. x2)*x3 +(~-.  x1)*x4 + x2*x5 + x3*x6 +(~-.  x5)*x6 +
  60                 x1*(~-. x1) + x1*(~-. x4) + x1*(x2 + x3 + x5 + x6),
  61         [ (~-. 2.0)* x1 + x2 + x3 + (~-.  2.0)* x4 + x5 + x6;
  62          x1 + (~-.  1.0) * x3 + x5;
  63          x1 + (~-.  1.0) * x2 + x6;
  64          (~-. 2.0) * x1;
  65          x1 + x2 + (~-. 1.0) * x6;
  66          x1 + x3 + (~-.  1.0)* x5;] in
  67       mk_line (mk_interval(flo,fhi),map (fun (x,y)->mk_interval(x,y)) (zip tdlo tdhi));;
  68
  69 let delta_x4DD =
  70   let m i = let r = float_of_int i in mk_interval(r,r) in
  71   let intdata = [[-2; 1; 1; -2; 1; 1]; [1; 0; -1; 0; 1; 0]; [1; -1; 0; 0; 0; 1];
  72                  [-2; 0; 0; 0; 0; 0]; [1; 1; 0; 0; 0; -1]; [1; 0; 1; 0; -1; 0]] in
  73     table2 (fun i j -> m (mth2 intdata i j));;
  74
  75 let delta_x4 = Prim_a (make_primitiveA ( delta_x4L, (fun x z -> delta_x4DD)));;
  76
  77 (* sample based on ineq.hl "JNTEFVP 1"; *)
  78
  79 let sample =
  80   let xx = [4.0;4.0;4.0;4.0;4.0;8.0] in
  81   let zz = let h02 = 6.3504 in [h02;h02;h02;h02;h02;25.4016] in
  82   let mone = mk_interval(-1.0,-1.0) in
  83   let mdelta_x4 = Scale(delta_x4,mone) in
  84   let testmaxat = 6.02525 in
  85   let ff = Plus(mdelta_x4,Scale(unit,mk_interval(testmaxat,testmaxat))) in
  86   let truemaxat = 6.02525951999999165 in
  87   let opt =  {
  88     only_check_deriv1_negative = false;
  89     is_using_dihmax =false;
  90     is_using_bigface126 =false;
  91     width_cutoff =0.05;
  92     allow_sharp =false;
  93     allow_derivatives =true;
  94     iteration_count =0;
  95     iteration_limit =0;
  96     recursion_depth =200;
  97   } in
  98     recursive_verifier(0,xx,zz,xx,zz,[ff],opt);;
  99
 100 end;;