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

Average Error: 5.7 → 4.4

Time: 9.0s

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}\;\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z = -\infty \lor \neg \left(\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z \le 1.704408942489215119874497056738392519937 \cdot 10^{297}\right):\\ \;\;\;\;\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{1}{\left(0.4000000000000064059868520871532382443547 \cdot \left(x \cdot z\right) + 12.00000000000004796163466380676254630089 \cdot x\right) - 0.1009522780952416126654114236771420110017 \cdot \left(x \cdot {z}^{2}\right)}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(x - 0.5\right) \cdot \left(2 \cdot \log \left(\sqrt[3]{x}\right)\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{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}\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r510435 = x;
        double r510436 = 0.5;
        double r510437 = r510435 - r510436;
        double r510438 = log(r510435);
        double r510439 = r510437 * r510438;
        double r510440 = r510439 - r510435;
        double r510441 = 0.91893853320467;
        double r510442 = r510440 + r510441;
        double r510443 = y;
        double r510444 = 0.0007936500793651;
        double r510445 = r510443 + r510444;
        double r510446 = z;
        double r510447 = r510445 * r510446;
        double r510448 = 0.0027777777777778;
        double r510449 = r510447 - r510448;
        double r510450 = r510449 * r510446;
        double r510451 = 0.083333333333333;
        double r510452 = r510450 + r510451;
        double r510453 = r510452 / r510435;
        double r510454 = r510442 + r510453;
        return r510454;
}

↓

double f(double x, double y, double z) {
        double r510455 = y;
        double r510456 = 0.0007936500793651;
        double r510457 = r510455 + r510456;
        double r510458 = z;
        double r510459 = r510457 * r510458;
        double r510460 = 0.0027777777777778;
        double r510461 = r510459 - r510460;
        double r510462 = r510461 * r510458;
        double r510463 = -inf.0;
        bool r510464 = r510462 <= r510463;
        double r510465 = 1.704408942489215e+297;
        bool r510466 = r510462 <= r510465;
        double r510467 = !r510466;
        bool r510468 = r510464 || r510467;
        double r510469 = x;
        double r510470 = 0.5;
        double r510471 = r510469 - r510470;
        double r510472 = log(r510469);
        double r510473 = r510471 * r510472;
        double r510474 = r510473 - r510469;
        double r510475 = 0.91893853320467;
        double r510476 = r510474 + r510475;
        double r510477 = 1.0;
        double r510478 = 0.4000000000000064;
        double r510479 = r510469 * r510458;
        double r510480 = r510478 * r510479;
        double r510481 = 12.000000000000048;
        double r510482 = r510481 * r510469;
        double r510483 = r510480 + r510482;
        double r510484 = 0.10095227809524161;
        double r510485 = 2.0;
        double r510486 = pow(r510458, r510485);
        double r510487 = r510469 * r510486;
        double r510488 = r510484 * r510487;
        double r510489 = r510483 - r510488;
        double r510490 = r510477 / r510489;
        double r510491 = r510476 + r510490;
        double r510492 = cbrt(r510469);
        double r510493 = log(r510492);
        double r510494 = r510485 * r510493;
        double r510495 = r510471 * r510494;
        double r510496 = r510471 * r510493;
        double r510497 = r510495 + r510496;
        double r510498 = r510497 - r510469;
        double r510499 = r510498 + r510475;
        double r510500 = 0.083333333333333;
        double r510501 = r510462 + r510500;
        double r510502 = r510501 / r510469;
        double r510503 = r510499 + r510502;
        double r510504 = r510468 ? r510491 : r510503;
        return r510504;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	5.7
Target	1.1
Herbie	4.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 (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z) < -inf.0 or 1.704408942489215e+297 < (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z)

   1. Initial program 60.6

      \[\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 clear-num 60.6

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

   4. Taylor expanded around 0 45.8

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{1}{\color{blue}{\left(0.4000000000000064059868520871532382443547 \cdot \left(x \cdot z\right) + 12.00000000000004796163466380676254630089 \cdot x\right) - 0.1009522780952416126654114236771420110017 \cdot \left(x \cdot {z}^{2}\right)}}\]

   if -inf.0 < (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z) < 1.704408942489215e+297

   1. Initial program 0.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-cube-cbrt 0.3

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

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

      \[\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.9189385332046700050057097541866824030876\right) + \frac{\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z + 0.08333333333333299564049667651488562114537}{x}\]

   6. Simplified 0.3

      \[\leadsto \left(\left(\left(\color{blue}{\left(x - 0.5\right) \cdot \left(2 \cdot \log \left(\sqrt[3]{x}\right)\right)} + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{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}\]
3. Recombined 2 regimes into one program.

4. Final simplification 4.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z = -\infty \lor \neg \left(\left(\left(y + 7.936500793651000149400709382518925849581 \cdot 10^{-4}\right) \cdot z - 0.002777777777777800001512975569539776188321\right) \cdot z \le 1.704408942489215119874497056738392519937 \cdot 10^{297}\right):\\ \;\;\;\;\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.9189385332046700050057097541866824030876\right) + \frac{1}{\left(0.4000000000000064059868520871532382443547 \cdot \left(x \cdot z\right) + 12.00000000000004796163466380676254630089 \cdot x\right) - 0.1009522780952416126654114236771420110017 \cdot \left(x \cdot {z}^{2}\right)}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(x - 0.5\right) \cdot \left(2 \cdot \log \left(\sqrt[3]{x}\right)\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{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}\\ \end{array}\]

Reproduce

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