Average Error: 6.3 → 3.6
Time: 57.0s
Precision: 64
\[\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}\]
↓
\[\begin{array}{l} \mathbf{if}\;z \cdot z \le 3.345732198298465416987509255748494394258 \cdot 10^{145}:\\ \;\;\;\;\frac{\frac{\frac{1}{x}}{y}}{\mathsf{fma}\left(z, z, 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{x}}{\left(y \cdot z\right) \cdot z}\\ \end{array}\]
\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}
↓
\begin{array}{l}
\mathbf{if}\;z \cdot z \le 3.345732198298465416987509255748494394258 \cdot 10^{145}:\\
\;\;\;\;\frac{\frac{\frac{1}{x}}{y}}{\mathsf{fma}\left(z, z, 1\right)}\\

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

\end{array}
double f(double x, double y, double z) {
        double r13230397 = 1.0;
        double r13230398 = x;
        double r13230399 = r13230397 / r13230398;
        double r13230400 = y;
        double r13230401 = z;
        double r13230402 = r13230401 * r13230401;
        double r13230403 = r13230397 + r13230402;
        double r13230404 = r13230400 * r13230403;
        double r13230405 = r13230399 / r13230404;
        return r13230405;
}
↓
double f(double x, double y, double z) {
        double r13230406 = z;
        double r13230407 = r13230406 * r13230406;
        double r13230408 = 3.3457321982984654e+145;
        bool r13230409 = r13230407 <= r13230408;
        double r13230410 = 1.0;
        double r13230411 = x;
        double r13230412 = r13230410 / r13230411;
        double r13230413 = y;
        double r13230414 = r13230412 / r13230413;
        double r13230415 = fma(r13230406, r13230406, r13230410);
        double r13230416 = r13230414 / r13230415;
        double r13230417 = r13230413 * r13230406;
        double r13230418 = r13230417 * r13230406;
        double r13230419 = r13230412 / r13230418;
        double r13230420 = r13230409 ? r13230416 : r13230419;
        return r13230420;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original6.3
Target5.5
Herbie3.6
\[\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 z) < 3.3457321982984654e+145

    1. Initial program 1.0

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

    2. Simplified0.9

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

    if 3.3457321982984654e+145 < (* z z)

    1. Initial program 14.0

      \[\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}\]
    2. Using strategy rm

    3. Applied add-cube-cbrt14.2

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

    4. Taylor expanded around inf 14.1

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

    5. Simplified7.4

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

  4. Final simplification3.6

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot z \le 3.345732198298465416987509255748494394258 \cdot 10^{145}:\\ \;\;\;\;\frac{\frac{\frac{1}{x}}{y}}{\mathsf{fma}\left(z, z, 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{x}}{\left(y \cdot z\right) \cdot z}\\ \end{array}\]

Reproduce

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