1# This file is part of crlibm, the correctly rounded mathematical library,
2# which has been developed by the Arénaire project at École normale supérieure
3# de Lyon.
4#
5# Copyright (C) 2004-2011 David Defour, Catherine Daramy-Loirat,
6# Florent de Dinechin, Matthieu Gallet, Nicolas Gast, Christoph Quirin Lauter,
7# and Jean-Michel Muller
8#
9# This library is free software; you can redistribute it and/or
10# modify it under the terms of the GNU Lesser General Public
11# License as published by the Free Software Foundation; either
12# version 2.1 of the License, or (at your option) any later version.
13#
14# This library is distributed in the hope that it will be useful,
15# but WITHOUT ANY WARRANTY; without even the implied warranty of
16# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
17# Lesser General Public License for more details.
18#
19# You should have received a copy of the GNU Lesser General Public
20# License along with this library; if not, write to the Free Software
21# Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
22
23logih = <float64ne> (_logih);
24logim = <float64ne> (_logim);
25logil = <float64ne> (_logil);
26
27Logihml = logih + logim + logil; #MAPLE
28
29
30accPolyC14 = <float64ne> (_accPolyC14);
31accPolyC13 = <float64ne> (_accPolyC13);
32accPolyC12 = <float64ne> (_accPolyC12);
33accPolyC11 = <float64ne> (_accPolyC11);
34accPolyC10 = <float64ne> (_accPolyC10);
35
36accPolyC9h = <float64ne> (_accPolyC9h);
37accPolyC9l = <float64ne> (_accPolyC9l);
38AccPolyC9hl = accPolyC9h + accPolyC9l; #MAPLE
39accPolyC8h = <float64ne> (_accPolyC8h);
40accPolyC8l = <float64ne> (_accPolyC8l);
41AccPolyC8hl = accPolyC8h + accPolyC8l; #MAPLE
42accPolyC7h = <float64ne> (_accPolyC7h);
43accPolyC7l = <float64ne> (_accPolyC7l);
44AccPolyC7hl = accPolyC7h + accPolyC7l; #MAPLE
45accPolyC6h = <float64ne> (_accPolyC6h);
46accPolyC6l = <float64ne> (_accPolyC6l);
47AccPolyC6hl = accPolyC6h + accPolyC6l; #MAPLE
48accPolyC5h = <float64ne> (_accPolyC5h);
49accPolyC5l = <float64ne> (_accPolyC5l);
50AccPolyC5hl = accPolyC5h + accPolyC5l; #MAPLE
51accPolyC4h = <float64ne> (_accPolyC4h);
52accPolyC4l = <float64ne> (_accPolyC4l);
53AccPolyC4hl = accPolyC4h + accPolyC4l; #MAPLE
54accPolyC3h = <float64ne> (_accPolyC3h);
55accPolyC3l = <float64ne> (_accPolyC3l);
56AccPolyC3hl = accPolyC3h + accPolyC3l; #MAPLE
57
58E = 0; #MAPLE
59
60zh = <float64ne> (Z);
61zl = Z - zh; #MAPLE
62
63highPoly <float64ne> = accPolyC10 + zh * (accPolyC11 + zh * (accPolyC12 + zh * (accPolyC13 + zh * accPolyC14)));
64
65T1hl = zh * highPoly; #MAPLE
66
67T2 = AccPolyC9hl + T1hl; #MAPLE
68T3 = Z * T2hl; #MAPLE
69T4 = AccPolyC8hl + T3hl; #MAPLE
70T5 = Z * T4hl; #MAPLE
71T6 = AccPolyC7hl + T5hl; #MAPLE
72T7 = Z * T6hl; #MAPLE
73T8 = AccPolyC6hl + T7hl; #MAPLE
74T9 = Z * T8hl; #MAPLE
75T10 = AccPolyC5hl + T9hl; #MAPLE
76T11 = Z * T10hl; #MAPLE
77T12 = AccPolyC4hl + T11hl; #MAPLE
78T13 = Z * T12hl; #MAPLE
79T14 = AccPolyC3hl + T13hl; #MAPLE
80
81
82ZSquare = Z * Z; #MAPLE
83ZCube = Z * ZSquarehml; #MAPLE
84HigherPolyMultZ = T14hl * ZCubehml; #MAPLE
85ZSquareHalfhml = -0.5 * ZSquarehml; #MAPLE
86PolyWithSquare = ZSquareHalfhml + HigherPolyMultZhml; #MAPLE
87Poly = Z + PolyWithSquarehml; #MAPLE
88Logy = Logihml + Polyhml; #MAPLE
89
90#We can simplify the proof in this case since we know that adding a triple double which is
91#equal to 0 exactly is exact.
92
93Loghml = Logyhml; #MAPLE
94
95
96#Mathematical definition of the logarithm
97
98MHighPoly = accPolyC10 + Z * (accPolyC11 + Z * (accPolyC12 + Z * (accPolyC13 + Z * accPolyC14))); #MAPLE
99MT1 = Z * MHighPoly; #MAPLE
100MT2 = AccPolyC9hl + MT1; #MAPLE
101MT3 = Z * MT2; #MAPLE
102MT4 = AccPolyC8hl + MT3; #MAPLE
103MT5 = Z * MT4; #MAPLE
104MT6 = AccPolyC7hl + MT5; #MAPLE
105MT7 = Z * MT6; #MAPLE
106MT8 = AccPolyC6hl + MT7; #MAPLE
107MT9 = Z * MT8; #MAPLE
108MT10 = AccPolyC5hl + MT9; #MAPLE
109MT11 = Z * MT10; #MAPLE
110MT12 = AccPolyC4hl + MT11; #MAPLE
111MT13 = Z * MT12; #MAPLE
112MT14 = AccPolyC3hl + MT13; #MAPLE
113MZSquare = Z * Z; #MAPLE
114MZCube = Z * MZSquare; #MAPLE
115MHigherPolyMultZ = MT14 * MZCube; #MAPLE
116MZSquareHalf = -0.5 * MZSquare; #MAPLE
117MPolyWithSquare = MZSquareHalf + MHigherPolyMultZ; #MAPLE
118MPoly = Z + MPolyWithSquare; #MAPLE
119MLogy = MLogi + MLog1pZ; #MAPLE
120
121#We apply the same simplification here
122
123MLog = MLogy; #MAPLE
124
125
126#Useful additional definitions
127
128delta1 = highPoly - MHighPoly; #MAPLE
129delta2 = T1hl - MT1; #MAPLE
130delta3 = T2hl - MT2; #MAPLE
131delta4 = T3hl - MT3; #MAPLE
132delta5 = T4hl - MT4; #MAPLE
133delta6 = T5hl - MT5; #MAPLE
134delta7 = T6hl - MT6; #MAPLE
135delta8 = T7hl - MT7; #MAPLE
136delta9 = T8hl - MT8; #MAPLE
137delta10 = T9hl - MT9; #MAPLE
138delta11 = T10hl - MT10; #MAPLE
139delta12 = T11hl - MT11; #MAPLE
140delta13 = T12hl - MT12; #MAPLE
141delta14 = T13hl - MT13; #MAPLE
142delta15 = T14hl - MT14; #MAPLE
143delta16 = ZSquarehml - MZSquare; #MAPLE
144delta17 = ZCubehml - MZCube; #MAPLE
145delta18 = HigherPolyMultZhml - MHigherPolyMultZ; #MAPLE
146delta19 = ZSquareHalfhml - MZSquareHalf; #MAPLE
147delta20 = PolyWithSquarehml - MPolyWithSquare; #MAPLE
148delta21 = Polyhml - MPoly; #MAPLE
149delta22 = Logyhml - MLogy; #MAPLE
150delta24 = Loghml - MLog; #MAPLE
151delta25 = Logihml - MLogi; #MAPLE
152delta26 = Polyhml - MLog1pZ; #MAPLE
153
154
155#End additional definitions
156
157{
158(T2hl - T2) / T2 in [-1b-103,1b-103]
159/\ (T3hl - T3) / T3 in [-1b-102,1b-102]
160/\ (T4hl - T4) / T4 in [-1b-103,1b-103]
161/\ (T5hl - T5) / T5 in [-1b-102,1b-102]
162/\ (T6hl - T6) / T6 in [-1b-103,1b-103]
163/\ (T7hl - T7) / T7 in [-1b-102,1b-102]
164/\ (T8hl - T8) / T8 in [-1b-103,1b-103]
165/\ (T9hl - T9) / T9 in [-1b-102,1b-102]
166/\ (T10hl - T10) / T10 in [-1b-103,1b-103]
167/\ (T11hl - T11) / T11 in [-1b-102,1b-102]
168/\ (T12hl - T12) / T12 in [-1b-103,1b-103]
169/\ (T13hl - T13) / T13 in [-1b-102,1b-102]
170/\ (T14hl - T14) / T14 in [-1b-103,1b-103]
171/\ (ZSquarehml - ZSquare) / ZSquare in [-1b-149,1b-149]
172/\ (ZCubehml - ZCube) / ZCube in [-1b-144,1b-144]
173/\ (HigherPolyMultZhml - HigherPolyMultZ) / HigherPolyMultZ in [-1b-141,1b-141]
174/\ (PolyWithSquarehml - PolyWithSquare) / PolyWithSquare in [-1b-137,1b-137]
175/\ (Polyhml - Poly) / Poly in [-1b-134,1b-134]
176/\ (Logyhml - Logy) / Logy in [-1b-128,1b-128]
177/\ (Logihml - MLogi) / MLogi in [-1b-159,1b-159]
178/\ (MPoly - MLog1pZ) / MLog1pZ in [-_epsilonApproxAccurate,_epsilonApproxAccurate]
179/\ Z in [_zmin,_zmax]
180/\ ((logh + logm + logl) - Loghml) / Loghml in [-1b-159,1b-159]
181->
182((logh + logm + logl) - MLog) / MLog in [-5735b-132,5735b-132]
183}
184
185MLog1pZ -> MPoly * (1 / (((MPoly - MLog1pZ) / MLog1pZ) + 1));
186MLog2 -> Log2hml * (1 / (((Log2hml - MLog2) / MLog2) + 1));
187MLogi -> Logihml * (1 / (((Logihml - MLogi) / MLogi) + 1));
188
189T2hl -> (T2 * ((T2hl - T2) / T2)) + T2;
190T3hl -> (T3 * ((T3hl - T3) / T3)) + T3;
191T4hl -> (T4 * ((T4hl - T4) / T4)) + T4;
192T5hl -> (T5 * ((T5hl - T5) / T5)) + T5;
193T6hl -> (T6 * ((T6hl - T6) / T6)) + T6;
194T7hl -> (T7 * ((T7hl - T7) / T7)) + T7;
195T8hl -> (T8 * ((T8hl - T8) / T8)) + T8;
196T9hl -> (T9 * ((T9hl - T9) / T9)) + T9;
197T10hl -> (T10 * ((T10hl - T10) / T10)) + T10;
198T11hl -> (T11 * ((T11hl - T11) / T11)) + T11;
199T12hl -> (T12 * ((T12hl - T12) / T12)) + T12;
200T13hl -> (T13 * ((T13hl - T13) / T13)) + T13;
201T14hl -> (T14 * ((T14hl - T14) / T14)) + T14;
202
203ZSquarehml -> (ZSquare * ((ZSquarehml - ZSquare) / ZSquare)) + ZSquare;
204ZCubehml -> (ZCube * ((ZCubehml - ZCube) / ZCube)) + ZCube;
205HigherPolyMultZhml -> (HigherPolyMultZ * ((HigherPolyMultZhml - HigherPolyMultZ) / HigherPolyMultZ)) + HigherPolyMultZ;
206PolyWithSquarehml -> (PolyWithSquare * ((PolyWithSquarehml - PolyWithSquare) / PolyWithSquare)) + PolyWithSquare;
207Polyhml -> (Poly * ((Polyhml - Poly) / Poly)) + Poly;
208Logyhml -> (Logy * ((Logyhml - Logy) / Logy)) + Logy;
209
210
211delta3 -> delta2 + (T2 * ((T2hl - T2) / T2));
212delta4 -> Z * delta3 + T3 * ((T3hl - T3) / T3);
213delta5 -> delta4 + (T4 * ((T4hl - T4) / T4));
214delta6 -> Z * delta5 + T5 * ((T5hl - T5) / T5);
215delta7 -> delta6 + (T6 * ((T6hl - T6) / T6));
216delta8 -> Z * delta7 + T7 * ((T7hl - T7) / T7);
217delta9 -> delta8 + (T8 * ((T8hl - T8) / T8));
218delta10 -> Z * delta9 + T9 * ((T9hl - T9) / T9);
219delta11 -> delta10 + (T10 * ((T10hl - T10) / T10));
220delta12 -> Z * delta11 + T11 * ((T11hl - T11) / T11);
221delta13 -> delta12 + (T12 * ((T12hl - T12) / T12));
222delta14 -> Z * delta13 + T13 * ((T13hl - T13) / T13);
223delta15 -> delta14 + (T14 * ((T14hl - T14) / T14));
224delta16 -> Z*Z*((ZSquarehml - ZSquare) / ZSquare);
225delta17 -> Z * delta16 + ZCube * ((ZCubehml - ZCube) / ZCube);
226delta18 -> delta15 * delta17 + delta15 * MZCube + delta17 * MT14 +
227		HigherPolyMultZ * ((HigherPolyMultZhml - HigherPolyMultZ) / HigherPolyMultZ);
228delta20 -> delta19 + delta18 + PolyWithSquare * ((PolyWithSquarehml - PolyWithSquare) / PolyWithSquare);
229delta21 -> delta20 + Poly * ((Polyhml - Poly) / Poly);
230delta22 -> delta25 + delta26 + Logy * ((Logyhml - Logy) / Logy);
231delta26 -> delta21 + MLog1pZ * ((MPoly - MLog1pZ) / MLog1pZ);
232
233
234((logh + logm + logl) - MLog) / MLog -> ((Loghml - MLog) / MLog) + ((((logh + logm + logl) - Loghml) / Loghml) * (((Loghml - MLog) / MLog) + 1));
235