Diagrams.ThreeD.Shapes:frustum from diagrams-lib-1.3.0.3, A

Percentage Accurate: 90.3% → 96.0%
Time: 10.1s
Alternatives: 13
Speedup: 0.5×

Specification

?
\[\begin{array}{l} \\ 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \end{array} \]
(FPCore (x y z t a b c i)
 :precision binary64
 (* 2.0 (- (+ (* x y) (* z t)) (* (* (+ a (* b c)) c) i))))
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	return 2.0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i));
}
real(8) function code(x, y, z, t, a, b, c, i)
    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), intent (in) :: b
    real(8), intent (in) :: c
    real(8), intent (in) :: i
    code = 2.0d0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i))
end function
public static double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	return 2.0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i));
}
def code(x, y, z, t, a, b, c, i):
	return 2.0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i))
function code(x, y, z, t, a, b, c, i)
	return Float64(2.0 * Float64(Float64(Float64(x * y) + Float64(z * t)) - Float64(Float64(Float64(a + Float64(b * c)) * c) * i)))
end
function tmp = code(x, y, z, t, a, b, c, i)
	tmp = 2.0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i));
end
code[x_, y_, z_, t_, a_, b_, c_, i_] := N[(2.0 * N[(N[(N[(x * y), $MachinePrecision] + N[(z * t), $MachinePrecision]), $MachinePrecision] - N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)
\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 13 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: 90.3% accurate, 1.0× speedup?

\[\begin{array}{l} \\ 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \end{array} \]
(FPCore (x y z t a b c i)
 :precision binary64
 (* 2.0 (- (+ (* x y) (* z t)) (* (* (+ a (* b c)) c) i))))
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	return 2.0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i));
}
real(8) function code(x, y, z, t, a, b, c, i)
    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), intent (in) :: b
    real(8), intent (in) :: c
    real(8), intent (in) :: i
    code = 2.0d0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i))
end function
public static double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	return 2.0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i));
}
def code(x, y, z, t, a, b, c, i):
	return 2.0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i))
function code(x, y, z, t, a, b, c, i)
	return Float64(2.0 * Float64(Float64(Float64(x * y) + Float64(z * t)) - Float64(Float64(Float64(a + Float64(b * c)) * c) * i)))
end
function tmp = code(x, y, z, t, a, b, c, i)
	tmp = 2.0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i));
end
code[x_, y_, z_, t_, a_, b_, c_, i_] := N[(2.0 * N[(N[(N[(x * y), $MachinePrecision] + N[(z * t), $MachinePrecision]), $MachinePrecision] - N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)
\end{array}

Alternative 1: 96.0% accurate, 0.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\ \mathbf{if}\;t\_1 \leq -\infty:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\ \mathbf{elif}\;t\_1 \leq 10^{+296}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\mathsf{fma}\left(i, \frac{a}{c}, i \cdot b\right) \cdot c\right) \cdot c\right)\\ \end{array} \end{array} \]
(FPCore (x y z t a b c i)
 :precision binary64
 (let* ((t_1 (* (* (+ a (* b c)) c) i)))
   (if (<= t_1 (- INFINITY))
     (* 2.0 (fma z t (* (- c) (* (fma b c a) i))))
     (if (<= t_1 1e+296)
       (* 2.0 (fma z t (- (* y x) (* i (* (fma c b a) c)))))
       (* 2.0 (- (+ (* x y) (* z t)) (* (* (fma i (/ a c) (* i b)) c) c)))))))
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	double t_1 = ((a + (b * c)) * c) * i;
	double tmp;
	if (t_1 <= -((double) INFINITY)) {
		tmp = 2.0 * fma(z, t, (-c * (fma(b, c, a) * i)));
	} else if (t_1 <= 1e+296) {
		tmp = 2.0 * fma(z, t, ((y * x) - (i * (fma(c, b, a) * c))));
	} else {
		tmp = 2.0 * (((x * y) + (z * t)) - ((fma(i, (a / c), (i * b)) * c) * c));
	}
	return tmp;
}
function code(x, y, z, t, a, b, c, i)
	t_1 = Float64(Float64(Float64(a + Float64(b * c)) * c) * i)
	tmp = 0.0
	if (t_1 <= Float64(-Inf))
		tmp = Float64(2.0 * fma(z, t, Float64(Float64(-c) * Float64(fma(b, c, a) * i))));
	elseif (t_1 <= 1e+296)
		tmp = Float64(2.0 * fma(z, t, Float64(Float64(y * x) - Float64(i * Float64(fma(c, b, a) * c)))));
	else
		tmp = Float64(2.0 * Float64(Float64(Float64(x * y) + Float64(z * t)) - Float64(Float64(fma(i, Float64(a / c), Float64(i * b)) * c) * c)));
	end
	return tmp
end
code[x_, y_, z_, t_, a_, b_, c_, i_] := Block[{t$95$1 = N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]}, If[LessEqual[t$95$1, (-Infinity)], N[(2.0 * N[(z * t + N[((-c) * N[(N[(b * c + a), $MachinePrecision] * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, 1e+296], N[(2.0 * N[(z * t + N[(N[(y * x), $MachinePrecision] - N[(i * N[(N[(c * b + a), $MachinePrecision] * c), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(2.0 * N[(N[(N[(x * y), $MachinePrecision] + N[(z * t), $MachinePrecision]), $MachinePrecision] - N[(N[(N[(i * N[(a / c), $MachinePrecision] + N[(i * b), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * c), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\
\mathbf{if}\;t\_1 \leq -\infty:\\
\;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\

\mathbf{elif}\;t\_1 \leq 10^{+296}:\\
\;\;\;\;2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)\\

\mathbf{else}:\\
\;\;\;\;2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\mathsf{fma}\left(i, \frac{a}{c}, i \cdot b\right) \cdot c\right) \cdot c\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < -inf.0

    1. Initial program 66.1%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      2. lift-+.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(x \cdot y + z \cdot t\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      3. +-commutativeN/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(z \cdot t + x \cdot y\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      4. associate--l+N/A

        \[\leadsto 2 \cdot \color{blue}{\left(z \cdot t + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{z \cdot t} + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right) \]
      6. lower-fma.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      7. lower--.f6468.2

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{x \cdot y} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      9. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{y \cdot x} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      10. lower-*.f6468.2

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i}\right) \]
      12. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      13. lower-*.f6468.2

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      14. lift-+.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\left(a + b \cdot c\right)} \cdot c\right)\right) \]
      15. +-commutativeN/A

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{b \cdot c} + a\right) \cdot c\right)\right) \]
      17. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{c \cdot b} + a\right) \cdot c\right)\right) \]
      18. lower-fma.f6468.2

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\mathsf{fma}\left(c, b, a\right)} \cdot c\right)\right) \]
    4. Applied rewrites68.2%

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)} \]
    5. Taylor expanded in x around 0

      \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{-1 \cdot \left(c \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right)}\right) \]
    6. Step-by-step derivation
      1. associate-*r*N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-1 \cdot c\right) \cdot \left(i \cdot \left(a + b \cdot c\right)\right)}\right) \]
      2. lower-*.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-1 \cdot c\right) \cdot \left(i \cdot \left(a + b \cdot c\right)\right)}\right) \]
      3. mul-1-negN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(\mathsf{neg}\left(c\right)\right)} \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right) \]
      4. lower-neg.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-c\right)} \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right) \]
      5. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \]
      6. lower-*.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \]
      7. +-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\color{blue}{\left(b \cdot c + a\right)} \cdot i\right)\right) \]
      8. lower-fma.f6494.1

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\color{blue}{\mathsf{fma}\left(b, c, a\right)} \cdot i\right)\right) \]
    7. Applied rewrites94.1%

      \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)}\right) \]

    if -inf.0 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < 9.99999999999999981e295

    1. Initial program 98.6%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      2. lift-+.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(x \cdot y + z \cdot t\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      3. +-commutativeN/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(z \cdot t + x \cdot y\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      4. associate--l+N/A

        \[\leadsto 2 \cdot \color{blue}{\left(z \cdot t + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{z \cdot t} + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right) \]
      6. lower-fma.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      7. lower--.f6498.6

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{x \cdot y} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      9. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{y \cdot x} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      10. lower-*.f6498.6

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i}\right) \]
      12. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      13. lower-*.f6498.6

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      14. lift-+.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\left(a + b \cdot c\right)} \cdot c\right)\right) \]
      15. +-commutativeN/A

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{b \cdot c} + a\right) \cdot c\right)\right) \]
      17. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{c \cdot b} + a\right) \cdot c\right)\right) \]
      18. lower-fma.f6498.6

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\mathsf{fma}\left(c, b, a\right)} \cdot c\right)\right) \]
    4. Applied rewrites98.6%

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)} \]

    if 9.99999999999999981e295 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)

    1. Initial program 71.8%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Taylor expanded in c around inf

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

        \[\leadsto 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \color{blue}{\left(b \cdot i + \frac{a \cdot i}{c}\right) \cdot {c}^{2}}\right) \]
      2. unpow2N/A

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

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

        \[\leadsto 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \color{blue}{\left(\left(b \cdot i + \frac{a \cdot i}{c}\right) \cdot c\right) \cdot c}\right) \]
      5. lower-*.f64N/A

        \[\leadsto 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \color{blue}{\left(\left(b \cdot i + \frac{a \cdot i}{c}\right) \cdot c\right)} \cdot c\right) \]
      6. +-commutativeN/A

        \[\leadsto 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\color{blue}{\left(\frac{a \cdot i}{c} + b \cdot i\right)} \cdot c\right) \cdot c\right) \]
      7. *-commutativeN/A

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

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

        \[\leadsto 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\color{blue}{\mathsf{fma}\left(i, \frac{a}{c}, b \cdot i\right)} \cdot c\right) \cdot c\right) \]
      10. lower-/.f64N/A

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

        \[\leadsto 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\mathsf{fma}\left(i, \frac{a}{c}, \color{blue}{i \cdot b}\right) \cdot c\right) \cdot c\right) \]
      12. lower-*.f6490.3

        \[\leadsto 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\mathsf{fma}\left(i, \frac{a}{c}, \color{blue}{i \cdot b}\right) \cdot c\right) \cdot c\right) \]
    5. Applied rewrites90.3%

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

Alternative 2: 96.7% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\ \mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 10^{+302}\right):\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)\\ \end{array} \end{array} \]
(FPCore (x y z t a b c i)
 :precision binary64
 (let* ((t_1 (* (* (+ a (* b c)) c) i)))
   (if (or (<= t_1 (- INFINITY)) (not (<= t_1 1e+302)))
     (* 2.0 (fma z t (* (- c) (* (fma b c a) i))))
     (* 2.0 (fma z t (- (* y x) (* i (* (fma c b a) c))))))))
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	double t_1 = ((a + (b * c)) * c) * i;
	double tmp;
	if ((t_1 <= -((double) INFINITY)) || !(t_1 <= 1e+302)) {
		tmp = 2.0 * fma(z, t, (-c * (fma(b, c, a) * i)));
	} else {
		tmp = 2.0 * fma(z, t, ((y * x) - (i * (fma(c, b, a) * c))));
	}
	return tmp;
}
function code(x, y, z, t, a, b, c, i)
	t_1 = Float64(Float64(Float64(a + Float64(b * c)) * c) * i)
	tmp = 0.0
	if ((t_1 <= Float64(-Inf)) || !(t_1 <= 1e+302))
		tmp = Float64(2.0 * fma(z, t, Float64(Float64(-c) * Float64(fma(b, c, a) * i))));
	else
		tmp = Float64(2.0 * fma(z, t, Float64(Float64(y * x) - Float64(i * Float64(fma(c, b, a) * c)))));
	end
	return tmp
end
code[x_, y_, z_, t_, a_, b_, c_, i_] := Block[{t$95$1 = N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]}, If[Or[LessEqual[t$95$1, (-Infinity)], N[Not[LessEqual[t$95$1, 1e+302]], $MachinePrecision]], N[(2.0 * N[(z * t + N[((-c) * N[(N[(b * c + a), $MachinePrecision] * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(2.0 * N[(z * t + N[(N[(y * x), $MachinePrecision] - N[(i * N[(N[(c * b + a), $MachinePrecision] * c), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\
\mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 10^{+302}\right):\\
\;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\

\mathbf{else}:\\
\;\;\;\;2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < -inf.0 or 1.0000000000000001e302 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)

    1. Initial program 68.8%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      2. lift-+.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(x \cdot y + z \cdot t\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      3. +-commutativeN/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(z \cdot t + x \cdot y\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      4. associate--l+N/A

        \[\leadsto 2 \cdot \color{blue}{\left(z \cdot t + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{z \cdot t} + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right) \]
      6. lower-fma.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      7. lower--.f6471.8

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{x \cdot y} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      9. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{y \cdot x} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      10. lower-*.f6471.8

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i}\right) \]
      12. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      13. lower-*.f6471.8

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      14. lift-+.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\left(a + b \cdot c\right)} \cdot c\right)\right) \]
      15. +-commutativeN/A

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{b \cdot c} + a\right) \cdot c\right)\right) \]
      17. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{c \cdot b} + a\right) \cdot c\right)\right) \]
      18. lower-fma.f6471.8

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\mathsf{fma}\left(c, b, a\right)} \cdot c\right)\right) \]
    4. Applied rewrites71.8%

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)} \]
    5. Taylor expanded in x around 0

      \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{-1 \cdot \left(c \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right)}\right) \]
    6. Step-by-step derivation
      1. associate-*r*N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-1 \cdot c\right) \cdot \left(i \cdot \left(a + b \cdot c\right)\right)}\right) \]
      2. lower-*.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-1 \cdot c\right) \cdot \left(i \cdot \left(a + b \cdot c\right)\right)}\right) \]
      3. mul-1-negN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(\mathsf{neg}\left(c\right)\right)} \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right) \]
      4. lower-neg.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-c\right)} \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right) \]
      5. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \]
      6. lower-*.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \]
      7. +-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\color{blue}{\left(b \cdot c + a\right)} \cdot i\right)\right) \]
      8. lower-fma.f6490.3

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\color{blue}{\mathsf{fma}\left(b, c, a\right)} \cdot i\right)\right) \]
    7. Applied rewrites90.3%

      \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)}\right) \]

    if -inf.0 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < 1.0000000000000001e302

    1. Initial program 98.6%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      2. lift-+.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(x \cdot y + z \cdot t\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      3. +-commutativeN/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(z \cdot t + x \cdot y\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      4. associate--l+N/A

        \[\leadsto 2 \cdot \color{blue}{\left(z \cdot t + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{z \cdot t} + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right) \]
      6. lower-fma.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      7. lower--.f6498.6

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{x \cdot y} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      9. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{y \cdot x} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      10. lower-*.f6498.6

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i}\right) \]
      12. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      13. lower-*.f6498.6

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      14. lift-+.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\left(a + b \cdot c\right)} \cdot c\right)\right) \]
      15. +-commutativeN/A

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{b \cdot c} + a\right) \cdot c\right)\right) \]
      17. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{c \cdot b} + a\right) \cdot c\right)\right) \]
      18. lower-fma.f6498.6

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\mathsf{fma}\left(c, b, a\right)} \cdot c\right)\right) \]
    4. Applied rewrites98.6%

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification95.4%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq -\infty \lor \neg \left(\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq 10^{+302}\right):\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)\\ \end{array} \]
  5. Add Preprocessing

Alternative 3: 90.7% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\ \mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 10^{+242}\right):\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(a \cdot c\right)\right)\\ \end{array} \end{array} \]
(FPCore (x y z t a b c i)
 :precision binary64
 (let* ((t_1 (* (* (+ a (* b c)) c) i)))
   (if (or (<= t_1 (- INFINITY)) (not (<= t_1 1e+242)))
     (* 2.0 (fma z t (* (- c) (* (fma b c a) i))))
     (* 2.0 (fma z t (- (* y x) (* i (* a c))))))))
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	double t_1 = ((a + (b * c)) * c) * i;
	double tmp;
	if ((t_1 <= -((double) INFINITY)) || !(t_1 <= 1e+242)) {
		tmp = 2.0 * fma(z, t, (-c * (fma(b, c, a) * i)));
	} else {
		tmp = 2.0 * fma(z, t, ((y * x) - (i * (a * c))));
	}
	return tmp;
}
function code(x, y, z, t, a, b, c, i)
	t_1 = Float64(Float64(Float64(a + Float64(b * c)) * c) * i)
	tmp = 0.0
	if ((t_1 <= Float64(-Inf)) || !(t_1 <= 1e+242))
		tmp = Float64(2.0 * fma(z, t, Float64(Float64(-c) * Float64(fma(b, c, a) * i))));
	else
		tmp = Float64(2.0 * fma(z, t, Float64(Float64(y * x) - Float64(i * Float64(a * c)))));
	end
	return tmp
end
code[x_, y_, z_, t_, a_, b_, c_, i_] := Block[{t$95$1 = N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]}, If[Or[LessEqual[t$95$1, (-Infinity)], N[Not[LessEqual[t$95$1, 1e+242]], $MachinePrecision]], N[(2.0 * N[(z * t + N[((-c) * N[(N[(b * c + a), $MachinePrecision] * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(2.0 * N[(z * t + N[(N[(y * x), $MachinePrecision] - N[(i * N[(a * c), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\
\mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 10^{+242}\right):\\
\;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\

\mathbf{else}:\\
\;\;\;\;2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(a \cdot c\right)\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < -inf.0 or 1.00000000000000005e242 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)

    1. Initial program 70.2%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      2. lift-+.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(x \cdot y + z \cdot t\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      3. +-commutativeN/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(z \cdot t + x \cdot y\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      4. associate--l+N/A

        \[\leadsto 2 \cdot \color{blue}{\left(z \cdot t + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{z \cdot t} + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right) \]
      6. lower-fma.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      7. lower--.f6473.0

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{x \cdot y} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      9. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{y \cdot x} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      10. lower-*.f6473.0

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i}\right) \]
      12. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      13. lower-*.f6473.0

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      14. lift-+.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\left(a + b \cdot c\right)} \cdot c\right)\right) \]
      15. +-commutativeN/A

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{b \cdot c} + a\right) \cdot c\right)\right) \]
      17. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{c \cdot b} + a\right) \cdot c\right)\right) \]
      18. lower-fma.f6473.0

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\mathsf{fma}\left(c, b, a\right)} \cdot c\right)\right) \]
    4. Applied rewrites73.0%

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)} \]
    5. Taylor expanded in x around 0

      \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{-1 \cdot \left(c \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right)}\right) \]
    6. Step-by-step derivation
      1. associate-*r*N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-1 \cdot c\right) \cdot \left(i \cdot \left(a + b \cdot c\right)\right)}\right) \]
      2. lower-*.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-1 \cdot c\right) \cdot \left(i \cdot \left(a + b \cdot c\right)\right)}\right) \]
      3. mul-1-negN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(\mathsf{neg}\left(c\right)\right)} \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right) \]
      4. lower-neg.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-c\right)} \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right) \]
      5. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \]
      6. lower-*.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \]
      7. +-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\color{blue}{\left(b \cdot c + a\right)} \cdot i\right)\right) \]
      8. lower-fma.f6488.3

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\color{blue}{\mathsf{fma}\left(b, c, a\right)} \cdot i\right)\right) \]
    7. Applied rewrites88.3%

      \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)}\right) \]

    if -inf.0 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < 1.00000000000000005e242

    1. Initial program 99.2%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      2. lift-+.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(x \cdot y + z \cdot t\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      3. +-commutativeN/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(z \cdot t + x \cdot y\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      4. associate--l+N/A

        \[\leadsto 2 \cdot \color{blue}{\left(z \cdot t + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{z \cdot t} + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right) \]
      6. lower-fma.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      7. lower--.f6499.2

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{x \cdot y} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      9. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{y \cdot x} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      10. lower-*.f6499.2

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i}\right) \]
      12. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      13. lower-*.f6499.2

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      14. lift-+.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\left(a + b \cdot c\right)} \cdot c\right)\right) \]
      15. +-commutativeN/A

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{b \cdot c} + a\right) \cdot c\right)\right) \]
      17. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{c \cdot b} + a\right) \cdot c\right)\right) \]
      18. lower-fma.f6499.2

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\mathsf{fma}\left(c, b, a\right)} \cdot c\right)\right) \]
    4. Applied rewrites99.2%

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)} \]
    5. Taylor expanded in a around inf

      \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \color{blue}{\left(a \cdot c\right)}\right) \]
    6. Step-by-step derivation
      1. lower-*.f6492.7

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \color{blue}{\left(a \cdot c\right)}\right) \]
    7. Applied rewrites92.7%

      \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \color{blue}{\left(a \cdot c\right)}\right) \]
  3. Recombined 2 regimes into one program.
  4. Final simplification90.9%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq -\infty \lor \neg \left(\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq 10^{+242}\right):\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(a \cdot c\right)\right)\\ \end{array} \]
  5. Add Preprocessing

Alternative 4: 90.7% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\ \mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 10^{+242}\right):\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, y \cdot x\right)\right)\\ \end{array} \end{array} \]
(FPCore (x y z t a b c i)
 :precision binary64
 (let* ((t_1 (* (* (+ a (* b c)) c) i)))
   (if (or (<= t_1 (- INFINITY)) (not (<= t_1 1e+242)))
     (* 2.0 (fma z t (* (- c) (* (fma b c a) i))))
     (* 2.0 (fma (- i) (* c a) (fma t z (* y x)))))))
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	double t_1 = ((a + (b * c)) * c) * i;
	double tmp;
	if ((t_1 <= -((double) INFINITY)) || !(t_1 <= 1e+242)) {
		tmp = 2.0 * fma(z, t, (-c * (fma(b, c, a) * i)));
	} else {
		tmp = 2.0 * fma(-i, (c * a), fma(t, z, (y * x)));
	}
	return tmp;
}
function code(x, y, z, t, a, b, c, i)
	t_1 = Float64(Float64(Float64(a + Float64(b * c)) * c) * i)
	tmp = 0.0
	if ((t_1 <= Float64(-Inf)) || !(t_1 <= 1e+242))
		tmp = Float64(2.0 * fma(z, t, Float64(Float64(-c) * Float64(fma(b, c, a) * i))));
	else
		tmp = Float64(2.0 * fma(Float64(-i), Float64(c * a), fma(t, z, Float64(y * x))));
	end
	return tmp
end
code[x_, y_, z_, t_, a_, b_, c_, i_] := Block[{t$95$1 = N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]}, If[Or[LessEqual[t$95$1, (-Infinity)], N[Not[LessEqual[t$95$1, 1e+242]], $MachinePrecision]], N[(2.0 * N[(z * t + N[((-c) * N[(N[(b * c + a), $MachinePrecision] * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(2.0 * N[((-i) * N[(c * a), $MachinePrecision] + N[(t * z + N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\
\mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 10^{+242}\right):\\
\;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\

\mathbf{else}:\\
\;\;\;\;2 \cdot \mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, y \cdot x\right)\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < -inf.0 or 1.00000000000000005e242 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)

    1. Initial program 70.2%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      2. lift-+.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(x \cdot y + z \cdot t\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      3. +-commutativeN/A

        \[\leadsto 2 \cdot \left(\color{blue}{\left(z \cdot t + x \cdot y\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      4. associate--l+N/A

        \[\leadsto 2 \cdot \color{blue}{\left(z \cdot t + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto 2 \cdot \left(\color{blue}{z \cdot t} + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right) \]
      6. lower-fma.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
      7. lower--.f6473.0

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{x \cdot y} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      9. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{y \cdot x} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      10. lower-*.f6473.0

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i}\right) \]
      12. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      13. lower-*.f6473.0

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
      14. lift-+.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\left(a + b \cdot c\right)} \cdot c\right)\right) \]
      15. +-commutativeN/A

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{b \cdot c} + a\right) \cdot c\right)\right) \]
      17. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{c \cdot b} + a\right) \cdot c\right)\right) \]
      18. lower-fma.f6473.0

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\mathsf{fma}\left(c, b, a\right)} \cdot c\right)\right) \]
    4. Applied rewrites73.0%

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)} \]
    5. Taylor expanded in x around 0

      \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{-1 \cdot \left(c \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right)}\right) \]
    6. Step-by-step derivation
      1. associate-*r*N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-1 \cdot c\right) \cdot \left(i \cdot \left(a + b \cdot c\right)\right)}\right) \]
      2. lower-*.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-1 \cdot c\right) \cdot \left(i \cdot \left(a + b \cdot c\right)\right)}\right) \]
      3. mul-1-negN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(\mathsf{neg}\left(c\right)\right)} \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right) \]
      4. lower-neg.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-c\right)} \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right) \]
      5. *-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \]
      6. lower-*.f64N/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \]
      7. +-commutativeN/A

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\color{blue}{\left(b \cdot c + a\right)} \cdot i\right)\right) \]
      8. lower-fma.f6488.3

        \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\color{blue}{\mathsf{fma}\left(b, c, a\right)} \cdot i\right)\right) \]
    7. Applied rewrites88.3%

      \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{\left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)}\right) \]

    if -inf.0 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < 1.00000000000000005e242

    1. Initial program 99.2%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Taylor expanded in b around 0

      \[\leadsto 2 \cdot \color{blue}{\left(\left(t \cdot z + x \cdot y\right) - a \cdot \left(c \cdot i\right)\right)} \]
    4. Step-by-step derivation
      1. fp-cancel-sub-sign-invN/A

        \[\leadsto 2 \cdot \color{blue}{\left(\left(t \cdot z + x \cdot y\right) + \left(\mathsf{neg}\left(a\right)\right) \cdot \left(c \cdot i\right)\right)} \]
      2. distribute-lft-neg-inN/A

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

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

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

        \[\leadsto 2 \cdot \left(\color{blue}{\left(\mathsf{neg}\left(a \cdot \left(c \cdot i\right)\right)\right)} + \left(t \cdot z + x \cdot y\right)\right) \]
      6. associate-*r*N/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{\left(a \cdot c\right) \cdot i}\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      7. *-commutativeN/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{\left(c \cdot a\right)} \cdot i\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      8. associate-*r*N/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{c \cdot \left(a \cdot i\right)}\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      9. associate-*r*N/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{\left(c \cdot a\right) \cdot i}\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      10. *-commutativeN/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{\left(a \cdot c\right)} \cdot i\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      11. *-commutativeN/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{i \cdot \left(a \cdot c\right)}\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      12. distribute-lft-neg-inN/A

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

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(i\right), a \cdot c, t \cdot z + x \cdot y\right)} \]
      14. lower-neg.f64N/A

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

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(-i, \color{blue}{c \cdot a}, t \cdot z + x \cdot y\right) \]
      17. lower-fma.f64N/A

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right)\right) \]
      19. lower-*.f6492.6

        \[\leadsto 2 \cdot \mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right)\right) \]
    5. Applied rewrites92.6%

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, y \cdot x\right)\right)} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification90.8%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq -\infty \lor \neg \left(\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq 10^{+242}\right):\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \left(-c\right) \cdot \left(\mathsf{fma}\left(b, c, a\right) \cdot i\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, y \cdot x\right)\right)\\ \end{array} \]
  5. Add Preprocessing

Alternative 5: 89.5% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\ \mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 10^{+242}\right):\\ \;\;\;\;\left(-2 \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right)\right) \cdot c\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, y \cdot x\right)\right)\\ \end{array} \end{array} \]
(FPCore (x y z t a b c i)
 :precision binary64
 (let* ((t_1 (* (* (+ a (* b c)) c) i)))
   (if (or (<= t_1 (- INFINITY)) (not (<= t_1 1e+242)))
     (* (* -2.0 (* (fma c b a) i)) c)
     (* 2.0 (fma (- i) (* c a) (fma t z (* y x)))))))
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	double t_1 = ((a + (b * c)) * c) * i;
	double tmp;
	if ((t_1 <= -((double) INFINITY)) || !(t_1 <= 1e+242)) {
		tmp = (-2.0 * (fma(c, b, a) * i)) * c;
	} else {
		tmp = 2.0 * fma(-i, (c * a), fma(t, z, (y * x)));
	}
	return tmp;
}
function code(x, y, z, t, a, b, c, i)
	t_1 = Float64(Float64(Float64(a + Float64(b * c)) * c) * i)
	tmp = 0.0
	if ((t_1 <= Float64(-Inf)) || !(t_1 <= 1e+242))
		tmp = Float64(Float64(-2.0 * Float64(fma(c, b, a) * i)) * c);
	else
		tmp = Float64(2.0 * fma(Float64(-i), Float64(c * a), fma(t, z, Float64(y * x))));
	end
	return tmp
end
code[x_, y_, z_, t_, a_, b_, c_, i_] := Block[{t$95$1 = N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]}, If[Or[LessEqual[t$95$1, (-Infinity)], N[Not[LessEqual[t$95$1, 1e+242]], $MachinePrecision]], N[(N[(-2.0 * N[(N[(c * b + a), $MachinePrecision] * i), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision], N[(2.0 * N[((-i) * N[(c * a), $MachinePrecision] + N[(t * z + N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\
\mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 10^{+242}\right):\\
\;\;\;\;\left(-2 \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right)\right) \cdot c\\

\mathbf{else}:\\
\;\;\;\;2 \cdot \mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, y \cdot x\right)\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < -inf.0 or 1.00000000000000005e242 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)

    1. Initial program 70.2%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Taylor expanded in i around inf

      \[\leadsto \color{blue}{-2 \cdot \left(c \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto -2 \cdot \color{blue}{\left(\left(i \cdot \left(a + b \cdot c\right)\right) \cdot c\right)} \]
      2. associate-*r*N/A

        \[\leadsto \color{blue}{\left(-2 \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right) \cdot c} \]
      3. distribute-rgt-inN/A

        \[\leadsto \left(-2 \cdot \color{blue}{\left(a \cdot i + \left(b \cdot c\right) \cdot i\right)}\right) \cdot c \]
      4. associate-*r*N/A

        \[\leadsto \left(-2 \cdot \left(a \cdot i + \color{blue}{b \cdot \left(c \cdot i\right)}\right)\right) \cdot c \]
      5. distribute-lft-outN/A

        \[\leadsto \color{blue}{\left(-2 \cdot \left(a \cdot i\right) + -2 \cdot \left(b \cdot \left(c \cdot i\right)\right)\right)} \cdot c \]
      6. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(-2 \cdot \left(a \cdot i\right) + -2 \cdot \left(b \cdot \left(c \cdot i\right)\right)\right) \cdot c} \]
      7. distribute-lft-outN/A

        \[\leadsto \color{blue}{\left(-2 \cdot \left(a \cdot i + b \cdot \left(c \cdot i\right)\right)\right)} \cdot c \]
      8. associate-*r*N/A

        \[\leadsto \left(-2 \cdot \left(a \cdot i + \color{blue}{\left(b \cdot c\right) \cdot i}\right)\right) \cdot c \]
      9. distribute-rgt-inN/A

        \[\leadsto \left(-2 \cdot \color{blue}{\left(i \cdot \left(a + b \cdot c\right)\right)}\right) \cdot c \]
      10. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(-2 \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right)} \cdot c \]
      11. *-commutativeN/A

        \[\leadsto \left(-2 \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \cdot c \]
      12. lower-*.f64N/A

        \[\leadsto \left(-2 \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \cdot c \]
      13. +-commutativeN/A

        \[\leadsto \left(-2 \cdot \left(\color{blue}{\left(b \cdot c + a\right)} \cdot i\right)\right) \cdot c \]
      14. *-commutativeN/A

        \[\leadsto \left(-2 \cdot \left(\left(\color{blue}{c \cdot b} + a\right) \cdot i\right)\right) \cdot c \]
      15. lower-fma.f6483.6

        \[\leadsto \left(-2 \cdot \left(\color{blue}{\mathsf{fma}\left(c, b, a\right)} \cdot i\right)\right) \cdot c \]
    5. Applied rewrites83.6%

      \[\leadsto \color{blue}{\left(-2 \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right)\right) \cdot c} \]

    if -inf.0 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < 1.00000000000000005e242

    1. Initial program 99.2%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Taylor expanded in b around 0

      \[\leadsto 2 \cdot \color{blue}{\left(\left(t \cdot z + x \cdot y\right) - a \cdot \left(c \cdot i\right)\right)} \]
    4. Step-by-step derivation
      1. fp-cancel-sub-sign-invN/A

        \[\leadsto 2 \cdot \color{blue}{\left(\left(t \cdot z + x \cdot y\right) + \left(\mathsf{neg}\left(a\right)\right) \cdot \left(c \cdot i\right)\right)} \]
      2. distribute-lft-neg-inN/A

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

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

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

        \[\leadsto 2 \cdot \left(\color{blue}{\left(\mathsf{neg}\left(a \cdot \left(c \cdot i\right)\right)\right)} + \left(t \cdot z + x \cdot y\right)\right) \]
      6. associate-*r*N/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{\left(a \cdot c\right) \cdot i}\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      7. *-commutativeN/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{\left(c \cdot a\right)} \cdot i\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      8. associate-*r*N/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{c \cdot \left(a \cdot i\right)}\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      9. associate-*r*N/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{\left(c \cdot a\right) \cdot i}\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      10. *-commutativeN/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{\left(a \cdot c\right)} \cdot i\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      11. *-commutativeN/A

        \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{i \cdot \left(a \cdot c\right)}\right)\right) + \left(t \cdot z + x \cdot y\right)\right) \]
      12. distribute-lft-neg-inN/A

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

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(i\right), a \cdot c, t \cdot z + x \cdot y\right)} \]
      14. lower-neg.f64N/A

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

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(-i, \color{blue}{c \cdot a}, t \cdot z + x \cdot y\right) \]
      17. lower-fma.f64N/A

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right)\right) \]
      19. lower-*.f6492.6

        \[\leadsto 2 \cdot \mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right)\right) \]
    5. Applied rewrites92.6%

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, y \cdot x\right)\right)} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification88.9%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq -\infty \lor \neg \left(\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq 10^{+242}\right):\\ \;\;\;\;\left(-2 \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right)\right) \cdot c\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(-i, c \cdot a, \mathsf{fma}\left(t, z, y \cdot x\right)\right)\\ \end{array} \]
  5. Add Preprocessing

Alternative 6: 81.6% accurate, 0.6× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\ \mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 2 \cdot 10^{+161}\right):\\ \;\;\;\;\left(-2 \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right)\right) \cdot c\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\ \end{array} \end{array} \]
(FPCore (x y z t a b c i)
 :precision binary64
 (let* ((t_1 (* (* (+ a (* b c)) c) i)))
   (if (or (<= t_1 (- INFINITY)) (not (<= t_1 2e+161)))
     (* (* -2.0 (* (fma c b a) i)) c)
     (* 2.0 (fma t z (* y x))))))
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	double t_1 = ((a + (b * c)) * c) * i;
	double tmp;
	if ((t_1 <= -((double) INFINITY)) || !(t_1 <= 2e+161)) {
		tmp = (-2.0 * (fma(c, b, a) * i)) * c;
	} else {
		tmp = 2.0 * fma(t, z, (y * x));
	}
	return tmp;
}
function code(x, y, z, t, a, b, c, i)
	t_1 = Float64(Float64(Float64(a + Float64(b * c)) * c) * i)
	tmp = 0.0
	if ((t_1 <= Float64(-Inf)) || !(t_1 <= 2e+161))
		tmp = Float64(Float64(-2.0 * Float64(fma(c, b, a) * i)) * c);
	else
		tmp = Float64(2.0 * fma(t, z, Float64(y * x)));
	end
	return tmp
end
code[x_, y_, z_, t_, a_, b_, c_, i_] := Block[{t$95$1 = N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]}, If[Or[LessEqual[t$95$1, (-Infinity)], N[Not[LessEqual[t$95$1, 2e+161]], $MachinePrecision]], N[(N[(-2.0 * N[(N[(c * b + a), $MachinePrecision] * i), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision], N[(2.0 * N[(t * z + N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\
\mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 2 \cdot 10^{+161}\right):\\
\;\;\;\;\left(-2 \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right)\right) \cdot c\\

\mathbf{else}:\\
\;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < -inf.0 or 2.0000000000000001e161 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)

    1. Initial program 72.7%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Taylor expanded in i around inf

      \[\leadsto \color{blue}{-2 \cdot \left(c \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto -2 \cdot \color{blue}{\left(\left(i \cdot \left(a + b \cdot c\right)\right) \cdot c\right)} \]
      2. associate-*r*N/A

        \[\leadsto \color{blue}{\left(-2 \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right) \cdot c} \]
      3. distribute-rgt-inN/A

        \[\leadsto \left(-2 \cdot \color{blue}{\left(a \cdot i + \left(b \cdot c\right) \cdot i\right)}\right) \cdot c \]
      4. associate-*r*N/A

        \[\leadsto \left(-2 \cdot \left(a \cdot i + \color{blue}{b \cdot \left(c \cdot i\right)}\right)\right) \cdot c \]
      5. distribute-lft-outN/A

        \[\leadsto \color{blue}{\left(-2 \cdot \left(a \cdot i\right) + -2 \cdot \left(b \cdot \left(c \cdot i\right)\right)\right)} \cdot c \]
      6. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(-2 \cdot \left(a \cdot i\right) + -2 \cdot \left(b \cdot \left(c \cdot i\right)\right)\right) \cdot c} \]
      7. distribute-lft-outN/A

        \[\leadsto \color{blue}{\left(-2 \cdot \left(a \cdot i + b \cdot \left(c \cdot i\right)\right)\right)} \cdot c \]
      8. associate-*r*N/A

        \[\leadsto \left(-2 \cdot \left(a \cdot i + \color{blue}{\left(b \cdot c\right) \cdot i}\right)\right) \cdot c \]
      9. distribute-rgt-inN/A

        \[\leadsto \left(-2 \cdot \color{blue}{\left(i \cdot \left(a + b \cdot c\right)\right)}\right) \cdot c \]
      10. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(-2 \cdot \left(i \cdot \left(a + b \cdot c\right)\right)\right)} \cdot c \]
      11. *-commutativeN/A

        \[\leadsto \left(-2 \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \cdot c \]
      12. lower-*.f64N/A

        \[\leadsto \left(-2 \cdot \color{blue}{\left(\left(a + b \cdot c\right) \cdot i\right)}\right) \cdot c \]
      13. +-commutativeN/A

        \[\leadsto \left(-2 \cdot \left(\color{blue}{\left(b \cdot c + a\right)} \cdot i\right)\right) \cdot c \]
      14. *-commutativeN/A

        \[\leadsto \left(-2 \cdot \left(\left(\color{blue}{c \cdot b} + a\right) \cdot i\right)\right) \cdot c \]
      15. lower-fma.f6480.9

        \[\leadsto \left(-2 \cdot \left(\color{blue}{\mathsf{fma}\left(c, b, a\right)} \cdot i\right)\right) \cdot c \]
    5. Applied rewrites80.9%

      \[\leadsto \color{blue}{\left(-2 \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right)\right) \cdot c} \]

    if -inf.0 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < 2.0000000000000001e161

    1. Initial program 99.2%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Taylor expanded in c around 0

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

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

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

        \[\leadsto 2 \cdot \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right) \]
      4. lower-*.f6473.9

        \[\leadsto 2 \cdot \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right) \]
    5. Applied rewrites73.9%

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

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq -\infty \lor \neg \left(\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq 2 \cdot 10^{+161}\right):\\ \;\;\;\;\left(-2 \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right)\right) \cdot c\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\ \end{array} \]
  5. Add Preprocessing

Alternative 7: 73.3% accurate, 0.6× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\ \mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 2 \cdot 10^{+161}\right):\\ \;\;\;\;\left(\left(c \cdot i\right) \cdot \left(b \cdot c\right)\right) \cdot -2\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\ \end{array} \end{array} \]
(FPCore (x y z t a b c i)
 :precision binary64
 (let* ((t_1 (* (* (+ a (* b c)) c) i)))
   (if (or (<= t_1 (- INFINITY)) (not (<= t_1 2e+161)))
     (* (* (* c i) (* b c)) -2.0)
     (* 2.0 (fma t z (* y x))))))
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	double t_1 = ((a + (b * c)) * c) * i;
	double tmp;
	if ((t_1 <= -((double) INFINITY)) || !(t_1 <= 2e+161)) {
		tmp = ((c * i) * (b * c)) * -2.0;
	} else {
		tmp = 2.0 * fma(t, z, (y * x));
	}
	return tmp;
}
function code(x, y, z, t, a, b, c, i)
	t_1 = Float64(Float64(Float64(a + Float64(b * c)) * c) * i)
	tmp = 0.0
	if ((t_1 <= Float64(-Inf)) || !(t_1 <= 2e+161))
		tmp = Float64(Float64(Float64(c * i) * Float64(b * c)) * -2.0);
	else
		tmp = Float64(2.0 * fma(t, z, Float64(y * x)));
	end
	return tmp
end
code[x_, y_, z_, t_, a_, b_, c_, i_] := Block[{t$95$1 = N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]}, If[Or[LessEqual[t$95$1, (-Infinity)], N[Not[LessEqual[t$95$1, 2e+161]], $MachinePrecision]], N[(N[(N[(c * i), $MachinePrecision] * N[(b * c), $MachinePrecision]), $MachinePrecision] * -2.0), $MachinePrecision], N[(2.0 * N[(t * z + N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\
\mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 2 \cdot 10^{+161}\right):\\
\;\;\;\;\left(\left(c \cdot i\right) \cdot \left(b \cdot c\right)\right) \cdot -2\\

\mathbf{else}:\\
\;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < -inf.0 or 2.0000000000000001e161 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)

    1. Initial program 72.7%

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
    2. Add Preprocessing
    3. Taylor expanded in b around inf

      \[\leadsto \color{blue}{-2 \cdot \left(b \cdot \left({c}^{2} \cdot i\right)\right)} \]
    4. Step-by-step derivation
      1. *-commutativeN/A

        \[\leadsto \color{blue}{\left(b \cdot \left({c}^{2} \cdot i\right)\right) \cdot -2} \]
      2. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(b \cdot \left({c}^{2} \cdot i\right)\right) \cdot -2} \]
      3. *-commutativeN/A

        \[\leadsto \color{blue}{\left(\left({c}^{2} \cdot i\right) \cdot b\right)} \cdot -2 \]
      4. lower-*.f64N/A

        \[\leadsto \color{blue}{\left(\left({c}^{2} \cdot i\right) \cdot b\right)} \cdot -2 \]
      5. lower-*.f64N/A

        \[\leadsto \left(\color{blue}{\left({c}^{2} \cdot i\right)} \cdot b\right) \cdot -2 \]
      6. unpow2N/A

        \[\leadsto \left(\left(\color{blue}{\left(c \cdot c\right)} \cdot i\right) \cdot b\right) \cdot -2 \]
      7. lower-*.f6457.0

        \[\leadsto \left(\left(\color{blue}{\left(c \cdot c\right)} \cdot i\right) \cdot b\right) \cdot -2 \]
    5. Applied rewrites57.0%

      \[\leadsto \color{blue}{\left(\left(\left(c \cdot c\right) \cdot i\right) \cdot b\right) \cdot -2} \]
    6. Step-by-step derivation
      1. Applied rewrites60.3%

        \[\leadsto \left(\left(c \cdot i\right) \cdot \left(b \cdot c\right)\right) \cdot -2 \]

      if -inf.0 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < 2.0000000000000001e161

      1. Initial program 99.2%

        \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      2. Add Preprocessing
      3. Taylor expanded in c around 0

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

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

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

          \[\leadsto 2 \cdot \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right) \]
        4. lower-*.f6473.9

          \[\leadsto 2 \cdot \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right) \]
      5. Applied rewrites73.9%

        \[\leadsto \color{blue}{2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)} \]
    7. Recombined 2 regimes into one program.
    8. Final simplification67.7%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq -\infty \lor \neg \left(\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq 2 \cdot 10^{+161}\right):\\ \;\;\;\;\left(\left(c \cdot i\right) \cdot \left(b \cdot c\right)\right) \cdot -2\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\ \end{array} \]
    9. Add Preprocessing

    Alternative 8: 73.8% accurate, 0.6× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\ \mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 2 \cdot 10^{+161}\right):\\ \;\;\;\;\left(\left(\left(c \cdot i\right) \cdot -2\right) \cdot b\right) \cdot c\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\ \end{array} \end{array} \]
    (FPCore (x y z t a b c i)
     :precision binary64
     (let* ((t_1 (* (* (+ a (* b c)) c) i)))
       (if (or (<= t_1 (- INFINITY)) (not (<= t_1 2e+161)))
         (* (* (* (* c i) -2.0) b) c)
         (* 2.0 (fma t z (* y x))))))
    double code(double x, double y, double z, double t, double a, double b, double c, double i) {
    	double t_1 = ((a + (b * c)) * c) * i;
    	double tmp;
    	if ((t_1 <= -((double) INFINITY)) || !(t_1 <= 2e+161)) {
    		tmp = (((c * i) * -2.0) * b) * c;
    	} else {
    		tmp = 2.0 * fma(t, z, (y * x));
    	}
    	return tmp;
    }
    
    function code(x, y, z, t, a, b, c, i)
    	t_1 = Float64(Float64(Float64(a + Float64(b * c)) * c) * i)
    	tmp = 0.0
    	if ((t_1 <= Float64(-Inf)) || !(t_1 <= 2e+161))
    		tmp = Float64(Float64(Float64(Float64(c * i) * -2.0) * b) * c);
    	else
    		tmp = Float64(2.0 * fma(t, z, Float64(y * x)));
    	end
    	return tmp
    end
    
    code[x_, y_, z_, t_, a_, b_, c_, i_] := Block[{t$95$1 = N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]}, If[Or[LessEqual[t$95$1, (-Infinity)], N[Not[LessEqual[t$95$1, 2e+161]], $MachinePrecision]], N[(N[(N[(N[(c * i), $MachinePrecision] * -2.0), $MachinePrecision] * b), $MachinePrecision] * c), $MachinePrecision], N[(2.0 * N[(t * z + N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\
    \mathbf{if}\;t\_1 \leq -\infty \lor \neg \left(t\_1 \leq 2 \cdot 10^{+161}\right):\\
    \;\;\;\;\left(\left(\left(c \cdot i\right) \cdot -2\right) \cdot b\right) \cdot c\\
    
    \mathbf{else}:\\
    \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < -inf.0 or 2.0000000000000001e161 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)

      1. Initial program 72.7%

        \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift--.f64N/A

          \[\leadsto 2 \cdot \color{blue}{\left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
        2. lift-+.f64N/A

          \[\leadsto 2 \cdot \left(\color{blue}{\left(x \cdot y + z \cdot t\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
        3. +-commutativeN/A

          \[\leadsto 2 \cdot \left(\color{blue}{\left(z \cdot t + x \cdot y\right)} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
        4. associate--l+N/A

          \[\leadsto 2 \cdot \color{blue}{\left(z \cdot t + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right)} \]
        5. lift-*.f64N/A

          \[\leadsto 2 \cdot \left(\color{blue}{z \cdot t} + \left(x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\right) \]
        6. lower-fma.f64N/A

          \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, x \cdot y - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)} \]
        7. lower--.f6475.2

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

          \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{x \cdot y} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
        9. *-commutativeN/A

          \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, \color{blue}{y \cdot x} - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
        10. lower-*.f6475.2

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

          \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i}\right) \]
        12. *-commutativeN/A

          \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
        13. lower-*.f6475.2

          \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - \color{blue}{i \cdot \left(\left(a + b \cdot c\right) \cdot c\right)}\right) \]
        14. lift-+.f64N/A

          \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\left(a + b \cdot c\right)} \cdot c\right)\right) \]
        15. +-commutativeN/A

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

          \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{b \cdot c} + a\right) \cdot c\right)\right) \]
        17. *-commutativeN/A

          \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\left(\color{blue}{c \cdot b} + a\right) \cdot c\right)\right) \]
        18. lower-fma.f6475.2

          \[\leadsto 2 \cdot \mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\color{blue}{\mathsf{fma}\left(c, b, a\right)} \cdot c\right)\right) \]
      4. Applied rewrites75.2%

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(z, t, y \cdot x - i \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot c\right)\right)} \]
      5. Taylor expanded in b around inf

        \[\leadsto \color{blue}{-2 \cdot \left(b \cdot \left({c}^{2} \cdot i\right)\right)} \]
      6. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto -2 \cdot \left(b \cdot \color{blue}{\left(i \cdot {c}^{2}\right)}\right) \]
        2. associate-*r*N/A

          \[\leadsto -2 \cdot \color{blue}{\left(\left(b \cdot i\right) \cdot {c}^{2}\right)} \]
        3. unpow2N/A

          \[\leadsto -2 \cdot \left(\left(b \cdot i\right) \cdot \color{blue}{\left(c \cdot c\right)}\right) \]
        4. associate-*r*N/A

          \[\leadsto -2 \cdot \color{blue}{\left(\left(\left(b \cdot i\right) \cdot c\right) \cdot c\right)} \]
        5. associate-*r*N/A

          \[\leadsto -2 \cdot \left(\color{blue}{\left(b \cdot \left(i \cdot c\right)\right)} \cdot c\right) \]
        6. *-commutativeN/A

          \[\leadsto -2 \cdot \left(\left(b \cdot \color{blue}{\left(c \cdot i\right)}\right) \cdot c\right) \]
        7. associate-*l*N/A

          \[\leadsto \color{blue}{\left(-2 \cdot \left(b \cdot \left(c \cdot i\right)\right)\right) \cdot c} \]
        8. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(-2 \cdot \left(b \cdot \left(c \cdot i\right)\right)\right) \cdot c} \]
        9. *-commutativeN/A

          \[\leadsto \left(-2 \cdot \color{blue}{\left(\left(c \cdot i\right) \cdot b\right)}\right) \cdot c \]
        10. associate-*r*N/A

          \[\leadsto \color{blue}{\left(\left(-2 \cdot \left(c \cdot i\right)\right) \cdot b\right)} \cdot c \]
        11. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(\left(-2 \cdot \left(c \cdot i\right)\right) \cdot b\right)} \cdot c \]
        12. *-commutativeN/A

          \[\leadsto \left(\color{blue}{\left(\left(c \cdot i\right) \cdot -2\right)} \cdot b\right) \cdot c \]
        13. lower-*.f64N/A

          \[\leadsto \left(\color{blue}{\left(\left(c \cdot i\right) \cdot -2\right)} \cdot b\right) \cdot c \]
        14. lower-*.f6459.1

          \[\leadsto \left(\left(\color{blue}{\left(c \cdot i\right)} \cdot -2\right) \cdot b\right) \cdot c \]
      7. Applied rewrites59.1%

        \[\leadsto \color{blue}{\left(\left(\left(c \cdot i\right) \cdot -2\right) \cdot b\right) \cdot c} \]

      if -inf.0 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < 2.0000000000000001e161

      1. Initial program 99.2%

        \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      2. Add Preprocessing
      3. Taylor expanded in c around 0

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

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

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

          \[\leadsto 2 \cdot \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right) \]
        4. lower-*.f6473.9

          \[\leadsto 2 \cdot \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right) \]
      5. Applied rewrites73.9%

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

      \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq -\infty \lor \neg \left(\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq 2 \cdot 10^{+161}\right):\\ \;\;\;\;\left(\left(\left(c \cdot i\right) \cdot -2\right) \cdot b\right) \cdot c\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\ \end{array} \]
    5. Add Preprocessing

    Alternative 9: 74.1% accurate, 0.6× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\ \mathbf{if}\;t\_1 \leq -\infty:\\ \;\;\;\;\left(\left(c \cdot i\right) \cdot \left(b \cdot c\right)\right) \cdot -2\\ \mathbf{elif}\;t\_1 \leq 4 \cdot 10^{+266}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(c \cdot i\right) \cdot c\right) \cdot b\right) \cdot -2\\ \end{array} \end{array} \]
    (FPCore (x y z t a b c i)
     :precision binary64
     (let* ((t_1 (* (* (+ a (* b c)) c) i)))
       (if (<= t_1 (- INFINITY))
         (* (* (* c i) (* b c)) -2.0)
         (if (<= t_1 4e+266)
           (* 2.0 (fma t z (* y x)))
           (* (* (* (* c i) c) b) -2.0)))))
    double code(double x, double y, double z, double t, double a, double b, double c, double i) {
    	double t_1 = ((a + (b * c)) * c) * i;
    	double tmp;
    	if (t_1 <= -((double) INFINITY)) {
    		tmp = ((c * i) * (b * c)) * -2.0;
    	} else if (t_1 <= 4e+266) {
    		tmp = 2.0 * fma(t, z, (y * x));
    	} else {
    		tmp = (((c * i) * c) * b) * -2.0;
    	}
    	return tmp;
    }
    
    function code(x, y, z, t, a, b, c, i)
    	t_1 = Float64(Float64(Float64(a + Float64(b * c)) * c) * i)
    	tmp = 0.0
    	if (t_1 <= Float64(-Inf))
    		tmp = Float64(Float64(Float64(c * i) * Float64(b * c)) * -2.0);
    	elseif (t_1 <= 4e+266)
    		tmp = Float64(2.0 * fma(t, z, Float64(y * x)));
    	else
    		tmp = Float64(Float64(Float64(Float64(c * i) * c) * b) * -2.0);
    	end
    	return tmp
    end
    
    code[x_, y_, z_, t_, a_, b_, c_, i_] := Block[{t$95$1 = N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]}, If[LessEqual[t$95$1, (-Infinity)], N[(N[(N[(c * i), $MachinePrecision] * N[(b * c), $MachinePrecision]), $MachinePrecision] * -2.0), $MachinePrecision], If[LessEqual[t$95$1, 4e+266], N[(2.0 * N[(t * z + N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(N[(N[(c * i), $MachinePrecision] * c), $MachinePrecision] * b), $MachinePrecision] * -2.0), $MachinePrecision]]]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_1 := \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\\
    \mathbf{if}\;t\_1 \leq -\infty:\\
    \;\;\;\;\left(\left(c \cdot i\right) \cdot \left(b \cdot c\right)\right) \cdot -2\\
    
    \mathbf{elif}\;t\_1 \leq 4 \cdot 10^{+266}:\\
    \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\left(\left(\left(c \cdot i\right) \cdot c\right) \cdot b\right) \cdot -2\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 3 regimes
    2. if (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < -inf.0

      1. Initial program 66.1%

        \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
      2. Add Preprocessing
      3. Taylor expanded in b around inf

        \[\leadsto \color{blue}{-2 \cdot \left(b \cdot \left({c}^{2} \cdot i\right)\right)} \]
      4. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \color{blue}{\left(b \cdot \left({c}^{2} \cdot i\right)\right) \cdot -2} \]
        2. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(b \cdot \left({c}^{2} \cdot i\right)\right) \cdot -2} \]
        3. *-commutativeN/A

          \[\leadsto \color{blue}{\left(\left({c}^{2} \cdot i\right) \cdot b\right)} \cdot -2 \]
        4. lower-*.f64N/A

          \[\leadsto \color{blue}{\left(\left({c}^{2} \cdot i\right) \cdot b\right)} \cdot -2 \]
        5. lower-*.f64N/A

          \[\leadsto \left(\color{blue}{\left({c}^{2} \cdot i\right)} \cdot b\right) \cdot -2 \]
        6. unpow2N/A

          \[\leadsto \left(\left(\color{blue}{\left(c \cdot c\right)} \cdot i\right) \cdot b\right) \cdot -2 \]
        7. lower-*.f6463.4

          \[\leadsto \left(\left(\color{blue}{\left(c \cdot c\right)} \cdot i\right) \cdot b\right) \cdot -2 \]
      5. Applied rewrites63.4%

        \[\leadsto \color{blue}{\left(\left(\left(c \cdot c\right) \cdot i\right) \cdot b\right) \cdot -2} \]
      6. Step-by-step derivation
        1. Applied rewrites65.8%

          \[\leadsto \left(\left(c \cdot i\right) \cdot \left(b \cdot c\right)\right) \cdot -2 \]

        if -inf.0 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) < 4.0000000000000001e266

        1. Initial program 98.5%

          \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
        2. Add Preprocessing
        3. Taylor expanded in c around 0

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

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

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

            \[\leadsto 2 \cdot \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right) \]
          4. lower-*.f6469.7

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

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

        if 4.0000000000000001e266 < (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)

        1. Initial program 73.3%

          \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
        2. Add Preprocessing
        3. Taylor expanded in b around inf

          \[\leadsto \color{blue}{-2 \cdot \left(b \cdot \left({c}^{2} \cdot i\right)\right)} \]
        4. Step-by-step derivation
          1. *-commutativeN/A

            \[\leadsto \color{blue}{\left(b \cdot \left({c}^{2} \cdot i\right)\right) \cdot -2} \]
          2. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(b \cdot \left({c}^{2} \cdot i\right)\right) \cdot -2} \]
          3. *-commutativeN/A

            \[\leadsto \color{blue}{\left(\left({c}^{2} \cdot i\right) \cdot b\right)} \cdot -2 \]
          4. lower-*.f64N/A

            \[\leadsto \color{blue}{\left(\left({c}^{2} \cdot i\right) \cdot b\right)} \cdot -2 \]
          5. lower-*.f64N/A

            \[\leadsto \left(\color{blue}{\left({c}^{2} \cdot i\right)} \cdot b\right) \cdot -2 \]
          6. unpow2N/A

            \[\leadsto \left(\left(\color{blue}{\left(c \cdot c\right)} \cdot i\right) \cdot b\right) \cdot -2 \]
          7. lower-*.f6462.5

            \[\leadsto \left(\left(\color{blue}{\left(c \cdot c\right)} \cdot i\right) \cdot b\right) \cdot -2 \]
        5. Applied rewrites62.5%

          \[\leadsto \color{blue}{\left(\left(\left(c \cdot c\right) \cdot i\right) \cdot b\right) \cdot -2} \]
        6. Step-by-step derivation
          1. Applied rewrites64.2%

            \[\leadsto \left(\left(\left(c \cdot i\right) \cdot c\right) \cdot b\right) \cdot -2 \]
        7. Recombined 3 regimes into one program.
        8. Final simplification67.8%

          \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq -\infty:\\ \;\;\;\;\left(\left(c \cdot i\right) \cdot \left(b \cdot c\right)\right) \cdot -2\\ \mathbf{elif}\;\left(\left(a + b \cdot c\right) \cdot c\right) \cdot i \leq 4 \cdot 10^{+266}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(c \cdot i\right) \cdot c\right) \cdot b\right) \cdot -2\\ \end{array} \]
        9. Add Preprocessing

        Alternative 10: 41.2% accurate, 1.1× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \cdot y \leq -4 \cdot 10^{+104} \lor \neg \left(x \cdot y \leq 2 \cdot 10^{+119}\right):\\ \;\;\;\;2 \cdot \left(y \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(i \cdot c\right) \cdot a\right) \cdot -2\\ \end{array} \end{array} \]
        (FPCore (x y z t a b c i)
         :precision binary64
         (if (or (<= (* x y) -4e+104) (not (<= (* x y) 2e+119)))
           (* 2.0 (* y x))
           (* (* (* i c) a) -2.0)))
        double code(double x, double y, double z, double t, double a, double b, double c, double i) {
        	double tmp;
        	if (((x * y) <= -4e+104) || !((x * y) <= 2e+119)) {
        		tmp = 2.0 * (y * x);
        	} else {
        		tmp = ((i * c) * a) * -2.0;
        	}
        	return tmp;
        }
        
        real(8) function code(x, y, z, t, a, b, c, i)
            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), intent (in) :: b
            real(8), intent (in) :: c
            real(8), intent (in) :: i
            real(8) :: tmp
            if (((x * y) <= (-4d+104)) .or. (.not. ((x * y) <= 2d+119))) then
                tmp = 2.0d0 * (y * x)
            else
                tmp = ((i * c) * a) * (-2.0d0)
            end if
            code = tmp
        end function
        
        public static double code(double x, double y, double z, double t, double a, double b, double c, double i) {
        	double tmp;
        	if (((x * y) <= -4e+104) || !((x * y) <= 2e+119)) {
        		tmp = 2.0 * (y * x);
        	} else {
        		tmp = ((i * c) * a) * -2.0;
        	}
        	return tmp;
        }
        
        def code(x, y, z, t, a, b, c, i):
        	tmp = 0
        	if ((x * y) <= -4e+104) or not ((x * y) <= 2e+119):
        		tmp = 2.0 * (y * x)
        	else:
        		tmp = ((i * c) * a) * -2.0
        	return tmp
        
        function code(x, y, z, t, a, b, c, i)
        	tmp = 0.0
        	if ((Float64(x * y) <= -4e+104) || !(Float64(x * y) <= 2e+119))
        		tmp = Float64(2.0 * Float64(y * x));
        	else
        		tmp = Float64(Float64(Float64(i * c) * a) * -2.0);
        	end
        	return tmp
        end
        
        function tmp_2 = code(x, y, z, t, a, b, c, i)
        	tmp = 0.0;
        	if (((x * y) <= -4e+104) || ~(((x * y) <= 2e+119)))
        		tmp = 2.0 * (y * x);
        	else
        		tmp = ((i * c) * a) * -2.0;
        	end
        	tmp_2 = tmp;
        end
        
        code[x_, y_, z_, t_, a_, b_, c_, i_] := If[Or[LessEqual[N[(x * y), $MachinePrecision], -4e+104], N[Not[LessEqual[N[(x * y), $MachinePrecision], 2e+119]], $MachinePrecision]], N[(2.0 * N[(y * x), $MachinePrecision]), $MachinePrecision], N[(N[(N[(i * c), $MachinePrecision] * a), $MachinePrecision] * -2.0), $MachinePrecision]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;x \cdot y \leq -4 \cdot 10^{+104} \lor \neg \left(x \cdot y \leq 2 \cdot 10^{+119}\right):\\
        \;\;\;\;2 \cdot \left(y \cdot x\right)\\
        
        \mathbf{else}:\\
        \;\;\;\;\left(\left(i \cdot c\right) \cdot a\right) \cdot -2\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if (*.f64 x y) < -4e104 or 1.99999999999999989e119 < (*.f64 x y)

          1. Initial program 81.6%

            \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
          2. Add Preprocessing
          3. Taylor expanded in x around inf

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

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

              \[\leadsto 2 \cdot \color{blue}{\left(y \cdot x\right)} \]
            3. lower-*.f6460.7

              \[\leadsto 2 \cdot \color{blue}{\left(y \cdot x\right)} \]
          5. Applied rewrites60.7%

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

          if -4e104 < (*.f64 x y) < 1.99999999999999989e119

          1. Initial program 90.0%

            \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
          2. Add Preprocessing
          3. Taylor expanded in a around inf

            \[\leadsto \color{blue}{-2 \cdot \left(a \cdot \left(c \cdot i\right)\right)} \]
          4. Step-by-step derivation
            1. *-commutativeN/A

              \[\leadsto \color{blue}{\left(a \cdot \left(c \cdot i\right)\right) \cdot -2} \]
            2. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(a \cdot \left(c \cdot i\right)\right) \cdot -2} \]
            3. *-commutativeN/A

              \[\leadsto \color{blue}{\left(\left(c \cdot i\right) \cdot a\right)} \cdot -2 \]
            4. lower-*.f64N/A

              \[\leadsto \color{blue}{\left(\left(c \cdot i\right) \cdot a\right)} \cdot -2 \]
            5. *-commutativeN/A

              \[\leadsto \left(\color{blue}{\left(i \cdot c\right)} \cdot a\right) \cdot -2 \]
            6. lower-*.f6436.3

              \[\leadsto \left(\color{blue}{\left(i \cdot c\right)} \cdot a\right) \cdot -2 \]
          5. Applied rewrites36.3%

            \[\leadsto \color{blue}{\left(\left(i \cdot c\right) \cdot a\right) \cdot -2} \]
        3. Recombined 2 regimes into one program.
        4. Final simplification44.9%

          \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y \leq -4 \cdot 10^{+104} \lor \neg \left(x \cdot y \leq 2 \cdot 10^{+119}\right):\\ \;\;\;\;2 \cdot \left(y \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(i \cdot c\right) \cdot a\right) \cdot -2\\ \end{array} \]
        5. Add Preprocessing

        Alternative 11: 43.6% accurate, 1.2× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;z \cdot t \leq -50000 \lor \neg \left(z \cdot t \leq 10^{+34}\right):\\ \;\;\;\;t \cdot \left(z + z\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \left(y \cdot x\right)\\ \end{array} \end{array} \]
        (FPCore (x y z t a b c i)
         :precision binary64
         (if (or (<= (* z t) -50000.0) (not (<= (* z t) 1e+34)))
           (* t (+ z z))
           (* 2.0 (* y x))))
        double code(double x, double y, double z, double t, double a, double b, double c, double i) {
        	double tmp;
        	if (((z * t) <= -50000.0) || !((z * t) <= 1e+34)) {
        		tmp = t * (z + z);
        	} else {
        		tmp = 2.0 * (y * x);
        	}
        	return tmp;
        }
        
        real(8) function code(x, y, z, t, a, b, c, i)
            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), intent (in) :: b
            real(8), intent (in) :: c
            real(8), intent (in) :: i
            real(8) :: tmp
            if (((z * t) <= (-50000.0d0)) .or. (.not. ((z * t) <= 1d+34))) then
                tmp = t * (z + z)
            else
                tmp = 2.0d0 * (y * x)
            end if
            code = tmp
        end function
        
        public static double code(double x, double y, double z, double t, double a, double b, double c, double i) {
        	double tmp;
        	if (((z * t) <= -50000.0) || !((z * t) <= 1e+34)) {
        		tmp = t * (z + z);
        	} else {
        		tmp = 2.0 * (y * x);
        	}
        	return tmp;
        }
        
        def code(x, y, z, t, a, b, c, i):
        	tmp = 0
        	if ((z * t) <= -50000.0) or not ((z * t) <= 1e+34):
        		tmp = t * (z + z)
        	else:
        		tmp = 2.0 * (y * x)
        	return tmp
        
        function code(x, y, z, t, a, b, c, i)
        	tmp = 0.0
        	if ((Float64(z * t) <= -50000.0) || !(Float64(z * t) <= 1e+34))
        		tmp = Float64(t * Float64(z + z));
        	else
        		tmp = Float64(2.0 * Float64(y * x));
        	end
        	return tmp
        end
        
        function tmp_2 = code(x, y, z, t, a, b, c, i)
        	tmp = 0.0;
        	if (((z * t) <= -50000.0) || ~(((z * t) <= 1e+34)))
        		tmp = t * (z + z);
        	else
        		tmp = 2.0 * (y * x);
        	end
        	tmp_2 = tmp;
        end
        
        code[x_, y_, z_, t_, a_, b_, c_, i_] := If[Or[LessEqual[N[(z * t), $MachinePrecision], -50000.0], N[Not[LessEqual[N[(z * t), $MachinePrecision], 1e+34]], $MachinePrecision]], N[(t * N[(z + z), $MachinePrecision]), $MachinePrecision], N[(2.0 * N[(y * x), $MachinePrecision]), $MachinePrecision]]
        
        \begin{array}{l}
        
        \\
        \begin{array}{l}
        \mathbf{if}\;z \cdot t \leq -50000 \lor \neg \left(z \cdot t \leq 10^{+34}\right):\\
        \;\;\;\;t \cdot \left(z + z\right)\\
        
        \mathbf{else}:\\
        \;\;\;\;2 \cdot \left(y \cdot x\right)\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if (*.f64 z t) < -5e4 or 9.99999999999999946e33 < (*.f64 z t)

          1. Initial program 84.2%

            \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
          2. Add Preprocessing
          3. Taylor expanded in z around inf

            \[\leadsto \color{blue}{2 \cdot \left(t \cdot z\right)} \]
          4. Step-by-step derivation
            1. lower-*.f64N/A

              \[\leadsto \color{blue}{2 \cdot \left(t \cdot z\right)} \]
            2. lower-*.f6452.2

              \[\leadsto 2 \cdot \color{blue}{\left(t \cdot z\right)} \]
          5. Applied rewrites52.2%

            \[\leadsto \color{blue}{2 \cdot \left(t \cdot z\right)} \]
          6. Step-by-step derivation
            1. Applied rewrites52.2%

              \[\leadsto t \cdot \color{blue}{\left(z + z\right)} \]

            if -5e4 < (*.f64 z t) < 9.99999999999999946e33

            1. Initial program 89.1%

              \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
            2. Add Preprocessing
            3. Taylor expanded in x around inf

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

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

                \[\leadsto 2 \cdot \color{blue}{\left(y \cdot x\right)} \]
              3. lower-*.f6439.0

                \[\leadsto 2 \cdot \color{blue}{\left(y \cdot x\right)} \]
            5. Applied rewrites39.0%

              \[\leadsto \color{blue}{2 \cdot \left(y \cdot x\right)} \]
          7. Recombined 2 regimes into one program.
          8. Final simplification44.5%

            \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot t \leq -50000 \lor \neg \left(z \cdot t \leq 10^{+34}\right):\\ \;\;\;\;t \cdot \left(z + z\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \left(y \cdot x\right)\\ \end{array} \]
          9. Add Preprocessing

          Alternative 12: 56.0% accurate, 1.7× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;a \leq -4.5 \cdot 10^{+153}:\\ \;\;\;\;\left(\left(i \cdot c\right) \cdot a\right) \cdot -2\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\ \end{array} \end{array} \]
          (FPCore (x y z t a b c i)
           :precision binary64
           (if (<= a -4.5e+153) (* (* (* i c) a) -2.0) (* 2.0 (fma t z (* y x)))))
          double code(double x, double y, double z, double t, double a, double b, double c, double i) {
          	double tmp;
          	if (a <= -4.5e+153) {
          		tmp = ((i * c) * a) * -2.0;
          	} else {
          		tmp = 2.0 * fma(t, z, (y * x));
          	}
          	return tmp;
          }
          
          function code(x, y, z, t, a, b, c, i)
          	tmp = 0.0
          	if (a <= -4.5e+153)
          		tmp = Float64(Float64(Float64(i * c) * a) * -2.0);
          	else
          		tmp = Float64(2.0 * fma(t, z, Float64(y * x)));
          	end
          	return tmp
          end
          
          code[x_, y_, z_, t_, a_, b_, c_, i_] := If[LessEqual[a, -4.5e+153], N[(N[(N[(i * c), $MachinePrecision] * a), $MachinePrecision] * -2.0), $MachinePrecision], N[(2.0 * N[(t * z + N[(y * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          \mathbf{if}\;a \leq -4.5 \cdot 10^{+153}:\\
          \;\;\;\;\left(\left(i \cdot c\right) \cdot a\right) \cdot -2\\
          
          \mathbf{else}:\\
          \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if a < -4.5000000000000001e153

            1. Initial program 81.0%

              \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
            2. Add Preprocessing
            3. Taylor expanded in a around inf

              \[\leadsto \color{blue}{-2 \cdot \left(a \cdot \left(c \cdot i\right)\right)} \]
            4. Step-by-step derivation
              1. *-commutativeN/A

                \[\leadsto \color{blue}{\left(a \cdot \left(c \cdot i\right)\right) \cdot -2} \]
              2. lower-*.f64N/A

                \[\leadsto \color{blue}{\left(a \cdot \left(c \cdot i\right)\right) \cdot -2} \]
              3. *-commutativeN/A

                \[\leadsto \color{blue}{\left(\left(c \cdot i\right) \cdot a\right)} \cdot -2 \]
              4. lower-*.f64N/A

                \[\leadsto \color{blue}{\left(\left(c \cdot i\right) \cdot a\right)} \cdot -2 \]
              5. *-commutativeN/A

                \[\leadsto \left(\color{blue}{\left(i \cdot c\right)} \cdot a\right) \cdot -2 \]
              6. lower-*.f6467.6

                \[\leadsto \left(\color{blue}{\left(i \cdot c\right)} \cdot a\right) \cdot -2 \]
            5. Applied rewrites67.6%

              \[\leadsto \color{blue}{\left(\left(i \cdot c\right) \cdot a\right) \cdot -2} \]

            if -4.5000000000000001e153 < a

            1. Initial program 88.2%

              \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
            2. Add Preprocessing
            3. Taylor expanded in c around 0

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

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

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

                \[\leadsto 2 \cdot \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right) \]
              4. lower-*.f6456.0

                \[\leadsto 2 \cdot \mathsf{fma}\left(t, z, \color{blue}{y \cdot x}\right) \]
            5. Applied rewrites56.0%

              \[\leadsto \color{blue}{2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)} \]
          3. Recombined 2 regimes into one program.
          4. Final simplification57.8%

            \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -4.5 \cdot 10^{+153}:\\ \;\;\;\;\left(\left(i \cdot c\right) \cdot a\right) \cdot -2\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(t, z, y \cdot x\right)\\ \end{array} \]
          5. Add Preprocessing

          Alternative 13: 28.3% accurate, 4.4× speedup?

          \[\begin{array}{l} \\ t \cdot \left(z + z\right) \end{array} \]
          (FPCore (x y z t a b c i) :precision binary64 (* t (+ z z)))
          double code(double x, double y, double z, double t, double a, double b, double c, double i) {
          	return t * (z + z);
          }
          
          real(8) function code(x, y, z, t, a, b, c, i)
              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), intent (in) :: b
              real(8), intent (in) :: c
              real(8), intent (in) :: i
              code = t * (z + z)
          end function
          
          public static double code(double x, double y, double z, double t, double a, double b, double c, double i) {
          	return t * (z + z);
          }
          
          def code(x, y, z, t, a, b, c, i):
          	return t * (z + z)
          
          function code(x, y, z, t, a, b, c, i)
          	return Float64(t * Float64(z + z))
          end
          
          function tmp = code(x, y, z, t, a, b, c, i)
          	tmp = t * (z + z);
          end
          
          code[x_, y_, z_, t_, a_, b_, c_, i_] := N[(t * N[(z + z), $MachinePrecision]), $MachinePrecision]
          
          \begin{array}{l}
          
          \\
          t \cdot \left(z + z\right)
          \end{array}
          
          Derivation
          1. Initial program 87.0%

            \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
          2. Add Preprocessing
          3. Taylor expanded in z around inf

            \[\leadsto \color{blue}{2 \cdot \left(t \cdot z\right)} \]
          4. Step-by-step derivation
            1. lower-*.f64N/A

              \[\leadsto \color{blue}{2 \cdot \left(t \cdot z\right)} \]
            2. lower-*.f6424.8

              \[\leadsto 2 \cdot \color{blue}{\left(t \cdot z\right)} \]
          5. Applied rewrites24.8%

            \[\leadsto \color{blue}{2 \cdot \left(t \cdot z\right)} \]
          6. Step-by-step derivation
            1. Applied rewrites24.8%

              \[\leadsto t \cdot \color{blue}{\left(z + z\right)} \]
            2. Final simplification24.8%

              \[\leadsto t \cdot \left(z + z\right) \]
            3. Add Preprocessing

            Developer Target 1: 94.2% accurate, 1.0× speedup?

            \[\begin{array}{l} \\ 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(a + b \cdot c\right) \cdot \left(c \cdot i\right)\right) \end{array} \]
            (FPCore (x y z t a b c i)
             :precision binary64
             (* 2.0 (- (+ (* x y) (* z t)) (* (+ a (* b c)) (* c i)))))
            double code(double x, double y, double z, double t, double a, double b, double c, double i) {
            	return 2.0 * (((x * y) + (z * t)) - ((a + (b * c)) * (c * i)));
            }
            
            real(8) function code(x, y, z, t, a, b, c, i)
                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), intent (in) :: b
                real(8), intent (in) :: c
                real(8), intent (in) :: i
                code = 2.0d0 * (((x * y) + (z * t)) - ((a + (b * c)) * (c * i)))
            end function
            
            public static double code(double x, double y, double z, double t, double a, double b, double c, double i) {
            	return 2.0 * (((x * y) + (z * t)) - ((a + (b * c)) * (c * i)));
            }
            
            def code(x, y, z, t, a, b, c, i):
            	return 2.0 * (((x * y) + (z * t)) - ((a + (b * c)) * (c * i)))
            
            function code(x, y, z, t, a, b, c, i)
            	return Float64(2.0 * Float64(Float64(Float64(x * y) + Float64(z * t)) - Float64(Float64(a + Float64(b * c)) * Float64(c * i))))
            end
            
            function tmp = code(x, y, z, t, a, b, c, i)
            	tmp = 2.0 * (((x * y) + (z * t)) - ((a + (b * c)) * (c * i)));
            end
            
            code[x_, y_, z_, t_, a_, b_, c_, i_] := N[(2.0 * N[(N[(N[(x * y), $MachinePrecision] + N[(z * t), $MachinePrecision]), $MachinePrecision] - N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * N[(c * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
            
            \begin{array}{l}
            
            \\
            2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(a + b \cdot c\right) \cdot \left(c \cdot i\right)\right)
            \end{array}
            

            Reproduce

            ?
            herbie shell --seed 2024342 
            (FPCore (x y z t a b c i)
              :name "Diagrams.ThreeD.Shapes:frustum from diagrams-lib-1.3.0.3, A"
              :precision binary64
            
              :alt
              (! :herbie-platform default (* 2 (- (+ (* x y) (* z t)) (* (+ a (* b c)) (* c i)))))
            
              (* 2.0 (- (+ (* x y) (* z t)) (* (* (+ a (* b c)) c) i))))