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

Average Error: 6.0 → 2.4

Time: 27.1s

Precision: 64

Math

\[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

↓

\[\begin{array}{l} \mathbf{if}\;z \le -1.124422890345471698653335501790027641217 \cdot 10^{64} \lor \neg \left(z \le 2.724809310324407650238250982535209616576 \cdot 10^{127}\right):\\ \;\;\;\;\left(7.936500793651000149400709382518925849581 \cdot 10^{-4} \cdot \frac{z}{\frac{x}{z}} + \left(\frac{0.08333333333333299564049667651488562114537}{x} - \frac{z \cdot 0.002777777777777800001512975569539776188321}{x}\right)\right) + \left(\left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.9189385332046700050057097541866824030876\right) + \log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.9189385332046700050057097541866824030876\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt{\sqrt{x}}\right)\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt{\sqrt{x}}\right)\right) + \frac{0.08333333333333299564049667651488562114537 + \left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z}{x}\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r976044 = x;
        double r976045 = 0.5;
        double r976046 = r976044 - r976045;
        double r976047 = log(r976044);
        double r976048 = r976046 * r976047;
        double r976049 = r976048 - r976044;
        double r976050 = 0.91893853320467;
        double r976051 = r976049 + r976050;
        double r976052 = y;
        double r976053 = 0.0007936500793651;
        double r976054 = r976052 + r976053;
        double r976055 = z;
        double r976056 = r976054 * r976055;
        double r976057 = 0.0027777777777778;
        double r976058 = r976056 - r976057;
        double r976059 = r976058 * r976055;
        double r976060 = 0.083333333333333;
        double r976061 = r976059 + r976060;
        double r976062 = r976061 / r976044;
        double r976063 = r976051 + r976062;
        return r976063;
}

↓

double f(double x, double y, double z) {
        double r976064 = z;
        double r976065 = -1.1244228903454717e+64;
        bool r976066 = r976064 <= r976065;
        double r976067 = 2.7248093103244077e+127;
        bool r976068 = r976064 <= r976067;
        double r976069 = !r976068;
        bool r976070 = r976066 || r976069;
        double r976071 = 0.0007936500793651;
        double r976072 = x;
        double r976073 = r976072 / r976064;
        double r976074 = r976064 / r976073;
        double r976075 = r976071 * r976074;
        double r976076 = 0.083333333333333;
        double r976077 = r976076 / r976072;
        double r976078 = 0.0027777777777778;
        double r976079 = r976064 * r976078;
        double r976080 = r976079 / r976072;
        double r976081 = r976077 - r976080;
        double r976082 = r976075 + r976081;
        double r976083 = sqrt(r976072);
        double r976084 = log(r976083);
        double r976085 = 0.5;
        double r976086 = r976072 - r976085;
        double r976087 = r976084 * r976086;
        double r976088 = r976087 - r976072;
        double r976089 = 0.91893853320467;
        double r976090 = r976088 + r976089;
        double r976091 = r976090 + r976087;
        double r976092 = r976082 + r976091;
        double r976093 = sqrt(r976083);
        double r976094 = log(r976093);
        double r976095 = r976086 * r976094;
        double r976096 = r976090 + r976095;
        double r976097 = r976096 + r976095;
        double r976098 = y;
        double r976099 = r976098 + r976071;
        double r976100 = r976099 * r976064;
        double r976101 = r976100 - r976078;
        double r976102 = r976101 * r976064;
        double r976103 = r976076 + r976102;
        double r976104 = r976103 / r976072;
        double r976105 = r976097 + r976104;
        double r976106 = r976070 ? r976092 : r976105;
        return r976106;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	6.0
Target	1.2
Herbie	2.4

\[\left(\left(\left(x - 0.5\right) \cdot \log x + \left(0.9189385332046700050057097541866824030876 - x\right)\right) + \frac{0.08333333333333299564049667651488562114537}{x}\right) + \frac{z}{x} \cdot \left(z \cdot \left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) - 0.002777777777777800001512975569539776188321\right)\]

Derivation

1. Split input into 2 regimes

2. if z < -1.1244228903454717e+64 or 2.7248093103244077e+127 < z

   1. Initial program 39.2

      \[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]
   2. Using strategy rm

   3. Applied add-sqr-sqrt 39.2

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)} - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   4. Applied log-prod 39.2

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \color{blue}{\left(\log \left(\sqrt{x}\right) + \log \left(\sqrt{x}\right)\right)} - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   5. Applied distribute-lft-in 39.2

      \[\leadsto \left(\left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right)\right)} - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   6. Applied associate--l+ 39.2

      \[\leadsto \left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right)\right)} + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   7. Applied associate-+l+ 39.2

      \[\leadsto \color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right) + 0.9189385332046700050057097541866824030876\right)\right)} + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   8. Taylor expanded around 0 36.8

      \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right) + 0.9189385332046700050057097541866824030876\right)\right) + \color{blue}{\left(\left(7.936500793651000149400709382518925849581 \cdot 10^{-4} \cdot \frac{{z}^{2}}{x} + 0.08333333333333299564049667651488562114537 \cdot \frac{1}{x}\right) - 0.002777777777777800001512975569539776188321 \cdot \frac{z}{x}\right)}\]

   9. Simplified 11.0

      \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right) + 0.9189385332046700050057097541866824030876\right)\right) + \color{blue}{\left(\frac{z}{\frac{x}{z}} \cdot 7.936500793651000149400709382518925849581 \cdot 10^{-4} + \left(\frac{0.08333333333333299564049667651488562114537}{x} - \frac{z \cdot 0.002777777777777800001512975569539776188321}{x}\right)\right)}\]

   if -1.1244228903454717e+64 < z < 2.7248093103244077e+127

   1. Initial program 1.2

      \[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]
   2. Using strategy rm

   3. Applied add-sqr-sqrt 1.2

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)} - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   4. Applied log-prod 1.2

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \color{blue}{\left(\log \left(\sqrt{x}\right) + \log \left(\sqrt{x}\right)\right)} - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   5. Applied distribute-lft-in 1.2

      \[\leadsto \left(\left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right)\right)} - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   6. Applied associate--l+ 1.2

      \[\leadsto \left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right)\right)} + 0.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   7. Applied associate-+l+ 1.2

      \[\leadsto \color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right) + 0.9189385332046700050057097541866824030876\right)\right)} + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]
   8. Using strategy rm

   9. Applied add-sqr-sqrt 1.2

      \[\leadsto \left(\left(x - 0.5\right) \cdot \log \left(\sqrt{\color{blue}{\sqrt{x} \cdot \sqrt{x}}}\right) + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right) + 0.9189385332046700050057097541866824030876\right)\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   10. Applied sqrt-prod 1.2

       \[\leadsto \left(\left(x - 0.5\right) \cdot \log \color{blue}{\left(\sqrt{\sqrt{x}} \cdot \sqrt{\sqrt{x}}\right)} + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right) + 0.9189385332046700050057097541866824030876\right)\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   11. Applied log-prod 1.2

       \[\leadsto \left(\left(x - 0.5\right) \cdot \color{blue}{\left(\log \left(\sqrt{\sqrt{x}}\right) + \log \left(\sqrt{\sqrt{x}}\right)\right)} + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right) + 0.9189385332046700050057097541866824030876\right)\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   12. Applied distribute-rgt-in 1.2

       \[\leadsto \left(\color{blue}{\left(\log \left(\sqrt{\sqrt{x}}\right) \cdot \left(x - 0.5\right) + \log \left(\sqrt{\sqrt{x}}\right) \cdot \left(x - 0.5\right)\right)} + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right) + 0.9189385332046700050057097541866824030876\right)\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   13. Applied associate-+l+ 1.2

       \[\leadsto \color{blue}{\left(\log \left(\sqrt{\sqrt{x}}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt{\sqrt{x}}\right) \cdot \left(x - 0.5\right) + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt{x}\right) - x\right) + 0.9189385332046700050057097541866824030876\right)\right)\right)} + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   14. Simplified 1.2

       \[\leadsto \left(\log \left(\sqrt{\sqrt{x}}\right) \cdot \left(x - 0.5\right) + \color{blue}{\left(\left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.9189385332046700050057097541866824030876\right) + \log \left(\sqrt{\sqrt{x}}\right) \cdot \left(x - 0.5\right)\right)}\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]
3. Recombined 2 regimes into one program.

4. Final simplification 2.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.124422890345471698653335501790027641217 \cdot 10^{64} \lor \neg \left(z \le 2.724809310324407650238250982535209616576 \cdot 10^{127}\right):\\ \;\;\;\;\left(7.936500793651000149400709382518925849581 \cdot 10^{-4} \cdot \frac{z}{\frac{x}{z}} + \left(\frac{0.08333333333333299564049667651488562114537}{x} - \frac{z \cdot 0.002777777777777800001512975569539776188321}{x}\right)\right) + \left(\left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.9189385332046700050057097541866824030876\right) + \log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right) + 0.9189385332046700050057097541866824030876\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt{\sqrt{x}}\right)\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt{\sqrt{x}}\right)\right) + \frac{0.08333333333333299564049667651488562114537 + \left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z}{x}\\ \end{array}\]

Reproduce

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

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