Average Error: 6.6 → 1.8
Time: 8.9s
Precision: binary64
Cost: 7240
\[ \begin{array}{c}[x, y] = \mathsf{sort}([x, y])\\ \end{array} \]
\[\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)} \]
\[\begin{array}{l} t_0 := y \cdot \left(x \cdot z\right)\\ \mathbf{if}\;z \leq -2.05 \cdot 10^{+82}:\\ \;\;\;\;\frac{1}{z \cdot t_0}\\ \mathbf{elif}\;z \leq 8 \cdot 10^{+93}:\\ \;\;\;\;\frac{\frac{\frac{1}{\mathsf{fma}\left(z, z, 1\right)}}{x}}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{t_0}}{z}\\ \end{array} \]
(FPCore (x y z) :precision binary64 (/ (/ 1.0 x) (* y (+ 1.0 (* z z)))))
(FPCore (x y z)
 :precision binary64
 (let* ((t_0 (* y (* x z))))
   (if (<= z -2.05e+82)
     (/ 1.0 (* z t_0))
     (if (<= z 8e+93) (/ (/ (/ 1.0 (fma z z 1.0)) x) y) (/ (/ 1.0 t_0) z)))))
double code(double x, double y, double z) {
	return (1.0 / x) / (y * (1.0 + (z * z)));
}
double code(double x, double y, double z) {
	double t_0 = y * (x * z);
	double tmp;
	if (z <= -2.05e+82) {
		tmp = 1.0 / (z * t_0);
	} else if (z <= 8e+93) {
		tmp = ((1.0 / fma(z, z, 1.0)) / x) / y;
	} else {
		tmp = (1.0 / t_0) / z;
	}
	return tmp;
}
function code(x, y, z)
	return Float64(Float64(1.0 / x) / Float64(y * Float64(1.0 + Float64(z * z))))
end
function code(x, y, z)
	t_0 = Float64(y * Float64(x * z))
	tmp = 0.0
	if (z <= -2.05e+82)
		tmp = Float64(1.0 / Float64(z * t_0));
	elseif (z <= 8e+93)
		tmp = Float64(Float64(Float64(1.0 / fma(z, z, 1.0)) / x) / y);
	else
		tmp = Float64(Float64(1.0 / t_0) / z);
	end
	return tmp
end
code[x_, y_, z_] := N[(N[(1.0 / x), $MachinePrecision] / N[(y * N[(1.0 + N[(z * z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
code[x_, y_, z_] := Block[{t$95$0 = N[(y * N[(x * z), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[z, -2.05e+82], N[(1.0 / N[(z * t$95$0), $MachinePrecision]), $MachinePrecision], If[LessEqual[z, 8e+93], N[(N[(N[(1.0 / N[(z * z + 1.0), $MachinePrecision]), $MachinePrecision] / x), $MachinePrecision] / y), $MachinePrecision], N[(N[(1.0 / t$95$0), $MachinePrecision] / z), $MachinePrecision]]]]
\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}
\begin{array}{l}
t_0 := y \cdot \left(x \cdot z\right)\\
\mathbf{if}\;z \leq -2.05 \cdot 10^{+82}:\\
\;\;\;\;\frac{1}{z \cdot t_0}\\

\mathbf{elif}\;z \leq 8 \cdot 10^{+93}:\\
\;\;\;\;\frac{\frac{\frac{1}{\mathsf{fma}\left(z, z, 1\right)}}{x}}{y}\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{1}{t_0}}{z}\\


\end{array}

Error

Target

Original6.6
Target5.3
Herbie1.8
\[\begin{array}{l} \mathbf{if}\;y \cdot \left(1 + z \cdot z\right) < -\infty:\\ \;\;\;\;\frac{\frac{1}{y}}{\left(1 + z \cdot z\right) \cdot x}\\ \mathbf{elif}\;y \cdot \left(1 + z \cdot z\right) < 8.680743250567252 \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 z < -2.04999999999999998e82

    1. Initial program 16.1

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

      \[\leadsto \color{blue}{\frac{1}{x \cdot \left(y \cdot \mathsf{fma}\left(z, z, 1\right)\right)}} \]
      Proof
      (/.f64 1 (*.f64 x (*.f64 y (fma.f64 z z 1)))): 0 points increase in error, 0 points decrease in error
      (/.f64 1 (*.f64 x (*.f64 y (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z z) 1))))): 0 points increase in error, 0 points decrease in error
      (/.f64 1 (*.f64 x (*.f64 y (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 z z)))))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 1 x) (*.f64 y (+.f64 1 (*.f64 z z))))): 32 points increase in error, 29 points decrease in error
    3. Taylor expanded in z around inf 15.9

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

      \[\leadsto \frac{1}{\color{blue}{z \cdot \left(\left(z \cdot x\right) \cdot y\right)}} \]
      Proof
      (*.f64 z (*.f64 (*.f64 z x) y)): 0 points increase in error, 0 points decrease in error
      (*.f64 z (Rewrite<= associate-*r*_binary64 (*.f64 z (*.f64 x y)))): 41 points increase in error, 18 points decrease in error
      (*.f64 z (*.f64 z (Rewrite<= *-commutative_binary64 (*.f64 y x)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z z) (*.f64 y x))): 35 points increase in error, 19 points decrease in error
      (*.f64 (*.f64 z z) (Rewrite=> *-commutative_binary64 (*.f64 x y))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 z z) x) y)): 23 points increase in error, 36 points decrease in error
      (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 z 2)) x) y): 0 points increase in error, 0 points decrease in error
      (Rewrite<= *-commutative_binary64 (*.f64 y (*.f64 (pow.f64 z 2) x))): 0 points increase in error, 0 points decrease in error

    if -2.04999999999999998e82 < z < 8.00000000000000035e93

    1. Initial program 1.1

      \[\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)} \]
    2. Simplified1.4

      \[\leadsto \color{blue}{\frac{1}{x \cdot \left(y \cdot \mathsf{fma}\left(z, z, 1\right)\right)}} \]
      Proof
      (/.f64 1 (*.f64 x (*.f64 y (fma.f64 z z 1)))): 0 points increase in error, 0 points decrease in error
      (/.f64 1 (*.f64 x (*.f64 y (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z z) 1))))): 0 points increase in error, 0 points decrease in error
      (/.f64 1 (*.f64 x (*.f64 y (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 z z)))))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 1 x) (*.f64 y (+.f64 1 (*.f64 z z))))): 32 points increase in error, 29 points decrease in error
    3. Taylor expanded in x around 0 1.6

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

      \[\leadsto \color{blue}{\frac{\frac{\frac{1}{\mathsf{fma}\left(z, z, 1\right)}}{x}}{y}} \]
      Proof
      (/.f64 (/.f64 (/.f64 1 (fma.f64 z z 1)) x) y): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 (fma.f64 z z 1) x))) y): 5 points increase in error, 8 points decrease in error
      (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 (*.f64 (fma.f64 z z 1) x) y))): 30 points increase in error, 24 points decrease in error
      (/.f64 1 (*.f64 (*.f64 (Rewrite=> fma-udef_binary64 (+.f64 (*.f64 z z) 1)) x) y)): 0 points increase in error, 0 points decrease in error
      (/.f64 1 (*.f64 (*.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 z 2)) 1) x) y)): 0 points increase in error, 0 points decrease in error
      (/.f64 1 (Rewrite<= *-commutative_binary64 (*.f64 y (*.f64 (+.f64 (pow.f64 z 2) 1) x)))): 0 points increase in error, 0 points decrease in error

    if 8.00000000000000035e93 < z

    1. Initial program 15.1

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

      \[\leadsto \color{blue}{\frac{1}{x \cdot \left(y \cdot \mathsf{fma}\left(z, z, 1\right)\right)}} \]
      Proof
      (/.f64 1 (*.f64 x (*.f64 y (fma.f64 z z 1)))): 0 points increase in error, 0 points decrease in error
      (/.f64 1 (*.f64 x (*.f64 y (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z z) 1))))): 0 points increase in error, 0 points decrease in error
      (/.f64 1 (*.f64 x (*.f64 y (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 z z)))))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 1 x) (*.f64 y (+.f64 1 (*.f64 z z))))): 32 points increase in error, 29 points decrease in error
    3. Taylor expanded in z around inf 15.8

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

      \[\leadsto \color{blue}{\frac{\frac{\frac{1}{z \cdot x}}{y}}{z}} \]
      Proof
      (/.f64 (/.f64 (/.f64 1 (*.f64 z x)) y) z): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 (*.f64 z x) y))) z): 17 points increase in error, 25 points decrease in error
      (/.f64 (/.f64 1 (Rewrite<= associate-*r*_binary64 (*.f64 z (*.f64 x y)))) z): 21 points increase in error, 28 points decrease in error
      (/.f64 (/.f64 1 (*.f64 z (Rewrite<= *-commutative_binary64 (*.f64 y x)))) z): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 1 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 y x) z))) z): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 (*.f64 (*.f64 y x) z) z))): 28 points increase in error, 21 points decrease in error
      (/.f64 1 (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 y x) (*.f64 z z)))): 47 points increase in error, 10 points decrease in error
      (/.f64 1 (Rewrite=> associate-*l*_binary64 (*.f64 y (*.f64 x (*.f64 z z))))): 20 points increase in error, 26 points decrease in error
      (/.f64 1 (*.f64 y (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 z z) x)))): 0 points increase in error, 0 points decrease in error
      (/.f64 1 (*.f64 y (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 z 2)) x))): 0 points increase in error, 0 points decrease in error
    5. Taylor expanded in z around 0 2.8

      \[\leadsto \frac{\color{blue}{\frac{1}{y \cdot \left(z \cdot x\right)}}}{z} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification1.8

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -2.05 \cdot 10^{+82}:\\ \;\;\;\;\frac{1}{z \cdot \left(y \cdot \left(x \cdot z\right)\right)}\\ \mathbf{elif}\;z \leq 8 \cdot 10^{+93}:\\ \;\;\;\;\frac{\frac{\frac{1}{\mathsf{fma}\left(z, z, 1\right)}}{x}}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{y \cdot \left(x \cdot z\right)}}{z}\\ \end{array} \]

Alternatives

Alternative 1
Error1.6
Cost13632
\[\frac{\frac{1}{x}}{\mathsf{hypot}\left(1, z\right)} \cdot \frac{\frac{1}{y}}{\mathsf{hypot}\left(1, z\right)} \]
Alternative 2
Error1.9
Cost972
\[\begin{array}{l} t_0 := y \cdot \left(x \cdot z\right)\\ \mathbf{if}\;z \leq -4.6 \cdot 10^{+26}:\\ \;\;\;\;\frac{1}{z \cdot t_0}\\ \mathbf{elif}\;z \leq 9.6 \cdot 10^{+35}:\\ \;\;\;\;\frac{\frac{1}{x}}{y \cdot \left(1 + z \cdot z\right)}\\ \mathbf{elif}\;z \leq 2.55 \cdot 10^{+119}:\\ \;\;\;\;\frac{\frac{1}{z \cdot \left(x \cdot z\right)}}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{t_0}}{z}\\ \end{array} \]
Alternative 3
Error1.9
Cost972
\[\begin{array}{l} t_0 := y \cdot \left(x \cdot z\right)\\ \mathbf{if}\;z \leq -2.05 \cdot 10^{+40}:\\ \;\;\;\;\frac{1}{z \cdot t_0}\\ \mathbf{elif}\;z \leq 1.4 \cdot 10^{+33}:\\ \;\;\;\;\frac{\frac{\frac{1}{x}}{y}}{1 + z \cdot z}\\ \mathbf{elif}\;z \leq 2.05 \cdot 10^{+119}:\\ \;\;\;\;\frac{\frac{1}{z \cdot \left(x \cdot z\right)}}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{t_0}}{z}\\ \end{array} \]
Alternative 4
Error2.0
Cost968
\[\begin{array}{l} t_0 := y \cdot \left(x \cdot z\right)\\ \mathbf{if}\;z \leq -2.85 \cdot 10^{+29}:\\ \;\;\;\;\frac{1}{z \cdot t_0}\\ \mathbf{elif}\;z \leq 3.6 \cdot 10^{+75}:\\ \;\;\;\;\frac{1}{x \cdot \left(y + y \cdot \left(z \cdot z\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{t_0}}{z}\\ \end{array} \]
Alternative 5
Error2.1
Cost964
\[\begin{array}{l} \mathbf{if}\;z \cdot z \leq 5 \cdot 10^{+238}:\\ \;\;\;\;\frac{1}{y \cdot \left(x + z \cdot \left(x \cdot z\right)\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{y \cdot \left(x \cdot z\right)}}{z}\\ \end{array} \]
Alternative 6
Error4.7
Cost840
\[\begin{array}{l} t_0 := \frac{1}{y \cdot \left(z \cdot \left(x \cdot z\right)\right)}\\ \mathbf{if}\;z \leq -1:\\ \;\;\;\;t_0\\ \mathbf{elif}\;z \leq 1:\\ \;\;\;\;\frac{\frac{1}{y}}{x}\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Alternative 7
Error2.5
Cost836
\[\begin{array}{l} \mathbf{if}\;z \cdot z \leq 5 \cdot 10^{-5}:\\ \;\;\;\;\frac{\frac{1}{y}}{x}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{z \cdot \left(y \cdot \left(x \cdot z\right)\right)}\\ \end{array} \]
Alternative 8
Error2.4
Cost836
\[\begin{array}{l} \mathbf{if}\;z \cdot z \leq 5 \cdot 10^{-5}:\\ \;\;\;\;\frac{\frac{1 - z \cdot z}{x}}{y}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{z \cdot \left(y \cdot \left(x \cdot z\right)\right)}\\ \end{array} \]
Alternative 9
Error29.0
Cost320
\[\frac{1}{x \cdot y} \]
Alternative 10
Error29.0
Cost320
\[\frac{\frac{1}{x}}{y} \]
Alternative 11
Error29.0
Cost320
\[\frac{\frac{1}{y}}{x} \]

Error

Reproduce

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

  :herbie-target
  (if (< (* y (+ 1.0 (* z z))) (- INFINITY)) (/ (/ 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)))))