Average Error: 6.4 → 5.1
Time: 5.7s
Precision: 64
\[\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}\]
↓
\[\begin{array}{l} \mathbf{if}\;y \le -5.7998173554975605 \cdot 10^{32}:\\ \;\;\;\;\frac{\frac{\frac{1}{y}}{x}}{1 + z \cdot z}\\ \mathbf{elif}\;y \le 643945125486439.25:\\ \;\;\;\;\frac{\frac{1}{x}}{\frac{\mathsf{fma}\left(z, z, 1\right)}{1} \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{x \cdot y}}{1 + z \cdot z}\\ \end{array}\]
\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}
↓
\begin{array}{l}
\mathbf{if}\;y \le -5.7998173554975605 \cdot 10^{32}:\\
\;\;\;\;\frac{\frac{\frac{1}{y}}{x}}{1 + z \cdot z}\\

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

\mathbf{else}:\\
\;\;\;\;\frac{\frac{1}{x \cdot y}}{1 + z \cdot z}\\

\end{array}
double f(double x, double y, double z) {
        double r419410 = 1.0;
        double r419411 = x;
        double r419412 = r419410 / r419411;
        double r419413 = y;
        double r419414 = z;
        double r419415 = r419414 * r419414;
        double r419416 = r419410 + r419415;
        double r419417 = r419413 * r419416;
        double r419418 = r419412 / r419417;
        return r419418;
}
↓
double f(double x, double y, double z) {
        double r419419 = y;
        double r419420 = -5.7998173554975605e+32;
        bool r419421 = r419419 <= r419420;
        double r419422 = 1.0;
        double r419423 = r419422 / r419419;
        double r419424 = x;
        double r419425 = r419423 / r419424;
        double r419426 = z;
        double r419427 = r419426 * r419426;
        double r419428 = r419422 + r419427;
        double r419429 = r419425 / r419428;
        double r419430 = 643945125486439.2;
        bool r419431 = r419419 <= r419430;
        double r419432 = 1.0;
        double r419433 = r419432 / r419424;
        double r419434 = fma(r419426, r419426, r419422);
        double r419435 = r419434 / r419422;
        double r419436 = r419435 * r419419;
        double r419437 = r419433 / r419436;
        double r419438 = r419424 * r419419;
        double r419439 = r419422 / r419438;
        double r419440 = r419439 / r419428;
        double r419441 = r419431 ? r419437 : r419440;
        double r419442 = r419421 ? r419429 : r419441;
        return r419442;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original6.4
Target5.8
Herbie5.1
\[\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.68074325056725162 \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 3 regimes

  2. if y < -5.7998173554975605e+32

    1. Initial program 4.2

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

    3. Applied associate-/r*1.2

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

    4. Simplified1.2

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

    if -5.7998173554975605e+32 < y < 643945125486439.2

    1. Initial program 8.9

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

    3. Applied associate-/r*11.6

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

    4. Simplified11.6

      \[\leadsto \frac{\color{blue}{\frac{\frac{1}{y}}{x}}}{1 + z \cdot z}\]
    5. Using strategy rm

    6. Applied div-inv11.6

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

    7. Applied associate-/l*11.6

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

    8. Simplified11.6

      \[\leadsto \frac{\frac{1}{\color{blue}{x \cdot y}}}{1 + z \cdot z}\]
    9. Using strategy rm

    10. Applied *-un-lft-identity11.6

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

    11. Applied times-frac11.6

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

    12. Applied associate-/l*9.0

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

    13. Simplified8.9

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

    if 643945125486439.2 < y

    1. Initial program 3.7

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

    3. Applied associate-/r*1.2

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

    4. Simplified1.2

      \[\leadsto \frac{\color{blue}{\frac{\frac{1}{y}}{x}}}{1 + z \cdot z}\]
    5. Using strategy rm

    6. Applied div-inv1.2

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

    7. Applied associate-/l*1.6

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

    8. Simplified1.5

      \[\leadsto \frac{\frac{1}{\color{blue}{x \cdot y}}}{1 + z \cdot z}\]
  3. Recombined 3 regimes into one program.

  4. Final simplification5.1

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

Reproduce

herbie shell --seed 2020034 +o rules:numerics
(FPCore (x y z)
  :name "Statistics.Distribution.CauchyLorentz:$cdensity from math-functions-0.1.5.2"
  :precision binary64

  :herbie-target
  (if (< (* y (+ 1 (* z z))) #f) (/ (/ 1 y) (* (+ 1 (* z z)) x)) (if (< (* y (+ 1 (* z z))) 8.680743250567252e+305) (/ (/ 1 x) (* (+ 1 (* z z)) y)) (/ (/ 1 y) (* (+ 1 (* z z)) x))))

  (/ (/ 1 x) (* y (+ 1 (* z z)))))