Average Error: 24.7 → 8.5
Time: 21.5s
Precision: 64
\[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
↓
\[\begin{array}{l} \mathbf{if}\;z \le -7.557323451675197409924132573708902840764 \cdot 10^{-160}:\\ \;\;\;\;x - \frac{3}{\frac{t}{\log \left(\sqrt[3]{\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)}\right)}}\\ \mathbf{else}:\\ \;\;\;\;x - \mathsf{fma}\left(1, \frac{z \cdot y}{t}, \mathsf{fma}\left(0.5, \frac{{z}^{2} \cdot y}{t}, \frac{\log 1}{t}\right)\right)\\ \end{array}\]
x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}
↓
\begin{array}{l}
\mathbf{if}\;z \le -7.557323451675197409924132573708902840764 \cdot 10^{-160}:\\
\;\;\;\;x - \frac{3}{\frac{t}{\log \left(\sqrt[3]{\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)}\right)}}\\

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

\end{array}
double f(double x, double y, double z, double t) {
        double r167293 = x;
        double r167294 = 1.0;
        double r167295 = y;
        double r167296 = r167294 - r167295;
        double r167297 = z;
        double r167298 = exp(r167297);
        double r167299 = r167295 * r167298;
        double r167300 = r167296 + r167299;
        double r167301 = log(r167300);
        double r167302 = t;
        double r167303 = r167301 / r167302;
        double r167304 = r167293 - r167303;
        return r167304;
}
↓
double f(double x, double y, double z, double t) {
        double r167305 = z;
        double r167306 = -7.557323451675197e-160;
        bool r167307 = r167305 <= r167306;
        double r167308 = x;
        double r167309 = 3.0;
        double r167310 = t;
        double r167311 = expm1(r167305);
        double r167312 = y;
        double r167313 = 1.0;
        double r167314 = fma(r167311, r167312, r167313);
        double r167315 = cbrt(r167314);
        double r167316 = log(r167315);
        double r167317 = r167310 / r167316;
        double r167318 = r167309 / r167317;
        double r167319 = r167308 - r167318;
        double r167320 = r167305 * r167312;
        double r167321 = r167320 / r167310;
        double r167322 = 0.5;
        double r167323 = 2.0;
        double r167324 = pow(r167305, r167323);
        double r167325 = r167324 * r167312;
        double r167326 = r167325 / r167310;
        double r167327 = log(r167313);
        double r167328 = r167327 / r167310;
        double r167329 = fma(r167322, r167326, r167328);
        double r167330 = fma(r167313, r167321, r167329);
        double r167331 = r167308 - r167330;
        double r167332 = r167307 ? r167319 : r167331;
        return r167332;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original24.7
Target15.9
Herbie8.5
\[\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 < -7.557323451675197e-160

    1. Initial program 17.7

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

    2. Simplified11.0

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

      \[\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-cube-cbrt11.1

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

    7. Applied log-prod11.1

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

    8. Simplified11.1

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

    10. Applied distribute-lft1-in11.1

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

    11. Applied *-un-lft-identity11.1

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

    12. Applied times-frac11.1

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

    13. Applied associate-/r*11.1

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

    14. Simplified11.1

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

    if -7.557323451675197e-160 < z

    1. Initial program 31.0

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

    2. Simplified11.1

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

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

    4. Simplified6.3

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

  4. Final simplification8.5

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

Reproduce

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

  :herbie-target
  (if (< z -2.88746230882079466e119) (- (- x (/ (/ (- 0.5) (* y t)) (* z z))) (* (/ (- 0.5) (* y t)) (/ (/ 2 z) (* z z)))) (- x (/ (log (+ 1 (* z y))) t)))

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