Numeric.SpecFunctions:$slogFactorial from math-functions-0.1.5.2, B

Average Error: 5.9 → 5.9

Time: 9.6s

Precision: 64

Math

\[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

↓

\[\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(1 \cdot \left({\left(\sqrt{x}\right)}^{\frac{1}{3}} \cdot {\left(\sqrt{x}\right)}^{\frac{1}{3}}\right)\right)\right) + \left(\left(\log \left({\left(\sqrt{x}\right)}^{\frac{1}{3}} \cdot {\left(\sqrt{x}\right)}^{\frac{1}{3}}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

C

double f(double x, double y, double z) {
        double r633735 = x;
        double r633736 = 0.5;
        double r633737 = r633735 - r633736;
        double r633738 = log(r633735);
        double r633739 = r633737 * r633738;
        double r633740 = r633739 - r633735;
        double r633741 = 0.91893853320467;
        double r633742 = r633740 + r633741;
        double r633743 = y;
        double r633744 = 0.0007936500793651;
        double r633745 = r633743 + r633744;
        double r633746 = z;
        double r633747 = r633745 * r633746;
        double r633748 = 0.0027777777777778;
        double r633749 = r633747 - r633748;
        double r633750 = r633749 * r633746;
        double r633751 = 0.083333333333333;
        double r633752 = r633750 + r633751;
        double r633753 = r633752 / r633735;
        double r633754 = r633742 + r633753;
        return r633754;
}

↓

double f(double x, double y, double z) {
        double r633755 = x;
        double r633756 = 0.5;
        double r633757 = r633755 - r633756;
        double r633758 = cbrt(r633755);
        double r633759 = 1.0;
        double r633760 = sqrt(r633755);
        double r633761 = 0.3333333333333333;
        double r633762 = pow(r633760, r633761);
        double r633763 = r633762 * r633762;
        double r633764 = r633759 * r633763;
        double r633765 = r633758 * r633764;
        double r633766 = log(r633765);
        double r633767 = r633757 * r633766;
        double r633768 = log(r633763);
        double r633769 = r633768 * r633757;
        double r633770 = r633769 - r633755;
        double r633771 = 0.91893853320467;
        double r633772 = r633770 + r633771;
        double r633773 = r633767 + r633772;
        double r633774 = y;
        double r633775 = 0.0007936500793651;
        double r633776 = r633774 + r633775;
        double r633777 = z;
        double r633778 = r633776 * r633777;
        double r633779 = 0.0027777777777778;
        double r633780 = r633778 - r633779;
        double r633781 = r633780 * r633777;
        double r633782 = 0.083333333333333;
        double r633783 = r633781 + r633782;
        double r633784 = r633783 / r633755;
        double r633785 = r633773 + r633784;
        return r633785;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	5.9
Target	1.2
Herbie	5.9

\[\left(\left(\left(x - 0.5\right) \cdot \log x + \left(0.91893853320467001 - x\right)\right) + \frac{0.0833333333333329956}{x}\right) + \frac{z}{x} \cdot \left(z \cdot \left(y + 7.93650079365100015 \cdot 10^{-4}\right) - 0.0027777777777778\right)\]

Derivation

1. Initial program 5.9

   \[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
2. Using strategy rm

3. Applied add-cube-cbrt 5.9

   \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \color{blue}{\left(\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \sqrt[3]{x}\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

4. Applied log-prod 5.9

   \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \color{blue}{\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \log \left(\sqrt[3]{x}\right)\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

5. Applied distribute-lft-in 5.9

   \[\leadsto \left(\left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right)\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

6. Applied associate--l+ 5.9

   \[\leadsto \left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right)\right)} + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

7. Applied associate-+l+ 5.9

   \[\leadsto \color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right) + 0.91893853320467001\right)\right)} + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

8. Simplified 5.9

   \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \color{blue}{\left(\left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)}\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
9. Using strategy rm

10. Applied *-un-lft-identity 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{\color{blue}{1 \cdot x}}\right) + \left(\left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

11. Applied cbrt-prod 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{x}\right)}\right) + \left(\left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

12. Simplified 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(\color{blue}{1} \cdot \sqrt[3]{x}\right)\right) + \left(\left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

13. Simplified 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(1 \cdot \color{blue}{{x}^{\frac{1}{3}}}\right)\right) + \left(\left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
14. Using strategy rm

15. Applied add-sqr-sqrt 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(1 \cdot {\color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)}}^{\frac{1}{3}}\right)\right) + \left(\left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

16. Applied unpow-prod-down 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(1 \cdot \color{blue}{\left({\left(\sqrt{x}\right)}^{\frac{1}{3}} \cdot {\left(\sqrt{x}\right)}^{\frac{1}{3}}\right)}\right)\right) + \left(\left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
17. Using strategy rm

18. Applied add-sqr-sqrt 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(1 \cdot \left({\left(\sqrt{x}\right)}^{\frac{1}{3}} \cdot {\left(\sqrt{x}\right)}^{\frac{1}{3}}\right)\right)\right) + \left(\left(\log \left(\sqrt[3]{\color{blue}{\sqrt{x} \cdot \sqrt{x}}}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

19. Applied cbrt-prod 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(1 \cdot \left({\left(\sqrt{x}\right)}^{\frac{1}{3}} \cdot {\left(\sqrt{x}\right)}^{\frac{1}{3}}\right)\right)\right) + \left(\left(\log \color{blue}{\left(\sqrt[3]{\sqrt{x}} \cdot \sqrt[3]{\sqrt{x}}\right)} \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

20. Simplified 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(1 \cdot \left({\left(\sqrt{x}\right)}^{\frac{1}{3}} \cdot {\left(\sqrt{x}\right)}^{\frac{1}{3}}\right)\right)\right) + \left(\left(\log \left(\color{blue}{{\left(\sqrt{x}\right)}^{\frac{1}{3}}} \cdot \sqrt[3]{\sqrt{x}}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

21. Simplified 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(1 \cdot \left({\left(\sqrt{x}\right)}^{\frac{1}{3}} \cdot {\left(\sqrt{x}\right)}^{\frac{1}{3}}\right)\right)\right) + \left(\left(\log \left({\left(\sqrt{x}\right)}^{\frac{1}{3}} \cdot \color{blue}{{\left(\sqrt{x}\right)}^{\frac{1}{3}}}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

22. Final simplification 5.9

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(1 \cdot \left({\left(\sqrt{x}\right)}^{\frac{1}{3}} \cdot {\left(\sqrt{x}\right)}^{\frac{1}{3}}\right)\right)\right) + \left(\left(\log \left({\left(\sqrt{x}\right)}^{\frac{1}{3}} \cdot {\left(\sqrt{x}\right)}^{\frac{1}{3}}\right) \cdot \left(x - 0.5\right) - x\right) + 0.91893853320467001\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

Reproduce

herbie shell --seed 2020035 
(FPCore (x y z)
  :name "Numeric.SpecFunctions:$slogFactorial from math-functions-0.1.5.2, B"
  :precision binary64

  :herbie-target
  (+ (+ (+ (* (- x 0.5) (log x)) (- 0.91893853320467 x)) (/ 0.083333333333333 x)) (* (/ z x) (- (* z (+ y 0.0007936500793651)) 0.0027777777777778)))

  (+ (+ (- (* (- x 0.5) (log x)) x) 0.91893853320467) (/ (+ (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z) 0.083333333333333) x)))