Average Error: 6.2 → 4.4
Time: 46.5s
Precision: 64
\[\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}\]
↓
\[\begin{array}{l} \mathbf{if}\;z \le -3.388362437333713663189698402008227229826 \cdot 10^{192}:\\ \;\;\;\;\frac{\frac{1}{x}}{\left(z \cdot y\right) \cdot z}\\ \mathbf{elif}\;z \le 98451557.57387264072895050048828125:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{fma}\left(z, z, 1\right)} \cdot \left(x \cdot \sqrt{\mathsf{fma}\left(z, z, 1\right)}\right)} \cdot \frac{1}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{x}}{\left(z \cdot y\right) \cdot z}\\ \end{array}\]
\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}
↓
\begin{array}{l}
\mathbf{if}\;z \le -3.388362437333713663189698402008227229826 \cdot 10^{192}:\\
\;\;\;\;\frac{\frac{1}{x}}{\left(z \cdot y\right) \cdot z}\\

\mathbf{elif}\;z \le 98451557.57387264072895050048828125:\\
\;\;\;\;\frac{1}{\sqrt{\mathsf{fma}\left(z, z, 1\right)} \cdot \left(x \cdot \sqrt{\mathsf{fma}\left(z, z, 1\right)}\right)} \cdot \frac{1}{y}\\

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

\end{array}
double f(double x, double y, double z) {
        double r15879440 = 1.0;
        double r15879441 = x;
        double r15879442 = r15879440 / r15879441;
        double r15879443 = y;
        double r15879444 = z;
        double r15879445 = r15879444 * r15879444;
        double r15879446 = r15879440 + r15879445;
        double r15879447 = r15879443 * r15879446;
        double r15879448 = r15879442 / r15879447;
        return r15879448;
}
↓
double f(double x, double y, double z) {
        double r15879449 = z;
        double r15879450 = -3.3883624373337137e+192;
        bool r15879451 = r15879449 <= r15879450;
        double r15879452 = 1.0;
        double r15879453 = x;
        double r15879454 = r15879452 / r15879453;
        double r15879455 = y;
        double r15879456 = r15879449 * r15879455;
        double r15879457 = r15879456 * r15879449;
        double r15879458 = r15879454 / r15879457;
        double r15879459 = 98451557.57387264;
        bool r15879460 = r15879449 <= r15879459;
        double r15879461 = fma(r15879449, r15879449, r15879452);
        double r15879462 = sqrt(r15879461);
        double r15879463 = r15879453 * r15879462;
        double r15879464 = r15879462 * r15879463;
        double r15879465 = r15879452 / r15879464;
        double r15879466 = 1.0;
        double r15879467 = r15879466 / r15879455;
        double r15879468 = r15879465 * r15879467;
        double r15879469 = r15879460 ? r15879468 : r15879458;
        double r15879470 = r15879451 ? r15879458 : r15879469;
        return r15879470;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original6.2
Target5.6
Herbie4.4
\[\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 < -3.3883624373337137e+192 or 98451557.57387264 < z

    1. Initial program 12.3

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

    3. Applied add-sqr-sqrt12.3

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

    4. Applied associate-*r*12.3

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

    5. Taylor expanded around inf 12.4

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

    6. Simplified7.1

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

    if -3.3883624373337137e+192 < z < 98451557.57387264

    1. Initial program 2.8

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

    3. Applied *-un-lft-identity2.8

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

    4. Applied *-un-lft-identity2.8

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

    5. Applied times-frac2.8

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

    6. Applied times-frac2.7

      \[\leadsto \color{blue}{\frac{\frac{1}{1}}{y} \cdot \frac{\frac{1}{x}}{1 + z \cdot z}}\]

    7. Simplified2.7

      \[\leadsto \color{blue}{\frac{1}{y}} \cdot \frac{\frac{1}{x}}{1 + z \cdot z}\]

    8. Simplified2.8

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

    10. Applied add-sqr-sqrt2.9

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

    11. Applied associate-*l*2.9

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

  4. Final simplification4.4

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

Reproduce

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