formal_lp/old/arith/informal/tests_poly.hl

   1 (* Tests *)
   2 needs "../formal_lp/formal_interval/m_verifier.hl";;
   3
   4 let reset_all () =
   5   Arith_cache.reset_stat();
   6   Arith_cache.reset_cache();
   7   Arith_float.reset_stat();
   8   Arith_float.reset_cache();;
   9
  10 let dest_int int =
  11   let f1, f2 = Informal_interval.dest_interval int in
  12     Informal_float.dest_float f1, Informal_float.dest_float f2;;
  13
  14 let dest_f = Informal_float.dest_float;;
  15
  16 let dest_dom dom =
  17   map dest_f dom.Informal_taylor.lo,
  18   map dest_f dom.Informal_taylor.hi,
  19   map dest_f dom.Informal_taylor.y,
  20   map dest_f dom.Informal_taylor.w;;
  21
  22 let dest_ti ti =
  23   dest_int ti.Informal_taylor.f,
  24   map dest_int ti.Informal_taylor.df,
  25   map (map dest_int) ti.Informal_taylor.ddf;;
  26
  27
  28 (***)
  29 let beale = expr_to_vector_fun `(#1.5 - x1 + x1 * x2) pow 2 + (#2.25 - x1 + x1 * x2 pow 2) pow 2 + (#2.625 - x1 + x1 * x2 pow 3) pow 2` and
  30     beale_dom = `[-- &10; -- &10], [&10; &10]` and
  31     beale_min = `-- (#0.1 pow 6)`;;
  32
  33 let camelback = expr_to_vector_fun `&12 * x1 pow 2 - #6.3 * x1 pow 4 + x1 pow 6 + &3 * x1 * x2 - &12 * x2 pow 2 + &12 * x2 pow 4` and
  34     camelback_dom = `[-- &5; -- &5], [&5; &5]` and
  35     camelback_min = `-- #3.0949288079362787`;;
  36
  37 let goldstein_price = expr_to_vector_fun
  38   `(&1 + (x1 + x2 + &1) pow 2 *
  39       (&19 - &14 * x1 + &13 * x1 pow 2 - &14 * x2 + &6 * x1 * x2 + &3 * x2 pow 2)) *
  40   (&30 + (&2 * x1 - &3 * x2) pow 2 *
  41      (&18 - &32 * x1 + &12 * x1 pow 2 + &48 * x2 - &36 * x1 * x2 + &27 * x2 pow 2))` and
  42     goldstein_price_dom = `[-- &2; -- &2], [&2; &2]` and
  43     goldstein_price_min = `#2.999948501586914`;;
  44
  45 (**********************)
  46
  47 let mk_doms pp dom_tm =
  48   let xx, zz = dest_pair dom_tm in
  49   let xx1, zz1 = convert_to_float_list pp true xx, convert_to_float_list pp false zz in
  50   let xx2, zz2 =
  51     let conv = Informal_taylor.convert_to_float_list pp in
  52       conv true xx, conv false zz in
  53   let xf, zf =
  54     let conv = map float_of_float_tm o dest_list in
  55       conv xx1, conv zz1 in
  56     (xx1, zz1), (xx2, zz2), (xf, zf);;
  57
  58
  59 let p_split = 8 and
  60     p_min = 1 and
  61     p_max = 10;;
  62
  63 (****************)
  64
  65 let n = 2;;
  66 let ineq_tm, dom_tm, min_tm = beale, beale_dom, beale_min;;
  67 let (xx1, zz1), (xx2, zz2), (xx_float, zz_float) = mk_doms p_split dom_tm;;
  68
  69 let eval_ineq, tf_ineq, ti_ineq = mk_verification_functions p_split ineq_tm true min_tm;;
  70 let certificate = run_test tf_ineq xx_float zz_float false 0.0 true true true true 0.0;;
  71 (* pass = 4585 (raw = 4500); pass_min = 59 *)
  72 result_stat certificate;;
  73 let c1 = transform_result xx_float zz_float certificate;;
  74
  75 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_ineq c1 xx2 zz2;;
  76 map (result_p_stat false o snd) cp1;;
  77
  78 (* 100 (cached): 67.984 *)
  79 reset_all();;
  80 test 1 (m_p_verify_list n p_split eval_ineq cp1 xx1) zz1;;
  81
  82
  83 (****************)
  84
  85 let n = 2;;
  86 let ineq_tm, dom_tm, min_tm = camelback, camelback_dom, camelback_min;;
  87 let (xx1, zz1), (xx2, zz2), (xx_float, zz_float) = mk_doms p_split dom_tm;;
  88
  89 let eval_ineq, tf_ineq, ti_ineq = mk_verification_functions p_split ineq_tm true min_tm;;
  90 let certificate = run_test tf_ineq xx_float zz_float false 0.0 true true true true 0.0;;
  91 let c0 = run_test tf_ineq xx_float zz_float false 0.0 true true false true 0.0;;
  92 (* pass = 78 (raw = 4); pass_min = 90 *)
  93 result_stat certificate;;
  94 (* pass = 272 (raw = 68); mono = 118 *)
  95 result_stat c0;;
  96 let c1 = transform_result xx_float zz_float certificate;;
  97
  98 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_ineq c1 xx2 zz2;;
  99 let cp0 = Informal_verifier.m_verify_raw0 p_split p_min p_max ti_ineq c0 xx2 zz2;;
 100 (* 100 - 4: 34; 3: 74; 2: 234; 1: 48 *)
 101 result_p_stat false cp0;;
 102
 103 (* 100 (cached): 3.68 *)
 104 reset_all();;
 105 test 1 (m_p_verify_list n p_split eval_ineq cp1 xx1) zz1;;
 106 (* 100: 2.268 *)
 107 test 1 (m_p_verify_list n p_split eval_ineq cp1 xx1) zz1;;
 108
 109 (* 100 (cached): 6.208 *)
 110 reset_all();;
 111 test 1 (m_p_verify_raw0 n p_split eval_ineq cp0 xx1) zz1;;
 112 (* 100: 3.676 *)
 113 test 1 (m_p_verify_raw0 n p_split eval_ineq cp0 xx1) zz1;;
 114
 115 (************)
 116
 117 let n = 2;;
 118 let ineq_tm, dom_tm, min_tm = goldstein_price, goldstein_price_dom, goldstein_price_min;;
 119 let (xx1, zz1), (xx2, zz2), (xx_float, zz_float) = mk_doms p_split dom_tm;;
 120
 121 let eval_ineq, tf_ineq, ti_ineq = mk_verification_functions p_split ineq_tm true min_tm;;
 122 let certificate = run_test tf_ineq xx_float zz_float false 0.0 true true true true 0.0;;
 123 (* pass = 2153 (raw = 333); pass_min = 29 *)
 124 result_stat certificate;;
 125 let c1 = transform_result xx_float zz_float certificate;;
 126
 127 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_ineq c1 xx2 zz2;;
 128 (* map (result_p_stat false o snd) cp1;; *)
 129
 130 (* 100 (cached): 428.127 *)
 131 reset_all();;
 132 test 1 (m_p_verify_list n p_split eval_ineq cp1 xx1) zz1;;
 133
 134