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

Average Error: 5.9 → 6.0

Time: 8.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}\]

↓

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

C

double f(double x, double y, double z) {
        double r527803 = x;
        double r527804 = 0.5;
        double r527805 = r527803 - r527804;
        double r527806 = log(r527803);
        double r527807 = r527805 * r527806;
        double r527808 = r527807 - r527803;
        double r527809 = 0.91893853320467;
        double r527810 = r527808 + r527809;
        double r527811 = y;
        double r527812 = 0.0007936500793651;
        double r527813 = r527811 + r527812;
        double r527814 = z;
        double r527815 = r527813 * r527814;
        double r527816 = 0.0027777777777778;
        double r527817 = r527815 - r527816;
        double r527818 = r527817 * r527814;
        double r527819 = 0.083333333333333;
        double r527820 = r527818 + r527819;
        double r527821 = r527820 / r527803;
        double r527822 = r527810 + r527821;
        return r527822;
}

↓

double f(double x, double y, double z) {
        double r527823 = y;
        double r527824 = 0.0007936500793651;
        double r527825 = r527823 + r527824;
        double r527826 = z;
        double r527827 = r527825 * r527826;
        double r527828 = 0.0027777777777778;
        double r527829 = r527827 - r527828;
        double r527830 = r527829 * r527826;
        double r527831 = 0.083333333333333;
        double r527832 = r527830 + r527831;
        double r527833 = x;
        double r527834 = r527832 / r527833;
        double r527835 = 0.91893853320467;
        double r527836 = 0.5;
        double r527837 = r527833 - r527836;
        double r527838 = log(r527833);
        double r527839 = exp(r527838);
        double r527840 = -r527839;
        double r527841 = fma(r527837, r527838, r527840);
        double r527842 = sqrt(r527841);
        double r527843 = r527842 * r527842;
        double r527844 = r527835 + r527843;
        double r527845 = r527834 + r527844;
        return r527845;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	5.9
Target	1.2
Herbie	6.0

\[\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-sqr-sqrt 5.9

   \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log x - \color{blue}{\sqrt{x} \cdot \sqrt{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 prod-diff 5.8

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

5. Applied associate-+l+ 5.8

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

6. Simplified 5.8

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

8. Applied add-exp-log 5.8

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

9. Applied add-exp-log 5.7

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

10. Applied prod-exp 5.7

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

11. Simplified 5.7

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

13. Applied unsub-neg 5.7

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

14. Applied associate-+l- 5.7

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

15. Simplified 5.7

    \[\leadsto \left(\mathsf{fma}\left(x - 0.5, \log x, -e^{\log x}\right) + \left(0.91893853320467001 - \color{blue}{0}\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
16. Using strategy rm

17. Applied add-sqr-sqrt 6.0

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

18. Final simplification 6.0

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

Reproduce

herbie shell --seed 2020035 +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)))