Average Error: 25.0 → 9.0
Time: 49.9s
Precision: 64
\[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
↓
\[\begin{array}{l} \mathbf{if}\;z \le -1.355985277760923721475726033060808414189 \cdot 10^{-91}:\\ \;\;\;\;x - \frac{1}{\frac{\frac{t}{\sqrt{\log \left(\mathsf{fma}\left(y, \mathsf{expm1}\left(z\right), 1\right)\right)}}}{\sqrt{\log \left(\mathsf{fma}\left(y, \mathsf{expm1}\left(z\right), 1\right)\right)}}}\\ \mathbf{else}:\\ \;\;\;\;x - \mathsf{fma}\left(\frac{z \cdot y}{t}, 1, \frac{\log 1}{t}\right)\\ \end{array}\]
x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}
↓
\begin{array}{l}
\mathbf{if}\;z \le -1.355985277760923721475726033060808414189 \cdot 10^{-91}:\\
\;\;\;\;x - \frac{1}{\frac{\frac{t}{\sqrt{\log \left(\mathsf{fma}\left(y, \mathsf{expm1}\left(z\right), 1\right)\right)}}}{\sqrt{\log \left(\mathsf{fma}\left(y, \mathsf{expm1}\left(z\right), 1\right)\right)}}}\\

\mathbf{else}:\\
\;\;\;\;x - \mathsf{fma}\left(\frac{z \cdot y}{t}, 1, \frac{\log 1}{t}\right)\\

\end{array}
double f(double x, double y, double z, double t) {
        double r12364401 = x;
        double r12364402 = 1.0;
        double r12364403 = y;
        double r12364404 = r12364402 - r12364403;
        double r12364405 = z;
        double r12364406 = exp(r12364405);
        double r12364407 = r12364403 * r12364406;
        double r12364408 = r12364404 + r12364407;
        double r12364409 = log(r12364408);
        double r12364410 = t;
        double r12364411 = r12364409 / r12364410;
        double r12364412 = r12364401 - r12364411;
        return r12364412;
}
↓
double f(double x, double y, double z, double t) {
        double r12364413 = z;
        double r12364414 = -1.3559852777609237e-91;
        bool r12364415 = r12364413 <= r12364414;
        double r12364416 = x;
        double r12364417 = 1.0;
        double r12364418 = t;
        double r12364419 = y;
        double r12364420 = expm1(r12364413);
        double r12364421 = 1.0;
        double r12364422 = fma(r12364419, r12364420, r12364421);
        double r12364423 = log(r12364422);
        double r12364424 = sqrt(r12364423);
        double r12364425 = r12364418 / r12364424;
        double r12364426 = r12364425 / r12364424;
        double r12364427 = r12364417 / r12364426;
        double r12364428 = r12364416 - r12364427;
        double r12364429 = r12364413 * r12364419;
        double r12364430 = r12364429 / r12364418;
        double r12364431 = log(r12364421);
        double r12364432 = r12364431 / r12364418;
        double r12364433 = fma(r12364430, r12364421, r12364432);
        double r12364434 = r12364416 - r12364433;
        double r12364435 = r12364415 ? r12364428 : r12364434;
        return r12364435;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original25.0
Target16.4
Herbie9.0
\[\begin{array}{l} \mathbf{if}\;z \lt -2.887462308820794658905265984545350618896 \cdot 10^{119}:\\ \;\;\;\;\left(x - \frac{\frac{-0.5}{y \cdot t}}{z \cdot z}\right) - \frac{-0.5}{y \cdot t} \cdot \frac{\frac{2}{z}}{z \cdot z}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{\log \left(1 + z \cdot y\right)}{t}\\ \end{array}\]

Derivation

  1. Split input into 2 regimes

  2. if z < -1.3559852777609237e-91

    1. Initial program 15.6

      \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]

    2. Simplified11.9

      \[\leadsto \color{blue}{x - \frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{t}}\]
    3. Using strategy rm

    4. Applied clear-num11.9

      \[\leadsto x - \color{blue}{\frac{1}{\frac{t}{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}\]
    5. Using strategy rm

    6. Applied add-sqr-sqrt12.8

      \[\leadsto x - \frac{1}{\frac{t}{\color{blue}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)} \cdot \sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}}\]

    7. Applied *-un-lft-identity12.8

      \[\leadsto x - \frac{1}{\frac{\color{blue}{1 \cdot t}}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)} \cdot \sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}\]

    8. Applied times-frac12.8

      \[\leadsto x - \frac{1}{\color{blue}{\frac{1}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}} \cdot \frac{t}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}}\]

    9. Applied *-un-lft-identity12.8

      \[\leadsto x - \frac{\color{blue}{1 \cdot 1}}{\frac{1}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}} \cdot \frac{t}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}\]

    10. Applied times-frac12.8

      \[\leadsto x - \color{blue}{\frac{1}{\frac{1}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}} \cdot \frac{1}{\frac{t}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}}\]
    11. Using strategy rm

    12. Applied expm1-log1p-u12.8

      \[\leadsto x - \frac{1}{\frac{1}{\sqrt{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)\right)\right)}}}} \cdot \frac{1}{\frac{t}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}\]
    13. Using strategy rm

    14. Applied frac-times12.8

      \[\leadsto x - \color{blue}{\frac{1 \cdot 1}{\frac{1}{\sqrt{\mathsf{expm1}\left(\mathsf{log1p}\left(\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)\right)\right)}} \cdot \frac{t}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}}\]

    15. Simplified12.8

      \[\leadsto x - \frac{\color{blue}{1}}{\frac{1}{\sqrt{\mathsf{expm1}\left(\mathsf{log1p}\left(\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)\right)\right)}} \cdot \frac{t}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}\]

    16. Simplified12.8

      \[\leadsto x - \frac{1}{\color{blue}{\frac{\frac{t}{\sqrt{\log \left(\mathsf{fma}\left(y, \mathsf{expm1}\left(z\right), 1\right)\right)}}}{\sqrt{\log \left(\mathsf{fma}\left(y, \mathsf{expm1}\left(z\right), 1\right)\right)}}}}\]

    if -1.3559852777609237e-91 < z

    1. Initial program 30.9

      \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]

    2. Simplified11.6

      \[\leadsto \color{blue}{x - \frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{t}}\]

    3. Taylor expanded around 0 6.6

      \[\leadsto \color{blue}{x - \left(1 \cdot \frac{z \cdot y}{t} + \frac{\log 1}{t}\right)}\]

    4. Simplified6.6

      \[\leadsto \color{blue}{x - \mathsf{fma}\left(\frac{z \cdot y}{t}, 1, \frac{\log 1}{t}\right)}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification9.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.355985277760923721475726033060808414189 \cdot 10^{-91}:\\ \;\;\;\;x - \frac{1}{\frac{\frac{t}{\sqrt{\log \left(\mathsf{fma}\left(y, \mathsf{expm1}\left(z\right), 1\right)\right)}}}{\sqrt{\log \left(\mathsf{fma}\left(y, \mathsf{expm1}\left(z\right), 1\right)\right)}}}\\ \mathbf{else}:\\ \;\;\;\;x - \mathsf{fma}\left(\frac{z \cdot y}{t}, 1, \frac{\log 1}{t}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019172 +o rules:numerics
(FPCore (x y z t)
  :name "System.Random.MWC.Distributions:truncatedExp from mwc-random-0.13.3.2"

  :herbie-target
  (if (< z -2.8874623088207947e+119) (- (- x (/ (/ (- 0.5) (* y t)) (* z z))) (* (/ (- 0.5) (* y t)) (/ (/ 2.0 z) (* z z)))) (- x (/ (log (+ 1.0 (* z y))) t)))

  (- x (/ (log (+ (- 1.0 y) (* y (exp z)))) t)))