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

Average Error: 6.0 → 5.2

Time: 16.2s

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}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \le 1.993574570781383 \cdot 10^{217}:\\ \;\;\;\;\left(\left(\left(x - 0.5\right) \cdot \log \left(\left({\left({\left({x}^{\frac{1}{3}}\right)}^{\left(\sqrt[3]{\frac{2}{3}} \cdot \sqrt[3]{\frac{2}{3}}\right)}\right)}^{\left(\sqrt[3]{\frac{2}{3}}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\frac{1}{3}}\right) \cdot \sqrt[3]{x}\right) + \left(\log \left(1 \cdot {x}^{\frac{1}{3}}\right) \cdot \left(x - 0.5\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}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \left(\left(7.93650079365100015 \cdot 10^{-4} \cdot \frac{{z}^{2}}{x} + 0.0833333333333329956 \cdot \frac{1}{x}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r1977 = x;
        double r1978 = 0.5;
        double r1979 = r1977 - r1978;
        double r1980 = log(r1977);
        double r1981 = r1979 * r1980;
        double r1982 = r1981 - r1977;
        double r1983 = 0.91893853320467;
        double r1984 = r1982 + r1983;
        double r1985 = y;
        double r1986 = 0.0007936500793651;
        double r1987 = r1985 + r1986;
        double r1988 = z;
        double r1989 = r1987 * r1988;
        double r1990 = 0.0027777777777778;
        double r1991 = r1989 - r1990;
        double r1992 = r1991 * r1988;
        double r1993 = 0.083333333333333;
        double r1994 = r1992 + r1993;
        double r1995 = r1994 / r1977;
        double r1996 = r1984 + r1995;
        return r1996;
}

↓

double f(double x, double y, double z) {
        double r1997 = x;
        double r1998 = 1.993574570781383e+217;
        bool r1999 = r1997 <= r1998;
        double r2000 = 0.5;
        double r2001 = r1997 - r2000;
        double r2002 = 0.3333333333333333;
        double r2003 = pow(r1997, r2002);
        double r2004 = 0.6666666666666666;
        double r2005 = cbrt(r2004);
        double r2006 = r2005 * r2005;
        double r2007 = pow(r2003, r2006);
        double r2008 = pow(r2007, r2005);
        double r2009 = cbrt(r1997);
        double r2010 = pow(r2009, r2002);
        double r2011 = r2008 * r2010;
        double r2012 = r2011 * r2009;
        double r2013 = log(r2012);
        double r2014 = r2001 * r2013;
        double r2015 = 1.0;
        double r2016 = r2015 * r2003;
        double r2017 = log(r2016);
        double r2018 = r2017 * r2001;
        double r2019 = r2018 - r1997;
        double r2020 = r2014 + r2019;
        double r2021 = 0.91893853320467;
        double r2022 = r2020 + r2021;
        double r2023 = y;
        double r2024 = 0.0007936500793651;
        double r2025 = r2023 + r2024;
        double r2026 = z;
        double r2027 = r2025 * r2026;
        double r2028 = 0.0027777777777778;
        double r2029 = r2027 - r2028;
        double r2030 = r2029 * r2026;
        double r2031 = 0.083333333333333;
        double r2032 = r2030 + r2031;
        double r2033 = r2032 / r1997;
        double r2034 = r2022 + r2033;
        double r2035 = log(r1997);
        double r2036 = r2001 * r2035;
        double r2037 = r2036 - r1997;
        double r2038 = r2037 + r2021;
        double r2039 = 2.0;
        double r2040 = pow(r2026, r2039);
        double r2041 = r2040 / r1997;
        double r2042 = r2024 * r2041;
        double r2043 = r2015 / r1997;
        double r2044 = r2031 * r2043;
        double r2045 = r2042 + r2044;
        double r2046 = r2026 / r1997;
        double r2047 = r2028 * r2046;
        double r2048 = r2045 - r2047;
        double r2049 = r2038 + r2048;
        double r2050 = r1999 ? r2034 : r2049;
        return r2050;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	6.0
Target	1.3
Herbie	5.2

\[\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. Split input into 2 regimes

2. if x < 1.993574570781383e+217

   1. Initial program 3.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 3.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 3.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 3.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+ 3.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. Simplified 3.9

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

   9. Applied *-un-lft-identity 3.9

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

   10. Applied cbrt-prod 3.9

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

   11. Simplified 3.9

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

   12. Simplified 3.8

       \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \left(\log \left(1 \cdot \color{blue}{{x}^{\frac{1}{3}}}\right) \cdot \left(x - 0.5\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}\]
   13. Using strategy rm

   14. Applied add-cube-cbrt 3.8

       \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \left(\color{blue}{\left(\left(\sqrt[3]{\sqrt[3]{x}} \cdot \sqrt[3]{\sqrt[3]{x}}\right) \cdot \sqrt[3]{\sqrt[3]{x}}\right)} \cdot \sqrt[3]{x}\right) + \left(\log \left(1 \cdot {x}^{\frac{1}{3}}\right) \cdot \left(x - 0.5\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}\]

   15. Simplified 3.9

       \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \left(\left(\color{blue}{{\left({x}^{\frac{1}{3}}\right)}^{\frac{2}{3}}} \cdot \sqrt[3]{\sqrt[3]{x}}\right) \cdot \sqrt[3]{x}\right) + \left(\log \left(1 \cdot {x}^{\frac{1}{3}}\right) \cdot \left(x - 0.5\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}\]

   16. Simplified 3.9

       \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \left(\left({\left({x}^{\frac{1}{3}}\right)}^{\frac{2}{3}} \cdot \color{blue}{{\left(\sqrt[3]{x}\right)}^{\frac{1}{3}}}\right) \cdot \sqrt[3]{x}\right) + \left(\log \left(1 \cdot {x}^{\frac{1}{3}}\right) \cdot \left(x - 0.5\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}\]
   17. Using strategy rm

   18. Applied add-cube-cbrt 3.8

       \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \left(\left({\left({x}^{\frac{1}{3}}\right)}^{\color{blue}{\left(\left(\sqrt[3]{\frac{2}{3}} \cdot \sqrt[3]{\frac{2}{3}}\right) \cdot \sqrt[3]{\frac{2}{3}}\right)}} \cdot {\left(\sqrt[3]{x}\right)}^{\frac{1}{3}}\right) \cdot \sqrt[3]{x}\right) + \left(\log \left(1 \cdot {x}^{\frac{1}{3}}\right) \cdot \left(x - 0.5\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}\]

   19. Applied pow-unpow 3.8

       \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \left(\left(\color{blue}{{\left({\left({x}^{\frac{1}{3}}\right)}^{\left(\sqrt[3]{\frac{2}{3}} \cdot \sqrt[3]{\frac{2}{3}}\right)}\right)}^{\left(\sqrt[3]{\frac{2}{3}}\right)}} \cdot {\left(\sqrt[3]{x}\right)}^{\frac{1}{3}}\right) \cdot \sqrt[3]{x}\right) + \left(\log \left(1 \cdot {x}^{\frac{1}{3}}\right) \cdot \left(x - 0.5\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}\]

   if 1.993574570781383e+217 < x

   1. Initial program 15.2

      \[\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. Taylor expanded around 0 10.9

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \color{blue}{\left(\left(7.93650079365100015 \cdot 10^{-4} \cdot \frac{{z}^{2}}{x} + 0.0833333333333329956 \cdot \frac{1}{x}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)}\]
3. Recombined 2 regimes into one program.

4. Final simplification 5.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 1.993574570781383 \cdot 10^{217}:\\ \;\;\;\;\left(\left(\left(x - 0.5\right) \cdot \log \left(\left({\left({\left({x}^{\frac{1}{3}}\right)}^{\left(\sqrt[3]{\frac{2}{3}} \cdot \sqrt[3]{\frac{2}{3}}\right)}\right)}^{\left(\sqrt[3]{\frac{2}{3}}\right)} \cdot {\left(\sqrt[3]{x}\right)}^{\frac{1}{3}}\right) \cdot \sqrt[3]{x}\right) + \left(\log \left(1 \cdot {x}^{\frac{1}{3}}\right) \cdot \left(x - 0.5\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}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \left(\left(7.93650079365100015 \cdot 10^{-4} \cdot \frac{{z}^{2}}{x} + 0.0833333333333329956 \cdot \frac{1}{x}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)\\ \end{array}\]

Reproduce

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