Average Error: 4.3 → 3.4
Time: 57.9s
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 r4694591 = 1.0;
        double r4694592 = /* ERROR: no posit support in C */;
        double r4694593 = 0.1049934947;
        double r4694594 = /* ERROR: no posit support in C */;
        double r4694595 = x;
        double r4694596 = r4694595 * r4694595;
        double r4694597 = r4694594 * r4694596;
        double r4694598 = r4694592 + r4694597;
        double r4694599 = 0.0424060604;
        double r4694600 = /* ERROR: no posit support in C */;
        double r4694601 = r4694596 * r4694596;
        double r4694602 = r4694600 * r4694601;
        double r4694603 = r4694598 + r4694602;
        double r4694604 = 0.0072644182;
        double r4694605 = /* ERROR: no posit support in C */;
        double r4694606 = r4694601 * r4694596;
        double r4694607 = r4694605 * r4694606;
        double r4694608 = r4694603 + r4694607;
        double r4694609 = 0.0005064034;
        double r4694610 = /* ERROR: no posit support in C */;
        double r4694611 = r4694606 * r4694596;
        double r4694612 = r4694610 * r4694611;
        double r4694613 = r4694608 + r4694612;
        double r4694614 = 0.0001789971;
        double r4694615 = /* ERROR: no posit support in C */;
        double r4694616 = r4694611 * r4694596;
        double r4694617 = r4694615 * r4694616;
        double r4694618 = r4694613 + r4694617;
        double r4694619 = 0.7715471019;
        double r4694620 = /* ERROR: no posit support in C */;
        double r4694621 = r4694620 * r4694596;
        double r4694622 = r4694592 + r4694621;
        double r4694623 = 0.2909738639;
        double r4694624 = /* ERROR: no posit support in C */;
        double r4694625 = r4694624 * r4694601;
        double r4694626 = r4694622 + r4694625;
        double r4694627 = 0.0694555761;
        double r4694628 = /* ERROR: no posit support in C */;
        double r4694629 = r4694628 * r4694606;
        double r4694630 = r4694626 + r4694629;
        double r4694631 = 0.0140005442;
        double r4694632 = /* ERROR: no posit support in C */;
        double r4694633 = r4694632 * r4694611;
        double r4694634 = r4694630 + r4694633;
        double r4694635 = 0.0008327945;
        double r4694636 = /* ERROR: no posit support in C */;
        double r4694637 = r4694636 * r4694616;
        double r4694638 = r4694634 + r4694637;
        double r4694639 = 2.0;
        double r4694640 = /* ERROR: no posit support in C */;
        double r4694641 = r4694640 * r4694615;
        double r4694642 = r4694616 * r4694596;
        double r4694643 = r4694641 * r4694642;
        double r4694644 = r4694638 + r4694643;
        double r4694645 = r4694618 / r4694644;
        double r4694646 = r4694645 * r4694595;
        return r4694646;
}
↓
double f(double x) {
        double r4694647 = x;
        double r4694648 = 0.1049934947;
        double r4694649 = 0.0424060604;
        double r4694650 = r4694647 * r4694647;
        double r4694651 = 0.0001789971;
        double r4694652 = r4694650 * r4694651;
        double r4694653 = 0.0005064034;
        double r4694654 = r4694652 + r4694653;
        double r4694655 = r4694650 * r4694654;
        double r4694656 = 0.0072644182;
        double r4694657 = r4694655 + r4694656;
        double r4694658 = r4694657 * r4694650;
        double r4694659 = r4694649 + r4694658;
        double r4694660 = r4694659 * r4694650;
        double r4694661 = r4694648 + r4694660;
        double r4694662 = r4694661 * r4694650;
        double r4694663 = 1.0;
        double r4694664 = r4694662 + r4694663;
        double r4694665 = r4694647 * r4694664;
        double r4694666 = 0.7715471019;
        double r4694667 = 0.0140005442;
        double r4694668 = 2.0;
        double r4694669 = r4694652 * r4694668;
        double r4694670 = 0.0008327945;
        double r4694671 = r4694669 + r4694670;
        double r4694672 = r4694671 * r4694650;
        double r4694673 = r4694667 + r4694672;
        double r4694674 = r4694673 * r4694650;
        double r4694675 = 0.0694555761;
        double r4694676 = r4694674 + r4694675;
        double r4694677 = r4694650 * r4694676;
        double r4694678 = 0.2909738639;
        double r4694679 = r4694677 + r4694678;
        double r4694680 = r4694650 * r4694679;
        double r4694681 = r4694666 + r4694680;
        double r4694682 = r4694650 * r4694681;
        double r4694683 = r4694663 + r4694682;
        double r4694684 = r4694665 / r4694683;
        return r4694684;
}

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 
(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))