formal_lp/old/arith/informal/informal_m_verifier.hl

   1 (* Dependencies *)
   2 needs "../formal_lp/arith/informal/informal_m_taylor.hl";;
   3 needs "../formal_lp/formal_interval/interval_m/verifier.hl";;
   4
   5 module Informal_verifier = struct
   6
   7 open Informal_float;;
   8 open Informal_interval;;
   9 open Informal_taylor;;
  10 open Recurse;;
  11
  12
  13 type verification_funs =
  14 {
  15   (* p_lin -> p_second -> dom -> ti *)
  16   taylor : int -> int -> m_cell_domain -> m_taylor_interval;
  17   (* pp -> xx -> zz -> interval *)
  18   f : int -> ifloat list -> ifloat list -> interval;
  19   (* j -> pp -> xx -> zz -> interval *)
  20   df : int -> int -> ifloat list -> ifloat list -> interval;
  21   (* i j -> pp -> xx -> zz -> interval *)
  22   ddf : int -> int -> int -> ifloat list -> ifloat list -> interval;
  23 };;
  24
  25
  26 (* m_subset_interval *)
  27 let m_subset_interval a b c d =
  28   let prove_le l1 l2 = itlist2 (fun x y r -> le_float x y && r) l1 l2 true in
  29     prove_le a c && prove_le d b;;
  30
  31 (* m_taylor_cell_pass *)
  32 let m_taylor_cell_pass pp ti =
  33   let upper = eval_m_taylor_upper_bound pp ti in
  34     lt0_float upper;;
  35
  36 (* m_taylor_cell_pass0 *)
  37 let m_taylor_cell_pass0 int =
  38   (lt0_float o snd o dest_interval) int;;
  39
  40 (* m_cell_pass_subdomain *)
  41 let m_cell_pass_subdomain domain2 pass_domain =
  42   let a, b = pass_domain.lo, pass_domain. hi in
  43   let c, d = domain2.lo, domain2.hi in
  44     m_subset_interval a b c d;;
  45
  46 (* m_incr_pass *)
  47 let m_incr_pass pp j ti =
  48   let partial_bound = eval_m_taylor_partial_lower pp j ti in
  49     ge0_float partial_bound;;
  50
  51 (* m_decr_pass *)
  52 let m_decr_pass pp j ti =
  53   let partial_bound = eval_m_taylor_partial_upper pp j ti in
  54     le0_float partial_bound;;
  55
  56 (* m_mono_pass_gen *)
  57 let m_mono_pass_gen decr_flag bound =
  58   (if decr_flag then le0_float else ge0_float) bound;;
  59
  60 (* m_convex_pass *)
  61 let m_convex_pass int =
  62   (ge0_float o fst o dest_interval) int;;
  63
  64
  65 (* mk_verification_functions *)
  66 let mk_verification_functions pp0 f partials partials2 =
  67   let n = length partials in
  68   let taylor = eval_m_taylor pp0 f partials partials2 in
  69   let eval0 = mk_eval_function pp0 f in
  70   let eval1 = map (fun i -> mk_eval_function pp0 ((rand o concl o List.nth partials) (i - 1))) (1--n) in
  71   let eval2 = map (fun i ->
  72                      map (fun j ->
  73                             let d2 = List.nth (List.nth partials2 (i - 1)) (j - 1) in
  74                               mk_eval_function pp0 ((rand o concl) d2)) (1--i)) (1--n) in
  75     {
  76       taylor = taylor;
  77       f = eval0;
  78       df = (fun i -> List.nth eval1 (i - 1));
  79       ddf = (fun i j -> List.nth (List.nth eval2 (j - 1)) (i - 1));
  80     };;
  81
  82
  83 (* split_domain *)
  84 let split_domain pp j domain =
  85   let n = length domain.w in
  86   let t = List.nth domain.y (j - 1) in
  87   let vv = map (fun i -> if i = j then t else List.nth domain.hi (i - 1)) (1--n) in
  88   let uu = map (fun i -> if i = j then t else List.nth domain.lo (i - 1)) (1--n) in
  89     mk_m_center_domain pp domain.lo vv, mk_m_center_domain pp uu domain.hi;;
  90
  91
  92 (* restrict_domain *)
  93 let restrict_domain j left_flag domain =
  94   let replace list j v = map (fun i -> if i = j then v else List.nth list (i - 1)) (1--length list) in
  95   let t = List.nth (if left_flag then domain.lo else domain.hi) (j - 1) in
  96   let lo = if left_flag then domain.lo else replace domain.lo j t in
  97   let hi = if left_flag then replace domain.hi j t else domain.hi in
  98   let w = replace domain.w j float_0 in
  99   let y = replace domain.y j t in
 100     {lo = lo; hi = hi; w = w; y = y};;
 101
 102
 103 (*****************************)
 104 let verbatim = ref true;;
 105
 106 (* m_verify_raw *)
 107 (* Constructs a p_result_tree from the given result_tree *)
 108 let m_verify_raw p_split p_min p_max fs certificate domain0 ref_list =
 109   let r_size = result_size certificate in
 110   let k = ref 0 in
 111   let ps = p_min -- p_max in
 112
 113   (* finds an optimal precision value *)
 114   let rec find_p p_fun p_list =
 115     match p_list with
 116       | [] -> failwith "find_p: no good p found"
 117       | p :: ps ->
 118           let flag = (try p_fun p with Failure _ -> false) in
 119             if flag then
 120               let _ = if !verbatim then report (sprintf "p = %d" p) else () in p
 121             else find_p p_fun ps in
 122
 123   (* pass_test *)
 124   let pass_test domain f0_flag pp =
 125     if f0_flag then
 126       m_taylor_cell_pass0 (fs.f pp domain.lo domain.hi)
 127     else
 128       m_taylor_cell_pass pp (fs.taylor pp pp domain) in
 129
 130   (* glue_test *)
 131   let glue_test domain i convex_flag pp =
 132     if convex_flag then
 133       m_convex_pass (fs.ddf (i + 1) (i + 1) pp domain.lo domain.hi)
 134     else
 135       true in
 136
 137   (* mono_test *)
 138   let mono_test mono domain domains pp =
 139     let xx, zz = domain.lo, domain.hi in
 140     let taylor = fs.taylor pp pp domain in
 141     let gen_mono m =
 142       if m.df0_flag then
 143         if m.decr_flag then
 144           (snd o dest_interval) (fs.df m.variable pp xx zz)
 145         else
 146           (fst o dest_interval) (fs.df m.variable pp xx zz)
 147       else
 148         if m.decr_flag then
 149           eval_m_taylor_partial_upper pp m.variable taylor
 150         else
 151           eval_m_taylor_partial_lower pp m.variable taylor in
 152     let monos = map gen_mono mono in
 153       rev_itlist (fun (m, bound) pass ->
 154                     let flag = m.decr_flag in
 155                       m_mono_pass_gen flag bound && pass) (rev (zip mono monos)) true in
 156
 157   (* mk_domains *)
 158   let rec mk_domains mono dom0 acc =
 159     match mono with
 160       | [] -> rev acc
 161       | m :: ms ->
 162           let j, flag = m.variable, m.decr_flag in
 163           let dom = restrict_domain j flag dom0 in
 164             mk_domains ms dom (dom :: acc) in
 165
 166   (* rec_verify *)
 167   let rec rec_verify domain certificate =
 168     match certificate with
 169       | Result_mono (mono, r1) ->
 170           let _ =
 171             if !verbatim then
 172               let mono_strs =
 173                 map (fun m -> sprintf "%s%d (%b)" (if m.decr_flag then "-" else "")
 174                        m.variable m.df0_flag) mono in
 175                 report (sprintf "Mono: [%s]" (String.concat ";" mono_strs))
 176             else () in
 177           let domains = mk_domains mono domain [] in
 178           let tree1 = rec_verify (last domains) r1 in
 179             (try
 180                let pp = find_p (mono_test mono domain domains) ps in
 181                  P_result_mono ({pp = pp}, mono, tree1)
 182              with Failure _ -> failwith "mono: failed")
 183
 184       | Result_pass (f0_flag, _, _) ->
 185           let _ = k := !k + 1 in
 186           let _ =
 187             if !verbatim then
 188               report (sprintf "Verifying: %d/%d (f0_flag = %b)" !k r_size f0_flag)
 189             else () in
 190             (try
 191                let pp = find_p (pass_test domain f0_flag) ps in
 192                  P_result_pass ({pp = pp}, f0_flag)
 193              with Failure _ -> failwith "pass: failed")
 194
 195       | Result_glue (i, convex_flag, r1, r2) ->
 196           let domain1, domain2 =
 197             if convex_flag then
 198               let d1 = restrict_domain (i + 1) true domain in
 199               let d2 = restrict_domain (i + 1) false domain in
 200                 d1, d2
 201             else
 202               split_domain p_split (i + 1) domain in
 203           let tree1 = rec_verify domain1 r1 in
 204           let tree2 = rec_verify domain2 r2 in
 205             (try
 206                let pp = find_p (glue_test domain i convex_flag) ps in
 207                  P_result_glue ({pp = pp}, i, convex_flag, tree1, tree2)
 208              with Failure _ -> failwith "glue: failed")
 209
 210       | Result_pass_ref i ->
 211           let _ = if !verbatim then report (sprintf "Ref: %d" i) else () in
 212           let pass_flag =
 213             if i > 0 then
 214               let _ = List.nth ref_list (i - 1) in
 215                 true
 216             else
 217               let pass_domain = List.nth ref_list (-i - 1) in
 218                 m_cell_pass_subdomain domain pass_domain in
 219             if not pass_flag then
 220               failwith "ref: failed"
 221             else
 222               P_result_ref i
 223
 224       | _ -> failwith "False result" in
 225
 226     rec_verify domain0 certificate;;
 227
 228
 229
 230 (*****************)
 231
 232 (* m_verify_raw0 *)
 233 let m_verify_raw0 p_split p_min p_max fs certificate xx zz =
 234   m_verify_raw p_split p_min p_max fs certificate (mk_m_center_domain p_split xx zz) [];;
 235
 236
 237 (* m_verify_list *)
 238 let m_verify_list p_split p_min p_max fs certificate_list xx zz =
 239   let domain_hash = Hashtbl.create (length certificate_list * 10) in
 240   let mem, find, add = Hashtbl.mem domain_hash,
 241     Hashtbl.find domain_hash, Hashtbl.add domain_hash in
 242
 243   let get_m_cell_domain pp domain0 path =
 244     let rec get_rec domain path hash =
 245       match path with
 246         | [] -> domain
 247         | (s, j) :: ps ->
 248             let hash' = hash^s^(string_of_int j) in
 249               if mem hash' then
 250                 get_rec (find hash') ps hash'
 251               else
 252                 if s = "l" or s = "r" then
 253                   let domain1, domain2 = split_domain pp j domain in
 254                   let hash1 = hash^"l"^(string_of_int j) and
 255                       hash2 = hash^"r"^(string_of_int j) in
 256                   let _ = add hash1 domain1; add hash2 domain2 in
 257                     if s = "l" then
 258                       get_rec domain1 ps hash'
 259                     else
 260                       get_rec domain2 ps hash'
 261                 else
 262                   let l_flag = (s = "ml") in
 263                   let domain' = restrict_domain j l_flag domain in
 264                   let _ = add hash' domain' in
 265                     get_rec domain' ps hash' in
 266       get_rec domain0 path "" in
 267
 268   let domain0 = mk_m_center_domain p_split xx zz in
 269   let size = length certificate_list in
 270   let k = ref 0 in
 271   let rec rec_verify certificate_list dom_list tree_list =
 272     match certificate_list with
 273       | [] -> rev tree_list
 274       | (path, certificate) :: cs ->
 275           let _ = k := !k + 1; report (sprintf "List: %d/%d" !k size) in
 276           let domain = get_m_cell_domain p_split domain0 path in
 277           let tree = m_verify_raw p_split p_min p_max fs certificate domain dom_list in
 278             rec_verify cs (dom_list @ [domain]) ((path, tree) :: tree_list) in
 279     rec_verify certificate_list [] [];;
 280
 281 end;;
 282
 283