Average Error: 6.4 → 1.7
Time: 3.0m
Precision: 64
\[\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}\]
↓
\[\begin{array}{l} \mathbf{if}\;z \le -4.351344512564880231704075632209688537162 \cdot 10^{97}:\\ \;\;\;\;\frac{1}{\left(z \cdot y\right) \cdot \left(x \cdot z\right)}\\ \mathbf{elif}\;z \le 1.424575886381938860449509537437903797365 \cdot 10^{84}:\\ \;\;\;\;\frac{\frac{\frac{1}{x}}{y}}{\mathsf{fma}\left(z, z, 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\left(z \cdot y\right) \cdot \left(x \cdot z\right)}\\ \end{array}\]
\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}
↓
\begin{array}{l}
\mathbf{if}\;z \le -4.351344512564880231704075632209688537162 \cdot 10^{97}:\\
\;\;\;\;\frac{1}{\left(z \cdot y\right) \cdot \left(x \cdot z\right)}\\

\mathbf{elif}\;z \le 1.424575886381938860449509537437903797365 \cdot 10^{84}:\\
\;\;\;\;\frac{\frac{\frac{1}{x}}{y}}{\mathsf{fma}\left(z, z, 1\right)}\\

\mathbf{else}:\\
\;\;\;\;\frac{1}{\left(z \cdot y\right) \cdot \left(x \cdot z\right)}\\

\end{array}
double f(double x, double y, double z) {
        double r13521512 = 1.0;
        double r13521513 = x;
        double r13521514 = r13521512 / r13521513;
        double r13521515 = y;
        double r13521516 = z;
        double r13521517 = r13521516 * r13521516;
        double r13521518 = r13521512 + r13521517;
        double r13521519 = r13521515 * r13521518;
        double r13521520 = r13521514 / r13521519;
        return r13521520;
}
↓
double f(double x, double y, double z) {
        double r13521521 = z;
        double r13521522 = -4.35134451256488e+97;
        bool r13521523 = r13521521 <= r13521522;
        double r13521524 = 1.0;
        double r13521525 = y;
        double r13521526 = r13521521 * r13521525;
        double r13521527 = x;
        double r13521528 = r13521527 * r13521521;
        double r13521529 = r13521526 * r13521528;
        double r13521530 = r13521524 / r13521529;
        double r13521531 = 1.4245758863819389e+84;
        bool r13521532 = r13521521 <= r13521531;
        double r13521533 = r13521524 / r13521527;
        double r13521534 = r13521533 / r13521525;
        double r13521535 = fma(r13521521, r13521521, r13521524);
        double r13521536 = r13521534 / r13521535;
        double r13521537 = r13521532 ? r13521536 : r13521530;
        double r13521538 = r13521523 ? r13521530 : r13521537;
        return r13521538;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original6.4
Target5.7
Herbie1.7
\[\begin{array}{l} \mathbf{if}\;y \cdot \left(1 + z \cdot z\right) \lt -\infty:\\ \;\;\;\;\frac{\frac{1}{y}}{\left(1 + z \cdot z\right) \cdot x}\\ \mathbf{elif}\;y \cdot \left(1 + z \cdot z\right) \lt 8.680743250567251617010582226806563373013 \cdot 10^{305}:\\ \;\;\;\;\frac{\frac{1}{x}}{\left(1 + z \cdot z\right) \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{y}}{\left(1 + z \cdot z\right) \cdot x}\\ \end{array}\]

Derivation

  1. Split input into 2 regimes

  2. if z < -4.35134451256488e+97 or 1.4245758863819389e+84 < z

    1. Initial program 14.9

      \[\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}\]

    2. Simplified15.1

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

    4. Applied *-un-lft-identity15.1

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

    5. Applied div-inv15.1

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

    6. Applied times-frac14.8

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

    7. Simplified14.8

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

    8. Taylor expanded around inf 15.0

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

    9. Simplified2.8

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

    if -4.35134451256488e+97 < z < 1.4245758863819389e+84

    1. Initial program 1.2

      \[\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}\]

    2. Simplified1.1

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

  4. Final simplification1.7

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -4.351344512564880231704075632209688537162 \cdot 10^{97}:\\ \;\;\;\;\frac{1}{\left(z \cdot y\right) \cdot \left(x \cdot z\right)}\\ \mathbf{elif}\;z \le 1.424575886381938860449509537437903797365 \cdot 10^{84}:\\ \;\;\;\;\frac{\frac{\frac{1}{x}}{y}}{\mathsf{fma}\left(z, z, 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\left(z \cdot y\right) \cdot \left(x \cdot z\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2019168 +o rules:numerics
(FPCore (x y z)
  :name "Statistics.Distribution.CauchyLorentz:$cdensity from math-functions-0.1.5.2"

  :herbie-target
  (if (< (* y (+ 1.0 (* z z))) -inf.0) (/ (/ 1.0 y) (* (+ 1.0 (* z z)) x)) (if (< (* y (+ 1.0 (* z z))) 8.680743250567252e+305) (/ (/ 1.0 x) (* (+ 1.0 (* z z)) y)) (/ (/ 1.0 y) (* (+ 1.0 (* z z)) x))))

  (/ (/ 1.0 x) (* y (+ 1.0 (* z z)))))