Average Error: 6.4 → 3.7
Time: 3.1m
Precision: 64
\[\frac{\frac{1.0}{x}}{y \cdot \left(1.0 + z \cdot z\right)}\]
\[\begin{array}{l} \mathbf{if}\;z \le -2.4299542345100543 \cdot 10^{+156}:\\ \;\;\;\;\frac{\frac{1.0}{\left(y \cdot z\right) \cdot z}}{x} - \frac{\frac{1.0}{x}}{\left(z \cdot z\right) \cdot \left(\left(z \cdot z\right) \cdot y\right)}\\ \mathbf{elif}\;z \le 8.656403785592857 \cdot 10^{+120}:\\ \;\;\;\;\frac{\frac{\frac{1.0}{y}}{\mathsf{fma}\left(z, z, 1.0\right)}}{x}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1.0}{\left(y \cdot z\right) \cdot z}}{x} - \frac{\frac{1.0}{x}}{\left(z \cdot z\right) \cdot \left(\left(z \cdot z\right) \cdot y\right)}\\ \end{array}\]
\frac{\frac{1.0}{x}}{y \cdot \left(1.0 + z \cdot z\right)}
\begin{array}{l}
\mathbf{if}\;z \le -2.4299542345100543 \cdot 10^{+156}:\\
\;\;\;\;\frac{\frac{1.0}{\left(y \cdot z\right) \cdot z}}{x} - \frac{\frac{1.0}{x}}{\left(z \cdot z\right) \cdot \left(\left(z \cdot z\right) \cdot y\right)}\\

\mathbf{elif}\;z \le 8.656403785592857 \cdot 10^{+120}:\\
\;\;\;\;\frac{\frac{\frac{1.0}{y}}{\mathsf{fma}\left(z, z, 1.0\right)}}{x}\\

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

\end{array}
double f(double x, double y, double z) {
        double r17048748 = 1.0;
        double r17048749 = x;
        double r17048750 = r17048748 / r17048749;
        double r17048751 = y;
        double r17048752 = z;
        double r17048753 = r17048752 * r17048752;
        double r17048754 = r17048748 + r17048753;
        double r17048755 = r17048751 * r17048754;
        double r17048756 = r17048750 / r17048755;
        return r17048756;
}

double f(double x, double y, double z) {
        double r17048757 = z;
        double r17048758 = -2.4299542345100543e+156;
        bool r17048759 = r17048757 <= r17048758;
        double r17048760 = 1.0;
        double r17048761 = y;
        double r17048762 = r17048761 * r17048757;
        double r17048763 = r17048762 * r17048757;
        double r17048764 = r17048760 / r17048763;
        double r17048765 = x;
        double r17048766 = r17048764 / r17048765;
        double r17048767 = r17048760 / r17048765;
        double r17048768 = r17048757 * r17048757;
        double r17048769 = r17048768 * r17048761;
        double r17048770 = r17048768 * r17048769;
        double r17048771 = r17048767 / r17048770;
        double r17048772 = r17048766 - r17048771;
        double r17048773 = 8.656403785592857e+120;
        bool r17048774 = r17048757 <= r17048773;
        double r17048775 = r17048760 / r17048761;
        double r17048776 = fma(r17048757, r17048757, r17048760);
        double r17048777 = r17048775 / r17048776;
        double r17048778 = r17048777 / r17048765;
        double r17048779 = r17048774 ? r17048778 : r17048772;
        double r17048780 = r17048759 ? r17048772 : r17048779;
        return r17048780;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

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

Derivation

  1. Split input into 2 regimes
  2. if z < -2.4299542345100543e+156 or 8.656403785592857e+120 < z

    1. Initial program 16.8

      \[\frac{\frac{1.0}{x}}{y \cdot \left(1.0 + z \cdot z\right)}\]
    2. Using strategy rm
    3. Applied div-inv16.8

      \[\leadsto \frac{\color{blue}{1.0 \cdot \frac{1}{x}}}{y \cdot \left(1.0 + z \cdot z\right)}\]
    4. Applied associate-/l*16.8

      \[\leadsto \color{blue}{\frac{1.0}{\frac{y \cdot \left(1.0 + z \cdot z\right)}{\frac{1}{x}}}}\]
    5. Simplified16.8

      \[\leadsto \frac{1.0}{\color{blue}{\left(y \cdot \mathsf{fma}\left(z, z, 1.0\right)\right) \cdot x}}\]
    6. Taylor expanded around inf 16.8

      \[\leadsto \color{blue}{1.0 \cdot \frac{1}{x \cdot \left({z}^{2} \cdot y\right)} - 1.0 \cdot \frac{1}{x \cdot \left({z}^{4} \cdot y\right)}}\]
    7. Simplified7.8

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

    if -2.4299542345100543e+156 < z < 8.656403785592857e+120

    1. Initial program 2.0

      \[\frac{\frac{1.0}{x}}{y \cdot \left(1.0 + z \cdot z\right)}\]
    2. Using strategy rm
    3. Applied div-inv2.1

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

      \[\leadsto \frac{1.0}{x} \cdot \color{blue}{\frac{1}{\mathsf{fma}\left(z, z, 1.0\right) \cdot y}}\]
    5. Using strategy rm
    6. Applied associate-*l/2.0

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

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

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -2.4299542345100543 \cdot 10^{+156}:\\ \;\;\;\;\frac{\frac{1.0}{\left(y \cdot z\right) \cdot z}}{x} - \frac{\frac{1.0}{x}}{\left(z \cdot z\right) \cdot \left(\left(z \cdot z\right) \cdot y\right)}\\ \mathbf{elif}\;z \le 8.656403785592857 \cdot 10^{+120}:\\ \;\;\;\;\frac{\frac{\frac{1.0}{y}}{\mathsf{fma}\left(z, z, 1.0\right)}}{x}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1.0}{\left(y \cdot z\right) \cdot z}}{x} - \frac{\frac{1.0}{x}}{\left(z \cdot z\right) \cdot \left(\left(z \cdot z\right) \cdot y\right)}\\ \end{array}\]

Reproduce

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