1 (* =========================================================== *)
2 (* OCaml verification and result transformation functions *)
3 (* Author: Alexey Solovyev *)
5 (* =========================================================== *)
7 needs "verifier/interval_m/recurse.ml";;
8 needs "verifier/interval_m/recurse0.ml";;
10 module Verifier = struct
20 type certificate_stats =
33 pass = 0; pass_raw = 0; pass_mono = 0;
34 mono = 0; glue = 0; glue_convex = 0;
38 (**********************************)
39 let run_test f x z min_flag min_max allow_d convex_flag mono_pass_flag raw_int_flag eps =
40 let pad = replicate 0.0 (8 - length x) in
41 let xx = x @ pad and zz = z @ pad in
42 let mone = mk_interval(-1.0,-1.0) in
43 let neg_f = Scale(f, mone) in
44 let ff = if min_flag then
45 Plus(neg_f, Scale(unit,mk_interval(min_max, min_max)))
47 Plus(f, Scale(unit, ineg (mk_interval(min_max, min_max)))) in
49 only_check_deriv1_negative = false;
50 is_using_dihmax =false;
51 is_using_bigface126 =false;
54 allow_derivatives =allow_d;
58 mono_pass = mono_pass_flag;
59 convex_flag = convex_flag;
60 raw_int_flag = raw_int_flag;
63 recursive_verifier(xx,zz,xx,zz,ff,opt);;
66 (* A verification procedure which uses raw interval arithmetic only *)
70 let run_test0 f x z min_flag min_max allow_d convex_flag mono_pass_flag eps =
71 let pad = replicate 0.0 (8 - length x) in
72 let xx = x @ pad and zz = z @ pad in
73 let mone = mk_interval(-1.0,-1.0) in
74 let neg_f = Scale(f, mone) in
75 let ff = if min_flag then
76 Plus(neg_f, Scale(unit,mk_interval(min_max, min_max)))
78 Plus(f, Scale(unit, ineg (mk_interval(min_max, min_max)))) in
80 only_check_deriv1_negative = false;
81 is_using_dihmax =false;
82 is_using_bigface126 =false;
85 allow_derivatives =allow_d;
89 mono_pass = mono_pass_flag;
90 convex_flag = convex_flag;
94 recursive_verifier0(0,xx,zz,xx,zz,ff,opt);;
98 (****************************************)
101 let s1 = map string_of_float x and
102 s2 = map string_of_float z in
103 sprintf "[%s], [%s]" (String.concat "; " s1) (String.concat "; " s2);;
106 String.concat "," (map (fun s, j -> sprintf "%s(%d)" s j) p);;
110 (* This function finds all subtrees of the given solution tree which can be
111 veified immediately (no Result_pass_mono). These subtrees are added to
112 the accumulator. Paths to the roots of all subtrees are also saved in
113 the accumulator. The third returned value is a solution tree where all
114 found subtrees are replaced with Result_pass_ref j, with j = #of the corresponding
115 subtree in the accumulator (1-based) *)
118 let get_results0 path r acc =
119 let dummy_tree = Result_false ([], []) in
120 let is_ref r = match r with Result_pass_ref _ -> true | _ -> false in
122 let rec get_rec path r acc =
124 | Result_mono (mono, r1) ->
125 let get_m m = (if m.decr_flag then "ml" else "mr"), m.variable in
126 let path' = rev_itlist (fun m l -> get_m m :: l) mono path in
127 let flag, acc', tree = get_rec path' r1 acc in
128 if flag then true, acc', dummy_tree
129 else false, acc', Result_mono (mono, tree)
130 | Result_glue (j, convex_flag, r1, r2) ->
131 let s1, s2 = if convex_flag then "ml", "mr" else "l", "r" in
132 let p1, p2 = ((s1, j + 1) :: path), ((s2, j + 1) :: path) in
133 let flag1, acc1, tree1 = get_rec p1 r1 acc in
134 let flag2, acc', tree2 = get_rec p2 r2 acc1 in
135 let n = (length acc' + 1) in
138 true, acc', dummy_tree
139 else if is_ref r1 then
140 false, acc', Result_glue (j, convex_flag, r1, tree2)
142 false, acc' @ [rev p1, r1], Result_glue (j, convex_flag, Result_pass_ref n, tree2)
146 false, acc', Result_glue (j, convex_flag, tree1, r2)
148 false, acc' @ [rev p2, r2], Result_glue (j, convex_flag, tree1, Result_pass_ref n)
150 false, acc', Result_glue (j, convex_flag, tree1, tree2)
152 | Result_pass_mono _ -> false, acc, r
153 | _ -> true, acc, dummy_tree in
160 (* transform_result *)
163 let transform_result x z r =
165 (* Subdivides the given domain (x,z) according to the given path *)
166 let domain_hash = Hashtbl.create 1000 in
167 let find_hash, mem_hash, add_hash =
168 Hashtbl.find domain_hash, Hashtbl.mem domain_hash, Hashtbl.add domain_hash in
170 let get_domain path =
172 let table f = map f (0--(n - 1)) in
173 let rec rec_domain (x, z) path hash =
177 let hash' = hash^s^(string_of_int j) in
178 if mem_hash hash' then
179 rec_domain (find_hash hash') ps hash'
183 if s = "l" or s = "r" then
184 let ( ++ ), ( / ) = up(); upadd, updiv in
185 let yj = (mth x j ++ mth z j) / 2.0 in
186 let delta b v = table (fun i -> if i = j && b then yj else mth v i) in
188 delta false x, delta true z
190 delta true x, delta false z
193 x, table (fun i -> if i = j then mth x i else mth z i)
195 table (fun i -> if i = j then mth z i else mth x i), z in
196 let _ = add_hash hash' domain' in
197 rec_domain domain' ps hash' in
198 rec_domain (x,z) path "" in
201 (* Verifies if interval [x',z'] SUBSET interval [x,z] *)
202 let sub_domain (x',z') (x,z) =
203 let le a b = itlist2 (fun a b c -> c & (a <= b)) a b true in
206 (* transform_pass_mono *)
207 (* Replaces all (Result_pass_mono m) with (Result_mono [m] (Result_ref j)) where
208 j is the reference to the corresponding domain *)
209 let transform_pass_mono x z domains r =
210 let domains_i = zip domains (1--length domains) in
212 let find_domain x' z' =
213 try find (fun d, _ -> sub_domain (x', z') d) domains_i with Failure _ -> (x,z), -1 in
215 let get_m m = (if m.decr_flag then "ml" else "mr"), m.variable in
217 let rec rec_transform path r =
219 | Result_mono (mono, r1) ->
220 let path' = rev_itlist (fun m l -> get_m m :: l) mono path in
221 Result_mono (mono, rec_transform path' r1)
222 | Result_glue (j, convex_flag, r1, r2) ->
223 let s1, s2 = if convex_flag then "ml", "mr" else "l", "r" in
224 let p1, p2 = ((s1, j + 1) :: path), ((s2, j + 1) :: path) in
225 let t1 = rec_transform p1 r1 in
226 let t2 = rec_transform p2 r2 in
227 Result_glue (j, convex_flag, t1, t2)
228 | Result_pass_mono m ->
229 let path' = rev (get_m m :: path) in
230 let x', z' = get_domain path' in
231 let _, i = find_domain x' z' in
232 (* let _ = report (sprintf "p = %s, d = %s, found: %d"
233 (domain_str x' z') (path_str path') i) in *)
234 if i >= 0 then Result_mono ([m], Result_pass_ref (-i)) else r
237 rec_transform [] r in
239 let rec transform acc r =
240 let flag, rs, r' = get_results0 [] r acc in
241 if flag then (rs @ [[], r])
243 let domains = map (fun p, _ -> get_domain p) rs in
244 let r_next = transform_pass_mono x z domains r' in
245 let _ = r_next <> r' or failwith "transform_result: deadlock" in
246 transform rs r_next in
250 (* Computes result statistics *)
252 let result_stats result =
256 pass_mono = ref 0 and
258 glue_convex = ref 0 in
262 | Result_false _ -> failwith "False result"
263 | Result_pass (flag, _, _) ->
265 if flag then pass_raw := !pass_raw + 1 else ()
266 | Result_pass_mono _ -> pass_mono := !pass_mono + 1
267 | Result_mono (_, r1) -> mono := !mono + 1; count r1
268 | Result_glue (_, flag, r1, r2) ->
270 if flag then glue_convex := !glue_convex + 1 else ();
271 count r1; count r2 in
273 let _ = count result in
274 {pass = !pass; pass_raw = !pass_raw; pass_mono = !pass_mono;
275 mono = !mono; glue = !glue; glue_convex = !glue_convex};;
278 let report_stats stats =
279 let s = sprintf "pass = %d (pass_raw = %d)\nmono = %d\nglue = %d (glue_convex = %d)\npass_mono = %d"
280 stats.pass stats.pass_raw stats.mono stats.glue stats.glue_convex stats.pass_mono in
284 let result_p_stats glue_flag p_result =
285 let p_table = Hashtbl.create 10 in
287 let c = if Hashtbl.mem p_table p then Hashtbl.find p_table p else 0 in
288 Hashtbl.replace p_table p (succ c) in
292 | P_result_ref _ -> ()
293 | P_result_pass (pp, _) -> add1 pp.pp
294 | P_result_mono (pp, _, r1) -> add1 pp.pp; count r1
295 | P_result_glue (pp, _, _, r1, r2) ->
296 if glue_flag then add1 pp.pp else ();
297 count r1; count r2 in
299 let _ = count p_result in
301 (fun p c s -> (sprintf "p = %d: %d\n" p c) ^ s) p_table "" in