Statistics.Math.RootFinding:ridders from math-functions-0.1.5.2

Percentage Accurate: 61.3% → 92.2%
Time: 8.2s
Alternatives: 7
Speedup: 4.1×

Specification

?
\[\begin{array}{l} \\ \frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \end{array} \]
(FPCore (x y z t a)
 :precision binary64
 (/ (* (* x y) z) (sqrt (- (* z z) (* t a)))))
double code(double x, double y, double z, double t, double a) {
	return ((x * y) * z) / sqrt(((z * z) - (t * a)));
}
real(8) function code(x, y, z, t, a)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    code = ((x * y) * z) / sqrt(((z * z) - (t * a)))
end function
public static double code(double x, double y, double z, double t, double a) {
	return ((x * y) * z) / Math.sqrt(((z * z) - (t * a)));
}
def code(x, y, z, t, a):
	return ((x * y) * z) / math.sqrt(((z * z) - (t * a)))
function code(x, y, z, t, a)
	return Float64(Float64(Float64(x * y) * z) / sqrt(Float64(Float64(z * z) - Float64(t * a))))
end
function tmp = code(x, y, z, t, a)
	tmp = ((x * y) * z) / sqrt(((z * z) - (t * a)));
end
code[x_, y_, z_, t_, a_] := N[(N[(N[(x * y), $MachinePrecision] * z), $MachinePrecision] / N[Sqrt[N[(N[(z * z), $MachinePrecision] - N[(t * a), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 7 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 61.3% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \end{array} \]
(FPCore (x y z t a)
 :precision binary64
 (/ (* (* x y) z) (sqrt (- (* z z) (* t a)))))
double code(double x, double y, double z, double t, double a) {
	return ((x * y) * z) / sqrt(((z * z) - (t * a)));
}
real(8) function code(x, y, z, t, a)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    code = ((x * y) * z) / sqrt(((z * z) - (t * a)))
end function
public static double code(double x, double y, double z, double t, double a) {
	return ((x * y) * z) / Math.sqrt(((z * z) - (t * a)));
}
def code(x, y, z, t, a):
	return ((x * y) * z) / math.sqrt(((z * z) - (t * a)))
function code(x, y, z, t, a)
	return Float64(Float64(Float64(x * y) * z) / sqrt(Float64(Float64(z * z) - Float64(t * a))))
end
function tmp = code(x, y, z, t, a)
	tmp = ((x * y) * z) / sqrt(((z * z) - (t * a)));
end
code[x_, y_, z_, t_, a_] := N[(N[(N[(x * y), $MachinePrecision] * z), $MachinePrecision] / N[Sqrt[N[(N[(z * z), $MachinePrecision] - N[(t * a), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}
\end{array}

Alternative 1: 92.2% accurate, 0.9× speedup?

\[\begin{array}{l} z\_m = \left|z\right| \\ z\_s = \mathsf{copysign}\left(1, z\right) \\ y\_m = \left|y\right| \\ y\_s = \mathsf{copysign}\left(1, y\right) \\ x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\ \\ x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \begin{array}{l} \mathbf{if}\;z\_m \leq 0.73:\\ \;\;\;\;\frac{y\_m \cdot z\_m}{\sqrt{\mathsf{fma}\left(-a, t, z\_m \cdot z\_m\right)}} \cdot x\_m\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{z\_m}{\mathsf{fma}\left(\frac{t}{z\_m}, -0.5 \cdot a, z\_m\right)} \cdot y\_m\right) \cdot x\_m\\ \end{array}\right)\right) \end{array} \]
z\_m = (fabs.f64 z)
z\_s = (copysign.f64 #s(literal 1 binary64) z)
y\_m = (fabs.f64 y)
y\_s = (copysign.f64 #s(literal 1 binary64) y)
x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
(FPCore (x_s y_s z_s x_m y_m z_m t a)
 :precision binary64
 (*
  x_s
  (*
   y_s
   (*
    z_s
    (if (<= z_m 0.73)
      (* (/ (* y_m z_m) (sqrt (fma (- a) t (* z_m z_m)))) x_m)
      (* (* (/ z_m (fma (/ t z_m) (* -0.5 a) z_m)) y_m) x_m))))))
z\_m = fabs(z);
z\_s = copysign(1.0, z);
y\_m = fabs(y);
y\_s = copysign(1.0, y);
x\_m = fabs(x);
x\_s = copysign(1.0, x);
assert(x_m < y_m && y_m < z_m && z_m < t && t < a);
double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
	double tmp;
	if (z_m <= 0.73) {
		tmp = ((y_m * z_m) / sqrt(fma(-a, t, (z_m * z_m)))) * x_m;
	} else {
		tmp = ((z_m / fma((t / z_m), (-0.5 * a), z_m)) * y_m) * x_m;
	}
	return x_s * (y_s * (z_s * tmp));
}
z\_m = abs(z)
z\_s = copysign(1.0, z)
y\_m = abs(y)
y\_s = copysign(1.0, y)
x\_m = abs(x)
x\_s = copysign(1.0, x)
x_m, y_m, z_m, t, a = sort([x_m, y_m, z_m, t, a])
function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
	tmp = 0.0
	if (z_m <= 0.73)
		tmp = Float64(Float64(Float64(y_m * z_m) / sqrt(fma(Float64(-a), t, Float64(z_m * z_m)))) * x_m);
	else
		tmp = Float64(Float64(Float64(z_m / fma(Float64(t / z_m), Float64(-0.5 * a), z_m)) * y_m) * x_m);
	end
	return Float64(x_s * Float64(y_s * Float64(z_s * tmp)))
end
z\_m = N[Abs[z], $MachinePrecision]
z\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[z]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
y\_m = N[Abs[y], $MachinePrecision]
y\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
x\_m = N[Abs[x], $MachinePrecision]
x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
code[x$95$s_, y$95$s_, z$95$s_, x$95$m_, y$95$m_, z$95$m_, t_, a_] := N[(x$95$s * N[(y$95$s * N[(z$95$s * If[LessEqual[z$95$m, 0.73], N[(N[(N[(y$95$m * z$95$m), $MachinePrecision] / N[Sqrt[N[((-a) * t + N[(z$95$m * z$95$m), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * x$95$m), $MachinePrecision], N[(N[(N[(z$95$m / N[(N[(t / z$95$m), $MachinePrecision] * N[(-0.5 * a), $MachinePrecision] + z$95$m), $MachinePrecision]), $MachinePrecision] * y$95$m), $MachinePrecision] * x$95$m), $MachinePrecision]]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
z\_m = \left|z\right|
\\
z\_s = \mathsf{copysign}\left(1, z\right)
\\
y\_m = \left|y\right|
\\
y\_s = \mathsf{copysign}\left(1, y\right)
\\
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)
\\
[x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\
\\
x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \begin{array}{l}
\mathbf{if}\;z\_m \leq 0.73:\\
\;\;\;\;\frac{y\_m \cdot z\_m}{\sqrt{\mathsf{fma}\left(-a, t, z\_m \cdot z\_m\right)}} \cdot x\_m\\

\mathbf{else}:\\
\;\;\;\;\left(\frac{z\_m}{\mathsf{fma}\left(\frac{t}{z\_m}, -0.5 \cdot a, z\_m\right)} \cdot y\_m\right) \cdot x\_m\\


\end{array}\right)\right)
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if z < 0.72999999999999998

    1. Initial program 67.1%

      \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
    2. Add Preprocessing
    3. Taylor expanded in z around inf

      \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{{z}^{2}}}} \]
    4. Step-by-step derivation
      1. unpow2N/A

        \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{z \cdot z}}} \]
      2. lower-*.f6444.7

        \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{z \cdot z}}} \]
    5. Applied rewrites44.7%

      \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{z \cdot z}}} \]
    6. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z}}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{\left(x \cdot y\right) \cdot z}}{\sqrt{z \cdot z}} \]
      3. associate-/l*N/A

        \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{z}{\sqrt{z \cdot z}}} \]
      4. lift-*.f64N/A

        \[\leadsto \color{blue}{\left(x \cdot y\right)} \cdot \frac{z}{\sqrt{z \cdot z}} \]
      5. associate-*l*N/A

        \[\leadsto \color{blue}{x \cdot \left(y \cdot \frac{z}{\sqrt{z \cdot z}}\right)} \]
      6. *-commutativeN/A

        \[\leadsto \color{blue}{\left(y \cdot \frac{z}{\sqrt{z \cdot z}}\right) \cdot x} \]
      7. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(y \cdot \frac{z}{\sqrt{z \cdot z}}\right) \cdot x} \]
      8. associate-*r/N/A

        \[\leadsto \color{blue}{\frac{y \cdot z}{\sqrt{z \cdot z}}} \cdot x \]
      9. *-commutativeN/A

        \[\leadsto \frac{\color{blue}{z \cdot y}}{\sqrt{z \cdot z}} \cdot x \]
      10. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{z \cdot y}}{\sqrt{z \cdot z}} \cdot x \]
      11. lower-/.f6443.4

        \[\leadsto \color{blue}{\frac{z \cdot y}{\sqrt{z \cdot z}}} \cdot x \]
      12. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{z \cdot y}}{\sqrt{z \cdot z}} \cdot x \]
      13. *-commutativeN/A

        \[\leadsto \frac{\color{blue}{y \cdot z}}{\sqrt{z \cdot z}} \cdot x \]
      14. lower-*.f6443.4

        \[\leadsto \frac{\color{blue}{y \cdot z}}{\sqrt{z \cdot z}} \cdot x \]
    7. Applied rewrites43.4%

      \[\leadsto \color{blue}{\frac{y \cdot z}{\sqrt{z \cdot z}} \cdot x} \]
    8. Taylor expanded in z around 0

      \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{{z}^{2} - a \cdot t}}} \cdot x \]
    9. Step-by-step derivation
      1. fp-cancel-sub-sign-invN/A

        \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{{z}^{2} + \left(\mathsf{neg}\left(a\right)\right) \cdot t}}} \cdot x \]
      2. mul-1-negN/A

        \[\leadsto \frac{y \cdot z}{\sqrt{{z}^{2} + \color{blue}{\left(-1 \cdot a\right)} \cdot t}} \cdot x \]
      3. associate-*r*N/A

        \[\leadsto \frac{y \cdot z}{\sqrt{{z}^{2} + \color{blue}{-1 \cdot \left(a \cdot t\right)}}} \cdot x \]
      4. +-commutativeN/A

        \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{-1 \cdot \left(a \cdot t\right) + {z}^{2}}}} \cdot x \]
      5. associate-*r*N/A

        \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{\left(-1 \cdot a\right) \cdot t} + {z}^{2}}} \cdot x \]
      6. mul-1-negN/A

        \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{\left(\mathsf{neg}\left(a\right)\right)} \cdot t + {z}^{2}}} \cdot x \]
      7. lower-fma.f64N/A

        \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(a\right), t, {z}^{2}\right)}}} \cdot x \]
      8. lower-neg.f64N/A

        \[\leadsto \frac{y \cdot z}{\sqrt{\mathsf{fma}\left(\color{blue}{-a}, t, {z}^{2}\right)}} \cdot x \]
      9. unpow2N/A

        \[\leadsto \frac{y \cdot z}{\sqrt{\mathsf{fma}\left(-a, t, \color{blue}{z \cdot z}\right)}} \cdot x \]
      10. lower-*.f6465.2

        \[\leadsto \frac{y \cdot z}{\sqrt{\mathsf{fma}\left(-a, t, \color{blue}{z \cdot z}\right)}} \cdot x \]
    10. Applied rewrites65.2%

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

    if 0.72999999999999998 < z

    1. Initial program 49.3%

      \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
    2. Add Preprocessing
    3. Taylor expanded in t around 0

      \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{z + \frac{-1}{2} \cdot \frac{a \cdot t}{z}}} \]
    4. Step-by-step derivation
      1. +-commutativeN/A

        \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\frac{-1}{2} \cdot \frac{a \cdot t}{z} + z}} \]
      2. associate-/l*N/A

        \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\frac{-1}{2} \cdot \color{blue}{\left(a \cdot \frac{t}{z}\right)} + z} \]
      3. associate-*r*N/A

        \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\left(\frac{-1}{2} \cdot a\right) \cdot \frac{t}{z}} + z} \]
      4. lower-fma.f64N/A

        \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
      5. lower-*.f64N/A

        \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\color{blue}{\frac{-1}{2} \cdot a}, \frac{t}{z}, z\right)} \]
      6. lower-/.f6484.9

        \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(-0.5 \cdot a, \color{blue}{\frac{t}{z}}, z\right)} \]
    5. Applied rewrites84.9%

      \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \]
    6. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{\left(x \cdot y\right) \cdot z}}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \]
      3. associate-/l*N/A

        \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
      4. *-commutativeN/A

        \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
      5. lift-*.f64N/A

        \[\leadsto \frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \color{blue}{\left(x \cdot y\right)} \]
      6. *-commutativeN/A

        \[\leadsto \frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
      7. associate-*r*N/A

        \[\leadsto \color{blue}{\left(\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot y\right) \cdot x} \]
      8. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot y\right) \cdot x} \]
    7. Applied rewrites94.5%

      \[\leadsto \color{blue}{\left(\frac{z}{\mathsf{fma}\left(\frac{t}{z}, -0.5 \cdot a, z\right)} \cdot y\right) \cdot x} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 2: 75.8% accurate, 0.4× speedup?

\[\begin{array}{l} z\_m = \left|z\right| \\ z\_s = \mathsf{copysign}\left(1, z\right) \\ y\_m = \left|y\right| \\ y\_s = \mathsf{copysign}\left(1, y\right) \\ x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\ \\ x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \begin{array}{l} \mathbf{if}\;z\_m \leq 1.35 \cdot 10^{-183}:\\ \;\;\;\;{z\_m}^{-1} \cdot \left(\left(z\_m \cdot y\_m\right) \cdot x\_m\right)\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \left(y\_m \cdot x\_m\right)\\ \end{array}\right)\right) \end{array} \]
z\_m = (fabs.f64 z)
z\_s = (copysign.f64 #s(literal 1 binary64) z)
y\_m = (fabs.f64 y)
y\_s = (copysign.f64 #s(literal 1 binary64) y)
x\_m = (fabs.f64 x)
x\_s = (copysign.f64 #s(literal 1 binary64) x)
NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
(FPCore (x_s y_s z_s x_m y_m z_m t a)
 :precision binary64
 (*
  x_s
  (*
   y_s
   (*
    z_s
    (if (<= z_m 1.35e-183)
      (* (pow z_m -1.0) (* (* z_m y_m) x_m))
      (* 1.0 (* y_m x_m)))))))
z\_m = fabs(z);
z\_s = copysign(1.0, z);
y\_m = fabs(y);
y\_s = copysign(1.0, y);
x\_m = fabs(x);
x\_s = copysign(1.0, x);
assert(x_m < y_m && y_m < z_m && z_m < t && t < a);
double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
	double tmp;
	if (z_m <= 1.35e-183) {
		tmp = pow(z_m, -1.0) * ((z_m * y_m) * x_m);
	} else {
		tmp = 1.0 * (y_m * x_m);
	}
	return x_s * (y_s * (z_s * tmp));
}
z\_m = abs(z)
z\_s = copysign(1.0d0, z)
y\_m = abs(y)
y\_s = copysign(1.0d0, y)
x\_m = abs(x)
x\_s = copysign(1.0d0, x)
NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
real(8) function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
    real(8), intent (in) :: x_s
    real(8), intent (in) :: y_s
    real(8), intent (in) :: z_s
    real(8), intent (in) :: x_m
    real(8), intent (in) :: y_m
    real(8), intent (in) :: z_m
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    real(8) :: tmp
    if (z_m <= 1.35d-183) then
        tmp = (z_m ** (-1.0d0)) * ((z_m * y_m) * x_m)
    else
        tmp = 1.0d0 * (y_m * x_m)
    end if
    code = x_s * (y_s * (z_s * tmp))
end function
z\_m = Math.abs(z);
z\_s = Math.copySign(1.0, z);
y\_m = Math.abs(y);
y\_s = Math.copySign(1.0, y);
x\_m = Math.abs(x);
x\_s = Math.copySign(1.0, x);
assert x_m < y_m && y_m < z_m && z_m < t && t < a;
public static double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
	double tmp;
	if (z_m <= 1.35e-183) {
		tmp = Math.pow(z_m, -1.0) * ((z_m * y_m) * x_m);
	} else {
		tmp = 1.0 * (y_m * x_m);
	}
	return x_s * (y_s * (z_s * tmp));
}
z\_m = math.fabs(z)
z\_s = math.copysign(1.0, z)
y\_m = math.fabs(y)
y\_s = math.copysign(1.0, y)
x\_m = math.fabs(x)
x\_s = math.copysign(1.0, x)
[x_m, y_m, z_m, t, a] = sort([x_m, y_m, z_m, t, a])
def code(x_s, y_s, z_s, x_m, y_m, z_m, t, a):
	tmp = 0
	if z_m <= 1.35e-183:
		tmp = math.pow(z_m, -1.0) * ((z_m * y_m) * x_m)
	else:
		tmp = 1.0 * (y_m * x_m)
	return x_s * (y_s * (z_s * tmp))
z\_m = abs(z)
z\_s = copysign(1.0, z)
y\_m = abs(y)
y\_s = copysign(1.0, y)
x\_m = abs(x)
x\_s = copysign(1.0, x)
x_m, y_m, z_m, t, a = sort([x_m, y_m, z_m, t, a])
function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
	tmp = 0.0
	if (z_m <= 1.35e-183)
		tmp = Float64((z_m ^ -1.0) * Float64(Float64(z_m * y_m) * x_m));
	else
		tmp = Float64(1.0 * Float64(y_m * x_m));
	end
	return Float64(x_s * Float64(y_s * Float64(z_s * tmp)))
end
z\_m = abs(z);
z\_s = sign(z) * abs(1.0);
y\_m = abs(y);
y\_s = sign(y) * abs(1.0);
x\_m = abs(x);
x\_s = sign(x) * abs(1.0);
x_m, y_m, z_m, t, a = num2cell(sort([x_m, y_m, z_m, t, a])){:}
function tmp_2 = code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
	tmp = 0.0;
	if (z_m <= 1.35e-183)
		tmp = (z_m ^ -1.0) * ((z_m * y_m) * x_m);
	else
		tmp = 1.0 * (y_m * x_m);
	end
	tmp_2 = x_s * (y_s * (z_s * tmp));
end
z\_m = N[Abs[z], $MachinePrecision]
z\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[z]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
y\_m = N[Abs[y], $MachinePrecision]
y\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
x\_m = N[Abs[x], $MachinePrecision]
x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
code[x$95$s_, y$95$s_, z$95$s_, x$95$m_, y$95$m_, z$95$m_, t_, a_] := N[(x$95$s * N[(y$95$s * N[(z$95$s * If[LessEqual[z$95$m, 1.35e-183], N[(N[Power[z$95$m, -1.0], $MachinePrecision] * N[(N[(z$95$m * y$95$m), $MachinePrecision] * x$95$m), $MachinePrecision]), $MachinePrecision], N[(1.0 * N[(y$95$m * x$95$m), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
z\_m = \left|z\right|
\\
z\_s = \mathsf{copysign}\left(1, z\right)
\\
y\_m = \left|y\right|
\\
y\_s = \mathsf{copysign}\left(1, y\right)
\\
x\_m = \left|x\right|
\\
x\_s = \mathsf{copysign}\left(1, x\right)
\\
[x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\
\\
x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \begin{array}{l}
\mathbf{if}\;z\_m \leq 1.35 \cdot 10^{-183}:\\
\;\;\;\;{z\_m}^{-1} \cdot \left(\left(z\_m \cdot y\_m\right) \cdot x\_m\right)\\

\mathbf{else}:\\
\;\;\;\;1 \cdot \left(y\_m \cdot x\_m\right)\\


\end{array}\right)\right)
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if z < 1.35000000000000004e-183

    1. Initial program 65.1%

      \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
    2. Add Preprocessing
    3. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\left(x \cdot \left(y \cdot z\right)\right) \cdot \sqrt{\frac{1}{{z}^{2} - a \cdot t}}} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto \color{blue}{\sqrt{\frac{1}{{z}^{2} - a \cdot t}} \cdot \left(x \cdot \left(y \cdot z\right)\right)} \]
      2. lower-*.f64N/A

        \[\leadsto \color{blue}{\sqrt{\frac{1}{{z}^{2} - a \cdot t}} \cdot \left(x \cdot \left(y \cdot z\right)\right)} \]
      3. lower-sqrt.f64N/A

        \[\leadsto \color{blue}{\sqrt{\frac{1}{{z}^{2} - a \cdot t}}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      4. lower-/.f64N/A

        \[\leadsto \sqrt{\color{blue}{\frac{1}{{z}^{2} - a \cdot t}}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      5. fp-cancel-sub-sign-invN/A

        \[\leadsto \sqrt{\frac{1}{\color{blue}{{z}^{2} + \left(\mathsf{neg}\left(a\right)\right) \cdot t}}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      6. mul-1-negN/A

        \[\leadsto \sqrt{\frac{1}{{z}^{2} + \color{blue}{\left(-1 \cdot a\right)} \cdot t}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      7. associate-*r*N/A

        \[\leadsto \sqrt{\frac{1}{{z}^{2} + \color{blue}{-1 \cdot \left(a \cdot t\right)}}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      8. +-commutativeN/A

        \[\leadsto \sqrt{\frac{1}{\color{blue}{-1 \cdot \left(a \cdot t\right) + {z}^{2}}}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      9. associate-*r*N/A

        \[\leadsto \sqrt{\frac{1}{\color{blue}{\left(-1 \cdot a\right) \cdot t} + {z}^{2}}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      10. mul-1-negN/A

        \[\leadsto \sqrt{\frac{1}{\color{blue}{\left(\mathsf{neg}\left(a\right)\right)} \cdot t + {z}^{2}}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      11. lower-fma.f64N/A

        \[\leadsto \sqrt{\frac{1}{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(a\right), t, {z}^{2}\right)}}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      12. lower-neg.f64N/A

        \[\leadsto \sqrt{\frac{1}{\mathsf{fma}\left(\color{blue}{-a}, t, {z}^{2}\right)}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      13. unpow2N/A

        \[\leadsto \sqrt{\frac{1}{\mathsf{fma}\left(-a, t, \color{blue}{z \cdot z}\right)}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      14. lower-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{\mathsf{fma}\left(-a, t, \color{blue}{z \cdot z}\right)}} \cdot \left(x \cdot \left(y \cdot z\right)\right) \]
      15. *-commutativeN/A

        \[\leadsto \sqrt{\frac{1}{\mathsf{fma}\left(-a, t, z \cdot z\right)}} \cdot \color{blue}{\left(\left(y \cdot z\right) \cdot x\right)} \]
      16. lower-*.f64N/A

        \[\leadsto \sqrt{\frac{1}{\mathsf{fma}\left(-a, t, z \cdot z\right)}} \cdot \color{blue}{\left(\left(y \cdot z\right) \cdot x\right)} \]
      17. *-commutativeN/A

        \[\leadsto \sqrt{\frac{1}{\mathsf{fma}\left(-a, t, z \cdot z\right)}} \cdot \left(\color{blue}{\left(z \cdot y\right)} \cdot x\right) \]
      18. lower-*.f6460.3

        \[\leadsto \sqrt{\frac{1}{\mathsf{fma}\left(-a, t, z \cdot z\right)}} \cdot \left(\color{blue}{\left(z \cdot y\right)} \cdot x\right) \]
    5. Applied rewrites60.3%

      \[\leadsto \color{blue}{\sqrt{\frac{1}{\mathsf{fma}\left(-a, t, z \cdot z\right)}} \cdot \left(\left(z \cdot y\right) \cdot x\right)} \]
    6. Taylor expanded in z around inf

      \[\leadsto \frac{1}{z} \cdot \left(\color{blue}{\left(z \cdot y\right)} \cdot x\right) \]
    7. Step-by-step derivation
      1. Applied rewrites23.4%

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

      if 1.35000000000000004e-183 < z

      1. Initial program 57.0%

        \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
      2. Add Preprocessing
      3. Taylor expanded in t around 0

        \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{z + \frac{-1}{2} \cdot \frac{a \cdot t}{z}}} \]
      4. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\frac{-1}{2} \cdot \frac{a \cdot t}{z} + z}} \]
        2. associate-/l*N/A

          \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\frac{-1}{2} \cdot \color{blue}{\left(a \cdot \frac{t}{z}\right)} + z} \]
        3. associate-*r*N/A

          \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\left(\frac{-1}{2} \cdot a\right) \cdot \frac{t}{z}} + z} \]
        4. lower-fma.f64N/A

          \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\color{blue}{\frac{-1}{2} \cdot a}, \frac{t}{z}, z\right)} \]
        6. lower-/.f6474.4

          \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(-0.5 \cdot a, \color{blue}{\frac{t}{z}}, z\right)} \]
      5. Applied rewrites74.4%

        \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \]
      6. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
        2. lift-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(x \cdot y\right) \cdot z}}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \]
        3. associate-/l*N/A

          \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
        4. *-commutativeN/A

          \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
        6. lower-/.f6482.6

          \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \cdot \left(x \cdot y\right) \]
        7. lift-*.f64N/A

          \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(x \cdot y\right)} \]
        8. *-commutativeN/A

          \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
        9. lower-*.f64N/A

          \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
      7. Applied rewrites82.6%

        \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{t}{z}, -0.5 \cdot a, z\right)} \cdot \left(y \cdot x\right)} \]
      8. Taylor expanded in z around inf

        \[\leadsto \color{blue}{1} \cdot \left(y \cdot x\right) \]
      9. Step-by-step derivation
        1. Applied rewrites81.8%

          \[\leadsto \color{blue}{1} \cdot \left(y \cdot x\right) \]
      10. Recombined 2 regimes into one program.
      11. Final simplification47.6%

        \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq 1.35 \cdot 10^{-183}:\\ \;\;\;\;{z}^{-1} \cdot \left(\left(z \cdot y\right) \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \left(y \cdot x\right)\\ \end{array} \]
      12. Add Preprocessing

      Alternative 3: 84.9% accurate, 1.0× speedup?

      \[\begin{array}{l} z\_m = \left|z\right| \\ z\_s = \mathsf{copysign}\left(1, z\right) \\ y\_m = \left|y\right| \\ y\_s = \mathsf{copysign}\left(1, y\right) \\ x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\ \\ x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \begin{array}{l} \mathbf{if}\;z\_m \leq 9.2 \cdot 10^{-96}:\\ \;\;\;\;\frac{y\_m \cdot z\_m}{\sqrt{\left(-a\right) \cdot t}} \cdot x\_m\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \left(y\_m \cdot x\_m\right)\\ \end{array}\right)\right) \end{array} \]
      z\_m = (fabs.f64 z)
      z\_s = (copysign.f64 #s(literal 1 binary64) z)
      y\_m = (fabs.f64 y)
      y\_s = (copysign.f64 #s(literal 1 binary64) y)
      x\_m = (fabs.f64 x)
      x\_s = (copysign.f64 #s(literal 1 binary64) x)
      NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
      (FPCore (x_s y_s z_s x_m y_m z_m t a)
       :precision binary64
       (*
        x_s
        (*
         y_s
         (*
          z_s
          (if (<= z_m 9.2e-96)
            (* (/ (* y_m z_m) (sqrt (* (- a) t))) x_m)
            (* 1.0 (* y_m x_m)))))))
      z\_m = fabs(z);
      z\_s = copysign(1.0, z);
      y\_m = fabs(y);
      y\_s = copysign(1.0, y);
      x\_m = fabs(x);
      x\_s = copysign(1.0, x);
      assert(x_m < y_m && y_m < z_m && z_m < t && t < a);
      double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
      	double tmp;
      	if (z_m <= 9.2e-96) {
      		tmp = ((y_m * z_m) / sqrt((-a * t))) * x_m;
      	} else {
      		tmp = 1.0 * (y_m * x_m);
      	}
      	return x_s * (y_s * (z_s * tmp));
      }
      
      z\_m = abs(z)
      z\_s = copysign(1.0d0, z)
      y\_m = abs(y)
      y\_s = copysign(1.0d0, y)
      x\_m = abs(x)
      x\_s = copysign(1.0d0, x)
      NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
      real(8) function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
          real(8), intent (in) :: x_s
          real(8), intent (in) :: y_s
          real(8), intent (in) :: z_s
          real(8), intent (in) :: x_m
          real(8), intent (in) :: y_m
          real(8), intent (in) :: z_m
          real(8), intent (in) :: t
          real(8), intent (in) :: a
          real(8) :: tmp
          if (z_m <= 9.2d-96) then
              tmp = ((y_m * z_m) / sqrt((-a * t))) * x_m
          else
              tmp = 1.0d0 * (y_m * x_m)
          end if
          code = x_s * (y_s * (z_s * tmp))
      end function
      
      z\_m = Math.abs(z);
      z\_s = Math.copySign(1.0, z);
      y\_m = Math.abs(y);
      y\_s = Math.copySign(1.0, y);
      x\_m = Math.abs(x);
      x\_s = Math.copySign(1.0, x);
      assert x_m < y_m && y_m < z_m && z_m < t && t < a;
      public static double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
      	double tmp;
      	if (z_m <= 9.2e-96) {
      		tmp = ((y_m * z_m) / Math.sqrt((-a * t))) * x_m;
      	} else {
      		tmp = 1.0 * (y_m * x_m);
      	}
      	return x_s * (y_s * (z_s * tmp));
      }
      
      z\_m = math.fabs(z)
      z\_s = math.copysign(1.0, z)
      y\_m = math.fabs(y)
      y\_s = math.copysign(1.0, y)
      x\_m = math.fabs(x)
      x\_s = math.copysign(1.0, x)
      [x_m, y_m, z_m, t, a] = sort([x_m, y_m, z_m, t, a])
      def code(x_s, y_s, z_s, x_m, y_m, z_m, t, a):
      	tmp = 0
      	if z_m <= 9.2e-96:
      		tmp = ((y_m * z_m) / math.sqrt((-a * t))) * x_m
      	else:
      		tmp = 1.0 * (y_m * x_m)
      	return x_s * (y_s * (z_s * tmp))
      
      z\_m = abs(z)
      z\_s = copysign(1.0, z)
      y\_m = abs(y)
      y\_s = copysign(1.0, y)
      x\_m = abs(x)
      x\_s = copysign(1.0, x)
      x_m, y_m, z_m, t, a = sort([x_m, y_m, z_m, t, a])
      function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
      	tmp = 0.0
      	if (z_m <= 9.2e-96)
      		tmp = Float64(Float64(Float64(y_m * z_m) / sqrt(Float64(Float64(-a) * t))) * x_m);
      	else
      		tmp = Float64(1.0 * Float64(y_m * x_m));
      	end
      	return Float64(x_s * Float64(y_s * Float64(z_s * tmp)))
      end
      
      z\_m = abs(z);
      z\_s = sign(z) * abs(1.0);
      y\_m = abs(y);
      y\_s = sign(y) * abs(1.0);
      x\_m = abs(x);
      x\_s = sign(x) * abs(1.0);
      x_m, y_m, z_m, t, a = num2cell(sort([x_m, y_m, z_m, t, a])){:}
      function tmp_2 = code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
      	tmp = 0.0;
      	if (z_m <= 9.2e-96)
      		tmp = ((y_m * z_m) / sqrt((-a * t))) * x_m;
      	else
      		tmp = 1.0 * (y_m * x_m);
      	end
      	tmp_2 = x_s * (y_s * (z_s * tmp));
      end
      
      z\_m = N[Abs[z], $MachinePrecision]
      z\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[z]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
      y\_m = N[Abs[y], $MachinePrecision]
      y\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
      x\_m = N[Abs[x], $MachinePrecision]
      x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
      NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
      code[x$95$s_, y$95$s_, z$95$s_, x$95$m_, y$95$m_, z$95$m_, t_, a_] := N[(x$95$s * N[(y$95$s * N[(z$95$s * If[LessEqual[z$95$m, 9.2e-96], N[(N[(N[(y$95$m * z$95$m), $MachinePrecision] / N[Sqrt[N[((-a) * t), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * x$95$m), $MachinePrecision], N[(1.0 * N[(y$95$m * x$95$m), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
      
      \begin{array}{l}
      z\_m = \left|z\right|
      \\
      z\_s = \mathsf{copysign}\left(1, z\right)
      \\
      y\_m = \left|y\right|
      \\
      y\_s = \mathsf{copysign}\left(1, y\right)
      \\
      x\_m = \left|x\right|
      \\
      x\_s = \mathsf{copysign}\left(1, x\right)
      \\
      [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\
      \\
      x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \begin{array}{l}
      \mathbf{if}\;z\_m \leq 9.2 \cdot 10^{-96}:\\
      \;\;\;\;\frac{y\_m \cdot z\_m}{\sqrt{\left(-a\right) \cdot t}} \cdot x\_m\\
      
      \mathbf{else}:\\
      \;\;\;\;1 \cdot \left(y\_m \cdot x\_m\right)\\
      
      
      \end{array}\right)\right)
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if z < 9.2e-96

        1. Initial program 65.0%

          \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
        2. Add Preprocessing
        3. Taylor expanded in z around inf

          \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{{z}^{2}}}} \]
        4. Step-by-step derivation
          1. unpow2N/A

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{z \cdot z}}} \]
          2. lower-*.f6444.2

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{z \cdot z}}} \]
        5. Applied rewrites44.2%

          \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{z \cdot z}}} \]
        6. Step-by-step derivation
          1. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z}}} \]
          2. lift-*.f64N/A

            \[\leadsto \frac{\color{blue}{\left(x \cdot y\right) \cdot z}}{\sqrt{z \cdot z}} \]
          3. associate-/l*N/A

            \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{z}{\sqrt{z \cdot z}}} \]
          4. lift-*.f64N/A

            \[\leadsto \color{blue}{\left(x \cdot y\right)} \cdot \frac{z}{\sqrt{z \cdot z}} \]
          5. associate-*l*N/A

            \[\leadsto \color{blue}{x \cdot \left(y \cdot \frac{z}{\sqrt{z \cdot z}}\right)} \]
          6. *-commutativeN/A

            \[\leadsto \color{blue}{\left(y \cdot \frac{z}{\sqrt{z \cdot z}}\right) \cdot x} \]
          7. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(y \cdot \frac{z}{\sqrt{z \cdot z}}\right) \cdot x} \]
          8. associate-*r/N/A

            \[\leadsto \color{blue}{\frac{y \cdot z}{\sqrt{z \cdot z}}} \cdot x \]
          9. *-commutativeN/A

            \[\leadsto \frac{\color{blue}{z \cdot y}}{\sqrt{z \cdot z}} \cdot x \]
          10. lift-*.f64N/A

            \[\leadsto \frac{\color{blue}{z \cdot y}}{\sqrt{z \cdot z}} \cdot x \]
          11. lower-/.f6442.3

            \[\leadsto \color{blue}{\frac{z \cdot y}{\sqrt{z \cdot z}}} \cdot x \]
          12. lift-*.f64N/A

            \[\leadsto \frac{\color{blue}{z \cdot y}}{\sqrt{z \cdot z}} \cdot x \]
          13. *-commutativeN/A

            \[\leadsto \frac{\color{blue}{y \cdot z}}{\sqrt{z \cdot z}} \cdot x \]
          14. lower-*.f6442.3

            \[\leadsto \frac{\color{blue}{y \cdot z}}{\sqrt{z \cdot z}} \cdot x \]
        7. Applied rewrites42.3%

          \[\leadsto \color{blue}{\frac{y \cdot z}{\sqrt{z \cdot z}} \cdot x} \]
        8. Taylor expanded in z around 0

          \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{-1 \cdot \left(a \cdot t\right)}}} \cdot x \]
        9. Step-by-step derivation
          1. associate-*r*N/A

            \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{\left(-1 \cdot a\right) \cdot t}}} \cdot x \]
          2. mul-1-negN/A

            \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{\left(\mathsf{neg}\left(a\right)\right)} \cdot t}} \cdot x \]
          3. lower-*.f64N/A

            \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{\left(\mathsf{neg}\left(a\right)\right) \cdot t}}} \cdot x \]
          4. lower-neg.f6430.9

            \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{\left(-a\right)} \cdot t}} \cdot x \]
        10. Applied rewrites30.9%

          \[\leadsto \frac{y \cdot z}{\sqrt{\color{blue}{\left(-a\right) \cdot t}}} \cdot x \]

        if 9.2e-96 < z

        1. Initial program 56.0%

          \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
        2. Add Preprocessing
        3. Taylor expanded in t around 0

          \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{z + \frac{-1}{2} \cdot \frac{a \cdot t}{z}}} \]
        4. Step-by-step derivation
          1. +-commutativeN/A

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\frac{-1}{2} \cdot \frac{a \cdot t}{z} + z}} \]
          2. associate-/l*N/A

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\frac{-1}{2} \cdot \color{blue}{\left(a \cdot \frac{t}{z}\right)} + z} \]
          3. associate-*r*N/A

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\left(\frac{-1}{2} \cdot a\right) \cdot \frac{t}{z}} + z} \]
          4. lower-fma.f64N/A

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
          5. lower-*.f64N/A

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\color{blue}{\frac{-1}{2} \cdot a}, \frac{t}{z}, z\right)} \]
          6. lower-/.f6478.7

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(-0.5 \cdot a, \color{blue}{\frac{t}{z}}, z\right)} \]
        5. Applied rewrites78.7%

          \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \]
        6. Step-by-step derivation
          1. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
          2. lift-*.f64N/A

            \[\leadsto \frac{\color{blue}{\left(x \cdot y\right) \cdot z}}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \]
          3. associate-/l*N/A

            \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
          4. *-commutativeN/A

            \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
          5. lower-*.f64N/A

            \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
          6. lower-/.f6487.5

            \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \cdot \left(x \cdot y\right) \]
          7. lift-*.f64N/A

            \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(x \cdot y\right)} \]
          8. *-commutativeN/A

            \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
          9. lower-*.f64N/A

            \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
        7. Applied rewrites87.5%

          \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{t}{z}, -0.5 \cdot a, z\right)} \cdot \left(y \cdot x\right)} \]
        8. Taylor expanded in z around inf

          \[\leadsto \color{blue}{1} \cdot \left(y \cdot x\right) \]
        9. Step-by-step derivation
          1. Applied rewrites87.6%

            \[\leadsto \color{blue}{1} \cdot \left(y \cdot x\right) \]
        10. Recombined 2 regimes into one program.
        11. Add Preprocessing

        Alternative 4: 76.0% accurate, 1.5× speedup?

        \[\begin{array}{l} z\_m = \left|z\right| \\ z\_s = \mathsf{copysign}\left(1, z\right) \\ y\_m = \left|y\right| \\ y\_s = \mathsf{copysign}\left(1, y\right) \\ x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\ \\ x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \begin{array}{l} \mathbf{if}\;z\_m \leq 2.8 \cdot 10^{-177}:\\ \;\;\;\;\frac{\left(x\_m \cdot z\_m\right) \cdot y\_m}{-z\_m}\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \left(y\_m \cdot x\_m\right)\\ \end{array}\right)\right) \end{array} \]
        z\_m = (fabs.f64 z)
        z\_s = (copysign.f64 #s(literal 1 binary64) z)
        y\_m = (fabs.f64 y)
        y\_s = (copysign.f64 #s(literal 1 binary64) y)
        x\_m = (fabs.f64 x)
        x\_s = (copysign.f64 #s(literal 1 binary64) x)
        NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
        (FPCore (x_s y_s z_s x_m y_m z_m t a)
         :precision binary64
         (*
          x_s
          (*
           y_s
           (*
            z_s
            (if (<= z_m 2.8e-177)
              (/ (* (* x_m z_m) y_m) (- z_m))
              (* 1.0 (* y_m x_m)))))))
        z\_m = fabs(z);
        z\_s = copysign(1.0, z);
        y\_m = fabs(y);
        y\_s = copysign(1.0, y);
        x\_m = fabs(x);
        x\_s = copysign(1.0, x);
        assert(x_m < y_m && y_m < z_m && z_m < t && t < a);
        double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
        	double tmp;
        	if (z_m <= 2.8e-177) {
        		tmp = ((x_m * z_m) * y_m) / -z_m;
        	} else {
        		tmp = 1.0 * (y_m * x_m);
        	}
        	return x_s * (y_s * (z_s * tmp));
        }
        
        z\_m = abs(z)
        z\_s = copysign(1.0d0, z)
        y\_m = abs(y)
        y\_s = copysign(1.0d0, y)
        x\_m = abs(x)
        x\_s = copysign(1.0d0, x)
        NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
        real(8) function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
            real(8), intent (in) :: x_s
            real(8), intent (in) :: y_s
            real(8), intent (in) :: z_s
            real(8), intent (in) :: x_m
            real(8), intent (in) :: y_m
            real(8), intent (in) :: z_m
            real(8), intent (in) :: t
            real(8), intent (in) :: a
            real(8) :: tmp
            if (z_m <= 2.8d-177) then
                tmp = ((x_m * z_m) * y_m) / -z_m
            else
                tmp = 1.0d0 * (y_m * x_m)
            end if
            code = x_s * (y_s * (z_s * tmp))
        end function
        
        z\_m = Math.abs(z);
        z\_s = Math.copySign(1.0, z);
        y\_m = Math.abs(y);
        y\_s = Math.copySign(1.0, y);
        x\_m = Math.abs(x);
        x\_s = Math.copySign(1.0, x);
        assert x_m < y_m && y_m < z_m && z_m < t && t < a;
        public static double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
        	double tmp;
        	if (z_m <= 2.8e-177) {
        		tmp = ((x_m * z_m) * y_m) / -z_m;
        	} else {
        		tmp = 1.0 * (y_m * x_m);
        	}
        	return x_s * (y_s * (z_s * tmp));
        }
        
        z\_m = math.fabs(z)
        z\_s = math.copysign(1.0, z)
        y\_m = math.fabs(y)
        y\_s = math.copysign(1.0, y)
        x\_m = math.fabs(x)
        x\_s = math.copysign(1.0, x)
        [x_m, y_m, z_m, t, a] = sort([x_m, y_m, z_m, t, a])
        def code(x_s, y_s, z_s, x_m, y_m, z_m, t, a):
        	tmp = 0
        	if z_m <= 2.8e-177:
        		tmp = ((x_m * z_m) * y_m) / -z_m
        	else:
        		tmp = 1.0 * (y_m * x_m)
        	return x_s * (y_s * (z_s * tmp))
        
        z\_m = abs(z)
        z\_s = copysign(1.0, z)
        y\_m = abs(y)
        y\_s = copysign(1.0, y)
        x\_m = abs(x)
        x\_s = copysign(1.0, x)
        x_m, y_m, z_m, t, a = sort([x_m, y_m, z_m, t, a])
        function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
        	tmp = 0.0
        	if (z_m <= 2.8e-177)
        		tmp = Float64(Float64(Float64(x_m * z_m) * y_m) / Float64(-z_m));
        	else
        		tmp = Float64(1.0 * Float64(y_m * x_m));
        	end
        	return Float64(x_s * Float64(y_s * Float64(z_s * tmp)))
        end
        
        z\_m = abs(z);
        z\_s = sign(z) * abs(1.0);
        y\_m = abs(y);
        y\_s = sign(y) * abs(1.0);
        x\_m = abs(x);
        x\_s = sign(x) * abs(1.0);
        x_m, y_m, z_m, t, a = num2cell(sort([x_m, y_m, z_m, t, a])){:}
        function tmp_2 = code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
        	tmp = 0.0;
        	if (z_m <= 2.8e-177)
        		tmp = ((x_m * z_m) * y_m) / -z_m;
        	else
        		tmp = 1.0 * (y_m * x_m);
        	end
        	tmp_2 = x_s * (y_s * (z_s * tmp));
        end
        
        z\_m = N[Abs[z], $MachinePrecision]
        z\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[z]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        y\_m = N[Abs[y], $MachinePrecision]
        y\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        x\_m = N[Abs[x], $MachinePrecision]
        x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
        NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
        code[x$95$s_, y$95$s_, z$95$s_, x$95$m_, y$95$m_, z$95$m_, t_, a_] := N[(x$95$s * N[(y$95$s * N[(z$95$s * If[LessEqual[z$95$m, 2.8e-177], N[(N[(N[(x$95$m * z$95$m), $MachinePrecision] * y$95$m), $MachinePrecision] / (-z$95$m)), $MachinePrecision], N[(1.0 * N[(y$95$m * x$95$m), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
        
        \begin{array}{l}
        z\_m = \left|z\right|
        \\
        z\_s = \mathsf{copysign}\left(1, z\right)
        \\
        y\_m = \left|y\right|
        \\
        y\_s = \mathsf{copysign}\left(1, y\right)
        \\
        x\_m = \left|x\right|
        \\
        x\_s = \mathsf{copysign}\left(1, x\right)
        \\
        [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\
        \\
        x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \begin{array}{l}
        \mathbf{if}\;z\_m \leq 2.8 \cdot 10^{-177}:\\
        \;\;\;\;\frac{\left(x\_m \cdot z\_m\right) \cdot y\_m}{-z\_m}\\
        
        \mathbf{else}:\\
        \;\;\;\;1 \cdot \left(y\_m \cdot x\_m\right)\\
        
        
        \end{array}\right)\right)
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if z < 2.79999999999999987e-177

          1. Initial program 64.9%

            \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
          2. Add Preprocessing
          3. Taylor expanded in z around -inf

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{-1 \cdot z}} \]
          4. Step-by-step derivation
            1. mul-1-negN/A

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{neg}\left(z\right)}} \]
            2. lower-neg.f6465.8

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{-z}} \]
          5. Applied rewrites65.8%

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{-z}} \]
          6. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \frac{\color{blue}{\left(x \cdot y\right) \cdot z}}{-z} \]
            2. lift-*.f64N/A

              \[\leadsto \frac{\color{blue}{\left(x \cdot y\right)} \cdot z}{-z} \]
            3. associate-*l*N/A

              \[\leadsto \frac{\color{blue}{x \cdot \left(y \cdot z\right)}}{-z} \]
            4. *-commutativeN/A

              \[\leadsto \frac{x \cdot \color{blue}{\left(z \cdot y\right)}}{-z} \]
            5. associate-*r*N/A

              \[\leadsto \frac{\color{blue}{\left(x \cdot z\right) \cdot y}}{-z} \]
            6. lower-*.f64N/A

              \[\leadsto \frac{\color{blue}{\left(x \cdot z\right) \cdot y}}{-z} \]
            7. lower-*.f6458.1

              \[\leadsto \frac{\color{blue}{\left(x \cdot z\right)} \cdot y}{-z} \]
          7. Applied rewrites58.1%

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

          if 2.79999999999999987e-177 < z

          1. Initial program 57.0%

            \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
          2. Add Preprocessing
          3. Taylor expanded in t around 0

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{z + \frac{-1}{2} \cdot \frac{a \cdot t}{z}}} \]
          4. Step-by-step derivation
            1. +-commutativeN/A

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\frac{-1}{2} \cdot \frac{a \cdot t}{z} + z}} \]
            2. associate-/l*N/A

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\frac{-1}{2} \cdot \color{blue}{\left(a \cdot \frac{t}{z}\right)} + z} \]
            3. associate-*r*N/A

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\left(\frac{-1}{2} \cdot a\right) \cdot \frac{t}{z}} + z} \]
            4. lower-fma.f64N/A

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
            5. lower-*.f64N/A

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\color{blue}{\frac{-1}{2} \cdot a}, \frac{t}{z}, z\right)} \]
            6. lower-/.f6474.8

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(-0.5 \cdot a, \color{blue}{\frac{t}{z}}, z\right)} \]
          5. Applied rewrites74.8%

            \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \]
          6. Step-by-step derivation
            1. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
            2. lift-*.f64N/A

              \[\leadsto \frac{\color{blue}{\left(x \cdot y\right) \cdot z}}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \]
            3. associate-/l*N/A

              \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
            4. *-commutativeN/A

              \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
            5. lower-*.f64N/A

              \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
            6. lower-/.f6483.2

              \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \cdot \left(x \cdot y\right) \]
            7. lift-*.f64N/A

              \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(x \cdot y\right)} \]
            8. *-commutativeN/A

              \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
            9. lower-*.f64N/A

              \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
          7. Applied rewrites83.2%

            \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{t}{z}, -0.5 \cdot a, z\right)} \cdot \left(y \cdot x\right)} \]
          8. Taylor expanded in z around inf

            \[\leadsto \color{blue}{1} \cdot \left(y \cdot x\right) \]
          9. Step-by-step derivation
            1. Applied rewrites83.3%

              \[\leadsto \color{blue}{1} \cdot \left(y \cdot x\right) \]
          10. Recombined 2 regimes into one program.
          11. Add Preprocessing

          Alternative 5: 75.1% accurate, 1.5× speedup?

          \[\begin{array}{l} z\_m = \left|z\right| \\ z\_s = \mathsf{copysign}\left(1, z\right) \\ y\_m = \left|y\right| \\ y\_s = \mathsf{copysign}\left(1, y\right) \\ x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\ \\ x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \begin{array}{l} \mathbf{if}\;z\_m \leq 1.05 \cdot 10^{-183}:\\ \;\;\;\;\frac{\left(x\_m \cdot y\_m\right) \cdot z\_m}{-z\_m}\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \left(y\_m \cdot x\_m\right)\\ \end{array}\right)\right) \end{array} \]
          z\_m = (fabs.f64 z)
          z\_s = (copysign.f64 #s(literal 1 binary64) z)
          y\_m = (fabs.f64 y)
          y\_s = (copysign.f64 #s(literal 1 binary64) y)
          x\_m = (fabs.f64 x)
          x\_s = (copysign.f64 #s(literal 1 binary64) x)
          NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
          (FPCore (x_s y_s z_s x_m y_m z_m t a)
           :precision binary64
           (*
            x_s
            (*
             y_s
             (*
              z_s
              (if (<= z_m 1.05e-183)
                (/ (* (* x_m y_m) z_m) (- z_m))
                (* 1.0 (* y_m x_m)))))))
          z\_m = fabs(z);
          z\_s = copysign(1.0, z);
          y\_m = fabs(y);
          y\_s = copysign(1.0, y);
          x\_m = fabs(x);
          x\_s = copysign(1.0, x);
          assert(x_m < y_m && y_m < z_m && z_m < t && t < a);
          double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
          	double tmp;
          	if (z_m <= 1.05e-183) {
          		tmp = ((x_m * y_m) * z_m) / -z_m;
          	} else {
          		tmp = 1.0 * (y_m * x_m);
          	}
          	return x_s * (y_s * (z_s * tmp));
          }
          
          z\_m = abs(z)
          z\_s = copysign(1.0d0, z)
          y\_m = abs(y)
          y\_s = copysign(1.0d0, y)
          x\_m = abs(x)
          x\_s = copysign(1.0d0, x)
          NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
          real(8) function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
              real(8), intent (in) :: x_s
              real(8), intent (in) :: y_s
              real(8), intent (in) :: z_s
              real(8), intent (in) :: x_m
              real(8), intent (in) :: y_m
              real(8), intent (in) :: z_m
              real(8), intent (in) :: t
              real(8), intent (in) :: a
              real(8) :: tmp
              if (z_m <= 1.05d-183) then
                  tmp = ((x_m * y_m) * z_m) / -z_m
              else
                  tmp = 1.0d0 * (y_m * x_m)
              end if
              code = x_s * (y_s * (z_s * tmp))
          end function
          
          z\_m = Math.abs(z);
          z\_s = Math.copySign(1.0, z);
          y\_m = Math.abs(y);
          y\_s = Math.copySign(1.0, y);
          x\_m = Math.abs(x);
          x\_s = Math.copySign(1.0, x);
          assert x_m < y_m && y_m < z_m && z_m < t && t < a;
          public static double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
          	double tmp;
          	if (z_m <= 1.05e-183) {
          		tmp = ((x_m * y_m) * z_m) / -z_m;
          	} else {
          		tmp = 1.0 * (y_m * x_m);
          	}
          	return x_s * (y_s * (z_s * tmp));
          }
          
          z\_m = math.fabs(z)
          z\_s = math.copysign(1.0, z)
          y\_m = math.fabs(y)
          y\_s = math.copysign(1.0, y)
          x\_m = math.fabs(x)
          x\_s = math.copysign(1.0, x)
          [x_m, y_m, z_m, t, a] = sort([x_m, y_m, z_m, t, a])
          def code(x_s, y_s, z_s, x_m, y_m, z_m, t, a):
          	tmp = 0
          	if z_m <= 1.05e-183:
          		tmp = ((x_m * y_m) * z_m) / -z_m
          	else:
          		tmp = 1.0 * (y_m * x_m)
          	return x_s * (y_s * (z_s * tmp))
          
          z\_m = abs(z)
          z\_s = copysign(1.0, z)
          y\_m = abs(y)
          y\_s = copysign(1.0, y)
          x\_m = abs(x)
          x\_s = copysign(1.0, x)
          x_m, y_m, z_m, t, a = sort([x_m, y_m, z_m, t, a])
          function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
          	tmp = 0.0
          	if (z_m <= 1.05e-183)
          		tmp = Float64(Float64(Float64(x_m * y_m) * z_m) / Float64(-z_m));
          	else
          		tmp = Float64(1.0 * Float64(y_m * x_m));
          	end
          	return Float64(x_s * Float64(y_s * Float64(z_s * tmp)))
          end
          
          z\_m = abs(z);
          z\_s = sign(z) * abs(1.0);
          y\_m = abs(y);
          y\_s = sign(y) * abs(1.0);
          x\_m = abs(x);
          x\_s = sign(x) * abs(1.0);
          x_m, y_m, z_m, t, a = num2cell(sort([x_m, y_m, z_m, t, a])){:}
          function tmp_2 = code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
          	tmp = 0.0;
          	if (z_m <= 1.05e-183)
          		tmp = ((x_m * y_m) * z_m) / -z_m;
          	else
          		tmp = 1.0 * (y_m * x_m);
          	end
          	tmp_2 = x_s * (y_s * (z_s * tmp));
          end
          
          z\_m = N[Abs[z], $MachinePrecision]
          z\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[z]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
          y\_m = N[Abs[y], $MachinePrecision]
          y\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
          x\_m = N[Abs[x], $MachinePrecision]
          x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
          NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
          code[x$95$s_, y$95$s_, z$95$s_, x$95$m_, y$95$m_, z$95$m_, t_, a_] := N[(x$95$s * N[(y$95$s * N[(z$95$s * If[LessEqual[z$95$m, 1.05e-183], N[(N[(N[(x$95$m * y$95$m), $MachinePrecision] * z$95$m), $MachinePrecision] / (-z$95$m)), $MachinePrecision], N[(1.0 * N[(y$95$m * x$95$m), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          z\_m = \left|z\right|
          \\
          z\_s = \mathsf{copysign}\left(1, z\right)
          \\
          y\_m = \left|y\right|
          \\
          y\_s = \mathsf{copysign}\left(1, y\right)
          \\
          x\_m = \left|x\right|
          \\
          x\_s = \mathsf{copysign}\left(1, x\right)
          \\
          [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\
          \\
          x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \begin{array}{l}
          \mathbf{if}\;z\_m \leq 1.05 \cdot 10^{-183}:\\
          \;\;\;\;\frac{\left(x\_m \cdot y\_m\right) \cdot z\_m}{-z\_m}\\
          
          \mathbf{else}:\\
          \;\;\;\;1 \cdot \left(y\_m \cdot x\_m\right)\\
          
          
          \end{array}\right)\right)
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if z < 1.0500000000000001e-183

            1. Initial program 65.1%

              \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
            2. Add Preprocessing
            3. Taylor expanded in z around -inf

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{-1 \cdot z}} \]
            4. Step-by-step derivation
              1. mul-1-negN/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{neg}\left(z\right)}} \]
              2. lower-neg.f6466.6

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{-z}} \]
            5. Applied rewrites66.6%

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

            if 1.0500000000000001e-183 < z

            1. Initial program 57.0%

              \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
            2. Add Preprocessing
            3. Taylor expanded in t around 0

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{z + \frac{-1}{2} \cdot \frac{a \cdot t}{z}}} \]
            4. Step-by-step derivation
              1. +-commutativeN/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\frac{-1}{2} \cdot \frac{a \cdot t}{z} + z}} \]
              2. associate-/l*N/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\frac{-1}{2} \cdot \color{blue}{\left(a \cdot \frac{t}{z}\right)} + z} \]
              3. associate-*r*N/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\left(\frac{-1}{2} \cdot a\right) \cdot \frac{t}{z}} + z} \]
              4. lower-fma.f64N/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
              5. lower-*.f64N/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\color{blue}{\frac{-1}{2} \cdot a}, \frac{t}{z}, z\right)} \]
              6. lower-/.f6474.4

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(-0.5 \cdot a, \color{blue}{\frac{t}{z}}, z\right)} \]
            5. Applied rewrites74.4%

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \]
            6. Step-by-step derivation
              1. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
              2. lift-*.f64N/A

                \[\leadsto \frac{\color{blue}{\left(x \cdot y\right) \cdot z}}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \]
              3. associate-/l*N/A

                \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
              4. *-commutativeN/A

                \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
              5. lower-*.f64N/A

                \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
              6. lower-/.f6482.6

                \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \cdot \left(x \cdot y\right) \]
              7. lift-*.f64N/A

                \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(x \cdot y\right)} \]
              8. *-commutativeN/A

                \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
              9. lower-*.f64N/A

                \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
            7. Applied rewrites82.6%

              \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{t}{z}, -0.5 \cdot a, z\right)} \cdot \left(y \cdot x\right)} \]
            8. Taylor expanded in z around inf

              \[\leadsto \color{blue}{1} \cdot \left(y \cdot x\right) \]
            9. Step-by-step derivation
              1. Applied rewrites81.8%

                \[\leadsto \color{blue}{1} \cdot \left(y \cdot x\right) \]
            10. Recombined 2 regimes into one program.
            11. Add Preprocessing

            Alternative 6: 73.1% accurate, 4.1× speedup?

            \[\begin{array}{l} z\_m = \left|z\right| \\ z\_s = \mathsf{copysign}\left(1, z\right) \\ y\_m = \left|y\right| \\ y\_s = \mathsf{copysign}\left(1, y\right) \\ x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\ \\ x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \left(1 \cdot \left(y\_m \cdot x\_m\right)\right)\right)\right) \end{array} \]
            z\_m = (fabs.f64 z)
            z\_s = (copysign.f64 #s(literal 1 binary64) z)
            y\_m = (fabs.f64 y)
            y\_s = (copysign.f64 #s(literal 1 binary64) y)
            x\_m = (fabs.f64 x)
            x\_s = (copysign.f64 #s(literal 1 binary64) x)
            NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
            (FPCore (x_s y_s z_s x_m y_m z_m t a)
             :precision binary64
             (* x_s (* y_s (* z_s (* 1.0 (* y_m x_m))))))
            z\_m = fabs(z);
            z\_s = copysign(1.0, z);
            y\_m = fabs(y);
            y\_s = copysign(1.0, y);
            x\_m = fabs(x);
            x\_s = copysign(1.0, x);
            assert(x_m < y_m && y_m < z_m && z_m < t && t < a);
            double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
            	return x_s * (y_s * (z_s * (1.0 * (y_m * x_m))));
            }
            
            z\_m = abs(z)
            z\_s = copysign(1.0d0, z)
            y\_m = abs(y)
            y\_s = copysign(1.0d0, y)
            x\_m = abs(x)
            x\_s = copysign(1.0d0, x)
            NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
            real(8) function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
                real(8), intent (in) :: x_s
                real(8), intent (in) :: y_s
                real(8), intent (in) :: z_s
                real(8), intent (in) :: x_m
                real(8), intent (in) :: y_m
                real(8), intent (in) :: z_m
                real(8), intent (in) :: t
                real(8), intent (in) :: a
                code = x_s * (y_s * (z_s * (1.0d0 * (y_m * x_m))))
            end function
            
            z\_m = Math.abs(z);
            z\_s = Math.copySign(1.0, z);
            y\_m = Math.abs(y);
            y\_s = Math.copySign(1.0, y);
            x\_m = Math.abs(x);
            x\_s = Math.copySign(1.0, x);
            assert x_m < y_m && y_m < z_m && z_m < t && t < a;
            public static double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
            	return x_s * (y_s * (z_s * (1.0 * (y_m * x_m))));
            }
            
            z\_m = math.fabs(z)
            z\_s = math.copysign(1.0, z)
            y\_m = math.fabs(y)
            y\_s = math.copysign(1.0, y)
            x\_m = math.fabs(x)
            x\_s = math.copysign(1.0, x)
            [x_m, y_m, z_m, t, a] = sort([x_m, y_m, z_m, t, a])
            def code(x_s, y_s, z_s, x_m, y_m, z_m, t, a):
            	return x_s * (y_s * (z_s * (1.0 * (y_m * x_m))))
            
            z\_m = abs(z)
            z\_s = copysign(1.0, z)
            y\_m = abs(y)
            y\_s = copysign(1.0, y)
            x\_m = abs(x)
            x\_s = copysign(1.0, x)
            x_m, y_m, z_m, t, a = sort([x_m, y_m, z_m, t, a])
            function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
            	return Float64(x_s * Float64(y_s * Float64(z_s * Float64(1.0 * Float64(y_m * x_m)))))
            end
            
            z\_m = abs(z);
            z\_s = sign(z) * abs(1.0);
            y\_m = abs(y);
            y\_s = sign(y) * abs(1.0);
            x\_m = abs(x);
            x\_s = sign(x) * abs(1.0);
            x_m, y_m, z_m, t, a = num2cell(sort([x_m, y_m, z_m, t, a])){:}
            function tmp = code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
            	tmp = x_s * (y_s * (z_s * (1.0 * (y_m * x_m))));
            end
            
            z\_m = N[Abs[z], $MachinePrecision]
            z\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[z]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
            y\_m = N[Abs[y], $MachinePrecision]
            y\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
            x\_m = N[Abs[x], $MachinePrecision]
            x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
            NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
            code[x$95$s_, y$95$s_, z$95$s_, x$95$m_, y$95$m_, z$95$m_, t_, a_] := N[(x$95$s * N[(y$95$s * N[(z$95$s * N[(1.0 * N[(y$95$m * x$95$m), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
            
            \begin{array}{l}
            z\_m = \left|z\right|
            \\
            z\_s = \mathsf{copysign}\left(1, z\right)
            \\
            y\_m = \left|y\right|
            \\
            y\_s = \mathsf{copysign}\left(1, y\right)
            \\
            x\_m = \left|x\right|
            \\
            x\_s = \mathsf{copysign}\left(1, x\right)
            \\
            [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\
            \\
            x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \left(1 \cdot \left(y\_m \cdot x\_m\right)\right)\right)\right)
            \end{array}
            
            Derivation
            1. Initial program 61.7%

              \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
            2. Add Preprocessing
            3. Taylor expanded in t around 0

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{z + \frac{-1}{2} \cdot \frac{a \cdot t}{z}}} \]
            4. Step-by-step derivation
              1. +-commutativeN/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\frac{-1}{2} \cdot \frac{a \cdot t}{z} + z}} \]
              2. associate-/l*N/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\frac{-1}{2} \cdot \color{blue}{\left(a \cdot \frac{t}{z}\right)} + z} \]
              3. associate-*r*N/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\left(\frac{-1}{2} \cdot a\right) \cdot \frac{t}{z}} + z} \]
              4. lower-fma.f64N/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
              5. lower-*.f64N/A

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\color{blue}{\frac{-1}{2} \cdot a}, \frac{t}{z}, z\right)} \]
              6. lower-/.f6444.8

                \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(-0.5 \cdot a, \color{blue}{\frac{t}{z}}, z\right)} \]
            5. Applied rewrites44.8%

              \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \]
            6. Step-by-step derivation
              1. lift-/.f64N/A

                \[\leadsto \color{blue}{\frac{\left(x \cdot y\right) \cdot z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
              2. lift-*.f64N/A

                \[\leadsto \frac{\color{blue}{\left(x \cdot y\right) \cdot z}}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \]
              3. associate-/l*N/A

                \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)}} \]
              4. *-commutativeN/A

                \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
              5. lower-*.f64N/A

                \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{-1}{2} \cdot a, \frac{t}{z}, z\right)} \cdot \left(x \cdot y\right)} \]
              6. lower-/.f6448.2

                \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(-0.5 \cdot a, \frac{t}{z}, z\right)}} \cdot \left(x \cdot y\right) \]
              7. lift-*.f64N/A

                \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(x \cdot y\right)} \]
              8. *-commutativeN/A

                \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
              9. lower-*.f64N/A

                \[\leadsto \frac{z}{\mathsf{Rewrite=>}\left(lower-fma.f64, \left(\mathsf{fma}\left(\frac{t}{z}, \frac{-1}{2} \cdot a, z\right)\right)\right)} \cdot \color{blue}{\left(y \cdot x\right)} \]
            7. Applied rewrites48.2%

              \[\leadsto \color{blue}{\frac{z}{\mathsf{fma}\left(\frac{t}{z}, -0.5 \cdot a, z\right)} \cdot \left(y \cdot x\right)} \]
            8. Taylor expanded in z around inf

              \[\leadsto \color{blue}{1} \cdot \left(y \cdot x\right) \]
            9. Step-by-step derivation
              1. Applied rewrites44.9%

                \[\leadsto \color{blue}{1} \cdot \left(y \cdot x\right) \]
              2. Add Preprocessing

              Alternative 7: 13.8% accurate, 5.6× speedup?

              \[\begin{array}{l} z\_m = \left|z\right| \\ z\_s = \mathsf{copysign}\left(1, z\right) \\ y\_m = \left|y\right| \\ y\_s = \mathsf{copysign}\left(1, y\right) \\ x\_m = \left|x\right| \\ x\_s = \mathsf{copysign}\left(1, x\right) \\ [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\ \\ x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \left(\left(-y\_m\right) \cdot x\_m\right)\right)\right) \end{array} \]
              z\_m = (fabs.f64 z)
              z\_s = (copysign.f64 #s(literal 1 binary64) z)
              y\_m = (fabs.f64 y)
              y\_s = (copysign.f64 #s(literal 1 binary64) y)
              x\_m = (fabs.f64 x)
              x\_s = (copysign.f64 #s(literal 1 binary64) x)
              NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
              (FPCore (x_s y_s z_s x_m y_m z_m t a)
               :precision binary64
               (* x_s (* y_s (* z_s (* (- y_m) x_m)))))
              z\_m = fabs(z);
              z\_s = copysign(1.0, z);
              y\_m = fabs(y);
              y\_s = copysign(1.0, y);
              x\_m = fabs(x);
              x\_s = copysign(1.0, x);
              assert(x_m < y_m && y_m < z_m && z_m < t && t < a);
              double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
              	return x_s * (y_s * (z_s * (-y_m * x_m)));
              }
              
              z\_m = abs(z)
              z\_s = copysign(1.0d0, z)
              y\_m = abs(y)
              y\_s = copysign(1.0d0, y)
              x\_m = abs(x)
              x\_s = copysign(1.0d0, x)
              NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
              real(8) function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
                  real(8), intent (in) :: x_s
                  real(8), intent (in) :: y_s
                  real(8), intent (in) :: z_s
                  real(8), intent (in) :: x_m
                  real(8), intent (in) :: y_m
                  real(8), intent (in) :: z_m
                  real(8), intent (in) :: t
                  real(8), intent (in) :: a
                  code = x_s * (y_s * (z_s * (-y_m * x_m)))
              end function
              
              z\_m = Math.abs(z);
              z\_s = Math.copySign(1.0, z);
              y\_m = Math.abs(y);
              y\_s = Math.copySign(1.0, y);
              x\_m = Math.abs(x);
              x\_s = Math.copySign(1.0, x);
              assert x_m < y_m && y_m < z_m && z_m < t && t < a;
              public static double code(double x_s, double y_s, double z_s, double x_m, double y_m, double z_m, double t, double a) {
              	return x_s * (y_s * (z_s * (-y_m * x_m)));
              }
              
              z\_m = math.fabs(z)
              z\_s = math.copysign(1.0, z)
              y\_m = math.fabs(y)
              y\_s = math.copysign(1.0, y)
              x\_m = math.fabs(x)
              x\_s = math.copysign(1.0, x)
              [x_m, y_m, z_m, t, a] = sort([x_m, y_m, z_m, t, a])
              def code(x_s, y_s, z_s, x_m, y_m, z_m, t, a):
              	return x_s * (y_s * (z_s * (-y_m * x_m)))
              
              z\_m = abs(z)
              z\_s = copysign(1.0, z)
              y\_m = abs(y)
              y\_s = copysign(1.0, y)
              x\_m = abs(x)
              x\_s = copysign(1.0, x)
              x_m, y_m, z_m, t, a = sort([x_m, y_m, z_m, t, a])
              function code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
              	return Float64(x_s * Float64(y_s * Float64(z_s * Float64(Float64(-y_m) * x_m))))
              end
              
              z\_m = abs(z);
              z\_s = sign(z) * abs(1.0);
              y\_m = abs(y);
              y\_s = sign(y) * abs(1.0);
              x\_m = abs(x);
              x\_s = sign(x) * abs(1.0);
              x_m, y_m, z_m, t, a = num2cell(sort([x_m, y_m, z_m, t, a])){:}
              function tmp = code(x_s, y_s, z_s, x_m, y_m, z_m, t, a)
              	tmp = x_s * (y_s * (z_s * (-y_m * x_m)));
              end
              
              z\_m = N[Abs[z], $MachinePrecision]
              z\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[z]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
              y\_m = N[Abs[y], $MachinePrecision]
              y\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
              x\_m = N[Abs[x], $MachinePrecision]
              x\_s = N[With[{TMP1 = Abs[1.0], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
              NOTE: x_m, y_m, z_m, t, and a should be sorted in increasing order before calling this function.
              code[x$95$s_, y$95$s_, z$95$s_, x$95$m_, y$95$m_, z$95$m_, t_, a_] := N[(x$95$s * N[(y$95$s * N[(z$95$s * N[((-y$95$m) * x$95$m), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
              
              \begin{array}{l}
              z\_m = \left|z\right|
              \\
              z\_s = \mathsf{copysign}\left(1, z\right)
              \\
              y\_m = \left|y\right|
              \\
              y\_s = \mathsf{copysign}\left(1, y\right)
              \\
              x\_m = \left|x\right|
              \\
              x\_s = \mathsf{copysign}\left(1, x\right)
              \\
              [x_m, y_m, z_m, t, a] = \mathsf{sort}([x_m, y_m, z_m, t, a])\\
              \\
              x\_s \cdot \left(y\_s \cdot \left(z\_s \cdot \left(\left(-y\_m\right) \cdot x\_m\right)\right)\right)
              \end{array}
              
              Derivation
              1. Initial program 61.7%

                \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}} \]
              2. Add Preprocessing
              3. Taylor expanded in z around -inf

                \[\leadsto \color{blue}{-1 \cdot \left(x \cdot y\right)} \]
              4. Step-by-step derivation
                1. mul-1-negN/A

                  \[\leadsto \color{blue}{\mathsf{neg}\left(x \cdot y\right)} \]
                2. *-commutativeN/A

                  \[\leadsto \mathsf{neg}\left(\color{blue}{y \cdot x}\right) \]
                3. distribute-lft-neg-inN/A

                  \[\leadsto \color{blue}{\left(\mathsf{neg}\left(y\right)\right) \cdot x} \]
                4. lower-*.f64N/A

                  \[\leadsto \color{blue}{\left(\mathsf{neg}\left(y\right)\right) \cdot x} \]
                5. lower-neg.f6444.8

                  \[\leadsto \color{blue}{\left(-y\right)} \cdot x \]
              5. Applied rewrites44.8%

                \[\leadsto \color{blue}{\left(-y\right) \cdot x} \]
              6. Add Preprocessing

              Developer Target 1: 87.9% accurate, 0.7× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;z < -3.1921305903852764 \cdot 10^{+46}:\\ \;\;\;\;-y \cdot x\\ \mathbf{elif}\;z < 5.976268120920894 \cdot 10^{+90}:\\ \;\;\;\;\frac{x \cdot z}{\frac{\sqrt{z \cdot z - a \cdot t}}{y}}\\ \mathbf{else}:\\ \;\;\;\;y \cdot x\\ \end{array} \end{array} \]
              (FPCore (x y z t a)
               :precision binary64
               (if (< z -3.1921305903852764e+46)
                 (- (* y x))
                 (if (< z 5.976268120920894e+90)
                   (/ (* x z) (/ (sqrt (- (* z z) (* a t))) y))
                   (* y x))))
              double code(double x, double y, double z, double t, double a) {
              	double tmp;
              	if (z < -3.1921305903852764e+46) {
              		tmp = -(y * x);
              	} else if (z < 5.976268120920894e+90) {
              		tmp = (x * z) / (sqrt(((z * z) - (a * t))) / y);
              	} else {
              		tmp = y * x;
              	}
              	return tmp;
              }
              
              real(8) function code(x, y, z, t, a)
                  real(8), intent (in) :: x
                  real(8), intent (in) :: y
                  real(8), intent (in) :: z
                  real(8), intent (in) :: t
                  real(8), intent (in) :: a
                  real(8) :: tmp
                  if (z < (-3.1921305903852764d+46)) then
                      tmp = -(y * x)
                  else if (z < 5.976268120920894d+90) then
                      tmp = (x * z) / (sqrt(((z * z) - (a * t))) / y)
                  else
                      tmp = y * x
                  end if
                  code = tmp
              end function
              
              public static double code(double x, double y, double z, double t, double a) {
              	double tmp;
              	if (z < -3.1921305903852764e+46) {
              		tmp = -(y * x);
              	} else if (z < 5.976268120920894e+90) {
              		tmp = (x * z) / (Math.sqrt(((z * z) - (a * t))) / y);
              	} else {
              		tmp = y * x;
              	}
              	return tmp;
              }
              
              def code(x, y, z, t, a):
              	tmp = 0
              	if z < -3.1921305903852764e+46:
              		tmp = -(y * x)
              	elif z < 5.976268120920894e+90:
              		tmp = (x * z) / (math.sqrt(((z * z) - (a * t))) / y)
              	else:
              		tmp = y * x
              	return tmp
              
              function code(x, y, z, t, a)
              	tmp = 0.0
              	if (z < -3.1921305903852764e+46)
              		tmp = Float64(-Float64(y * x));
              	elseif (z < 5.976268120920894e+90)
              		tmp = Float64(Float64(x * z) / Float64(sqrt(Float64(Float64(z * z) - Float64(a * t))) / y));
              	else
              		tmp = Float64(y * x);
              	end
              	return tmp
              end
              
              function tmp_2 = code(x, y, z, t, a)
              	tmp = 0.0;
              	if (z < -3.1921305903852764e+46)
              		tmp = -(y * x);
              	elseif (z < 5.976268120920894e+90)
              		tmp = (x * z) / (sqrt(((z * z) - (a * t))) / y);
              	else
              		tmp = y * x;
              	end
              	tmp_2 = tmp;
              end
              
              code[x_, y_, z_, t_, a_] := If[Less[z, -3.1921305903852764e+46], (-N[(y * x), $MachinePrecision]), If[Less[z, 5.976268120920894e+90], N[(N[(x * z), $MachinePrecision] / N[(N[Sqrt[N[(N[(z * z), $MachinePrecision] - N[(a * t), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] / y), $MachinePrecision]), $MachinePrecision], N[(y * x), $MachinePrecision]]]
              
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              \mathbf{if}\;z < -3.1921305903852764 \cdot 10^{+46}:\\
              \;\;\;\;-y \cdot x\\
              
              \mathbf{elif}\;z < 5.976268120920894 \cdot 10^{+90}:\\
              \;\;\;\;\frac{x \cdot z}{\frac{\sqrt{z \cdot z - a \cdot t}}{y}}\\
              
              \mathbf{else}:\\
              \;\;\;\;y \cdot x\\
              
              
              \end{array}
              \end{array}
              

              Reproduce

              ?
              herbie shell --seed 2024329 
              (FPCore (x y z t a)
                :name "Statistics.Math.RootFinding:ridders from math-functions-0.1.5.2"
                :precision binary64
              
                :alt
                (! :herbie-platform default (if (< z -31921305903852764000000000000000000000000000000) (- (* y x)) (if (< z 5976268120920894000000000000000000000000000000000000000000000000000000000000000000000000000) (/ (* x z) (/ (sqrt (- (* z z) (* a t))) y)) (* y x))))
              
                (/ (* (* x y) z) (sqrt (- (* z z) (* t a)))))