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

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

\end{array}
double f(double x, double y, double z, double t) {
        double r165683 = x;
        double r165684 = 1.0;
        double r165685 = y;
        double r165686 = r165684 - r165685;
        double r165687 = z;
        double r165688 = exp(r165687);
        double r165689 = r165685 * r165688;
        double r165690 = r165686 + r165689;
        double r165691 = log(r165690);
        double r165692 = t;
        double r165693 = r165691 / r165692;
        double r165694 = r165683 - r165693;
        return r165694;
}
↓
double f(double x, double y, double z, double t) {
        double r165695 = z;
        double r165696 = exp(r165695);
        double r165697 = 0.9999999999999999;
        bool r165698 = r165696 <= r165697;
        double r165699 = x;
        double r165700 = y;
        double r165701 = 1.0;
        double r165702 = r165701 - r165700;
        double r165703 = fma(r165696, r165700, r165702);
        double r165704 = log(r165703);
        double r165705 = 1.0;
        double r165706 = t;
        double r165707 = r165705 / r165706;
        double r165708 = r165704 * r165707;
        double r165709 = r165699 - r165708;
        double r165710 = cbrt(r165706);
        double r165711 = cbrt(r165710);
        double r165712 = r165711 * r165711;
        double r165713 = r165712 * r165711;
        double r165714 = r165710 * r165713;
        double r165715 = r165695 / r165714;
        double r165716 = r165700 / r165710;
        double r165717 = r165715 * r165716;
        double r165718 = log(r165701);
        double r165719 = r165718 / r165706;
        double r165720 = fma(r165701, r165717, r165719);
        double r165721 = r165699 - r165720;
        double r165722 = r165698 ? r165709 : r165721;
        return r165722;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original25.0
Target16.0
Herbie8.7
\[\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 (exp z) < 0.9999999999999999

    1. Initial program 12.3

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

    2. Simplified12.3

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

    4. Applied div-inv12.3

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

    if 0.9999999999999999 < (exp z)

    1. Initial program 31.0

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

    2. Simplified31.0

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

    3. Taylor expanded around 0 7.3

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

    4. Simplified7.3

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

    6. Applied add-cube-cbrt7.5

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

    7. Applied times-frac7.0

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

    9. Applied add-cube-cbrt7.0

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

  4. Final simplification8.7

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

Reproduce

herbie shell --seed 2019305 +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)))