Average Error: 25.0 → 9.0
Time: 24.8s
Precision: 64
\[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
↓
\[\begin{array}{l} \mathbf{if}\;z \le -1.618024548704766232621305821308410610726 \cdot 10^{-12}:\\ \;\;\;\;x - \frac{1}{\frac{t}{\log \left(\mathsf{fma}\left(y, e^{z}, 1 - y\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;x - \mathsf{fma}\left(1, \frac{z}{t} \cdot y, \mathsf{fma}\left(\frac{\log \left(e^{z \cdot \left(z \cdot y\right)}\right)}{t}, 0.5, \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 -1.618024548704766232621305821308410610726 \cdot 10^{-12}:\\
\;\;\;\;x - \frac{1}{\frac{t}{\log \left(\mathsf{fma}\left(y, e^{z}, 1 - y\right)\right)}}\\

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

\end{array}
double f(double x, double y, double z, double t) {
        double r11933675 = x;
        double r11933676 = 1.0;
        double r11933677 = y;
        double r11933678 = r11933676 - r11933677;
        double r11933679 = z;
        double r11933680 = exp(r11933679);
        double r11933681 = r11933677 * r11933680;
        double r11933682 = r11933678 + r11933681;
        double r11933683 = log(r11933682);
        double r11933684 = t;
        double r11933685 = r11933683 / r11933684;
        double r11933686 = r11933675 - r11933685;
        return r11933686;
}
↓
double f(double x, double y, double z, double t) {
        double r11933687 = z;
        double r11933688 = -1.6180245487047662e-12;
        bool r11933689 = r11933687 <= r11933688;
        double r11933690 = x;
        double r11933691 = 1.0;
        double r11933692 = t;
        double r11933693 = y;
        double r11933694 = exp(r11933687);
        double r11933695 = 1.0;
        double r11933696 = r11933695 - r11933693;
        double r11933697 = fma(r11933693, r11933694, r11933696);
        double r11933698 = log(r11933697);
        double r11933699 = r11933692 / r11933698;
        double r11933700 = r11933691 / r11933699;
        double r11933701 = r11933690 - r11933700;
        double r11933702 = r11933687 / r11933692;
        double r11933703 = r11933702 * r11933693;
        double r11933704 = r11933687 * r11933693;
        double r11933705 = r11933687 * r11933704;
        double r11933706 = exp(r11933705);
        double r11933707 = log(r11933706);
        double r11933708 = r11933707 / r11933692;
        double r11933709 = 0.5;
        double r11933710 = log(r11933695);
        double r11933711 = r11933710 / r11933692;
        double r11933712 = fma(r11933708, r11933709, r11933711);
        double r11933713 = fma(r11933695, r11933703, r11933712);
        double r11933714 = r11933690 - r11933713;
        double r11933715 = r11933689 ? r11933701 : r11933714;
        return r11933715;
}

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.6180245487047662e-12

    1. Initial program 12.0

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

    2. Simplified12.0

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

    4. Applied clear-num12.0

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

    if -1.6180245487047662e-12 < z

    1. Initial program 30.8

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

    2. Simplified30.8

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

    3. Taylor expanded around 0 6.9

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

    4. Simplified6.1

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

    6. Applied add-log-exp7.6

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

  4. Final simplification9.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.618024548704766232621305821308410610726 \cdot 10^{-12}:\\ \;\;\;\;x - \frac{1}{\frac{t}{\log \left(\mathsf{fma}\left(y, e^{z}, 1 - y\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;x - \mathsf{fma}\left(1, \frac{z}{t} \cdot y, \mathsf{fma}\left(\frac{\log \left(e^{z \cdot \left(z \cdot y\right)}\right)}{t}, 0.5, \frac{\log 1}{t}\right)\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)))