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

Average Error: 5.8 → 5.8

Time: 7.8s

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 {x}^{\frac{1}{3}}\right)\right) + \mathsf{fma}\left(\log \left(\sqrt[3]{x}\right), x - 0.5, 0.91893853320467001 - x\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 r506063 = x;
        double r506064 = 0.5;
        double r506065 = r506063 - r506064;
        double r506066 = log(r506063);
        double r506067 = r506065 * r506066;
        double r506068 = r506067 - r506063;
        double r506069 = 0.91893853320467;
        double r506070 = r506068 + r506069;
        double r506071 = y;
        double r506072 = 0.0007936500793651;
        double r506073 = r506071 + r506072;
        double r506074 = z;
        double r506075 = r506073 * r506074;
        double r506076 = 0.0027777777777778;
        double r506077 = r506075 - r506076;
        double r506078 = r506077 * r506074;
        double r506079 = 0.083333333333333;
        double r506080 = r506078 + r506079;
        double r506081 = r506080 / r506063;
        double r506082 = r506070 + r506081;
        return r506082;
}

↓

double f(double x, double y, double z) {
        double r506083 = x;
        double r506084 = 0.5;
        double r506085 = r506083 - r506084;
        double r506086 = cbrt(r506083);
        double r506087 = 1.0;
        double r506088 = 0.3333333333333333;
        double r506089 = pow(r506083, r506088);
        double r506090 = r506087 * r506089;
        double r506091 = r506086 * r506090;
        double r506092 = log(r506091);
        double r506093 = r506085 * r506092;
        double r506094 = log(r506086);
        double r506095 = 0.91893853320467;
        double r506096 = r506095 - r506083;
        double r506097 = fma(r506094, r506085, r506096);
        double r506098 = r506093 + r506097;
        double r506099 = y;
        double r506100 = 0.0007936500793651;
        double r506101 = r506099 + r506100;
        double r506102 = z;
        double r506103 = r506101 * r506102;
        double r506104 = 0.0027777777777778;
        double r506105 = r506103 - r506104;
        double r506106 = r506105 * r506102;
        double r506107 = 0.083333333333333;
        double r506108 = r506106 + r506107;
        double r506109 = r506108 / r506083;
        double r506110 = r506098 + r506109;
        return r506110;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	5.8
Target	1.2
Herbie	5.8

\[\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.8

   \[\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.8

   \[\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.8

   \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \color{blue}{\mathsf{fma}\left(\log \left(\sqrt[3]{x}\right), x - 0.5, 0.91893853320467001 - x\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.8

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{\color{blue}{1 \cdot x}}\right) + \mathsf{fma}\left(\log \left(\sqrt[3]{x}\right), x - 0.5, 0.91893853320467001 - x\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.8

    \[\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) + \mathsf{fma}\left(\log \left(\sqrt[3]{x}\right), x - 0.5, 0.91893853320467001 - x\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.8

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(\color{blue}{1} \cdot \sqrt[3]{x}\right)\right) + \mathsf{fma}\left(\log \left(\sqrt[3]{x}\right), x - 0.5, 0.91893853320467001 - x\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.8

    \[\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) + \mathsf{fma}\left(\log \left(\sqrt[3]{x}\right), x - 0.5, 0.91893853320467001 - x\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

14. Final simplification 5.8

    \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \left(1 \cdot {x}^{\frac{1}{3}}\right)\right) + \mathsf{fma}\left(\log \left(\sqrt[3]{x}\right), x - 0.5, 0.91893853320467001 - x\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 2020021 +o rules:numerics
(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)))