needs "../formal_lp/formal_interval/m_taylor_arith.hl";; needs "../formal_lp/formal_interval/m_verifier.hl";; needs "../formal_lp/arith/informal/informal_m_verifier.hl";; let reset_all () = Arith_cache.reset_stat(); Arith_cache.reset_cache(); Arith_float.reset_stat(); Arith_float.reset_cache();; let dest_int int = let f1, f2 = Informal_interval.dest_interval int in Informal_float.dest_float f1, Informal_float.dest_float f2;; let dest_f = Informal_float.dest_float;; let dest_dom dom = map dest_f dom.Informal_taylor.lo, map dest_f dom.Informal_taylor.hi, map dest_f dom.Informal_taylor.y, map dest_f dom.Informal_taylor.w;; let dest_ti ti = dest_int ti.Informal_taylor.f, map dest_int ti.Informal_taylor.df, map (map dest_int) ti.Informal_taylor.ddf;; (******************************) (* dummy functions *) let eval_d0 i pp t1 t2 = failwith "eval_d0";; let eval_dd0 i j pp t1 t2 = failwith "eval_dd0";; let eval_0 pp t1 t2 = failwith "eval_0";; let eval_diff2 t1 t2 = failwith "eval_diff2";; (********************************) (* ArcProperties.hl inequality *) let n = 2;; let p_split = 8 and p_min = 1 and p_max = 10;; let poly1 = `\x:real^2. x$1 * x$1 + x$2 * x$2 - &2 * &2`;; let poly2 = `\x:real^2. &2 * x$1 * x$2`;; let lm2_poly = `\x:real^2. (#2.52 - x$1 * inv(&2)) * inv(#2.52 - &1)`;; let eval1, tf1, ti1 = mk_verification_functions p_split poly1 false `&0`;; let eval2, tf2, ti2 = mk_verification_functions p_split poly2 false `&0`;; let eval_lm2, tf_lm2, ti_lm2 = mk_verification_functions p_split lm2_poly false `&0`;; (* arc *) open Univariate;; let tf_arc = let r = Product (tf1, Uni_compose (uinv, tf2)) in Uni_compose (uacos, r);; let eval_arc p_lin p_second th = let inv, acs, ( * ) = eval_m_taylor_inv n p_lin p_second, eval_m_taylor_acs n p_lin p_second, eval_m_taylor_mul n p_lin p_second in let r1 = eval1.taylor p_lin p_second th and r2 = eval2.taylor p_lin p_second th in acs (r1 * inv r2);; let ti_arc p_lin p_second dom = let inv, acs, ( * ) = Informal_taylor.eval_m_taylor_inv p_lin p_second, Informal_taylor.eval_m_taylor_acs p_lin p_second, Informal_taylor.eval_m_taylor_mul p_lin p_second in let r1 = ti1.Informal_verifier.taylor p_lin p_second dom and r2 = ti2.Informal_verifier.taylor p_lin p_second dom in acs (r1 * inv r2);; (*********************) let eval_ineq p_lin p_second th = let arc = eval_arc p_lin p_second Sphere.lmfun;; let eval_taylor = {taylor = eval_dih_y_hi; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};; let ti = {Informal_verifier.taylor = ti_dih_y_hi; Informal_verifier.f = eval_0; Informal_verifier.df = eval_d0; Informal_verifier.ddf = eval_dd0};; (************) (* Small domain *) let xx_s = `[&2; &2; &2; &2; &2; &2]` and zz_s = `[#2.1; #2.1; #2.1; #2.1; #2.1; #2.1]`;; let domain_th = let xx1_s = convert_to_float_list pp true xx_s and zz1_s = convert_to_float_list pp false zz_s in mk_m_center_domain n pp xx1_s zz1_s;; let dom = let xx2_s = Informal_taylor.convert_to_float_list pp true xx_s and zz2_s = Informal_taylor.convert_to_float_list pp false zz_s in Informal_taylor.mk_m_center_domain pp xx2_s zz2_s;; (* 10: 9.121 (pp = 15) *) (* 300: 5.5 (pp = 8) *) (* 100 (cached, float_cached, pp = 8): 2.68 *) reset_all();; test 1 (eval_dih_y_hi pp pp) domain_th;; (* 100: 1.668 *) test 1 (eval_dih_y_hi pp pp) domain_th;; (* 100: 0.088 *) test 1 (ti_dih_y_hi pp pp) dom;; Arith_cache.print_stat();; Arith_float.print_stat();; (***) let th1 = eval_4y1_delta_y.taylor pp pp domain_th;; let th2 = eval_neg_delta_y4.taylor pp pp domain_th;; let pi2_th = eval_pi2_plus.taylor pp pp domain_th;; let r1 = eval_m_taylor_sqrt n pp th1;; let r2 = eval_m_taylor_inv n pp r1;; let r3 = eval_m_taylor_mul n pp th2 r2;; let r4 = eval_m_taylor_atn n pp r3;; let r5 = eval_m_taylor_add n pp pi2_th r4;; reset_all();; (* 100: 0.264 (second: 0.084) *) test 1 (eval_4y1_delta_y.taylor pp pp) domain_th;; (* 100: 0.032 (second: 0.020) *) test 1 (eval_neg_delta_y4.taylor pp pp) domain_th;; (* 100: 0.000 (second: 0.000) *) test 1 (eval_pi2_plus.taylor pp pp) domain_th;; (* 100: 0.444 (second: 0.280) *) test 1 (eval_m_taylor_sqrt n pp) th1;; (* 100: 0.496 (second: 0.284) *) test 1 (eval_m_taylor_inv n pp) r1;; (* 100: 0.512 (second: 0.396) *) test 1 (eval_m_taylor_mul n pp th2) r2;; (* 100: 0.780 (second: 0.444) *) test 1 (eval_m_taylor_atn n pp) r3;; (* 100: 0.264 (second: 0.256) *) test 1 (eval_m_taylor_add n pp pi2_th) r4;; (***) let xx = `[&2; &2; &2; &2; &2; &2]` and zz = `[#2.52; #2.52; #2.52; #2.52; #2.52; #2.52]`;; let xx_s = `[&2; &2; &2; &2; &2; &2]` and zz_s = `[#2.52; #2.1; #2.1; #2.1; #2.1; #2.1]`;; let xx_s2 = `[&2; &2; &2; &2; &2; &2]` and zz_s2 = `[#2.52; #2.2; #2.2; #2.2; #2.2; #2.2]`;; let pp0 = 3;; let xx1 = convert_to_float_list pp0 true xx and zz1 = convert_to_float_list pp0 false zz and xx1_s = convert_to_float_list pp0 true xx_s and zz1_s = convert_to_float_list pp0 false zz_s and xx1_s2 = convert_to_float_list pp0 true xx_s2 and zz1_s2 = convert_to_float_list pp0 false zz_s2;; let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and zz2 = Informal_taylor.convert_to_float_list pp0 false zz and xx2_s = Informal_taylor.convert_to_float_list pp0 true xx_s and zz2_s = Informal_taylor.convert_to_float_list pp0 false zz_s and xx2_s2 = Informal_taylor.convert_to_float_list pp0 true xx_s2 and zz2_s2 = Informal_taylor.convert_to_float_list pp0 false zz_s2;; let xx_float, zz_float, xx_s_float, zz_s_float, xx_s2_float, zz_s2_float = let pad = replicate 0.0 (8 - length (dest_list xx1)) in map float_of_float_tm (dest_list xx1) @ pad, map float_of_float_tm (dest_list zz1) @ pad, map float_of_float_tm (dest_list xx1_s) @ pad, map float_of_float_tm (dest_list zz1_s) @ pad, map float_of_float_tm (dest_list xx1_s2) @ pad, map float_of_float_tm (dest_list zz1_s2) @ pad;; (***) 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;; 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;; let c_dih_y0 = run_test tf_dih_y_hi xx_float zz_float false 0.0 true false false false 0.0;; (* pass = 4 *) result_stat c_dih_y_s;; (* pass = 63 *) result_stat c_dih_y_s2;; (* pass = 4294, mono = 10 *) result_stat c_dih_y0;; let p_split = pp and p_min = 1 and p_max = pp;; let cp_s = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y_s xx2_s zz2_s;; let cp_s2 = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y_s2 xx2_s2 zz2_s2;; (*********************) reset_all();; (* 10 (pp = 15): 38.418 *) (* 300 (pp = 8): 22.289 *) (* 100 (cached, float_cached, pp = 8): 12.229 *) let _ = let start = Sys.time() in let result = m_verify_raw0 n pp eval_taylor c_dih_y_s xx1_s zz1_s in let finish = Sys.time() in let _ = report (sprintf "Verification time: %f" (finish -. start)) in result;;