Average Error: 4.3 → 3.4
Time: 59.4s
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(1 + \left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(0.0005064034 + \left(0.0001789971 \cdot x\right) \cdot x\right) \cdot \left(x \cdot x\right) + 0.0072644182\right) + 0.0424060604\right) + 0.1049934947\right)\right)}{\left(0.7715471019 + \left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot 2\right) \cdot \left(0.0001789971 \cdot \left(x \cdot x\right)\right) + \left(0.0140005442 + \left(x \cdot x\right) \cdot 0.0008327945\right)\right) + 0.0694555761\right) \cdot \left(x \cdot x\right) + 0.2909738639\right)\right) \cdot \left(x \cdot x\right) + 1}\]
\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(1 + \left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\left(0.0005064034 + \left(0.0001789971 \cdot x\right) \cdot x\right) \cdot \left(x \cdot x\right) + 0.0072644182\right) + 0.0424060604\right) + 0.1049934947\right)\right)}{\left(0.7715471019 + \left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(\left(\left(x \cdot x\right) \cdot 2\right) \cdot \left(0.0001789971 \cdot \left(x \cdot x\right)\right) + \left(0.0140005442 + \left(x \cdot x\right) \cdot 0.0008327945\right)\right) + 0.0694555761\right) \cdot \left(x \cdot x\right) + 0.2909738639\right)\right) \cdot \left(x \cdot x\right) + 1}
double f(double x) {
        double r6685432 = 1.0;
        double r6685433 = /* ERROR: no posit support in C */;
        double r6685434 = 0.1049934947;
        double r6685435 = /* ERROR: no posit support in C */;
        double r6685436 = x;
        double r6685437 = r6685436 * r6685436;
        double r6685438 = r6685435 * r6685437;
        double r6685439 = r6685433 + r6685438;
        double r6685440 = 0.0424060604;
        double r6685441 = /* ERROR: no posit support in C */;
        double r6685442 = r6685437 * r6685437;
        double r6685443 = r6685441 * r6685442;
        double r6685444 = r6685439 + r6685443;
        double r6685445 = 0.0072644182;
        double r6685446 = /* ERROR: no posit support in C */;
        double r6685447 = r6685442 * r6685437;
        double r6685448 = r6685446 * r6685447;
        double r6685449 = r6685444 + r6685448;
        double r6685450 = 0.0005064034;
        double r6685451 = /* ERROR: no posit support in C */;
        double r6685452 = r6685447 * r6685437;
        double r6685453 = r6685451 * r6685452;
        double r6685454 = r6685449 + r6685453;
        double r6685455 = 0.0001789971;
        double r6685456 = /* ERROR: no posit support in C */;
        double r6685457 = r6685452 * r6685437;
        double r6685458 = r6685456 * r6685457;
        double r6685459 = r6685454 + r6685458;
        double r6685460 = 0.7715471019;
        double r6685461 = /* ERROR: no posit support in C */;
        double r6685462 = r6685461 * r6685437;
        double r6685463 = r6685433 + r6685462;
        double r6685464 = 0.2909738639;
        double r6685465 = /* ERROR: no posit support in C */;
        double r6685466 = r6685465 * r6685442;
        double r6685467 = r6685463 + r6685466;
        double r6685468 = 0.0694555761;
        double r6685469 = /* ERROR: no posit support in C */;
        double r6685470 = r6685469 * r6685447;
        double r6685471 = r6685467 + r6685470;
        double r6685472 = 0.0140005442;
        double r6685473 = /* ERROR: no posit support in C */;
        double r6685474 = r6685473 * r6685452;
        double r6685475 = r6685471 + r6685474;
        double r6685476 = 0.0008327945;
        double r6685477 = /* ERROR: no posit support in C */;
        double r6685478 = r6685477 * r6685457;
        double r6685479 = r6685475 + r6685478;
        double r6685480 = 2.0;
        double r6685481 = /* ERROR: no posit support in C */;
        double r6685482 = r6685481 * r6685456;
        double r6685483 = r6685457 * r6685437;
        double r6685484 = r6685482 * r6685483;
        double r6685485 = r6685479 + r6685484;
        double r6685486 = r6685459 / r6685485;
        double r6685487 = r6685486 * r6685436;
        return r6685487;
}
↓
double f(double x) {
        double r6685488 = x;
        double r6685489 = 1.0;
        double r6685490 = r6685488 * r6685488;
        double r6685491 = 0.0005064034;
        double r6685492 = 0.0001789971;
        double r6685493 = r6685492 * r6685488;
        double r6685494 = r6685493 * r6685488;
        double r6685495 = r6685491 + r6685494;
        double r6685496 = r6685495 * r6685490;
        double r6685497 = 0.0072644182;
        double r6685498 = r6685496 + r6685497;
        double r6685499 = r6685490 * r6685498;
        double r6685500 = 0.0424060604;
        double r6685501 = r6685499 + r6685500;
        double r6685502 = r6685490 * r6685501;
        double r6685503 = 0.1049934947;
        double r6685504 = r6685502 + r6685503;
        double r6685505 = r6685490 * r6685504;
        double r6685506 = r6685489 + r6685505;
        double r6685507 = r6685488 * r6685506;
        double r6685508 = 0.7715471019;
        double r6685509 = 2.0;
        double r6685510 = r6685490 * r6685509;
        double r6685511 = r6685492 * r6685490;
        double r6685512 = r6685510 * r6685511;
        double r6685513 = 0.0140005442;
        double r6685514 = 0.0008327945;
        double r6685515 = r6685490 * r6685514;
        double r6685516 = r6685513 + r6685515;
        double r6685517 = r6685512 + r6685516;
        double r6685518 = r6685490 * r6685517;
        double r6685519 = 0.0694555761;
        double r6685520 = r6685518 + r6685519;
        double r6685521 = r6685520 * r6685490;
        double r6685522 = 0.2909738639;
        double r6685523 = r6685521 + r6685522;
        double r6685524 = r6685490 * r6685523;
        double r6685525 = r6685508 + r6685524;
        double r6685526 = r6685525 * r6685490;
        double r6685527 = r6685526 + r6685489;
        double r6685528 = r6685507 / r6685527;
        return r6685528;
}

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.5

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

  4. Simplified3.4

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

  6. Applied associate-*r*3.4

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

  7. Final simplification3.4

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

Reproduce

herbie shell --seed 2019135 
(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))