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