Average Error: 6.5 → 2.9
Time: 48.7s
Precision: 64
\[\frac{\frac{1.0}{x}}{y \cdot \left(1.0 + z \cdot z\right)}\]
\[\begin{array}{l} \mathbf{if}\;\left(1.0 + z \cdot z\right) \cdot y = -\infty:\\ \;\;\;\;\frac{1.0}{y} \cdot \left(\frac{1}{\left(z \cdot x\right) \cdot z} - \frac{\frac{1.0}{x}}{\left(z \cdot z\right) \cdot \left(z \cdot z\right)}\right)\\ \mathbf{elif}\;\left(1.0 + z \cdot z\right) \cdot y \le 7.715242497005938 \cdot 10^{+300}:\\ \;\;\;\;\frac{1}{x \cdot \frac{\mathsf{fma}\left(z, z, 1.0\right) \cdot y}{1.0}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1.0}{y} \cdot \left(\frac{1}{\left(z \cdot x\right) \cdot z} - \frac{\frac{1.0}{x}}{\left(z \cdot z\right) \cdot \left(z \cdot z\right)}\right)\\ \end{array}\]
\frac{\frac{1.0}{x}}{y \cdot \left(1.0 + z \cdot z\right)}
\begin{array}{l}
\mathbf{if}\;\left(1.0 + z \cdot z\right) \cdot y = -\infty:\\
\;\;\;\;\frac{1.0}{y} \cdot \left(\frac{1}{\left(z \cdot x\right) \cdot z} - \frac{\frac{1.0}{x}}{\left(z \cdot z\right) \cdot \left(z \cdot z\right)}\right)\\

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

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

\end{array}
double f(double x, double y, double z) {
        double r17640210 = 1.0;
        double r17640211 = x;
        double r17640212 = r17640210 / r17640211;
        double r17640213 = y;
        double r17640214 = z;
        double r17640215 = r17640214 * r17640214;
        double r17640216 = r17640210 + r17640215;
        double r17640217 = r17640213 * r17640216;
        double r17640218 = r17640212 / r17640217;
        return r17640218;
}

double f(double x, double y, double z) {
        double r17640219 = 1.0;
        double r17640220 = z;
        double r17640221 = r17640220 * r17640220;
        double r17640222 = r17640219 + r17640221;
        double r17640223 = y;
        double r17640224 = r17640222 * r17640223;
        double r17640225 = -inf.0;
        bool r17640226 = r17640224 <= r17640225;
        double r17640227 = r17640219 / r17640223;
        double r17640228 = 1.0;
        double r17640229 = x;
        double r17640230 = r17640220 * r17640229;
        double r17640231 = r17640230 * r17640220;
        double r17640232 = r17640228 / r17640231;
        double r17640233 = r17640219 / r17640229;
        double r17640234 = r17640221 * r17640221;
        double r17640235 = r17640233 / r17640234;
        double r17640236 = r17640232 - r17640235;
        double r17640237 = r17640227 * r17640236;
        double r17640238 = 7.715242497005938e+300;
        bool r17640239 = r17640224 <= r17640238;
        double r17640240 = fma(r17640220, r17640220, r17640219);
        double r17640241 = r17640240 * r17640223;
        double r17640242 = r17640241 / r17640219;
        double r17640243 = r17640229 * r17640242;
        double r17640244 = r17640228 / r17640243;
        double r17640245 = r17640239 ? r17640244 : r17640237;
        double r17640246 = r17640226 ? r17640237 : r17640245;
        return r17640246;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original6.5
Target5.9
Herbie2.9
\[\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 (* y (+ 1.0 (* z z))) < -inf.0 or 7.715242497005938e+300 < (* y (+ 1.0 (* z z)))

    1. Initial program 18.4

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

      \[\leadsto \frac{\color{blue}{1.0 \cdot \frac{1}{x}}}{y \cdot \left(1.0 + z \cdot z\right)}\]
    4. Applied times-frac14.8

      \[\leadsto \color{blue}{\frac{1.0}{y} \cdot \frac{\frac{1}{x}}{1.0 + z \cdot z}}\]
    5. Simplified14.8

      \[\leadsto \frac{1.0}{y} \cdot \color{blue}{\frac{\frac{1}{x}}{\mathsf{fma}\left(z, z, 1.0\right)}}\]
    6. Using strategy rm
    7. Applied clear-num14.8

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

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

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

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

    if -inf.0 < (* y (+ 1.0 (* z z))) < 7.715242497005938e+300

    1. Initial program 0.3

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

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

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

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(1.0 + z \cdot z\right) \cdot y = -\infty:\\ \;\;\;\;\frac{1.0}{y} \cdot \left(\frac{1}{\left(z \cdot x\right) \cdot z} - \frac{\frac{1.0}{x}}{\left(z \cdot z\right) \cdot \left(z \cdot z\right)}\right)\\ \mathbf{elif}\;\left(1.0 + z \cdot z\right) \cdot y \le 7.715242497005938 \cdot 10^{+300}:\\ \;\;\;\;\frac{1}{x \cdot \frac{\mathsf{fma}\left(z, z, 1.0\right) \cdot y}{1.0}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1.0}{y} \cdot \left(\frac{1}{\left(z \cdot x\right) \cdot z} - \frac{\frac{1.0}{x}}{\left(z \cdot z\right) \cdot \left(z \cdot z\right)}\right)\\ \end{array}\]

Reproduce

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