1 needs "../formal_lp/formal_interval/m_taylor_arith.hl";;
2 needs "../formal_lp/formal_interval/m_verifier.hl";;
3 needs "../formal_lp/arith/informal/informal_m_verifier.hl";;
7 Arith_cache.reset_stat();
8 Arith_cache.reset_cache();
9 Arith_float.reset_stat();
10 Arith_float.reset_cache();;
14 let f1, f2 = Informal_interval.dest_interval int in
15 Informal_float.dest_float f1, Informal_float.dest_float f2;;
17 let dest_f = Informal_float.dest_float;;
20 map dest_f dom.Informal_taylor.lo,
21 map dest_f dom.Informal_taylor.hi,
22 map dest_f dom.Informal_taylor.y,
23 map dest_f dom.Informal_taylor.w;;
26 dest_int ti.Informal_taylor.f,
27 map dest_int ti.Informal_taylor.df,
28 map (map dest_int) ti.Informal_taylor.ddf;;
32 (******************************)
36 let eval_d0 i pp t1 t2 = failwith "eval_d0";;
37 let eval_dd0 i j pp t1 t2 = failwith "eval_dd0";;
38 let eval_0 pp t1 t2 = failwith "eval_0";;
39 let eval_diff2 t1 t2 = failwith "eval_diff2";;
42 (********************************)
43 (* ArcProperties.hl inequality *)
50 let poly1 = `\x:real^2. x$1 * x$1 + x$2 * x$2 - &2 * &2`;;
51 let poly2 = `\x:real^2. &2 * x$1 * x$2`;;
52 let lm2_poly = `\x:real^2. (#2.52 - x$1 * inv(&2)) * inv(#2.52 - &1)`;;
55 mk_verification_functions p_split poly1 false `&0`;;
58 mk_verification_functions p_split poly2 false `&0`;;
60 let eval_lm2, tf_lm2, ti_lm2 =
61 mk_verification_functions p_split lm2_poly false `&0`;;
68 let r = Product (tf1, Uni_compose (uinv, tf2)) in
69 Uni_compose (uacos, r);;
72 let eval_arc p_lin p_second th =
74 eval_m_taylor_inv n p_lin p_second, eval_m_taylor_acs n p_lin p_second,
75 eval_m_taylor_mul n p_lin p_second in
76 let r1 = eval1.taylor p_lin p_second th and
77 r2 = eval2.taylor p_lin p_second th in
81 let ti_arc p_lin p_second dom =
83 Informal_taylor.eval_m_taylor_inv p_lin p_second, Informal_taylor.eval_m_taylor_acs p_lin p_second,
84 Informal_taylor.eval_m_taylor_mul p_lin p_second in
85 let r1 = ti1.Informal_verifier.taylor p_lin p_second dom and
86 r2 = ti2.Informal_verifier.taylor p_lin p_second dom in
90 (*********************)
92 let eval_ineq p_lin p_second th =
93 let arc = eval_arc p_lin p_second
99 {taylor = eval_dih_y_hi; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;
102 {Informal_verifier.taylor = ti_dih_y_hi;
103 Informal_verifier.f = eval_0;
104 Informal_verifier.df = eval_d0;
105 Informal_verifier.ddf = eval_dd0};;
111 let xx_s = `[&2; &2; &2; &2; &2; &2]` and
112 zz_s = `[#2.1; #2.1; #2.1; #2.1; #2.1; #2.1]`;;
115 let xx1_s = convert_to_float_list pp true xx_s and
116 zz1_s = convert_to_float_list pp false zz_s in
117 mk_m_center_domain n pp xx1_s zz1_s;;
120 let xx2_s = Informal_taylor.convert_to_float_list pp true xx_s and
121 zz2_s = Informal_taylor.convert_to_float_list pp false zz_s in
122 Informal_taylor.mk_m_center_domain pp xx2_s zz2_s;;
126 (* 10: 9.121 (pp = 15) *)
127 (* 300: 5.5 (pp = 8) *)
128 (* 100 (cached, float_cached, pp = 8): 2.68 *)
130 test 1 (eval_dih_y_hi pp pp) domain_th;;
132 test 1 (eval_dih_y_hi pp pp) domain_th;;
134 test 1 (ti_dih_y_hi pp pp) dom;;
137 Arith_cache.print_stat();;
138 Arith_float.print_stat();;
142 let th1 = eval_4y1_delta_y.taylor pp pp domain_th;;
143 let th2 = eval_neg_delta_y4.taylor pp pp domain_th;;
144 let pi2_th = eval_pi2_plus.taylor pp pp domain_th;;
146 let r1 = eval_m_taylor_sqrt n pp th1;;
147 let r2 = eval_m_taylor_inv n pp r1;;
148 let r3 = eval_m_taylor_mul n pp th2 r2;;
149 let r4 = eval_m_taylor_atn n pp r3;;
150 let r5 = eval_m_taylor_add n pp pi2_th r4;;
154 (* 100: 0.264 (second: 0.084) *)
155 test 1 (eval_4y1_delta_y.taylor pp pp) domain_th;;
156 (* 100: 0.032 (second: 0.020) *)
157 test 1 (eval_neg_delta_y4.taylor pp pp) domain_th;;
158 (* 100: 0.000 (second: 0.000) *)
159 test 1 (eval_pi2_plus.taylor pp pp) domain_th;;
161 (* 100: 0.444 (second: 0.280) *)
162 test 1 (eval_m_taylor_sqrt n pp) th1;;
163 (* 100: 0.496 (second: 0.284) *)
164 test 1 (eval_m_taylor_inv n pp) r1;;
165 (* 100: 0.512 (second: 0.396) *)
166 test 1 (eval_m_taylor_mul n pp th2) r2;;
167 (* 100: 0.780 (second: 0.444) *)
168 test 1 (eval_m_taylor_atn n pp) r3;;
169 (* 100: 0.264 (second: 0.256) *)
170 test 1 (eval_m_taylor_add n pp pi2_th) r4;;
175 let xx = `[&2; &2; &2; &2; &2; &2]` and
176 zz = `[#2.52; #2.52; #2.52; #2.52; #2.52; #2.52]`;;
178 let xx_s = `[&2; &2; &2; &2; &2; &2]` and
179 zz_s = `[#2.52; #2.1; #2.1; #2.1; #2.1; #2.1]`;;
181 let xx_s2 = `[&2; &2; &2; &2; &2; &2]` and
182 zz_s2 = `[#2.52; #2.2; #2.2; #2.2; #2.2; #2.2]`;;
186 let xx1 = convert_to_float_list pp0 true xx and
187 zz1 = convert_to_float_list pp0 false zz and
188 xx1_s = convert_to_float_list pp0 true xx_s and
189 zz1_s = convert_to_float_list pp0 false zz_s and
190 xx1_s2 = convert_to_float_list pp0 true xx_s2 and
191 zz1_s2 = convert_to_float_list pp0 false zz_s2;;
193 let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
194 zz2 = Informal_taylor.convert_to_float_list pp0 false zz and
195 xx2_s = Informal_taylor.convert_to_float_list pp0 true xx_s and
196 zz2_s = Informal_taylor.convert_to_float_list pp0 false zz_s and
197 xx2_s2 = Informal_taylor.convert_to_float_list pp0 true xx_s2 and
198 zz2_s2 = Informal_taylor.convert_to_float_list pp0 false zz_s2;;
201 let xx_float, zz_float, xx_s_float, zz_s_float, xx_s2_float, zz_s2_float =
202 let pad = replicate 0.0 (8 - length (dest_list xx1)) in
203 map float_of_float_tm (dest_list xx1) @ pad,
204 map float_of_float_tm (dest_list zz1) @ pad,
205 map float_of_float_tm (dest_list xx1_s) @ pad,
206 map float_of_float_tm (dest_list zz1_s) @ pad,
207 map float_of_float_tm (dest_list xx1_s2) @ pad,
208 map float_of_float_tm (dest_list zz1_s2) @ pad;;
215 let c_dih_y_s = run_test tf_dih_y_hi xx_s_float zz_s_float false 0.0 true false true false 0.0;;
216 let c_dih_y_s2 = run_test tf_dih_y_hi xx_s2_float zz_s2_float false 0.0 true false true false 0.0;;
217 let c_dih_y0 = run_test tf_dih_y_hi xx_float zz_float false 0.0 true false false false 0.0;;
220 result_stat c_dih_y_s;;
222 result_stat c_dih_y_s2;;
223 (* pass = 4294, mono = 10 *)
224 result_stat c_dih_y0;;
230 let cp_s = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y_s xx2_s zz2_s;;
231 let cp_s2 = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y_s2 xx2_s2 zz2_s2;;
234 (*********************)
238 (* 10 (pp = 15): 38.418 *)
239 (* 300 (pp = 8): 22.289 *)
240 (* 100 (cached, float_cached, pp = 8): 12.229 *)
242 let start = Sys.time() in
243 let result = m_verify_raw0 n pp eval_taylor c_dih_y_s xx1_s zz1_s in
244 let finish = Sys.time() in
246 (sprintf "Verification time: %f" (finish -. start)) in