Average Error: 6.4 → 4.1
Time: 2.9m
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{\frac{1.0}{x}}{z \cdot \left(y \cdot z\right)}\\ \mathbf{elif}\;\left(1.0 + z \cdot z\right) \cdot y \le 1.8567029449727538 \cdot 10^{+290}:\\ \;\;\;\;\frac{\frac{\frac{1.0}{y}}{1.0 + z \cdot z}}{x}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1.0}{z \cdot \left(y \cdot z\right)} - \frac{\frac{1.0}{y}}{\left(z \cdot z\right) \cdot \left(z \cdot z\right)}}{x}\\ \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{\frac{1.0}{x}}{z \cdot \left(y \cdot z\right)}\\

\mathbf{elif}\;\left(1.0 + z \cdot z\right) \cdot y \le 1.8567029449727538 \cdot 10^{+290}:\\
\;\;\;\;\frac{\frac{\frac{1.0}{y}}{1.0 + z \cdot z}}{x}\\

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

\end{array}
double f(double x, double y, double z) {
        double r15646719 = 1.0;
        double r15646720 = x;
        double r15646721 = r15646719 / r15646720;
        double r15646722 = y;
        double r15646723 = z;
        double r15646724 = r15646723 * r15646723;
        double r15646725 = r15646719 + r15646724;
        double r15646726 = r15646722 * r15646725;
        double r15646727 = r15646721 / r15646726;
        return r15646727;
}
↓
double f(double x, double y, double z) {
        double r15646728 = 1.0;
        double r15646729 = z;
        double r15646730 = r15646729 * r15646729;
        double r15646731 = r15646728 + r15646730;
        double r15646732 = y;
        double r15646733 = r15646731 * r15646732;
        double r15646734 = -inf.0;
        bool r15646735 = r15646733 <= r15646734;
        double r15646736 = x;
        double r15646737 = r15646728 / r15646736;
        double r15646738 = r15646732 * r15646729;
        double r15646739 = r15646729 * r15646738;
        double r15646740 = r15646737 / r15646739;
        double r15646741 = 1.8567029449727538e+290;
        bool r15646742 = r15646733 <= r15646741;
        double r15646743 = r15646728 / r15646732;
        double r15646744 = r15646743 / r15646731;
        double r15646745 = r15646744 / r15646736;
        double r15646746 = r15646728 / r15646739;
        double r15646747 = r15646730 * r15646730;
        double r15646748 = r15646743 / r15646747;
        double r15646749 = r15646746 - r15646748;
        double r15646750 = r15646749 / r15646736;
        double r15646751 = r15646742 ? r15646745 : r15646750;
        double r15646752 = r15646735 ? r15646740 : r15646751;
        return r15646752;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

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

  2. if (* y (+ 1.0 (* z z))) < -inf.0

    1. Initial program 19.6

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

    3. Applied div-inv19.6

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

    4. Taylor expanded around inf 19.6

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

    5. Simplified10.8

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

    if -inf.0 < (* y (+ 1.0 (* z z))) < 1.8567029449727538e+290

    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 div-inv0.4

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

    5. Applied associate-*l/0.3

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

    6. Simplified0.3

      \[\leadsto \frac{\color{blue}{\frac{1.0}{y \cdot \left(1.0 + z \cdot z\right)}}}{x}\]
    7. Using strategy rm

    8. Applied associate-/r*0.3

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

    if 1.8567029449727538e+290 < (* y (+ 1.0 (* z z)))

    1. Initial program 16.1

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

    3. Applied div-inv16.1

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

    5. Applied associate-*l/16.1

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

    6. Simplified16.1

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

    7. Taylor expanded around inf 18.5

      \[\leadsto \frac{\color{blue}{1.0 \cdot \frac{1}{{z}^{2} \cdot y} - 1.0 \cdot \frac{1}{{z}^{4} \cdot y}}}{x}\]

    8. Simplified11.8

      \[\leadsto \frac{\color{blue}{\frac{1.0}{\left(y \cdot z\right) \cdot z} - \frac{\frac{1.0}{y}}{\left(z \cdot z\right) \cdot \left(z \cdot z\right)}}}{x}\]
  3. Recombined 3 regimes into one program.

  4. Final simplification4.1

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

Reproduce

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