2 needs "../formal_lp/arith/informal/informal_m_taylor.hl";;
3 needs "../formal_lp/formal_interval/interval_m/verifier.hl";;
5 module Informal_verifier = struct
8 open Informal_interval;;
13 type verification_funs =
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;
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;;
31 (* m_taylor_cell_pass *)
32 let m_taylor_cell_pass pp ti =
33 let upper = eval_m_taylor_upper_bound pp ti in
36 (* m_taylor_cell_pass0 *)
37 let m_taylor_cell_pass0 int =
38 (lt0_float o snd o dest_interval) int;;
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;;
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;;
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;;
57 let m_mono_pass_gen decr_flag bound =
58 (if decr_flag then le0_float else ge0_float) bound;;
61 let m_convex_pass int =
62 (ge0_float o fst o dest_interval) int;;
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 ->
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
78 df = (fun i -> List.nth eval1 (i - 1));
79 ddf = (fun i j -> List.nth (List.nth eval2 (j - 1)) (i - 1));
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;;
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};;
103 (*****************************)
104 let verbatim = ref true;;
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
111 let ps = p_min -- p_max in
113 (* finds an optimal precision value *)
114 let rec find_p p_fun p_list =
116 | [] -> failwith "find_p: no good p found"
118 let flag = (try p_fun p with Failure _ -> false) in
120 let _ = if !verbatim then report (sprintf "p = %d" p) else () in p
121 else find_p p_fun ps in
124 let pass_test domain f0_flag pp =
126 m_taylor_cell_pass0 (fs.f pp domain.lo domain.hi)
128 m_taylor_cell_pass pp (fs.taylor pp pp domain) in
131 let glue_test domain i convex_flag pp =
133 m_convex_pass (fs.ddf (i + 1) (i + 1) pp domain.lo domain.hi)
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
144 (snd o dest_interval) (fs.df m.variable pp xx zz)
146 (fst o dest_interval) (fs.df m.variable pp xx zz)
149 eval_m_taylor_partial_upper pp m.variable taylor
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
158 let rec mk_domains mono dom0 acc =
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
167 let rec rec_verify domain certificate =
168 match certificate with
169 | Result_mono (mono, r1) ->
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))
177 let domains = mk_domains mono domain [] in
178 let tree1 = rec_verify (last domains) r1 in
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")
184 | Result_pass (f0_flag, _, _) ->
185 let _ = k := !k + 1 in
188 report (sprintf "Verifying: %d/%d (f0_flag = %b)" !k r_size f0_flag)
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")
195 | Result_glue (i, convex_flag, r1, r2) ->
196 let domain1, domain2 =
198 let d1 = restrict_domain (i + 1) true domain in
199 let d2 = restrict_domain (i + 1) false domain in
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
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")
210 | Result_pass_ref i ->
211 let _ = if !verbatim then report (sprintf "Ref: %d" i) else () in
214 let _ = List.nth ref_list (i - 1) in
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"
224 | _ -> failwith "False result" in
226 rec_verify domain0 certificate;;
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) [];;
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
243 let get_m_cell_domain pp domain0 path =
244 let rec get_rec domain path hash =
248 let hash' = hash^s^(string_of_int j) in
250 get_rec (find hash') ps hash'
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
258 get_rec domain1 ps hash'
260 get_rec domain2 ps hash'
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
268 let domain0 = mk_m_center_domain p_split xx zz in
269 let size = length certificate_list 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 [] [];;