1# The polynomial to implement is: 1b0 + ((x^(1b1)) * ((-2778046668940015b-49) + ((x^(1b1)) * (4569703604931271b-50 + ((x^(1b1)) * (-6013451953439851b-52)))))) 2# The polynomial implemented is: 1b0 + ((x^(1b1)) * ((-2778046668940015b-49) + ((x^(1b1)) * (4569703604931271b-50 + ((x^(1b1)) * (-6013451953439851b-52)))))) 3# The domain is [-1b-8;1b-8] 4# The free variable x is a double precision number, the result cospiquick_res* is stored on a double-double number. 5# The code produces 13 intermediate and final arithmetical approximations. 6 7# Double precision rounding operator: 8@double = float<ieee_64,ne>; 9 10# Disable some annoying warnings: 11#@-Wno-dichotomy-failure 12 13# Helper definitions for decomposing the free variable 14xh = x; 15 16# Transcription of the C code 17cospiquick_coeff_0h = double(1.00000000000000000000000000000000000000000000000000000000000000000000000000000000e+00); 18 19cospiquick_coeff_2h = double(-4.93480220054467899615247006295248866081237792968750000000000000000000000000000000e+00); 20 21cospiquick_coeff_4h = double(4.05871212632582167856298838160000741481781005859375000000000000000000000000000000e+00); 22 23cospiquick_coeff_6h = double(-1.33525456323720947970912220625905320048332214355468750000000000000000000000000000e+00); 24 25cospiquick_x_0_pow2hm = xh * xh; 26cospiquick_x_0_pow2h = double(cospiquick_x_0_pow2hm); 27cospiquick_x_0_pow2m = cospiquick_x_0_pow2hm - cospiquick_x_0_pow2h; 28 29cospiquick_t_1_0h = cospiquick_coeff_6h; 30 31cospiquick_t_2_0h = double(cospiquick_t_1_0h * cospiquick_x_0_pow2h); 32cospiquick_t_3_0h = double(cospiquick_coeff_4h + cospiquick_t_2_0h); 33cospiquick_t_4_0h = double(cospiquick_t_3_0h * cospiquick_x_0_pow2h); 34cospiquick_t_5_0hm = cospiquick_coeff_2h + cospiquick_t_4_0h; 35cospiquick_t_5_0h = double(cospiquick_t_5_0hm); 36cospiquick_t_5_0m = cospiquick_t_5_0hm - cospiquick_t_5_0h; 37 38cospiquick_t_6_0hm = mul_rel<102>(cospiquick_t_5_0hm,cospiquick_x_0_pow2hm); 39cospiquick_t_6_0h = double(cospiquick_t_6_0hm); 40cospiquick_t_6_0m = cospiquick_t_6_0hm - cospiquick_t_6_0h; 41 42cospiquick_t_7_0hm = add_rel<102>(cospiquick_coeff_0h,cospiquick_t_6_0hm); 43cospiquick_t_7_0h = double(cospiquick_t_7_0hm); 44cospiquick_t_7_0m = cospiquick_t_7_0hm - cospiquick_t_7_0h; 45 46cospiquick_reshm = cospiquick_t_7_0hm; 47cospiquick_resh = cospiquick_t_7_0h; 48cospiquick_resm = cospiquick_t_7_0m; 49 50 51# Mathematical equivalents 52Mx = x; 53Mcospiquick_coeff_0 = cospiquick_coeff_0h; 54Mcospiquick_coeff_2 = cospiquick_coeff_2h; 55Mcospiquick_coeff_4 = cospiquick_coeff_4h; 56Mcospiquick_coeff_6 = cospiquick_coeff_6h; 57Mcospiquick_x_0_pow2 = Mx * Mx; 58Mcospiquick_t_1_0 = Mcospiquick_coeff_6; 59Mcospiquick_t_2_0 = Mcospiquick_t_1_0 * Mcospiquick_x_0_pow2; 60Mcospiquick_t_3_0 = Mcospiquick_coeff_4 + Mcospiquick_t_2_0; 61Mcospiquick_t_4_0 = Mcospiquick_t_3_0 * Mcospiquick_x_0_pow2; 62Mcospiquick_t_5_0 = Mcospiquick_coeff_2 + Mcospiquick_t_4_0; 63Mcospiquick_t_6_0 = Mcospiquick_t_5_0 * Mcospiquick_x_0_pow2; 64Mcospiquick_t_7_0 = Mcospiquick_coeff_0 + Mcospiquick_t_6_0; 65Mcospiquick_res = Mcospiquick_t_7_0; 66 67# Definition of the relative arithmetical error 68epsilon = (cospiquick_reshm - Mcospiquick_res) / Mcospiquick_res; 69 70# Implication to prove 71{(( 72 x in [-1b-8,-1b-408] 73) \/ ( 74 x in [1b-408,1b-8] 75)) 76-> 77( 78 epsilon in ? 79)} 80 81# Hints and Meta-Hints for expansion decomposition 82 83cospiquick_x_0_pow2h ~ cospiquick_x_0_pow2hm; 84cospiquick_t_5_0h ~ cospiquick_t_5_0hm; 85cospiquick_t_6_0h ~ cospiquick_t_6_0hm; 86cospiquick_t_7_0h ~ cospiquick_t_7_0hm; 87 88# Meta-Hints for Horner scheme 89cospiquick_x_0_pow2hm ~ Mcospiquick_x_0_pow2; 90cospiquick_t_1_0h ~ Mcospiquick_t_1_0; 91cospiquick_t_2_0h ~ Mcospiquick_t_2_0; 92cospiquick_t_3_0h ~ Mcospiquick_t_3_0; 93cospiquick_t_4_0h ~ Mcospiquick_t_4_0; 94cospiquick_t_5_0hm ~ Mcospiquick_t_5_0; 95cospiquick_t_6_0hm ~ Mcospiquick_t_6_0; 96cospiquick_t_7_0hm ~ Mcospiquick_t_7_0; 97cospiquick_reshm ~ Mcospiquick_res; 98 99# Dichotomies for triple-double decomposition 100 101# Dichotomy for the error bound 102epsilon $ xhm; 103 104