Skip to content

Commit 4949097

Browse files
author
fdedinec
committed
cleaning up
1 parent 9eab51a commit 4949097

File tree

3 files changed

+38
-51
lines changed

3 files changed

+38
-51
lines changed

‎log-de.c

+2-2
Original file line numberDiff line numberDiff line change
@@ -89,10 +89,10 @@ double log_rn(double x) {
8989
#if defined(CRLIBM_TYPECPU_X86) || defined(CRLIBM_TYPECPU_AMD64)
9090
db_number xdb;
9191
int E, index, index0, roundtestmask;
92-
#else
92+
#else /* assuming Itanium here */
9393
int64_t E, i;
9494
uint64_t index, roundtestmask;
95-
double_ext c1,c2,c3,c4,c5,c6,c7;
95+
double c2,c3,c4,c5,c6,c7;
9696
#endif
9797

9898

‎log-de.h

+12-27
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
11
/*File generated by maple/log-de.mpl*/
22

3-
#if 1
3+
#define L 7
4+
#define MAXINDEX 53
5+
#define INDEXMASK 127
6+
static const double two64 = 1.84467440737095516160000000000000000000000000000000e+19 ;
7+
#if 0
48
#define ESTRIN
59
#else
610
#define PATERSON
@@ -24,29 +28,14 @@ static const long double ps_c = 3.9996232349493188306809206278291668468227726407
2428
#define c4 c[3]
2529
#define c3 c[4]
2630
#define c2 c[5]
27-
#define c1 c[6]
28-
#if 1
2931
static const double c[7] = {
30-
/* c7 = */ 0.142860563385550420889558154158294200897216796875000000,
31-
/* c6 = */ -0.166669572609547372854521540830319281667470932006835937500000,
32-
/* c5 = */ 0.19999999996748479835773082413652446120977401733398437500000,
33-
/* c4 = */ -0.249999999984237081251947643067978788167238235473632812500000,
34-
/* c3 = */ 0.33333333333333342585191871876304503530263900756835937500000,
35-
/* c2 = */ -0.5,
36-
/* c1 = */ 1.0,
37-
};
38-
#else
39-
static const long double c[7] = {
40-
/* c7 = */ 1.42860987471441585385531838903183654565509641543031e-01L,
41-
/* c6 = */ -1.66670030707931824157878170078461721459461841732264e-01L,
42-
/* c5 = */ 1.99999999957299715572971512966837792646401794627309e-01L,
43-
/* c4 = */ -2.49999999974133361728043621619033132219556136988103e-01L,
44-
/* c3 = */ 3.33333333333333491175099611014687184251670259982347e-01L,
45-
/* c2 = */ -5.00000000000000049710669608460378299241710919886827e-01L,
46-
/* c1 = */ 1.00000000000000000000000000000000000000000000000000e+00L,
32+
/* c7 = */ 1.42860563385550420889558154158294200897216796875000e-01L,
33+
/* c6 = */ -1.66669572609547372854521540830319281667470932006836e-01L,
34+
/* c5 = */ 1.99999999967484798357730824136524461209774017333984e-01L,
35+
/* c4 = */ -2.49999999984237081251947643067978788167238235473633e-01L,
36+
/* c3 = */ 3.33333333333333425851918718763045035302639007568359e-01L,
37+
/* c2 = */ -5.00000000000000000000000000000000000000000000000000e-01L,
4738
};
48-
49-
#endif
5039

5140
#endif/* ESTRIN */
5241

@@ -76,20 +65,16 @@ static const long double c[7] = {
7665
#else /* not(defined(CRLIBM_TYPECPU_X86) || defined(CRLIBM_TYPECPU_AMD64)),
7766
assuming Itanium, otherwise we shouldn't be there */
7867

79-
#define PREFETCH_POLY_QUICK c7=c[0]; c6=c[1]; c5=c[2]; c4=c[3]; c3=c[4]; c2=c[5]; c1=c[6];
68+
#define PREFETCH_POLY_QUICK c7=c[0]; c6=c[1]; c5=c[2]; c4=c[3]; c3=c[4]; c2=c[5];
8069
#define PREFETCH_POLY_ACCURATE c14h=ch[0]; c13h=ch[1]; c12h=ch[2]; \
8170
c11h=ch[3]; c10h=ch[4]; c9h=ch[5]; c8h=ch[6]; \
8271
c7h=ch[7]; c6h=ch[8]; c5h=ch[9]; c4h=ch[10]; \
8372
c3h=ch[11]; c2h=ch[12]; c1h=ch[13]; \
8473
c7l=cl[0]; c6l=cl[1]; c5l=cl[2]; c4l=cl[3]; c3l=cl[4]; c2l=cl[5]; c1l=cl[6];
8574
#endif /* defined(CRLIBM_TYPECPU_X86) || defined(CRLIBM_TYPECPU_AMD64) */
8675

87-
#define L 7
88-
#define MAXINDEX 53
89-
#define INDEXMASK 127
9076
static const long double log2H = 6.93147180559945309428690474184975300886435434222221e-01L ;
9177
static const long double log2L = -1.14583527267987328109462081210062935494878745868567e-20L ;
92-
static const long double two64 = 1.84467440737095516160000000000000000000000000000000e+19L ;
9378
static const long double ch[14] = {
9479
/* ch14 = */ -7.14324161786485507414918953716931326880512642674148e-02L,
9580
/* ch13 = */ 7.69266652810744782218957231456624157317492063157260e-02L,

‎maple/log-de.mpl

+24-22
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
# the LGPL.
44
# To use:
55
# restart; read "log-de.mpl";
6-
#TODO Gappa proof out for Paterson/Stockmayer
6+
#TODO output scripts for the Gappa proof out for Paterson/Stockmayer
77
Digits := 100:
88

99
interface(quiet=true):
@@ -79,8 +79,8 @@ else
7979
polyQuick := x * (1 + (x * ((-0.50000000000000000000000000000000000000000000000000000000000000e0) + (x * (0.33333333333333342585191871876304503530263900756835937500000000e0 + (x * ((-0.24999999998423708125194764306797878816723823547363281250000000e0) + (x * (0.19999999996748479835773082413652446120977401733398437500000000e0 + (x * ((-0.16666957260954737285452154083031928166747093200683593750000000e0) + (x * 0.14286056338555042088955815415829420089721679687500000000000000e0)))))))))))):
8080

8181
# validated infinite norms given by Christoph's tool
82-
epsilonApproxQuick := 2^(-64.119667587220):
83-
deltaApproxQuick := 2^(-72.230387592106):
82+
epsilonApproxQuick := 2^(-64.119667587221):
83+
deltaApproxQuick := 2^(-72.230387592107):
8484
fi:
8585
printf(" rel approximation error for the quick phase is 2^(%2f)\n", log2(epsilonApproxQuick) ) :
8686
printf(" abs approximation error for the quick phase is 2^(%2f)\n", log2(deltaApproxQuick) ) :
@@ -161,7 +161,13 @@ filename:="TEMPLOG/log-de.h":
161161
fd:=fopen(filename, WRITE, TEXT):
162162

163163
fprintf(fd, "/*File generated by maple/log-de.mpl*/\n\n"):
164-
fprintf(fd, "#if 0\n#define ESTRIN\n#else\n#define PATERSON\n#endif\n"):
164+
# some constants
165+
fprintf(fd, "#define L %d\n", L):
166+
fprintf(fd, "#define MAXINDEX %d\n", MAXINDEX):
167+
fprintf(fd, "#define INDEXMASK %d\n", 2^L-1):
168+
fprintf(fd, "static const double two64 = %1.25e ;\n", evalf(2^64)):
169+
170+
fprintf(fd, "#if 1\n#define ESTRIN\n#else\n#define PATERSON\n#endif\n"):
165171

166172
fprintf(fd, "#if defined(CRLIBM_TYPECPU_X86) || defined(CRLIBM_TYPECPU_AMD64)\n\n"):
167173

@@ -177,11 +183,11 @@ fprintf(fd, "#endif/* PATERSON*/\n\n"):
177183

178184
fprintf(fd, "#ifdef ESTRIN\n"):
179185
fprintf(fd, " /* Coefficients are read directly from the array thanks to the following macros */ \n"):
180-
for i from PolyDegreeQuick to 1 by -1 do
186+
for i from PolyDegreeQuick to 2 by -1 do
181187
fprintf(fd, "#define c%d c[%d]\n", i, PolyDegreeQuick-i):
182188
od:
183-
fprintf(fd, "static const long double c[%d] = {\n",PolyDegreeQuick):
184-
for i from PolyDegreeQuick to 1 by -1 do
189+
fprintf(fd, "static const double c[%d] = {\n",PolyDegreeQuick):
190+
for i from PolyDegreeQuick to 2 by -1 do
185191
fprintf(fd, " /* c%d = */ %1.50eL, \n", i, coeff(polyQuick,x,i)):
186192
od:
187193
fprintf(fd, "}; \n \n"):
@@ -199,7 +205,7 @@ fprintf(fd, "#endif/* ESTRIN */\n\n"):
199205
fprintf(fd, "#define PREFETCH_POLY_ACCURATE \n"):
200206
fprintf(fd, "\n#else /* not(defined(CRLIBM_TYPECPU_X86) || defined(CRLIBM_TYPECPU_AMD64)),\n assuming Itanium, otherwise we shouldn't be there */ \n\n"):
201207
fprintf(fd, "#define PREFETCH_POLY_QUICK "):
202-
for i from PolyDegreeQuick to 1 by -1 do
208+
for i from PolyDegreeQuick to 2 by -1 do
203209
fprintf(fd, "c%d=c[%d]; ", i, PolyDegreeQuick-i):
204210
od:
205211
fprintf(fd, "\n#define PREFETCH_POLY_ACCURATE "):
@@ -215,12 +221,8 @@ fprintf(fd, "#endif/* ESTRIN */\n\n"):
215221
fprintf(fd, "\n#endif /* defined(CRLIBM_TYPECPU_X86) || defined(CRLIBM_TYPECPU_AMD64) */ \n\n"):
216222

217223
# Various constants
218-
fprintf(fd, "#define L %d\n", L):
219-
fprintf(fd, "#define MAXINDEX %d\n", MAXINDEX):
220-
fprintf(fd, "#define INDEXMASK %d\n", 2^L-1):
221224
fprintf(fd, "static const long double log2H = %1.50eL ;\n", log2h):
222225
fprintf(fd, "static const long double log2L = %1.50eL ;\n", log2l):
223-
fprintf(fd, "static const long double two64 = %1.50eL ;\n", evalf(2^64)):
224226

225227
# The polynomials
226228
# polynomial for quick phase
@@ -303,51 +305,51 @@ for j from 0 to 2^L-1 do
303305
printf("\n************ DONE TEMPLOG/log-de*.sed ************\n");
304306

305307
# A shell script to use them
306-
filename:="../gappa/run-log-de-proof.sh":
308+
filename:="../gappa/log-de/run-log-de-proof.sh":
307309
fd:=fopen(filename, WRITE, TEXT):
308310
fprintf(fd, "#!/bin/sh\n"):
309311
fprintf(fd, "# You probably need to edit the path to the gappa executable\n"):
310-
fprintf(fd, "GAPPA=~/gappa/src/gappa\n"):
312+
fprintf(fd, "GAPPA=~/local/src/gappa/src/gappa\n"):
311313

312314
fprintf(fd, "echo Accurate phase, case E=0, index=0: 1>&2\n"):
313-
fprintf(fd, "sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_0.sed ../gappa/log-de-acc-index0-E0.gappa | $GAPPA \n"):
315+
fprintf(fd, "sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_0.sed ../gappa/log-de/log-de-acc-index0-E0.gappa | $GAPPA \n"):
314316

315317
fprintf(fd, "echo Accurate phase, case E!=0, index=0 1>&2\n"):
316-
fprintf(fd, "sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_0.sed ../gappa/log-de-acc-index0-E1N.gappa | $GAPPA \n"):
318+
fprintf(fd, "sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_0.sed ../gappa/log-de/log-de-acc-index0-E1N.gappa | $GAPPA \n"):
317319

318320
fprintf(fd, "for num in `seq 1 %d`; do\n", 2^L-1):
319321
fprintf(fd, " echo Accurate phase, case E=0, index=$num 1>&2\n"):
320-
fprintf(fd, " sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_$num.sed ../gappa/log-de-acc-index1N-E0.gappa | $GAPPA \n"):
322+
fprintf(fd, " sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_$num.sed ../gappa/log-de/log-de-acc-index1N-E0.gappa | $GAPPA \n"):
321323
fprintf(fd, " echo 1>&2\n"):
322324
fprintf(fd, "done\n"):
323325

324326
fprintf(fd, "for num in `seq 1 %d`; do\n", 2^L-1):
325327
fprintf(fd, " echo Accurate phase, case E!=0, index = $num 1>&2 \n"):
326-
fprintf(fd, " sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_$num.sed ../gappa/log-de-acc-index1N-E1N.gappa | $GAPPA \n"):
328+
fprintf(fd, " sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_$num.sed ../gappa/log-de/log-de-acc-index1N-E1N.gappa | $GAPPA \n"):
327329
fprintf(fd, " echo 1>&2\n"):
328330
fprintf(fd, "done\n\n"):
329331

330332

331333
fprintf(fd, "echo Quick phase, case E=0, index=0 1>&2\n"):
332-
fprintf(fd, "sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_0.sed ../gappa/log-de-index0-E0.gappa | $GAPPA \n"):
334+
fprintf(fd, "sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_0.sed ../gappa/log-de/log-de-index0-E0.gappa | $GAPPA \n"):
333335
fprintf(fd, " echo 1>&2\n"):
334336

335337
fprintf(fd, "echo Quick phase, case E!=0, index=0 1>&2 \n"):
336-
fprintf(fd, "sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_0.sed ../gappa/log-de-index0-E1N.gappa | $GAPPA \n"):
338+
fprintf(fd, "sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_0.sed ../gappa/log-de/log-de-index0-E1N.gappa | $GAPPA \n"):
337339
fprintf(fd, " echo 1>&2\n"):
338340

339341

340342
fprintf(fd, "for num in `seq 1 %d`; do\n", 2^L-1):
341343
fprintf(fd, " echo Quick phase, for all E, index=$num 1>&2\n"):
342-
fprintf(fd, " sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_$num.sed ../gappa/log-de-index1N-E0N.gappa | $GAPPA \n"):
344+
fprintf(fd, " sed -f ../maple/TEMPLOG/polynomials.sed -f ../maple/TEMPLOG/log-de_$num.sed ../gappa/log-de/log-de-index1N-E0N.gappa | $GAPPA \n"):
343345
fprintf(fd, " echo 1>&2\n"):
344346
fprintf(fd, "done\n"):
345347

346348
fclose(fd):
347349

348350
printf("\n************ DONE TEMPLOG/run-log-de-proof.sh ************\n"):
349351
printf("Now you should run \n"):
350-
printf(" sh ../gappa/run-log-de-proof.sh 2> ../maple/TEMPLOG/Gappa.out\n"):
352+
printf(" sh ../gappa/log-de/run-log-de-proof.sh 2> ../maple/TEMPLOG/Gappa.out\n"):
351353
printf(" (You probably need to edit the path to the gappa executable within run-log-de-proof.sh)\n"):
352354
printf("Then look at TEMPLOG/Gappa.out. It shouldn't contain 'some enclosures were not satisfied'.\n If it does, report it !\n"):
353355

0 commit comments

Comments
 (0)