Average Error: 6.4 → 3.6
Time: 23.5s
Precision: 64
\[\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}\]
↓
\[\begin{array}{l} \mathbf{if}\;z \le -392280970.284367382526397705078125:\\ \;\;\;\;\frac{\frac{1}{x}}{\left(z \cdot y\right) \cdot z}\\ \mathbf{elif}\;z \le 7.814277317978629161433837029021119691196 \cdot 10^{142}:\\ \;\;\;\;1 \cdot \frac{\frac{\frac{1}{x}}{\mathsf{fma}\left(z, z, 1\right)}}{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 -392280970.284367382526397705078125:\\
\;\;\;\;\frac{\frac{1}{x}}{\left(z \cdot y\right) \cdot z}\\

\mathbf{elif}\;z \le 7.814277317978629161433837029021119691196 \cdot 10^{142}:\\
\;\;\;\;1 \cdot \frac{\frac{\frac{1}{x}}{\mathsf{fma}\left(z, z, 1\right)}}{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 r13169696 = 1.0;
        double r13169697 = x;
        double r13169698 = r13169696 / r13169697;
        double r13169699 = y;
        double r13169700 = z;
        double r13169701 = r13169700 * r13169700;
        double r13169702 = r13169696 + r13169701;
        double r13169703 = r13169699 * r13169702;
        double r13169704 = r13169698 / r13169703;
        return r13169704;
}
↓
double f(double x, double y, double z) {
        double r13169705 = z;
        double r13169706 = -392280970.2843674;
        bool r13169707 = r13169705 <= r13169706;
        double r13169708 = 1.0;
        double r13169709 = x;
        double r13169710 = r13169708 / r13169709;
        double r13169711 = y;
        double r13169712 = r13169705 * r13169711;
        double r13169713 = r13169712 * r13169705;
        double r13169714 = r13169710 / r13169713;
        double r13169715 = 7.814277317978629e+142;
        bool r13169716 = r13169705 <= r13169715;
        double r13169717 = 1.0;
        double r13169718 = r13169717 / r13169709;
        double r13169719 = fma(r13169705, r13169705, r13169708);
        double r13169720 = r13169718 / r13169719;
        double r13169721 = r13169720 / r13169711;
        double r13169722 = r13169708 * r13169721;
        double r13169723 = r13169716 ? r13169722 : r13169714;
        double r13169724 = r13169707 ? r13169714 : r13169723;
        return r13169724;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original6.4
Target5.7
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 < -392280970.2843674 or 7.814277317978629e+142 < z

    1. Initial program 13.7

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

    2. Taylor expanded around inf 13.9

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

    3. Simplified7.1

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

    if -392280970.2843674 < z < 7.814277317978629e+142

    1. Initial program 1.4

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

    3. Applied div-inv1.4

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

    4. Applied times-frac1.3

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

    5. Simplified1.3

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

    7. Applied div-inv1.3

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

    8. Applied associate-*l*1.3

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

    9. Simplified1.2

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

  4. Final simplification3.6

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

Reproduce

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