Average Error: 6.3 → 3.6
Time: 55.9s
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 r11404035 = 1.0;
        double r11404036 = x;
        double r11404037 = r11404035 / r11404036;
        double r11404038 = y;
        double r11404039 = z;
        double r11404040 = r11404039 * r11404039;
        double r11404041 = r11404035 + r11404040;
        double r11404042 = r11404038 * r11404041;
        double r11404043 = r11404037 / r11404042;
        return r11404043;
}
↓
double f(double x, double y, double z) {
        double r11404044 = z;
        double r11404045 = r11404044 * r11404044;
        double r11404046 = 3.3457321982984654e+145;
        bool r11404047 = r11404045 <= r11404046;
        double r11404048 = 1.0;
        double r11404049 = x;
        double r11404050 = r11404048 / r11404049;
        double r11404051 = y;
        double r11404052 = r11404050 / r11404051;
        double r11404053 = fma(r11404044, r11404044, r11404048);
        double r11404054 = r11404052 / r11404053;
        double r11404055 = r11404051 * r11404044;
        double r11404056 = r11404055 * r11404044;
        double r11404057 = r11404050 / r11404056;
        double r11404058 = r11404047 ? r11404054 : r11404057;
        return r11404058;
}

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)))))