Average Error: 4.3 → 3.4
Time: 59.7s
Precision: 64
\[\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x\]
↓
\[\frac{x \cdot \left(\left(0.1049934947 + \left(0.0424060604 + \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971 + 0.0005064034\right) + 0.0072644182\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right) + 1\right)}{1 + \left(x \cdot x\right) \cdot \left(0.7715471019 + \left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(0.0140005442 + \left(\left(\left(x \cdot x\right) \cdot 0.0001789971\right) \cdot 2 + 0.0008327945\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right) + 0.0694555761\right) + 0.2909738639\right)\right)}\]
\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x
↓
\frac{x \cdot \left(\left(0.1049934947 + \left(0.0424060604 + \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971 + 0.0005064034\right) + 0.0072644182\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right) + 1\right)}{1 + \left(x \cdot x\right) \cdot \left(0.7715471019 + \left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(0.0140005442 + \left(\left(\left(x \cdot x\right) \cdot 0.0001789971\right) \cdot 2 + 0.0008327945\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right) + 0.0694555761\right) + 0.2909738639\right)\right)}
double f(double x) {
        double r4587281 = 1.0;
        double r4587282 = /* ERROR: no posit support in C */;
        double r4587283 = 0.1049934947;
        double r4587284 = /* ERROR: no posit support in C */;
        double r4587285 = x;
        double r4587286 = r4587285 * r4587285;
        double r4587287 = r4587284 * r4587286;
        double r4587288 = r4587282 + r4587287;
        double r4587289 = 0.0424060604;
        double r4587290 = /* ERROR: no posit support in C */;
        double r4587291 = r4587286 * r4587286;
        double r4587292 = r4587290 * r4587291;
        double r4587293 = r4587288 + r4587292;
        double r4587294 = 0.0072644182;
        double r4587295 = /* ERROR: no posit support in C */;
        double r4587296 = r4587291 * r4587286;
        double r4587297 = r4587295 * r4587296;
        double r4587298 = r4587293 + r4587297;
        double r4587299 = 0.0005064034;
        double r4587300 = /* ERROR: no posit support in C */;
        double r4587301 = r4587296 * r4587286;
        double r4587302 = r4587300 * r4587301;
        double r4587303 = r4587298 + r4587302;
        double r4587304 = 0.0001789971;
        double r4587305 = /* ERROR: no posit support in C */;
        double r4587306 = r4587301 * r4587286;
        double r4587307 = r4587305 * r4587306;
        double r4587308 = r4587303 + r4587307;
        double r4587309 = 0.7715471019;
        double r4587310 = /* ERROR: no posit support in C */;
        double r4587311 = r4587310 * r4587286;
        double r4587312 = r4587282 + r4587311;
        double r4587313 = 0.2909738639;
        double r4587314 = /* ERROR: no posit support in C */;
        double r4587315 = r4587314 * r4587291;
        double r4587316 = r4587312 + r4587315;
        double r4587317 = 0.0694555761;
        double r4587318 = /* ERROR: no posit support in C */;
        double r4587319 = r4587318 * r4587296;
        double r4587320 = r4587316 + r4587319;
        double r4587321 = 0.0140005442;
        double r4587322 = /* ERROR: no posit support in C */;
        double r4587323 = r4587322 * r4587301;
        double r4587324 = r4587320 + r4587323;
        double r4587325 = 0.0008327945;
        double r4587326 = /* ERROR: no posit support in C */;
        double r4587327 = r4587326 * r4587306;
        double r4587328 = r4587324 + r4587327;
        double r4587329 = 2.0;
        double r4587330 = /* ERROR: no posit support in C */;
        double r4587331 = r4587330 * r4587305;
        double r4587332 = r4587306 * r4587286;
        double r4587333 = r4587331 * r4587332;
        double r4587334 = r4587328 + r4587333;
        double r4587335 = r4587308 / r4587334;
        double r4587336 = r4587335 * r4587285;
        return r4587336;
}
↓
double f(double x) {
        double r4587337 = x;
        double r4587338 = 0.1049934947;
        double r4587339 = 0.0424060604;
        double r4587340 = r4587337 * r4587337;
        double r4587341 = 0.0001789971;
        double r4587342 = r4587340 * r4587341;
        double r4587343 = 0.0005064034;
        double r4587344 = r4587342 + r4587343;
        double r4587345 = r4587340 * r4587344;
        double r4587346 = 0.0072644182;
        double r4587347 = r4587345 + r4587346;
        double r4587348 = r4587347 * r4587340;
        double r4587349 = r4587339 + r4587348;
        double r4587350 = r4587349 * r4587340;
        double r4587351 = r4587338 + r4587350;
        double r4587352 = r4587351 * r4587340;
        double r4587353 = 1.0;
        double r4587354 = r4587352 + r4587353;
        double r4587355 = r4587337 * r4587354;
        double r4587356 = 0.7715471019;
        double r4587357 = 0.0140005442;
        double r4587358 = 2.0;
        double r4587359 = r4587342 * r4587358;
        double r4587360 = 0.0008327945;
        double r4587361 = r4587359 + r4587360;
        double r4587362 = r4587361 * r4587340;
        double r4587363 = r4587357 + r4587362;
        double r4587364 = r4587363 * r4587340;
        double r4587365 = 0.0694555761;
        double r4587366 = r4587364 + r4587365;
        double r4587367 = r4587340 * r4587366;
        double r4587368 = 0.2909738639;
        double r4587369 = r4587367 + r4587368;
        double r4587370 = r4587340 * r4587369;
        double r4587371 = r4587356 + r4587370;
        double r4587372 = r4587340 * r4587371;
        double r4587373 = r4587353 + r4587372;
        double r4587374 = r4587355 / r4587373;
        return r4587374;
}

Error

Bits error versus x

Derivation

  1. Initial program 4.3

    \[\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x\]

  2. Simplified3.7

    \[\leadsto \color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}{\left(0.0005064034\right)}\right)\right)}{\left(\frac{\left(0.0424060604\right)}{\left(\left(0.0072644182\right) \cdot \left(x \cdot x\right)\right)}\right)}\right)\right)}{\left(1\right)}\right)}{\left(\left(x \cdot x\right) \cdot \left(0.1049934947\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(0.0001789971\right) \cdot \left(\left(2\right) \cdot \left(x \cdot x\right)\right)\right)}{\left(0.0008327945\right)}\right)\right)}{\left(0.0140005442\right)}\right)\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}{\left(0.2909738639\right)}\right)\right)}\right)}{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\right)\right)}\right)}\right)}\right) \cdot x}\]

  3. Simplified3.4

    \[\leadsto \color{blue}{\frac{\left(x \cdot \left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0072644182\right)}{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(0.0001789971\right)\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0005064034\right)\right)}\right)}\right)\right)}{\left(0.0424060604\right)}\right)\right)}\right)\right)}{\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(0.0694555761\right) \cdot \left(x \cdot x\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(0.0001789971\right) \cdot \left(\left(x \cdot x\right) \cdot \left(2\right)\right)\right)}{\left(0.0008327945\right)}\right)\right)}{\left(0.0140005442\right)}\right)\right)}\right)\right)}{\left(\frac{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}{\left(1\right)}\right)}\right)}}\]

  4. Simplified3.5

    \[\leadsto \color{blue}{\left(\frac{x}{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.7715471019\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(\frac{\left(0.0140005442\right)}{\left(\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right) \cdot \left(2\right)\right)}{\left(0.0008327945\right)}\right) \cdot \left(x \cdot x\right)\right)}\right) \cdot \left(x \cdot x\right)\right)}{\left(0.0694555761\right)}\right)\right)}{\left(0.2909738639\right)}\right)\right)}\right)\right)}\right)}\right) \cdot \left(\frac{\left(\left(\frac{\left(0.1049934947\right)}{\left(\left(\frac{\left(0.0424060604\right)}{\left(\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}{\left(0.0005064034\right)}\right)\right)}{\left(0.0072644182\right)}\right) \cdot \left(x \cdot x\right)\right)}\right) \cdot \left(x \cdot x\right)\right)}\right) \cdot \left(x \cdot x\right)\right)}{\left(1\right)}\right)}\]
  5. Using strategy rm

  6. Applied associate-*l/3.4

    \[\leadsto \color{blue}{\frac{\left(x \cdot \left(\frac{\left(\left(\frac{\left(0.1049934947\right)}{\left(\left(\frac{\left(0.0424060604\right)}{\left(\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}{\left(0.0005064034\right)}\right)\right)}{\left(0.0072644182\right)}\right) \cdot \left(x \cdot x\right)\right)}\right) \cdot \left(x \cdot x\right)\right)}\right) \cdot \left(x \cdot x\right)\right)}{\left(1\right)}\right)\right)}{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.7715471019\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(\frac{\left(0.0140005442\right)}{\left(\left(\frac{\left(\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right) \cdot \left(2\right)\right)}{\left(0.0008327945\right)}\right) \cdot \left(x \cdot x\right)\right)}\right) \cdot \left(x \cdot x\right)\right)}{\left(0.0694555761\right)}\right)\right)}{\left(0.2909738639\right)}\right)\right)}\right)\right)}\right)}}\]

  7. Final simplification3.4

    \[\leadsto \frac{x \cdot \left(\left(0.1049934947 + \left(0.0424060604 + \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 0.0001789971 + 0.0005064034\right) + 0.0072644182\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right) + 1\right)}{1 + \left(x \cdot x\right) \cdot \left(0.7715471019 + \left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(0.0140005442 + \left(\left(\left(x \cdot x\right) \cdot 0.0001789971\right) \cdot 2 + 0.0008327945\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right) + 0.0694555761\right) + 0.2909738639\right)\right)}\]

Reproduce

herbie shell --seed 2019130 +o rules:numerics
(FPCore (x)
  :name "Jmat.Real.dawson"
  (*.p16 (/.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0072644182) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.7715471019) (*.p16 x x))) (*.p16 (real->posit16 0.2909738639) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0694555761) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (*.p16 (real->posit16 2) (real->posit16 0.0001789971)) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x))))) x))