2 needs "../formal_lp/formal_interval/m_verifier.hl";;
5 Arith_cache.reset_stat();
6 Arith_cache.reset_cache();
7 Arith_float.reset_stat();
8 Arith_float.reset_cache();;
11 let f1, f2 = Informal_interval.dest_interval int in
12 Informal_float.dest_float f1, Informal_float.dest_float f2;;
14 let dest_f = Informal_float.dest_float;;
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;;
23 dest_int ti.Informal_taylor.f,
24 map dest_int ti.Informal_taylor.df,
25 map (map dest_int) ti.Informal_taylor.ddf;;
28 needs "../formal_lp/formal_interval/m_examples_poly.hl";;
35 let tm = (rand o concl o SPEC_ALL o REWRITE_RULE[Sphere.delta_x]) Sphere.delta_y in
36 expr_to_vector_fun tm;;
42 let xx = `[&2;&2;&2;&2;&2;&2]` and
43 zz = `[#2.52;#2.52;#2.52;#2.52;#2.52;#2.52]`;;
45 let xx1 = convert_to_float_list pp0 true xx and
46 zz1 = convert_to_float_list pp0 false zz;;
47 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
48 zz2 = Informal_taylor.convert_to_float_list pp0 false zz;;
49 let xx_float = map float_of_float_tm (dest_list xx1) and
50 zz_float = map float_of_float_tm (dest_list zz1);;
52 let eval_delta_y, tf_delta_y, ti_delta_y = mk_verification_functions pp delta_y_poly true `#127.999`;;
53 let certificate = run_test tf_delta_y xx_float zz_float false 0.0 true true true true 0.0;;
54 let c1 = transform_result xx_float zz_float certificate;;
57 (* 10: 362; 165 (find_and_replace_all); 300: 75 *)
58 (* 10 (cached, float_cached): 33.778 *)
60 test 1 (m_verify_list n pp eval_delta_y c1 xx1) zz1;;
66 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_delta_y c1 xx2 zz2;;
70 test 1 (m_p_verify_list n pp eval_delta_y cp1 xx1) zz1;;
75 (************************)
76 let poly1 = `x2 + x3 + x5 + x6 - #7.99 - #0.00385 * delta_y x1 x2 x3 x4 x5 x6 -
77 #2.75 * ((x1 + x4) * #0.5 - sqrt (&8))`;;
78 let poly_ineq = (expr_to_vector_fun o rand o concl o
79 REWRITE_CONV[Sphere.delta_y; Sphere.delta_x]) poly1;;
84 let xx = `[sqrt (&8); &2; &2; sqrt (&8); &2; &2]` and
85 zz = `[&3; #2.07; #2.07; &4 * #1.26; #2.07; #2.07]`;;
87 let xx1 = convert_to_float_list pp0 true xx and
88 zz1 = convert_to_float_list pp0 false zz;;
89 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
90 zz2 = Informal_taylor.convert_to_float_list pp0 false zz;;
91 let xx_float = map float_of_float_tm (dest_list xx1) and
92 zz_float = map float_of_float_tm (dest_list zz1);;
94 let eval_ineq, tf_ineq, ti_ineq = mk_verification_functions pp poly_ineq true `&0`;;
95 let certificate = run_test tf_ineq xx_float zz_float false 0.0 true true true true 0.0;;
96 let c1 = transform_result xx_float zz_float certificate;;
101 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_ineq c1 xx2 zz2;;
106 test 1 (m_verify_list n pp eval_ineq c1 xx1) zz1;;
108 test 1 (m_verify_list n pp eval_ineq c1 xx1) zz1;;
113 test 1 (m_p_verify_list n p_split eval_ineq cp1 xx1) zz1;;
115 test 1 (m_p_verify_list n p_split eval_ineq cp1 xx1) zz1;;
120 (*******************************)
122 let get_m_cell_domain =
123 let domain_hash = Hashtbl.create 20 in
124 let mem, find, add = Hashtbl.mem domain_hash,
125 Hashtbl.find domain_hash, Hashtbl.add domain_hash in
126 fun n pp domain0 path ->
127 let rec get_rec domain_th path hash =
131 let hash' = hash^s^(string_of_int j) in
133 get_rec (find hash') ps hash'
135 if s = "l" or s = "r" then
136 let domain1_th, domain2_th = split_domain n pp j domain_th in
137 let hash1 = hash^"l"^(string_of_int j) and
138 hash2 = hash^"r"^(string_of_int j) in
139 let _ = add hash1 domain1_th; add hash2 domain2_th in
141 get_rec domain1_th ps hash'
143 get_rec domain2_th ps hash'
145 let l_flag = (s = "ml") in
146 let domain_th', _ = restrict_domain n j l_flag domain_th in
147 let _ = add hash' domain_th' in
148 get_rec domain_th' ps hash' in
149 get_rec domain0 path "";;
152 let m_p_verify_list0 n p_split fs certificate_list xx zz th_refs =
153 let domain_th0 = mk_m_center_domain n p_split xx zz in
154 let size = length certificate_list in
156 let rec rec_verify certificate_list th_list =
157 match certificate_list with
159 | (path, certificate) :: cs ->
160 let _ = k := !k + 1; report (sprintf "List: %d/%d" !k size) in
161 let domain_th = get_m_cell_domain n p_split domain_th0 path in
162 let th = m_p_verify_raw n p_split fs certificate domain_th th_list in
163 rec_verify cs (th_list @ [th]) in
164 rec_verify certificate_list th_refs;;
167 let i_get_m_cell_domain =
168 let domain_hash = Hashtbl.create 20 in
169 let mem, find, add = Hashtbl.mem domain_hash,
170 Hashtbl.find domain_hash, Hashtbl.add domain_hash in
171 fun pp domain0 path ->
172 let rec get_rec domain_th path hash =
176 let hash' = hash^s^(string_of_int j) in
178 get_rec (find hash') ps hash'
180 if s = "l" or s = "r" then
181 let domain1_th, domain2_th = Informal_verifier.split_domain pp j domain_th in
182 let hash1 = hash^"l"^(string_of_int j) and
183 hash2 = hash^"r"^(string_of_int j) in
184 let _ = add hash1 domain1_th; add hash2 domain2_th in
186 get_rec domain1_th ps hash'
188 get_rec domain2_th ps hash'
190 let l_flag = (s = "ml") in
191 let domain_th' = Informal_verifier.restrict_domain j l_flag domain_th in
192 let _ = add hash' domain_th' in
193 get_rec domain_th' ps hash' in
194 get_rec domain0 path "";;
197 let i_m_verify_list p_split p_min p_max fs certificate_list xx zz =
198 let domain0 = Informal_taylor.mk_m_center_domain p_split xx zz in
199 let size = length certificate_list in
201 let rec rec_verify certificate_list dom_list tree_list =
202 match certificate_list with
203 | [] -> rev tree_list, dom_list
204 | (path, certificate) :: cs ->
205 let _ = k := !k + 1; report (sprintf "List: %d/%d" !k size) in
206 let domain = i_get_m_cell_domain p_split domain0 path in
207 let tree = Informal_verifier.m_verify_raw p_split p_min p_max fs certificate domain dom_list in
208 rec_verify cs (dom_list @ [domain]) ((path, tree) :: tree_list) in
209 rec_verify certificate_list [] [];;
212 (***********************)
215 let l1, l2 = chop_list 26 cp1;;
216 let ths1 = m_p_verify_list0 n p_split eval_ineq l1 xx1 zz1 [];;
217 let path2, c2 = hd l2;;
218 let dom2_th = get_m_cell_domain n p_split (mk_m_center_domain n p_split xx1 zz1) path2;;
219 let dom2 = i_get_m_cell_domain p_split (Informal_taylor.mk_m_center_domain p_split xx2 zz2) path2;;
223 m_p_verify_raw n p_split eval_ineq c2 dom2_th ths1;;
226 let d1_th, d2_th = split_domain n p_split (3 + 1) dom2_th;;
227 let d1, d2 = Informal_verifier.split_domain p_split (3 + 1) dom2;;
229 let t2_th = eval_ineq.taylor 4 4 d2_th;;
230 eval_m_taylor_upper_partial n 4 4 t2_th;;
232 let t2 = ti_ineq.Informal_verifier.taylor 4 d2;;
233 dest_f (Informal_taylor.eval_m_taylor_upper_partial 4 4 t2);;
235 let f0, df0, ddf0 = dest_ti t2;;
236 let _, _, _, _, f1, df1, ddf1 = dest_m_taylor (concl t2_th);;
240 (* partial 4, upper bound: -67 * 10^-2, (true, 671, 47) *)
242 let x_tm, body_tm = dest_abs poly_ineq;;
243 let new_f = mk_abs (x_tm, mk_binop sub_op_real `&0` body_tm);;
244 let partial4 = gen_partial_poly 4 new_f;;
246 let g1 = mk_eval_function_eq pp partial4;;
247 let g0 = Informal_taylor.mk_eval_function pp (rand (concl partial4));;
249 let _, y1, _ = dest_m_cell_domain (concl d2_th);;
250 let y0 = d2.Informal_taylor.y;;
253 dest_int (g0 2 y0 y0);;
255 float_interval_pow_simple 2 4 (mk_const_interval (mk_float 29 49));;
256 let ff = Informal_float.mk_float (Int 29) 49;;
257 dest_int (Informal_interval.pow_interval 2 4 (Informal_interval.mk_interval (ff, ff)));;
259 let g_test = `\x:real^2. (-- &77 / &10000) * x$2 * x$1 pow 4`;;
261 let g1 = mk_eval_function_eq pp (REFL g_test);;
262 let g0 = Informal_taylor.mk_eval_function pp g_test;;
264 let yy = `[#2.9; &3]`;;
265 let y1' = mk_vector (convert_to_float_list pp true yy);;
266 let y0' = Informal_taylor.convert_to_float_list pp true yy;;
269 dest_int (g0 2 y0' y0');;
277 List.nth (dest_list ddf1) 5;;
286 m_p_verify_list0 n p_split eval_ineq l2 xx1 zz1 ths1;;
307 let xx = `[-- &10; -- &10; -- &10]` and
308 zz = `[&10; &10; &10]`;;
310 let xx1 = convert_to_float_list pp true xx and
311 zz1 = convert_to_float_list pp false zz;;
312 let xx2 = Informal_taylor.convert_to_float_list pp true xx and
313 zz2 = Informal_taylor.convert_to_float_list pp false zz;;
314 let xx_float = map float_of_float_tm (dest_list xx1) and
315 zz_float = map float_of_float_tm (dest_list zz1);;
317 let eval_schwefel, tf_schwefel, i_schwefel = mk_verification_functions pp schwefel_poly true schwefel_min;;
318 let c00 = run_test tf_schwefel xx_float zz_float false 0.0 true true false false 0.0;;
319 let c0 = run_test tf_schwefel xx_float zz_float false 0.0 true true false true 0.0;;
321 let c1' = run_test tf_schwefel xx_float zz_float false 0.0 true true true true 0.0;;
322 let c1 = transform_result xx_float zz_float c1';;
325 p_min = 1 and p_max = pp;;
328 let cp0 = Informal_verifier.m_verify_raw0 p_split p_min p_max i_schwefel c0 xx2 zz2;;
332 test 1 (m_verify_raw0 n pp eval_schwefel c0 xx1) zz1;;
336 test 1 (m_p_verify_raw0 n p_split eval_schwefel cp0 xx1) zz1;;
341 test 1 (m_verify_raw0 n pp eval_schwefel c00 xx1) zz1;;
343 let cp00 = Informal_verifier.m_verify_raw0 p_split p_min p_max i_schwefel c00 xx2 zz2;;
347 test 1 (m_p_verify_raw0 n p_split eval_schwefel cp00 xx1) zz1;;
351 test 1 (m_verify_list n pp eval_schwefel c1 xx1) zz1;;
353 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max i_schwefel c1 xx2 zz2;;
357 test 1 (m_p_verify_list n p_split eval_schwefel cp1 xx1) zz1;;
365 let xx = `[-- &5; -- &5; -- &5]` and
366 zz = `[&5; &5; &5]`;;
368 let xx1 = convert_to_float_list pp true xx and
369 zz1 = convert_to_float_list pp false zz;;
370 let xx2 = Informal_taylor.convert_to_float_list pp true xx and
371 zz2 = Informal_taylor.convert_to_float_list pp false zz;;
372 let xx_float = map float_of_float_tm (dest_list xx1) and
373 zz_float = map float_of_float_tm (dest_list zz1);;
375 let eval_rd, tf_rd, i_rd = mk_verification_functions pp rd_poly true rd_min;;
376 let certificate = run_test tf_rd xx_float zz_float false 0.0 true true true false 0.0;;
378 result_size certificate;;
379 m_verify_raw0 n pp eval_rd certificate xx1 zz1;;
385 Informal_verifier.m_verify_raw0 p_split p_min p_max i_rd certificate xx2 zz2;;
393 let xx = `[-- #0.5; -- #0.5; -- #0.5; -- #0.5]` and
394 zz = `[#0.5; #0.5; #0.5; #0.5]`;;
396 let xx1 = convert_to_float_list pp true xx and
397 zz1 = convert_to_float_list pp false zz;;
398 let xx2 = Informal_taylor.convert_to_float_list pp true xx and
399 zz2 = Informal_taylor.convert_to_float_list pp false zz;;
400 let xx_float = map float_of_float_tm (dest_list xx1) and
401 zz_float = map float_of_float_tm (dest_list zz1);;
403 let eval_caprasse, tf_caprasse, ti_caprasse = mk_verification_functions pp caprasse_poly true caprasse_min;;
404 let c0 = run_test tf_caprasse xx_float zz_float false 0.0 true true false true 0.0;;
405 let certificate = run_test tf_caprasse xx_float zz_float false 0.0 true true true true 0.0;;
406 let c1 = transform_result xx_float zz_float certificate;;
410 test 1 (m_verify_list n pp eval_caprasse c1 xx1) zz1;;
416 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_caprasse c1 xx2 zz2;;
420 test 1 (m_p_verify_list n p_split eval_caprasse cp1 xx1) zz1;;
428 let xx = `[-- &1; -- &1; -- &1; -- &1; -- &1; -- &1; -- &1]` and
429 zz = `[&1; &1; &1; &1; &1; &1; &1]`;;
431 let xx1 = convert_to_float_list pp true xx and
432 zz1 = convert_to_float_list pp false zz;;
433 let xx2 = Informal_taylor.convert_to_float_list pp true xx and
434 zz2 = Informal_taylor.convert_to_float_list pp false zz;;
435 let xx_float = map float_of_float_tm (dest_list xx1) and
436 zz_float = map float_of_float_tm (dest_list zz1);;
438 let eval_magnetism, tf_magnetism, ti_magnetism =
439 mk_verification_functions pp magnetism_poly true magnetism_min;;
440 let certificate = run_test tf_magnetism xx_float zz_float false 0.0 true true true true 0.0;;
441 result_stat certificate;;
443 let c1 = transform_result xx_float zz_float certificate;;
447 test 1 (m_verify_list n pp eval_magnetism c1 xx1) zz1;;
453 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_magnetism c1 xx2 zz2;;
457 test 1 (m_p_verify_list n p_split eval_magnetism cp1 xx1) zz1;;
466 let xx = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]` and
467 zz = `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;
469 let xx1 = convert_to_float_list pp0 true xx and
470 zz1 = convert_to_float_list pp0 false zz;;
471 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
472 zz2 = Informal_taylor.convert_to_float_list pp0 false zz;;
473 let xx_float = map float_of_float_tm (dest_list xx1) and
474 zz_float = map float_of_float_tm (dest_list zz1);;
476 let eval_heart, tf_heart, ti_heart = mk_verification_functions pp heart_poly true heart_min;;
477 let certificate = run_test tf_heart xx_float zz_float false 0.0 true true true true 1e-10;;
478 let c1 = transform_result xx_float zz_float certificate;;
484 let cp1 = Informal_verifier.m_verify_list p_split p_min p_max ti_heart c1 xx2 zz2;;
488 test 1 (m_verify_list n pp eval_heart c1 xx1) zz1;;
492 test 1 (m_p_verify_list n p_split eval_heart cp1 xx1) zz1;;