Diagrams.Solve.Polynomial:quartForm from diagrams-solve-0.1, C

Percentage Accurate: 97.9% → 97.9%

Time: 15.1s

Alternatives: 13

Speedup: 1.0×

• 32.0% of points produce a very large (infinite) output. You may want to add a precondition.

Specification

Math

\[\begin{array}{l} \\ \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (+ (- (+ (* x y) (/ (* z t) 16.0)) (/ (* a b) 4.0)) c))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	return (((x * y) + ((z * t) / 16.0)) - ((a * b) / 4.0)) + c;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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
    code = (((x * y) + ((z * t) / 16.0d0)) - ((a * b) / 4.0d0)) + c
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	return (((x * y) + ((z * t) / 16.0)) - ((a * b) / 4.0)) + c;
}

Python

def code(x, y, z, t, a, b, c):
	return (((x * y) + ((z * t) / 16.0)) - ((a * b) / 4.0)) + c

Julia

function code(x, y, z, t, a, b, c)
	return Float64(Float64(Float64(Float64(x * y) + Float64(Float64(z * t) / 16.0)) - Float64(Float64(a * b) / 4.0)) + c)
end

MATLAB

function tmp = code(x, y, z, t, a, b, c)
	tmp = (((x * y) + ((z * t) / 16.0)) - ((a * b) / 4.0)) + c;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := N[(N[(N[(N[(x * y), $MachinePrecision] + N[(N[(z * t), $MachinePrecision] / 16.0), $MachinePrecision]), $MachinePrecision] - N[(N[(a * b), $MachinePrecision] / 4.0), $MachinePrecision]), $MachinePrecision] + c), $MachinePrecision]

Initial Program: 97.9% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (+ (- (+ (* x y) (/ (* z t) 16.0)) (/ (* a b) 4.0)) c))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	return (((x * y) + ((z * t) / 16.0)) - ((a * b) / 4.0)) + c;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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
    code = (((x * y) + ((z * t) / 16.0d0)) - ((a * b) / 4.0d0)) + c
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	return (((x * y) + ((z * t) / 16.0)) - ((a * b) / 4.0)) + c;
}

Python

def code(x, y, z, t, a, b, c):
	return (((x * y) + ((z * t) / 16.0)) - ((a * b) / 4.0)) + c

Julia

function code(x, y, z, t, a, b, c)
	return Float64(Float64(Float64(Float64(x * y) + Float64(Float64(z * t) / 16.0)) - Float64(Float64(a * b) / 4.0)) + c)
end

MATLAB

function tmp = code(x, y, z, t, a, b, c)
	tmp = (((x * y) + ((z * t) / 16.0)) - ((a * b) / 4.0)) + c;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := N[(N[(N[(N[(x * y), $MachinePrecision] + N[(N[(z * t), $MachinePrecision] / 16.0), $MachinePrecision]), $MachinePrecision] - N[(N[(a * b), $MachinePrecision] / 4.0), $MachinePrecision]), $MachinePrecision] + c), $MachinePrecision]

Alternative 1: 97.9% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{b \cdot a}{4}\right) + c \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (+ (- (+ (* x y) (/ (* z t) 16.0)) (/ (* b a) 4.0)) c))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	return (((x * y) + ((z * t) / 16.0)) - ((b * a) / 4.0)) + c;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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
    code = (((x * y) + ((z * t) / 16.0d0)) - ((b * a) / 4.0d0)) + c
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	return (((x * y) + ((z * t) / 16.0)) - ((b * a) / 4.0)) + c;
}

Python

def code(x, y, z, t, a, b, c):
	return (((x * y) + ((z * t) / 16.0)) - ((b * a) / 4.0)) + c

Julia

function code(x, y, z, t, a, b, c)
	return Float64(Float64(Float64(Float64(x * y) + Float64(Float64(z * t) / 16.0)) - Float64(Float64(b * a) / 4.0)) + c)
end

MATLAB

function tmp = code(x, y, z, t, a, b, c)
	tmp = (((x * y) + ((z * t) / 16.0)) - ((b * a) / 4.0)) + c;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := N[(N[(N[(N[(x * y), $MachinePrecision] + N[(N[(z * t), $MachinePrecision] / 16.0), $MachinePrecision]), $MachinePrecision] - N[(N[(b * a), $MachinePrecision] / 4.0), $MachinePrecision]), $MachinePrecision] + c), $MachinePrecision]

Derivation

1. Initial program 98.8%

   \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
2. Add Preprocessing

3. Final simplification 98.8%

   \[\leadsto \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{b \cdot a}{4}\right) + c \]
4. Add Preprocessing

Alternative 2: 43.3% accurate, 0.4× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := b \cdot \left(-0.25 \cdot a\right)\\ \mathbf{if}\;x \cdot y \leq -2.35 \cdot 10^{+55}:\\ \;\;\;\;x \cdot y\\ \mathbf{elif}\;x \cdot y \leq -7.2 \cdot 10^{-186}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;x \cdot y \leq 1.9 \cdot 10^{-289}:\\ \;\;\;\;c\\ \mathbf{elif}\;x \cdot y \leq 5 \cdot 10^{-68}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;x \cdot y \leq 1.55 \cdot 10^{+46}:\\ \;\;\;\;c\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (let* ((t_1 (* b (* -0.25 a))))
   (if (<= (* x y) -2.35e+55)
     (* x y)
     (if (<= (* x y) -7.2e-186)
       t_1
       (if (<= (* x y) 1.9e-289)
         c
         (if (<= (* x y) 5e-68) t_1 (if (<= (* x y) 1.55e+46) c (* x y))))))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = b * (-0.25 * a);
	double tmp;
	if ((x * y) <= -2.35e+55) {
		tmp = x * y;
	} else if ((x * y) <= -7.2e-186) {
		tmp = t_1;
	} else if ((x * y) <= 1.9e-289) {
		tmp = c;
	} else if ((x * y) <= 5e-68) {
		tmp = t_1;
	} else if ((x * y) <= 1.55e+46) {
		tmp = c;
	} else {
		tmp = x * y;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: t_1
    real(8) :: tmp
    t_1 = b * ((-0.25d0) * a)
    if ((x * y) <= (-2.35d+55)) then
        tmp = x * y
    else if ((x * y) <= (-7.2d-186)) then
        tmp = t_1
    else if ((x * y) <= 1.9d-289) then
        tmp = c
    else if ((x * y) <= 5d-68) then
        tmp = t_1
    else if ((x * y) <= 1.55d+46) then
        tmp = c
    else
        tmp = x * y
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = b * (-0.25 * a);
	double tmp;
	if ((x * y) <= -2.35e+55) {
		tmp = x * y;
	} else if ((x * y) <= -7.2e-186) {
		tmp = t_1;
	} else if ((x * y) <= 1.9e-289) {
		tmp = c;
	} else if ((x * y) <= 5e-68) {
		tmp = t_1;
	} else if ((x * y) <= 1.55e+46) {
		tmp = c;
	} else {
		tmp = x * y;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	t_1 = b * (-0.25 * a)
	tmp = 0
	if (x * y) <= -2.35e+55:
		tmp = x * y
	elif (x * y) <= -7.2e-186:
		tmp = t_1
	elif (x * y) <= 1.9e-289:
		tmp = c
	elif (x * y) <= 5e-68:
		tmp = t_1
	elif (x * y) <= 1.55e+46:
		tmp = c
	else:
		tmp = x * y
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	t_1 = Float64(b * Float64(-0.25 * a))
	tmp = 0.0
	if (Float64(x * y) <= -2.35e+55)
		tmp = Float64(x * y);
	elseif (Float64(x * y) <= -7.2e-186)
		tmp = t_1;
	elseif (Float64(x * y) <= 1.9e-289)
		tmp = c;
	elseif (Float64(x * y) <= 5e-68)
		tmp = t_1;
	elseif (Float64(x * y) <= 1.55e+46)
		tmp = c;
	else
		tmp = Float64(x * y);
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	t_1 = b * (-0.25 * a);
	tmp = 0.0;
	if ((x * y) <= -2.35e+55)
		tmp = x * y;
	elseif ((x * y) <= -7.2e-186)
		tmp = t_1;
	elseif ((x * y) <= 1.9e-289)
		tmp = c;
	elseif ((x * y) <= 5e-68)
		tmp = t_1;
	elseif ((x * y) <= 1.55e+46)
		tmp = c;
	else
		tmp = x * y;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := Block[{t$95$1 = N[(b * N[(-0.25 * a), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(x * y), $MachinePrecision], -2.35e+55], N[(x * y), $MachinePrecision], If[LessEqual[N[(x * y), $MachinePrecision], -7.2e-186], t$95$1, If[LessEqual[N[(x * y), $MachinePrecision], 1.9e-289], c, If[LessEqual[N[(x * y), $MachinePrecision], 5e-68], t$95$1, If[LessEqual[N[(x * y), $MachinePrecision], 1.55e+46], c, N[(x * y), $MachinePrecision]]]]]]]

Derivation

1. Split input into 3 regimes

2. if (*.f64 x y) < -2.35e55 or 1.54999999999999988e46 < (*.f64 x y)

   1. Initial program 97.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 97.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf

      \[\leadsto \color{blue}{x \cdot y} \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 65.8%

         \[\leadsto \mathsf{*.f64}\left(x, \color{blue}{y}\right) \]

   7. Simplified 65.8%

      \[\leadsto \color{blue}{x \cdot y} \]

   if -2.35e55 < (*.f64 x y) < -7.1999999999999997e-186 or 1.90000000000000005e-289 < (*.f64 x y) < 4.99999999999999971e-68

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in a around inf

      \[\leadsto \color{blue}{\frac{-1}{4} \cdot \left(a \cdot b\right)} \]
   6. Step-by-step derivation

      1. associate-*r* N/A

         \[\leadsto \left(\frac{-1}{4} \cdot a\right) \cdot \color{blue}{b} \]

      2. *-commutative N/A

         \[\leadsto b \cdot \color{blue}{\left(\frac{-1}{4} \cdot a\right)} \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{*.f64}\left(b, \color{blue}{\left(\frac{-1}{4} \cdot a\right)}\right) \]

      4. *-commutative N/A

         \[\leadsto \mathsf{*.f64}\left(b, \left(a \cdot \color{blue}{\frac{-1}{4}}\right)\right) \]

      5. *-lowering-*.f64 42.7%

         \[\leadsto \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \color{blue}{\frac{-1}{4}}\right)\right) \]

   7. Simplified 42.7%

      \[\leadsto \color{blue}{b \cdot \left(a \cdot -0.25\right)} \]

   if -7.1999999999999997e-186 < (*.f64 x y) < 1.90000000000000005e-289 or 4.99999999999999971e-68 < (*.f64 x y) < 1.54999999999999988e46

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in c around inf

      \[\leadsto \color{blue}{c} \]
   6. Step-by-step derivation

   7. Simplified 45.0%

      \[\leadsto \color{blue}{c} \]
3. Recombined 3 regimes into one program.

4. Final simplification 52.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y \leq -2.35 \cdot 10^{+55}:\\ \;\;\;\;x \cdot y\\ \mathbf{elif}\;x \cdot y \leq -7.2 \cdot 10^{-186}:\\ \;\;\;\;b \cdot \left(-0.25 \cdot a\right)\\ \mathbf{elif}\;x \cdot y \leq 1.9 \cdot 10^{-289}:\\ \;\;\;\;c\\ \mathbf{elif}\;x \cdot y \leq 5 \cdot 10^{-68}:\\ \;\;\;\;b \cdot \left(-0.25 \cdot a\right)\\ \mathbf{elif}\;x \cdot y \leq 1.55 \cdot 10^{+46}:\\ \;\;\;\;c\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array} \]
5. Add Preprocessing

Alternative 3: 44.5% accurate, 0.5× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \cdot y \leq -1.3 \cdot 10^{+54}:\\ \;\;\;\;x \cdot y\\ \mathbf{elif}\;x \cdot y \leq -7.2 \cdot 10^{-153}:\\ \;\;\;\;b \cdot \left(-0.25 \cdot a\right)\\ \mathbf{elif}\;x \cdot y \leq 3.7 \cdot 10^{-68}:\\ \;\;\;\;t \cdot \left(z \cdot 0.0625\right)\\ \mathbf{elif}\;x \cdot y \leq 1.2 \cdot 10^{+46}:\\ \;\;\;\;c\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (if (<= (* x y) -1.3e+54)
   (* x y)
   (if (<= (* x y) -7.2e-153)
     (* b (* -0.25 a))
     (if (<= (* x y) 3.7e-68)
       (* t (* z 0.0625))
       (if (<= (* x y) 1.2e+46) c (* x y))))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double tmp;
	if ((x * y) <= -1.3e+54) {
		tmp = x * y;
	} else if ((x * y) <= -7.2e-153) {
		tmp = b * (-0.25 * a);
	} else if ((x * y) <= 3.7e-68) {
		tmp = t * (z * 0.0625);
	} else if ((x * y) <= 1.2e+46) {
		tmp = c;
	} else {
		tmp = x * y;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: tmp
    if ((x * y) <= (-1.3d+54)) then
        tmp = x * y
    else if ((x * y) <= (-7.2d-153)) then
        tmp = b * ((-0.25d0) * a)
    else if ((x * y) <= 3.7d-68) then
        tmp = t * (z * 0.0625d0)
    else if ((x * y) <= 1.2d+46) then
        tmp = c
    else
        tmp = x * y
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double tmp;
	if ((x * y) <= -1.3e+54) {
		tmp = x * y;
	} else if ((x * y) <= -7.2e-153) {
		tmp = b * (-0.25 * a);
	} else if ((x * y) <= 3.7e-68) {
		tmp = t * (z * 0.0625);
	} else if ((x * y) <= 1.2e+46) {
		tmp = c;
	} else {
		tmp = x * y;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	tmp = 0
	if (x * y) <= -1.3e+54:
		tmp = x * y
	elif (x * y) <= -7.2e-153:
		tmp = b * (-0.25 * a)
	elif (x * y) <= 3.7e-68:
		tmp = t * (z * 0.0625)
	elif (x * y) <= 1.2e+46:
		tmp = c
	else:
		tmp = x * y
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	tmp = 0.0
	if (Float64(x * y) <= -1.3e+54)
		tmp = Float64(x * y);
	elseif (Float64(x * y) <= -7.2e-153)
		tmp = Float64(b * Float64(-0.25 * a));
	elseif (Float64(x * y) <= 3.7e-68)
		tmp = Float64(t * Float64(z * 0.0625));
	elseif (Float64(x * y) <= 1.2e+46)
		tmp = c;
	else
		tmp = Float64(x * y);
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	tmp = 0.0;
	if ((x * y) <= -1.3e+54)
		tmp = x * y;
	elseif ((x * y) <= -7.2e-153)
		tmp = b * (-0.25 * a);
	elseif ((x * y) <= 3.7e-68)
		tmp = t * (z * 0.0625);
	elseif ((x * y) <= 1.2e+46)
		tmp = c;
	else
		tmp = x * y;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := If[LessEqual[N[(x * y), $MachinePrecision], -1.3e+54], N[(x * y), $MachinePrecision], If[LessEqual[N[(x * y), $MachinePrecision], -7.2e-153], N[(b * N[(-0.25 * a), $MachinePrecision]), $MachinePrecision], If[LessEqual[N[(x * y), $MachinePrecision], 3.7e-68], N[(t * N[(z * 0.0625), $MachinePrecision]), $MachinePrecision], If[LessEqual[N[(x * y), $MachinePrecision], 1.2e+46], c, N[(x * y), $MachinePrecision]]]]]

Derivation

1. Split input into 4 regimes

2. if (*.f64 x y) < -1.30000000000000003e54 or 1.20000000000000004e46 < (*.f64 x y)

   1. Initial program 97.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 97.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf

      \[\leadsto \color{blue}{x \cdot y} \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 65.8%

         \[\leadsto \mathsf{*.f64}\left(x, \color{blue}{y}\right) \]

   7. Simplified 65.8%

      \[\leadsto \color{blue}{x \cdot y} \]

   if -1.30000000000000003e54 < (*.f64 x y) < -7.1999999999999995e-153

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in a around inf

      \[\leadsto \color{blue}{\frac{-1}{4} \cdot \left(a \cdot b\right)} \]
   6. Step-by-step derivation

      1. associate-*r* N/A

         \[\leadsto \left(\frac{-1}{4} \cdot a\right) \cdot \color{blue}{b} \]

      2. *-commutative N/A

         \[\leadsto b \cdot \color{blue}{\left(\frac{-1}{4} \cdot a\right)} \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{*.f64}\left(b, \color{blue}{\left(\frac{-1}{4} \cdot a\right)}\right) \]

      4. *-commutative N/A

         \[\leadsto \mathsf{*.f64}\left(b, \left(a \cdot \color{blue}{\frac{-1}{4}}\right)\right) \]

      5. *-lowering-*.f64 46.6%

         \[\leadsto \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \color{blue}{\frac{-1}{4}}\right)\right) \]

   7. Simplified 46.6%

      \[\leadsto \color{blue}{b \cdot \left(a \cdot -0.25\right)} \]

   if -7.1999999999999995e-153 < (*.f64 x y) < 3.70000000000000002e-68

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around inf

      \[\leadsto \color{blue}{\frac{1}{16} \cdot \left(t \cdot z\right)} \]
   6. Step-by-step derivation

      1. *-commutative N/A

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

      2. associate-*r* N/A

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

      3. *-commutative N/A

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

      4. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{*.f64}\left(t, \color{blue}{\left(\frac{1}{16} \cdot z\right)}\right) \]

      5. *-commutative N/A

         \[\leadsto \mathsf{*.f64}\left(t, \left(z \cdot \color{blue}{\frac{1}{16}}\right)\right) \]

      6. *-lowering-*.f64 41.3%

         \[\leadsto \mathsf{*.f64}\left(t, \mathsf{*.f64}\left(z, \color{blue}{\frac{1}{16}}\right)\right) \]

   7. Simplified 41.3%

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

   if 3.70000000000000002e-68 < (*.f64 x y) < 1.20000000000000004e46

   1. Initial program 99.9%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 99.9%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in c around inf

      \[\leadsto \color{blue}{c} \]
   6. Step-by-step derivation

   7. Simplified 51.3%

      \[\leadsto \color{blue}{c} \]
3. Recombined 4 regimes into one program.

4. Final simplification 52.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y \leq -1.3 \cdot 10^{+54}:\\ \;\;\;\;x \cdot y\\ \mathbf{elif}\;x \cdot y \leq -7.2 \cdot 10^{-153}:\\ \;\;\;\;b \cdot \left(-0.25 \cdot a\right)\\ \mathbf{elif}\;x \cdot y \leq 3.7 \cdot 10^{-68}:\\ \;\;\;\;t \cdot \left(z \cdot 0.0625\right)\\ \mathbf{elif}\;x \cdot y \leq 1.2 \cdot 10^{+46}:\\ \;\;\;\;c\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array} \]
5. Add Preprocessing

Alternative 4: 66.4% accurate, 0.6× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot y + b \cdot \left(-0.25 \cdot a\right)\\ \mathbf{if}\;x \cdot y \leq -2 \cdot 10^{+59}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;x \cdot y \leq -1 \cdot 10^{-173}:\\ \;\;\;\;c - \left(b \cdot a\right) \cdot 0.25\\ \mathbf{elif}\;x \cdot y \leq 10^{+49}:\\ \;\;\;\;c - -0.0625 \cdot \left(z \cdot t\right)\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (let* ((t_1 (+ (* x y) (* b (* -0.25 a)))))
   (if (<= (* x y) -2e+59)
     t_1
     (if (<= (* x y) -1e-173)
       (- c (* (* b a) 0.25))
       (if (<= (* x y) 1e+49) (- c (* -0.0625 (* z t))) t_1)))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = (x * y) + (b * (-0.25 * a));
	double tmp;
	if ((x * y) <= -2e+59) {
		tmp = t_1;
	} else if ((x * y) <= -1e-173) {
		tmp = c - ((b * a) * 0.25);
	} else if ((x * y) <= 1e+49) {
		tmp = c - (-0.0625 * (z * t));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: t_1
    real(8) :: tmp
    t_1 = (x * y) + (b * ((-0.25d0) * a))
    if ((x * y) <= (-2d+59)) then
        tmp = t_1
    else if ((x * y) <= (-1d-173)) then
        tmp = c - ((b * a) * 0.25d0)
    else if ((x * y) <= 1d+49) then
        tmp = c - ((-0.0625d0) * (z * t))
    else
        tmp = t_1
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = (x * y) + (b * (-0.25 * a));
	double tmp;
	if ((x * y) <= -2e+59) {
		tmp = t_1;
	} else if ((x * y) <= -1e-173) {
		tmp = c - ((b * a) * 0.25);
	} else if ((x * y) <= 1e+49) {
		tmp = c - (-0.0625 * (z * t));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	t_1 = (x * y) + (b * (-0.25 * a))
	tmp = 0
	if (x * y) <= -2e+59:
		tmp = t_1
	elif (x * y) <= -1e-173:
		tmp = c - ((b * a) * 0.25)
	elif (x * y) <= 1e+49:
		tmp = c - (-0.0625 * (z * t))
	else:
		tmp = t_1
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	t_1 = Float64(Float64(x * y) + Float64(b * Float64(-0.25 * a)))
	tmp = 0.0
	if (Float64(x * y) <= -2e+59)
		tmp = t_1;
	elseif (Float64(x * y) <= -1e-173)
		tmp = Float64(c - Float64(Float64(b * a) * 0.25));
	elseif (Float64(x * y) <= 1e+49)
		tmp = Float64(c - Float64(-0.0625 * Float64(z * t)));
	else
		tmp = t_1;
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	t_1 = (x * y) + (b * (-0.25 * a));
	tmp = 0.0;
	if ((x * y) <= -2e+59)
		tmp = t_1;
	elseif ((x * y) <= -1e-173)
		tmp = c - ((b * a) * 0.25);
	elseif ((x * y) <= 1e+49)
		tmp = c - (-0.0625 * (z * t));
	else
		tmp = t_1;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := Block[{t$95$1 = N[(N[(x * y), $MachinePrecision] + N[(b * N[(-0.25 * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(x * y), $MachinePrecision], -2e+59], t$95$1, If[LessEqual[N[(x * y), $MachinePrecision], -1e-173], N[(c - N[(N[(b * a), $MachinePrecision] * 0.25), $MachinePrecision]), $MachinePrecision], If[LessEqual[N[(x * y), $MachinePrecision], 1e+49], N[(c - N[(-0.0625 * N[(z * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]]

Derivation

1. Split input into 3 regimes

2. if (*.f64 x y) < -1.99999999999999994e59 or 9.99999999999999946e48 < (*.f64 x y)

   1. Initial program 96.9%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 96.9%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around 0

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{1}{4} \cdot \left(a \cdot b\right) - x \cdot y\right)}\right) \]
   6. Step-by-step derivation

      1. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\left(\frac{1}{4} \cdot \left(a \cdot b\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      2. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \left(a \cdot b\right)\right), \left(\color{blue}{x} \cdot y\right)\right)\right) \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \left(x \cdot y\right)\right)\right) \]

      4. *-lowering-*.f64 88.9%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 88.9%

      \[\leadsto c - \color{blue}{\left(0.25 \cdot \left(a \cdot b\right) - x \cdot y\right)} \]

   8. Taylor expanded in c around 0

      \[\leadsto \color{blue}{x \cdot y - \frac{1}{4} \cdot \left(a \cdot b\right)} \]
   9. Step-by-step derivation

      1. cancel-sign-sub-inv N/A

         \[\leadsto x \cdot y + \color{blue}{\left(\mathsf{neg}\left(\frac{1}{4}\right)\right) \cdot \left(a \cdot b\right)} \]

      2. metadata-eval N/A

         \[\leadsto x \cdot y + \frac{-1}{4} \cdot \left(\color{blue}{a} \cdot b\right) \]

      3. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\left(x \cdot y\right), \color{blue}{\left(\frac{-1}{4} \cdot \left(a \cdot b\right)\right)}\right) \]

      4. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \left(\color{blue}{\frac{-1}{4}} \cdot \left(a \cdot b\right)\right)\right) \]

      5. associate-*r* N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \left(\left(\frac{-1}{4} \cdot a\right) \cdot \color{blue}{b}\right)\right) \]

      6. *-commutative N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \left(b \cdot \color{blue}{\left(\frac{-1}{4} \cdot a\right)}\right)\right) \]

      7. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \mathsf{*.f64}\left(b, \color{blue}{\left(\frac{-1}{4} \cdot a\right)}\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \mathsf{*.f64}\left(b, \left(a \cdot \color{blue}{\frac{-1}{4}}\right)\right)\right) \]

      9. *-lowering-*.f64 83.1%

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \color{blue}{\frac{-1}{4}}\right)\right)\right) \]

   10. Simplified 83.1%

       \[\leadsto \color{blue}{x \cdot y + b \cdot \left(a \cdot -0.25\right)} \]

   if -1.99999999999999994e59 < (*.f64 x y) < -1e-173

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in a around inf

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{1}{4} \cdot \left(a \cdot b\right)\right)}\right) \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(\frac{1}{4}, \color{blue}{\left(a \cdot b\right)}\right)\right) \]

      2. *-lowering-*.f64 75.1%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, \color{blue}{b}\right)\right)\right) \]

   7. Simplified 75.1%

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

   if -1e-173 < (*.f64 x y) < 9.99999999999999946e48

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{-1}{16} \cdot \left(t \cdot z\right)\right)}\right) \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(\frac{-1}{16}, \color{blue}{\left(t \cdot z\right)}\right)\right) \]

      2. *-lowering-*.f64 69.2%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, \color{blue}{z}\right)\right)\right) \]

   7. Simplified 69.2%

      \[\leadsto c - \color{blue}{-0.0625 \cdot \left(t \cdot z\right)} \]
3. Recombined 3 regimes into one program.

4. Final simplification 75.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y \leq -2 \cdot 10^{+59}:\\ \;\;\;\;x \cdot y + b \cdot \left(-0.25 \cdot a\right)\\ \mathbf{elif}\;x \cdot y \leq -1 \cdot 10^{-173}:\\ \;\;\;\;c - \left(b \cdot a\right) \cdot 0.25\\ \mathbf{elif}\;x \cdot y \leq 10^{+49}:\\ \;\;\;\;c - -0.0625 \cdot \left(z \cdot t\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot y + b \cdot \left(-0.25 \cdot a\right)\\ \end{array} \]
5. Add Preprocessing

Alternative 5: 88.1% accurate, 0.7× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;b \cdot a \leq -5 \cdot 10^{+119}:\\ \;\;\;\;c + b \cdot \left(\frac{x \cdot y}{b} - 0.25 \cdot a\right)\\ \mathbf{elif}\;b \cdot a \leq 10^{-46}:\\ \;\;\;\;c + \left(x \cdot y - -0.0625 \cdot \left(z \cdot t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;c + \left(x \cdot y - \left(b \cdot a\right) \cdot 0.25\right)\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (if (<= (* b a) -5e+119)
   (+ c (* b (- (/ (* x y) b) (* 0.25 a))))
   (if (<= (* b a) 1e-46)
     (+ c (- (* x y) (* -0.0625 (* z t))))
     (+ c (- (* x y) (* (* b a) 0.25))))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double tmp;
	if ((b * a) <= -5e+119) {
		tmp = c + (b * (((x * y) / b) - (0.25 * a)));
	} else if ((b * a) <= 1e-46) {
		tmp = c + ((x * y) - (-0.0625 * (z * t)));
	} else {
		tmp = c + ((x * y) - ((b * a) * 0.25));
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: tmp
    if ((b * a) <= (-5d+119)) then
        tmp = c + (b * (((x * y) / b) - (0.25d0 * a)))
    else if ((b * a) <= 1d-46) then
        tmp = c + ((x * y) - ((-0.0625d0) * (z * t)))
    else
        tmp = c + ((x * y) - ((b * a) * 0.25d0))
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double tmp;
	if ((b * a) <= -5e+119) {
		tmp = c + (b * (((x * y) / b) - (0.25 * a)));
	} else if ((b * a) <= 1e-46) {
		tmp = c + ((x * y) - (-0.0625 * (z * t)));
	} else {
		tmp = c + ((x * y) - ((b * a) * 0.25));
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	tmp = 0
	if (b * a) <= -5e+119:
		tmp = c + (b * (((x * y) / b) - (0.25 * a)))
	elif (b * a) <= 1e-46:
		tmp = c + ((x * y) - (-0.0625 * (z * t)))
	else:
		tmp = c + ((x * y) - ((b * a) * 0.25))
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	tmp = 0.0
	if (Float64(b * a) <= -5e+119)
		tmp = Float64(c + Float64(b * Float64(Float64(Float64(x * y) / b) - Float64(0.25 * a))));
	elseif (Float64(b * a) <= 1e-46)
		tmp = Float64(c + Float64(Float64(x * y) - Float64(-0.0625 * Float64(z * t))));
	else
		tmp = Float64(c + Float64(Float64(x * y) - Float64(Float64(b * a) * 0.25)));
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	tmp = 0.0;
	if ((b * a) <= -5e+119)
		tmp = c + (b * (((x * y) / b) - (0.25 * a)));
	elseif ((b * a) <= 1e-46)
		tmp = c + ((x * y) - (-0.0625 * (z * t)));
	else
		tmp = c + ((x * y) - ((b * a) * 0.25));
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := If[LessEqual[N[(b * a), $MachinePrecision], -5e+119], N[(c + N[(b * N[(N[(N[(x * y), $MachinePrecision] / b), $MachinePrecision] - N[(0.25 * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[N[(b * a), $MachinePrecision], 1e-46], N[(c + N[(N[(x * y), $MachinePrecision] - N[(-0.0625 * N[(z * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(c + N[(N[(x * y), $MachinePrecision] - N[(N[(b * a), $MachinePrecision] * 0.25), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]

Derivation

1. Split input into 3 regimes

2. if (*.f64 a b) < -4.9999999999999999e119

   1. Initial program 97.3%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 97.3%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in b around inf

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(b \cdot \left(\left(\frac{-1}{16} \cdot \frac{t \cdot z}{b} + \frac{1}{4} \cdot a\right) - \frac{x \cdot y}{b}\right)\right)}\right) \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \color{blue}{\left(\left(\frac{-1}{16} \cdot \frac{t \cdot z}{b} + \frac{1}{4} \cdot a\right) - \frac{x \cdot y}{b}\right)}\right)\right) \]

      2. +-commutative N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \left(\left(\frac{1}{4} \cdot a + \frac{-1}{16} \cdot \frac{t \cdot z}{b}\right) - \frac{\color{blue}{x \cdot y}}{b}\right)\right)\right) \]

      3. associate--l+ N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \left(\frac{1}{4} \cdot a + \color{blue}{\left(\frac{-1}{16} \cdot \frac{t \cdot z}{b} - \frac{x \cdot y}{b}\right)}\right)\right)\right) \]

      4. associate-*r/ N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \left(\frac{1}{4} \cdot a + \left(\frac{\frac{-1}{16} \cdot \left(t \cdot z\right)}{b} - \frac{\color{blue}{x \cdot y}}{b}\right)\right)\right)\right) \]

      5. div-sub N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \left(\frac{1}{4} \cdot a + \frac{\frac{-1}{16} \cdot \left(t \cdot z\right) - x \cdot y}{\color{blue}{b}}\right)\right)\right) \]

      6. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{+.f64}\left(\left(\frac{1}{4} \cdot a\right), \color{blue}{\left(\frac{\frac{-1}{16} \cdot \left(t \cdot z\right) - x \cdot y}{b}\right)}\right)\right)\right) \]

      7. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, a\right), \left(\frac{\color{blue}{\frac{-1}{16} \cdot \left(t \cdot z\right) - x \cdot y}}{b}\right)\right)\right)\right) \]

      8. /-lowering-/.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, a\right), \mathsf{/.f64}\left(\left(\frac{-1}{16} \cdot \left(t \cdot z\right) - x \cdot y\right), \color{blue}{b}\right)\right)\right)\right) \]

      9. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, a\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\left(\frac{-1}{16} \cdot \left(t \cdot z\right)\right), \left(x \cdot y\right)\right), b\right)\right)\right)\right) \]

      10. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, a\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \left(t \cdot z\right)\right), \left(x \cdot y\right)\right), b\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, a\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, z\right)\right), \left(x \cdot y\right)\right), b\right)\right)\right)\right) \]

      12. *-lowering-*.f64 97.5%

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, a\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, z\right)\right), \mathsf{*.f64}\left(x, y\right)\right), b\right)\right)\right)\right) \]

   7. Simplified 97.5%

      \[\leadsto c - \color{blue}{b \cdot \left(0.25 \cdot a + \frac{-0.0625 \cdot \left(t \cdot z\right) - x \cdot y}{b}\right)} \]

   8. Taylor expanded in t around 0

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(b \cdot \left(\frac{1}{4} \cdot a - \frac{x \cdot y}{b}\right)\right)}\right) \]
   9. Step-by-step derivation

      1. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \color{blue}{\left(\frac{1}{4} \cdot a - \frac{x \cdot y}{b}\right)}\right)\right) \]

      2. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{\_.f64}\left(\left(\frac{1}{4} \cdot a\right), \color{blue}{\left(\frac{x \cdot y}{b}\right)}\right)\right)\right) \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, a\right), \left(\frac{\color{blue}{x \cdot y}}{b}\right)\right)\right)\right) \]

      4. /-lowering-/.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, a\right), \mathsf{/.f64}\left(\left(x \cdot y\right), \color{blue}{b}\right)\right)\right)\right) \]

      5. *-lowering-*.f64 88.6%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(b, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, a\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(x, y\right), b\right)\right)\right)\right) \]

   10. Simplified 88.6%

       \[\leadsto c - \color{blue}{b \cdot \left(0.25 \cdot a - \frac{x \cdot y}{b}\right)} \]

   if -4.9999999999999999e119 < (*.f64 a b) < 1.00000000000000002e-46

   1. Initial program 99.3%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 99.3%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in a around 0

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{-1}{16} \cdot \left(t \cdot z\right) - x \cdot y\right)}\right) \]
   6. Step-by-step derivation

      1. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\left(\frac{-1}{16} \cdot \left(t \cdot z\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      2. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \left(t \cdot z\right)\right), \left(\color{blue}{x} \cdot y\right)\right)\right) \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, z\right)\right), \left(x \cdot y\right)\right)\right) \]

      4. *-lowering-*.f64 95.9%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, z\right)\right), \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 95.9%

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

   if 1.00000000000000002e-46 < (*.f64 a b)

   1. Initial program 98.5%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 98.5%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around 0

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{1}{4} \cdot \left(a \cdot b\right) - x \cdot y\right)}\right) \]
   6. Step-by-step derivation

      1. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\left(\frac{1}{4} \cdot \left(a \cdot b\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      2. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \left(a \cdot b\right)\right), \left(\color{blue}{x} \cdot y\right)\right)\right) \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \left(x \cdot y\right)\right)\right) \]

      4. *-lowering-*.f64 88.7%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 88.7%

      \[\leadsto c - \color{blue}{\left(0.25 \cdot \left(a \cdot b\right) - x \cdot y\right)} \]
3. Recombined 3 regimes into one program.

4. Final simplification 92.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \cdot a \leq -5 \cdot 10^{+119}:\\ \;\;\;\;c + b \cdot \left(\frac{x \cdot y}{b} - 0.25 \cdot a\right)\\ \mathbf{elif}\;b \cdot a \leq 10^{-46}:\\ \;\;\;\;c + \left(x \cdot y - -0.0625 \cdot \left(z \cdot t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;c + \left(x \cdot y - \left(b \cdot a\right) \cdot 0.25\right)\\ \end{array} \]
5. Add Preprocessing

Alternative 6: 87.9% accurate, 0.7× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := c + \left(x \cdot y - \left(b \cdot a\right) \cdot 0.25\right)\\ \mathbf{if}\;b \cdot a \leq -5 \cdot 10^{+119}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;b \cdot a \leq 10^{-46}:\\ \;\;\;\;c + \left(x \cdot y - -0.0625 \cdot \left(z \cdot t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (let* ((t_1 (+ c (- (* x y) (* (* b a) 0.25)))))
   (if (<= (* b a) -5e+119)
     t_1
     (if (<= (* b a) 1e-46) (+ c (- (* x y) (* -0.0625 (* z t)))) t_1))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = c + ((x * y) - ((b * a) * 0.25));
	double tmp;
	if ((b * a) <= -5e+119) {
		tmp = t_1;
	} else if ((b * a) <= 1e-46) {
		tmp = c + ((x * y) - (-0.0625 * (z * t)));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: t_1
    real(8) :: tmp
    t_1 = c + ((x * y) - ((b * a) * 0.25d0))
    if ((b * a) <= (-5d+119)) then
        tmp = t_1
    else if ((b * a) <= 1d-46) then
        tmp = c + ((x * y) - ((-0.0625d0) * (z * t)))
    else
        tmp = t_1
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = c + ((x * y) - ((b * a) * 0.25));
	double tmp;
	if ((b * a) <= -5e+119) {
		tmp = t_1;
	} else if ((b * a) <= 1e-46) {
		tmp = c + ((x * y) - (-0.0625 * (z * t)));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	t_1 = c + ((x * y) - ((b * a) * 0.25))
	tmp = 0
	if (b * a) <= -5e+119:
		tmp = t_1
	elif (b * a) <= 1e-46:
		tmp = c + ((x * y) - (-0.0625 * (z * t)))
	else:
		tmp = t_1
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	t_1 = Float64(c + Float64(Float64(x * y) - Float64(Float64(b * a) * 0.25)))
	tmp = 0.0
	if (Float64(b * a) <= -5e+119)
		tmp = t_1;
	elseif (Float64(b * a) <= 1e-46)
		tmp = Float64(c + Float64(Float64(x * y) - Float64(-0.0625 * Float64(z * t))));
	else
		tmp = t_1;
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	t_1 = c + ((x * y) - ((b * a) * 0.25));
	tmp = 0.0;
	if ((b * a) <= -5e+119)
		tmp = t_1;
	elseif ((b * a) <= 1e-46)
		tmp = c + ((x * y) - (-0.0625 * (z * t)));
	else
		tmp = t_1;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := Block[{t$95$1 = N[(c + N[(N[(x * y), $MachinePrecision] - N[(N[(b * a), $MachinePrecision] * 0.25), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(b * a), $MachinePrecision], -5e+119], t$95$1, If[LessEqual[N[(b * a), $MachinePrecision], 1e-46], N[(c + N[(N[(x * y), $MachinePrecision] - N[(-0.0625 * N[(z * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]

Derivation

1. Split input into 2 regimes

2. if (*.f64 a b) < -4.9999999999999999e119 or 1.00000000000000002e-46 < (*.f64 a b)

   1. Initial program 98.1%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 98.1%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around 0

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{1}{4} \cdot \left(a \cdot b\right) - x \cdot y\right)}\right) \]
   6. Step-by-step derivation

      1. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\left(\frac{1}{4} \cdot \left(a \cdot b\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      2. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \left(a \cdot b\right)\right), \left(\color{blue}{x} \cdot y\right)\right)\right) \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \left(x \cdot y\right)\right)\right) \]

      4. *-lowering-*.f64 88.6%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 88.6%

      \[\leadsto c - \color{blue}{\left(0.25 \cdot \left(a \cdot b\right) - x \cdot y\right)} \]

   if -4.9999999999999999e119 < (*.f64 a b) < 1.00000000000000002e-46

   1. Initial program 99.3%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 99.3%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in a around 0

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{-1}{16} \cdot \left(t \cdot z\right) - x \cdot y\right)}\right) \]
   6. Step-by-step derivation

      1. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\left(\frac{-1}{16} \cdot \left(t \cdot z\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      2. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \left(t \cdot z\right)\right), \left(\color{blue}{x} \cdot y\right)\right)\right) \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, z\right)\right), \left(x \cdot y\right)\right)\right) \]

      4. *-lowering-*.f64 95.9%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, z\right)\right), \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 95.9%

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

4. Final simplification 92.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \cdot a \leq -5 \cdot 10^{+119}:\\ \;\;\;\;c + \left(x \cdot y - \left(b \cdot a\right) \cdot 0.25\right)\\ \mathbf{elif}\;b \cdot a \leq 10^{-46}:\\ \;\;\;\;c + \left(x \cdot y - -0.0625 \cdot \left(z \cdot t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;c + \left(x \cdot y - \left(b \cdot a\right) \cdot 0.25\right)\\ \end{array} \]
5. Add Preprocessing

Alternative 7: 86.9% accurate, 0.7× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := b \cdot \left(-0.25 \cdot a\right)\\ \mathbf{if}\;b \cdot a \leq -5 \cdot 10^{+119}:\\ \;\;\;\;\frac{y}{\frac{1}{x}} + t\_1\\ \mathbf{elif}\;b \cdot a \leq 2 \cdot 10^{+128}:\\ \;\;\;\;c + \left(x \cdot y - -0.0625 \cdot \left(z \cdot t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot y + t\_1\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (let* ((t_1 (* b (* -0.25 a))))
   (if (<= (* b a) -5e+119)
     (+ (/ y (/ 1.0 x)) t_1)
     (if (<= (* b a) 2e+128)
       (+ c (- (* x y) (* -0.0625 (* z t))))
       (+ (* x y) t_1)))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = b * (-0.25 * a);
	double tmp;
	if ((b * a) <= -5e+119) {
		tmp = (y / (1.0 / x)) + t_1;
	} else if ((b * a) <= 2e+128) {
		tmp = c + ((x * y) - (-0.0625 * (z * t)));
	} else {
		tmp = (x * y) + t_1;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: t_1
    real(8) :: tmp
    t_1 = b * ((-0.25d0) * a)
    if ((b * a) <= (-5d+119)) then
        tmp = (y / (1.0d0 / x)) + t_1
    else if ((b * a) <= 2d+128) then
        tmp = c + ((x * y) - ((-0.0625d0) * (z * t)))
    else
        tmp = (x * y) + t_1
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = b * (-0.25 * a);
	double tmp;
	if ((b * a) <= -5e+119) {
		tmp = (y / (1.0 / x)) + t_1;
	} else if ((b * a) <= 2e+128) {
		tmp = c + ((x * y) - (-0.0625 * (z * t)));
	} else {
		tmp = (x * y) + t_1;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	t_1 = b * (-0.25 * a)
	tmp = 0
	if (b * a) <= -5e+119:
		tmp = (y / (1.0 / x)) + t_1
	elif (b * a) <= 2e+128:
		tmp = c + ((x * y) - (-0.0625 * (z * t)))
	else:
		tmp = (x * y) + t_1
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	t_1 = Float64(b * Float64(-0.25 * a))
	tmp = 0.0
	if (Float64(b * a) <= -5e+119)
		tmp = Float64(Float64(y / Float64(1.0 / x)) + t_1);
	elseif (Float64(b * a) <= 2e+128)
		tmp = Float64(c + Float64(Float64(x * y) - Float64(-0.0625 * Float64(z * t))));
	else
		tmp = Float64(Float64(x * y) + t_1);
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	t_1 = b * (-0.25 * a);
	tmp = 0.0;
	if ((b * a) <= -5e+119)
		tmp = (y / (1.0 / x)) + t_1;
	elseif ((b * a) <= 2e+128)
		tmp = c + ((x * y) - (-0.0625 * (z * t)));
	else
		tmp = (x * y) + t_1;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := Block[{t$95$1 = N[(b * N[(-0.25 * a), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(b * a), $MachinePrecision], -5e+119], N[(N[(y / N[(1.0 / x), $MachinePrecision]), $MachinePrecision] + t$95$1), $MachinePrecision], If[LessEqual[N[(b * a), $MachinePrecision], 2e+128], N[(c + N[(N[(x * y), $MachinePrecision] - N[(-0.0625 * N[(z * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x * y), $MachinePrecision] + t$95$1), $MachinePrecision]]]]

Derivation

1. Split input into 3 regimes

2. if (*.f64 a b) < -4.9999999999999999e119

   1. Initial program 97.3%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 97.3%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around 0

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{1}{4} \cdot \left(a \cdot b\right) - x \cdot y\right)}\right) \]
   6. Step-by-step derivation

      1. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\left(\frac{1}{4} \cdot \left(a \cdot b\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      2. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \left(a \cdot b\right)\right), \left(\color{blue}{x} \cdot y\right)\right)\right) \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \left(x \cdot y\right)\right)\right) \]

      4. *-lowering-*.f64 88.5%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 88.5%

      \[\leadsto c - \color{blue}{\left(0.25 \cdot \left(a \cdot b\right) - x \cdot y\right)} \]

   8. Taylor expanded in c around 0

      \[\leadsto \color{blue}{x \cdot y - \frac{1}{4} \cdot \left(a \cdot b\right)} \]
   9. Step-by-step derivation

      1. cancel-sign-sub-inv N/A

         \[\leadsto x \cdot y + \color{blue}{\left(\mathsf{neg}\left(\frac{1}{4}\right)\right) \cdot \left(a \cdot b\right)} \]

      2. metadata-eval N/A

         \[\leadsto x \cdot y + \frac{-1}{4} \cdot \left(\color{blue}{a} \cdot b\right) \]

      3. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\left(x \cdot y\right), \color{blue}{\left(\frac{-1}{4} \cdot \left(a \cdot b\right)\right)}\right) \]

      4. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \left(\color{blue}{\frac{-1}{4}} \cdot \left(a \cdot b\right)\right)\right) \]

      5. associate-*r* N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \left(\left(\frac{-1}{4} \cdot a\right) \cdot \color{blue}{b}\right)\right) \]

      6. *-commutative N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \left(b \cdot \color{blue}{\left(\frac{-1}{4} \cdot a\right)}\right)\right) \]

      7. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \mathsf{*.f64}\left(b, \color{blue}{\left(\frac{-1}{4} \cdot a\right)}\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \mathsf{*.f64}\left(b, \left(a \cdot \color{blue}{\frac{-1}{4}}\right)\right)\right) \]

      9. *-lowering-*.f64 80.6%

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \color{blue}{\frac{-1}{4}}\right)\right)\right) \]

   10. Simplified 80.6%

       \[\leadsto \color{blue}{x \cdot y + b \cdot \left(a \cdot -0.25\right)} \]
   11. Step-by-step derivation

       1. *-commutative N/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot x\right), \mathsf{*.f64}\left(\color{blue}{b}, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       2. /-rgt-identity N/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \frac{x}{1}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       3. div-inv N/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(x \cdot \frac{1}{1}\right)\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       4. metadata-eval N/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(x \cdot 1\right)\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       5. *-inverses N/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \left(x \cdot \frac{c}{c}\right)\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       6. associate-/l* N/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \frac{x \cdot c}{c}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       7. *-commutative N/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \frac{c \cdot x}{c}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       8. clear-num N/A

          \[\leadsto \mathsf{+.f64}\left(\left(y \cdot \frac{1}{\frac{c}{c \cdot x}}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       9. un-div-inv N/A

          \[\leadsto \mathsf{+.f64}\left(\left(\frac{y}{\frac{c}{c \cdot x}}\right), \mathsf{*.f64}\left(\color{blue}{b}, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       10. clear-num N/A

           \[\leadsto \mathsf{+.f64}\left(\left(\frac{y}{\frac{1}{\frac{c \cdot x}{c}}}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       11. *-commutative N/A

           \[\leadsto \mathsf{+.f64}\left(\left(\frac{y}{\frac{1}{\frac{x \cdot c}{c}}}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       12. associate-/l* N/A

           \[\leadsto \mathsf{+.f64}\left(\left(\frac{y}{\frac{1}{x \cdot \frac{c}{c}}}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       13. *-inverses N/A

           \[\leadsto \mathsf{+.f64}\left(\left(\frac{y}{\frac{1}{x \cdot 1}}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       14. metadata-eval N/A

           \[\leadsto \mathsf{+.f64}\left(\left(\frac{y}{\frac{1}{x \cdot \frac{1}{1}}}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       15. div-inv N/A

           \[\leadsto \mathsf{+.f64}\left(\left(\frac{y}{\frac{1}{\frac{x}{1}}}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       16. /-rgt-identity N/A

           \[\leadsto \mathsf{+.f64}\left(\left(\frac{y}{\frac{1}{x}}\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       17. /-lowering-/.f64 N/A

           \[\leadsto \mathsf{+.f64}\left(\mathsf{/.f64}\left(y, \left(\frac{1}{x}\right)\right), \mathsf{*.f64}\left(\color{blue}{b}, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

       18. /-lowering-/.f64 80.6%

           \[\leadsto \mathsf{+.f64}\left(\mathsf{/.f64}\left(y, \mathsf{/.f64}\left(1, x\right)\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-1}{4}\right)\right)\right) \]

   12. Applied egg-rr 80.6%

       \[\leadsto \color{blue}{\frac{y}{\frac{1}{x}}} + b \cdot \left(a \cdot -0.25\right) \]

   if -4.9999999999999999e119 < (*.f64 a b) < 2.0000000000000002e128

   1. Initial program 98.9%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 98.9%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in a around 0

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{-1}{16} \cdot \left(t \cdot z\right) - x \cdot y\right)}\right) \]
   6. Step-by-step derivation

      1. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\left(\frac{-1}{16} \cdot \left(t \cdot z\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      2. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \left(t \cdot z\right)\right), \left(\color{blue}{x} \cdot y\right)\right)\right) \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, z\right)\right), \left(x \cdot y\right)\right)\right) \]

      4. *-lowering-*.f64 92.1%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, z\right)\right), \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 92.1%

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

   if 2.0000000000000002e128 < (*.f64 a b)

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around 0

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{1}{4} \cdot \left(a \cdot b\right) - x \cdot y\right)}\right) \]
   6. Step-by-step derivation

      1. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\left(\frac{1}{4} \cdot \left(a \cdot b\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      2. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \left(a \cdot b\right)\right), \left(\color{blue}{x} \cdot y\right)\right)\right) \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \left(x \cdot y\right)\right)\right) \]

      4. *-lowering-*.f64 91.4%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 91.4%

      \[\leadsto c - \color{blue}{\left(0.25 \cdot \left(a \cdot b\right) - x \cdot y\right)} \]

   8. Taylor expanded in c around 0

      \[\leadsto \color{blue}{x \cdot y - \frac{1}{4} \cdot \left(a \cdot b\right)} \]
   9. Step-by-step derivation

      1. cancel-sign-sub-inv N/A

         \[\leadsto x \cdot y + \color{blue}{\left(\mathsf{neg}\left(\frac{1}{4}\right)\right) \cdot \left(a \cdot b\right)} \]

      2. metadata-eval N/A

         \[\leadsto x \cdot y + \frac{-1}{4} \cdot \left(\color{blue}{a} \cdot b\right) \]

      3. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\left(x \cdot y\right), \color{blue}{\left(\frac{-1}{4} \cdot \left(a \cdot b\right)\right)}\right) \]

      4. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \left(\color{blue}{\frac{-1}{4}} \cdot \left(a \cdot b\right)\right)\right) \]

      5. associate-*r* N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \left(\left(\frac{-1}{4} \cdot a\right) \cdot \color{blue}{b}\right)\right) \]

      6. *-commutative N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \left(b \cdot \color{blue}{\left(\frac{-1}{4} \cdot a\right)}\right)\right) \]

      7. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \mathsf{*.f64}\left(b, \color{blue}{\left(\frac{-1}{4} \cdot a\right)}\right)\right) \]

      8. *-commutative N/A

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \mathsf{*.f64}\left(b, \left(a \cdot \color{blue}{\frac{-1}{4}}\right)\right)\right) \]

      9. *-lowering-*.f64 88.4%

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(a, \color{blue}{\frac{-1}{4}}\right)\right)\right) \]

   10. Simplified 88.4%

       \[\leadsto \color{blue}{x \cdot y + b \cdot \left(a \cdot -0.25\right)} \]
3. Recombined 3 regimes into one program.

4. Final simplification 89.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \cdot a \leq -5 \cdot 10^{+119}:\\ \;\;\;\;\frac{y}{\frac{1}{x}} + b \cdot \left(-0.25 \cdot a\right)\\ \mathbf{elif}\;b \cdot a \leq 2 \cdot 10^{+128}:\\ \;\;\;\;c + \left(x \cdot y - -0.0625 \cdot \left(z \cdot t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot y + b \cdot \left(-0.25 \cdot a\right)\\ \end{array} \]
5. Add Preprocessing

Alternative 8: 83.9% accurate, 0.7× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := c + \left(x \cdot y - \left(b \cdot a\right) \cdot 0.25\right)\\ \mathbf{if}\;x \leq -2.4 \cdot 10^{+52}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;x \leq 4.1 \cdot 10^{-38}:\\ \;\;\;\;c - \left(-0.0625 \cdot \left(z \cdot t\right) + \frac{b \cdot a}{4}\right)\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (let* ((t_1 (+ c (- (* x y) (* (* b a) 0.25)))))
   (if (<= x -2.4e+52)
     t_1
     (if (<= x 4.1e-38) (- c (+ (* -0.0625 (* z t)) (/ (* b a) 4.0))) t_1))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = c + ((x * y) - ((b * a) * 0.25));
	double tmp;
	if (x <= -2.4e+52) {
		tmp = t_1;
	} else if (x <= 4.1e-38) {
		tmp = c - ((-0.0625 * (z * t)) + ((b * a) / 4.0));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: t_1
    real(8) :: tmp
    t_1 = c + ((x * y) - ((b * a) * 0.25d0))
    if (x <= (-2.4d+52)) then
        tmp = t_1
    else if (x <= 4.1d-38) then
        tmp = c - (((-0.0625d0) * (z * t)) + ((b * a) / 4.0d0))
    else
        tmp = t_1
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = c + ((x * y) - ((b * a) * 0.25));
	double tmp;
	if (x <= -2.4e+52) {
		tmp = t_1;
	} else if (x <= 4.1e-38) {
		tmp = c - ((-0.0625 * (z * t)) + ((b * a) / 4.0));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	t_1 = c + ((x * y) - ((b * a) * 0.25))
	tmp = 0
	if x <= -2.4e+52:
		tmp = t_1
	elif x <= 4.1e-38:
		tmp = c - ((-0.0625 * (z * t)) + ((b * a) / 4.0))
	else:
		tmp = t_1
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	t_1 = Float64(c + Float64(Float64(x * y) - Float64(Float64(b * a) * 0.25)))
	tmp = 0.0
	if (x <= -2.4e+52)
		tmp = t_1;
	elseif (x <= 4.1e-38)
		tmp = Float64(c - Float64(Float64(-0.0625 * Float64(z * t)) + Float64(Float64(b * a) / 4.0)));
	else
		tmp = t_1;
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	t_1 = c + ((x * y) - ((b * a) * 0.25));
	tmp = 0.0;
	if (x <= -2.4e+52)
		tmp = t_1;
	elseif (x <= 4.1e-38)
		tmp = c - ((-0.0625 * (z * t)) + ((b * a) / 4.0));
	else
		tmp = t_1;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := Block[{t$95$1 = N[(c + N[(N[(x * y), $MachinePrecision] - N[(N[(b * a), $MachinePrecision] * 0.25), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[x, -2.4e+52], t$95$1, If[LessEqual[x, 4.1e-38], N[(c - N[(N[(-0.0625 * N[(z * t), $MachinePrecision]), $MachinePrecision] + N[(N[(b * a), $MachinePrecision] / 4.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]

Derivation

1. Split input into 2 regimes

2. if x < -2.4e52 or 4.0999999999999998e-38 < x

   1. Initial program 97.6%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 97.6%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around 0

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{1}{4} \cdot \left(a \cdot b\right) - x \cdot y\right)}\right) \]
   6. Step-by-step derivation

      1. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\left(\frac{1}{4} \cdot \left(a \cdot b\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      2. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \left(a \cdot b\right)\right), \left(\color{blue}{x} \cdot y\right)\right)\right) \]

      3. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \left(x \cdot y\right)\right)\right) \]

      4. *-lowering-*.f64 84.2%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, b\right)\right), \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 84.2%

      \[\leadsto c - \color{blue}{\left(0.25 \cdot \left(a \cdot b\right) - x \cdot y\right)} \]

   if -2.4e52 < x < 4.0999999999999998e-38

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \color{blue}{\left(\frac{-1}{16} \cdot \left(t \cdot z\right)\right)}\right)\right) \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{*.f64}\left(\frac{-1}{16}, \color{blue}{\left(t \cdot z\right)}\right)\right)\right) \]

      2. *-lowering-*.f64 86.5%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, \color{blue}{z}\right)\right)\right)\right) \]

   7. Simplified 86.5%

      \[\leadsto c - \left(\frac{a \cdot b}{4} + \color{blue}{-0.0625 \cdot \left(t \cdot z\right)}\right) \]
3. Recombined 2 regimes into one program.

4. Final simplification 85.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -2.4 \cdot 10^{+52}:\\ \;\;\;\;c + \left(x \cdot y - \left(b \cdot a\right) \cdot 0.25\right)\\ \mathbf{elif}\;x \leq 4.1 \cdot 10^{-38}:\\ \;\;\;\;c - \left(-0.0625 \cdot \left(z \cdot t\right) + \frac{b \cdot a}{4}\right)\\ \mathbf{else}:\\ \;\;\;\;c + \left(x \cdot y - \left(b \cdot a\right) \cdot 0.25\right)\\ \end{array} \]
5. Add Preprocessing

Alternative 9: 56.4% accurate, 0.8× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -2.05 \cdot 10^{+52}:\\ \;\;\;\;x \cdot y + c\\ \mathbf{elif}\;x \leq 1.36 \cdot 10^{-250}:\\ \;\;\;\;c - -0.0625 \cdot \left(z \cdot t\right)\\ \mathbf{elif}\;x \leq 35000:\\ \;\;\;\;c - \left(b \cdot a\right) \cdot 0.25\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (if (<= x -2.05e+52)
   (+ (* x y) c)
   (if (<= x 1.36e-250)
     (- c (* -0.0625 (* z t)))
     (if (<= x 35000.0) (- c (* (* b a) 0.25)) (* x y)))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double tmp;
	if (x <= -2.05e+52) {
		tmp = (x * y) + c;
	} else if (x <= 1.36e-250) {
		tmp = c - (-0.0625 * (z * t));
	} else if (x <= 35000.0) {
		tmp = c - ((b * a) * 0.25);
	} else {
		tmp = x * y;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: tmp
    if (x <= (-2.05d+52)) then
        tmp = (x * y) + c
    else if (x <= 1.36d-250) then
        tmp = c - ((-0.0625d0) * (z * t))
    else if (x <= 35000.0d0) then
        tmp = c - ((b * a) * 0.25d0)
    else
        tmp = x * y
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double tmp;
	if (x <= -2.05e+52) {
		tmp = (x * y) + c;
	} else if (x <= 1.36e-250) {
		tmp = c - (-0.0625 * (z * t));
	} else if (x <= 35000.0) {
		tmp = c - ((b * a) * 0.25);
	} else {
		tmp = x * y;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	tmp = 0
	if x <= -2.05e+52:
		tmp = (x * y) + c
	elif x <= 1.36e-250:
		tmp = c - (-0.0625 * (z * t))
	elif x <= 35000.0:
		tmp = c - ((b * a) * 0.25)
	else:
		tmp = x * y
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	tmp = 0.0
	if (x <= -2.05e+52)
		tmp = Float64(Float64(x * y) + c);
	elseif (x <= 1.36e-250)
		tmp = Float64(c - Float64(-0.0625 * Float64(z * t)));
	elseif (x <= 35000.0)
		tmp = Float64(c - Float64(Float64(b * a) * 0.25));
	else
		tmp = Float64(x * y);
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	tmp = 0.0;
	if (x <= -2.05e+52)
		tmp = (x * y) + c;
	elseif (x <= 1.36e-250)
		tmp = c - (-0.0625 * (z * t));
	elseif (x <= 35000.0)
		tmp = c - ((b * a) * 0.25);
	else
		tmp = x * y;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := If[LessEqual[x, -2.05e+52], N[(N[(x * y), $MachinePrecision] + c), $MachinePrecision], If[LessEqual[x, 1.36e-250], N[(c - N[(-0.0625 * N[(z * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[x, 35000.0], N[(c - N[(N[(b * a), $MachinePrecision] * 0.25), $MachinePrecision]), $MachinePrecision], N[(x * y), $MachinePrecision]]]]

Derivation

1. Split input into 4 regimes

2. if x < -2.05e52

   1. Initial program 98.2%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 98.2%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(-1 \cdot \left(x \cdot y\right)\right)}\right) \]
   6. Step-by-step derivation

      1. mul-1-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\mathsf{neg}\left(x \cdot y\right)\right)\right) \]

      2. neg-sub0 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(0 - \color{blue}{x \cdot y}\right)\right) \]

      3. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(0, \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      4. *-lowering-*.f64 75.4%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 75.4%

      \[\leadsto c - \color{blue}{\left(0 - x \cdot y\right)} \]
   8. Step-by-step derivation

      1. associate--r- N/A

         \[\leadsto \left(c - 0\right) + \color{blue}{x \cdot y} \]

      2. --rgt-identity N/A

         \[\leadsto c + \color{blue}{x} \cdot y \]

      3. +-commutative N/A

         \[\leadsto x \cdot y + \color{blue}{c} \]

      4. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\left(x \cdot y\right), \color{blue}{c}\right) \]

      5. *-lowering-*.f64 75.4%

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), c\right) \]

   9. Applied egg-rr 75.4%

      \[\leadsto \color{blue}{x \cdot y + c} \]

   if -2.05e52 < x < 1.36000000000000007e-250

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{-1}{16} \cdot \left(t \cdot z\right)\right)}\right) \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(\frac{-1}{16}, \color{blue}{\left(t \cdot z\right)}\right)\right) \]

      2. *-lowering-*.f64 64.9%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, \color{blue}{z}\right)\right)\right) \]

   7. Simplified 64.9%

      \[\leadsto c - \color{blue}{-0.0625 \cdot \left(t \cdot z\right)} \]

   if 1.36000000000000007e-250 < x < 35000

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in a around inf

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{1}{4} \cdot \left(a \cdot b\right)\right)}\right) \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(\frac{1}{4}, \color{blue}{\left(a \cdot b\right)}\right)\right) \]

      2. *-lowering-*.f64 73.5%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(a, \color{blue}{b}\right)\right)\right) \]

   7. Simplified 73.5%

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

   if 35000 < x

   1. Initial program 97.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 97.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf

      \[\leadsto \color{blue}{x \cdot y} \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 38.8%

         \[\leadsto \mathsf{*.f64}\left(x, \color{blue}{y}\right) \]

   7. Simplified 38.8%

      \[\leadsto \color{blue}{x \cdot y} \]
3. Recombined 4 regimes into one program.

4. Final simplification 61.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -2.05 \cdot 10^{+52}:\\ \;\;\;\;x \cdot y + c\\ \mathbf{elif}\;x \leq 1.36 \cdot 10^{-250}:\\ \;\;\;\;c - -0.0625 \cdot \left(z \cdot t\right)\\ \mathbf{elif}\;x \leq 35000:\\ \;\;\;\;c - \left(b \cdot a\right) \cdot 0.25\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array} \]
5. Add Preprocessing

Alternative 10: 59.7% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := x \cdot y + c\\ \mathbf{if}\;x \leq -1.8 \cdot 10^{+52}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;x \leq 1.6 \cdot 10^{-37}:\\ \;\;\;\;c - -0.0625 \cdot \left(z \cdot t\right)\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (let* ((t_1 (+ (* x y) c)))
   (if (<= x -1.8e+52) t_1 (if (<= x 1.6e-37) (- c (* -0.0625 (* z t))) t_1))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = (x * y) + c;
	double tmp;
	if (x <= -1.8e+52) {
		tmp = t_1;
	} else if (x <= 1.6e-37) {
		tmp = c - (-0.0625 * (z * t));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: t_1
    real(8) :: tmp
    t_1 = (x * y) + c
    if (x <= (-1.8d+52)) then
        tmp = t_1
    else if (x <= 1.6d-37) then
        tmp = c - ((-0.0625d0) * (z * t))
    else
        tmp = t_1
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = (x * y) + c;
	double tmp;
	if (x <= -1.8e+52) {
		tmp = t_1;
	} else if (x <= 1.6e-37) {
		tmp = c - (-0.0625 * (z * t));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	t_1 = (x * y) + c
	tmp = 0
	if x <= -1.8e+52:
		tmp = t_1
	elif x <= 1.6e-37:
		tmp = c - (-0.0625 * (z * t))
	else:
		tmp = t_1
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	t_1 = Float64(Float64(x * y) + c)
	tmp = 0.0
	if (x <= -1.8e+52)
		tmp = t_1;
	elseif (x <= 1.6e-37)
		tmp = Float64(c - Float64(-0.0625 * Float64(z * t)));
	else
		tmp = t_1;
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	t_1 = (x * y) + c;
	tmp = 0.0;
	if (x <= -1.8e+52)
		tmp = t_1;
	elseif (x <= 1.6e-37)
		tmp = c - (-0.0625 * (z * t));
	else
		tmp = t_1;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := Block[{t$95$1 = N[(N[(x * y), $MachinePrecision] + c), $MachinePrecision]}, If[LessEqual[x, -1.8e+52], t$95$1, If[LessEqual[x, 1.6e-37], N[(c - N[(-0.0625 * N[(z * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]

Derivation

1. Split input into 2 regimes

2. if x < -1.8e52 or 1.5999999999999999e-37 < x

   1. Initial program 97.6%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 97.6%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(-1 \cdot \left(x \cdot y\right)\right)}\right) \]
   6. Step-by-step derivation

      1. mul-1-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\mathsf{neg}\left(x \cdot y\right)\right)\right) \]

      2. neg-sub0 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(0 - \color{blue}{x \cdot y}\right)\right) \]

      3. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(0, \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      4. *-lowering-*.f64 67.0%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 67.0%

      \[\leadsto c - \color{blue}{\left(0 - x \cdot y\right)} \]
   8. Step-by-step derivation

      1. associate--r- N/A

         \[\leadsto \left(c - 0\right) + \color{blue}{x \cdot y} \]

      2. --rgt-identity N/A

         \[\leadsto c + \color{blue}{x} \cdot y \]

      3. +-commutative N/A

         \[\leadsto x \cdot y + \color{blue}{c} \]

      4. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\left(x \cdot y\right), \color{blue}{c}\right) \]

      5. *-lowering-*.f64 67.0%

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), c\right) \]

   9. Applied egg-rr 67.0%

      \[\leadsto \color{blue}{x \cdot y + c} \]

   if -1.8e52 < x < 1.5999999999999999e-37

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around inf

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{-1}{16} \cdot \left(t \cdot z\right)\right)}\right) \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(\frac{-1}{16}, \color{blue}{\left(t \cdot z\right)}\right)\right) \]

      2. *-lowering-*.f64 58.0%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{*.f64}\left(\frac{-1}{16}, \mathsf{*.f64}\left(t, \color{blue}{z}\right)\right)\right) \]

   7. Simplified 58.0%

      \[\leadsto c - \color{blue}{-0.0625 \cdot \left(t \cdot z\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification 62.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1.8 \cdot 10^{+52}:\\ \;\;\;\;x \cdot y + c\\ \mathbf{elif}\;x \leq 1.6 \cdot 10^{-37}:\\ \;\;\;\;c - -0.0625 \cdot \left(z \cdot t\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot y + c\\ \end{array} \]
5. Add Preprocessing

Alternative 11: 41.3% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \cdot y \leq -2.9 \cdot 10^{+58}:\\ \;\;\;\;x \cdot y\\ \mathbf{elif}\;x \cdot y \leq 6.2 \cdot 10^{+47}:\\ \;\;\;\;c\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (if (<= (* x y) -2.9e+58) (* x y) (if (<= (* x y) 6.2e+47) c (* x y))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double tmp;
	if ((x * y) <= -2.9e+58) {
		tmp = x * y;
	} else if ((x * y) <= 6.2e+47) {
		tmp = c;
	} else {
		tmp = x * y;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: tmp
    if ((x * y) <= (-2.9d+58)) then
        tmp = x * y
    else if ((x * y) <= 6.2d+47) then
        tmp = c
    else
        tmp = x * y
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double tmp;
	if ((x * y) <= -2.9e+58) {
		tmp = x * y;
	} else if ((x * y) <= 6.2e+47) {
		tmp = c;
	} else {
		tmp = x * y;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	tmp = 0
	if (x * y) <= -2.9e+58:
		tmp = x * y
	elif (x * y) <= 6.2e+47:
		tmp = c
	else:
		tmp = x * y
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	tmp = 0.0
	if (Float64(x * y) <= -2.9e+58)
		tmp = Float64(x * y);
	elseif (Float64(x * y) <= 6.2e+47)
		tmp = c;
	else
		tmp = Float64(x * y);
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	tmp = 0.0;
	if ((x * y) <= -2.9e+58)
		tmp = x * y;
	elseif ((x * y) <= 6.2e+47)
		tmp = c;
	else
		tmp = x * y;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := If[LessEqual[N[(x * y), $MachinePrecision], -2.9e+58], N[(x * y), $MachinePrecision], If[LessEqual[N[(x * y), $MachinePrecision], 6.2e+47], c, N[(x * y), $MachinePrecision]]]

Derivation

1. Split input into 2 regimes

2. if (*.f64 x y) < -2.90000000000000002e58 or 6.2000000000000001e47 < (*.f64 x y)

   1. Initial program 96.9%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 96.9%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf

      \[\leadsto \color{blue}{x \cdot y} \]
   6. Step-by-step derivation

      1. *-lowering-*.f64 66.0%

         \[\leadsto \mathsf{*.f64}\left(x, \color{blue}{y}\right) \]

   7. Simplified 66.0%

      \[\leadsto \color{blue}{x \cdot y} \]

   if -2.90000000000000002e58 < (*.f64 x y) < 6.2000000000000001e47

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in c around inf

      \[\leadsto \color{blue}{c} \]
   6. Step-by-step derivation

   7. Simplified 34.6%

      \[\leadsto \color{blue}{c} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 12: 55.7% accurate, 1.1× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_1 := t \cdot \left(z \cdot 0.0625\right)\\ \mathbf{if}\;z \leq -1 \cdot 10^{+159}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;z \leq 2.4 \cdot 10^{+85}:\\ \;\;\;\;x \cdot y + c\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z t a b c)
 :precision binary64
 (let* ((t_1 (* t (* z 0.0625))))
   (if (<= z -1e+159) t_1 (if (<= z 2.4e+85) (+ (* x y) c) t_1))))

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = t * (z * 0.0625);
	double tmp;
	if (z <= -1e+159) {
		tmp = t_1;
	} else if (z <= 2.4e+85) {
		tmp = (x * y) + c;
	} else {
		tmp = t_1;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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) :: t_1
    real(8) :: tmp
    t_1 = t * (z * 0.0625d0)
    if (z <= (-1d+159)) then
        tmp = t_1
    else if (z <= 2.4d+85) then
        tmp = (x * y) + c
    else
        tmp = t_1
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	double t_1 = t * (z * 0.0625);
	double tmp;
	if (z <= -1e+159) {
		tmp = t_1;
	} else if (z <= 2.4e+85) {
		tmp = (x * y) + c;
	} else {
		tmp = t_1;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b, c):
	t_1 = t * (z * 0.0625)
	tmp = 0
	if z <= -1e+159:
		tmp = t_1
	elif z <= 2.4e+85:
		tmp = (x * y) + c
	else:
		tmp = t_1
	return tmp

Julia

function code(x, y, z, t, a, b, c)
	t_1 = Float64(t * Float64(z * 0.0625))
	tmp = 0.0
	if (z <= -1e+159)
		tmp = t_1;
	elseif (z <= 2.4e+85)
		tmp = Float64(Float64(x * y) + c);
	else
		tmp = t_1;
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b, c)
	t_1 = t * (z * 0.0625);
	tmp = 0.0;
	if (z <= -1e+159)
		tmp = t_1;
	elseif (z <= 2.4e+85)
		tmp = (x * y) + c;
	else
		tmp = t_1;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := Block[{t$95$1 = N[(t * N[(z * 0.0625), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[z, -1e+159], t$95$1, If[LessEqual[z, 2.4e+85], N[(N[(x * y), $MachinePrecision] + c), $MachinePrecision], t$95$1]]]

Derivation

1. Split input into 2 regimes

2. if z < -9.9999999999999993e158 or 2.39999999999999997e85 < z

   1. Initial program 95.9%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 95.9%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in z around inf

      \[\leadsto \color{blue}{\frac{1}{16} \cdot \left(t \cdot z\right)} \]
   6. Step-by-step derivation

      1. *-commutative N/A

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

      2. associate-*r* N/A

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

      3. *-commutative N/A

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

      4. *-lowering-*.f64 N/A

         \[\leadsto \mathsf{*.f64}\left(t, \color{blue}{\left(\frac{1}{16} \cdot z\right)}\right) \]

      5. *-commutative N/A

         \[\leadsto \mathsf{*.f64}\left(t, \left(z \cdot \color{blue}{\frac{1}{16}}\right)\right) \]

      6. *-lowering-*.f64 56.4%

         \[\leadsto \mathsf{*.f64}\left(t, \mathsf{*.f64}\left(z, \color{blue}{\frac{1}{16}}\right)\right) \]

   7. Simplified 56.4%

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

   if -9.9999999999999993e158 < z < 2.39999999999999997e85

   1. Initial program 100.0%

      \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
   2. Step-by-step derivation

      1. +-commutative N/A

         \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

      2. sub-neg N/A

         \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

      3. +-commutative N/A

         \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

      4. associate-+r+ N/A

         \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

      5. unsub-neg N/A

         \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

      6. associate-+l- N/A

         \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

      7. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

      8. sub-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      9. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

      10. /-lowering-/.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

      11. *-lowering-*.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

      12. +-commutative N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

      13. distribute-neg-in N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

      14. unsub-neg N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

      15. --lowering--.f64 N/A

          \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

   3. Simplified 100.0%

      \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(-1 \cdot \left(x \cdot y\right)\right)}\right) \]
   6. Step-by-step derivation

      1. mul-1-neg N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(\mathsf{neg}\left(x \cdot y\right)\right)\right) \]

      2. neg-sub0 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \left(0 - \color{blue}{x \cdot y}\right)\right) \]

      3. --lowering--.f64 N/A

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(0, \color{blue}{\left(x \cdot y\right)}\right)\right) \]

      4. *-lowering-*.f64 60.7%

         \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(x, \color{blue}{y}\right)\right)\right) \]

   7. Simplified 60.7%

      \[\leadsto c - \color{blue}{\left(0 - x \cdot y\right)} \]
   8. Step-by-step derivation

      1. associate--r- N/A

         \[\leadsto \left(c - 0\right) + \color{blue}{x \cdot y} \]

      2. --rgt-identity N/A

         \[\leadsto c + \color{blue}{x} \cdot y \]

      3. +-commutative N/A

         \[\leadsto x \cdot y + \color{blue}{c} \]

      4. +-lowering-+.f64 N/A

         \[\leadsto \mathsf{+.f64}\left(\left(x \cdot y\right), \color{blue}{c}\right) \]

      5. *-lowering-*.f64 60.7%

         \[\leadsto \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, y\right), c\right) \]

   9. Applied egg-rr 60.7%

      \[\leadsto \color{blue}{x \cdot y + c} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 13: 21.9% accurate, 17.0× speedup

Math

\[\begin{array}{l} \\ c \end{array} \]

FPCore

(FPCore (x y z t a b c) :precision binary64 c)

C

double code(double x, double y, double z, double t, double a, double b, double c) {
	return c;
}

Fortran

real(8) function code(x, y, z, t, a, b, c)
    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
    code = c
end function

Java

public static double code(double x, double y, double z, double t, double a, double b, double c) {
	return c;
}

Python

def code(x, y, z, t, a, b, c):
	return c

Julia

function code(x, y, z, t, a, b, c)
	return c
end

MATLAB

function tmp = code(x, y, z, t, a, b, c)
	tmp = c;
end

Wolfram

code[x_, y_, z_, t_, a_, b_, c_] := c

Derivation

1. Initial program 98.8%

   \[\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right) + c \]
2. Step-by-step derivation

   1. +-commutative N/A

      \[\leadsto c + \color{blue}{\left(\left(x \cdot y + \frac{z \cdot t}{16}\right) - \frac{a \cdot b}{4}\right)} \]

   2. sub-neg N/A

      \[\leadsto c + \left(\left(x \cdot y + \frac{z \cdot t}{16}\right) + \color{blue}{\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)}\right) \]

   3. +-commutative N/A

      \[\leadsto c + \left(\left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right) \]

   4. associate-+r+ N/A

      \[\leadsto \left(c + \left(\mathsf{neg}\left(\frac{a \cdot b}{4}\right)\right)\right) + \color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)} \]

   5. unsub-neg N/A

      \[\leadsto \left(c - \frac{a \cdot b}{4}\right) + \left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right) \]

   6. associate-+l- N/A

      \[\leadsto c - \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)} \]

   7. --lowering--.f64 N/A

      \[\leadsto \mathsf{\_.f64}\left(c, \color{blue}{\left(\frac{a \cdot b}{4} - \left(x \cdot y + \frac{z \cdot t}{16}\right)\right)}\right) \]

   8. sub-neg N/A

      \[\leadsto \mathsf{\_.f64}\left(c, \left(\frac{a \cdot b}{4} + \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

   9. +-lowering-+.f64 N/A

      \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\left(\frac{a \cdot b}{4}\right), \color{blue}{\left(\mathsf{neg}\left(\left(x \cdot y + \frac{z \cdot t}{16}\right)\right)\right)}\right)\right) \]

   10. /-lowering-/.f64 N/A

       \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\left(a \cdot b\right), 4\right), \left(\mathsf{neg}\left(\color{blue}{\left(x \cdot y + \frac{z \cdot t}{16}\right)}\right)\right)\right)\right) \]

   11. *-lowering-*.f64 N/A

       \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\color{blue}{x \cdot y} + \frac{z \cdot t}{16}\right)\right)\right)\right)\right) \]

   12. +-commutative N/A

       \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\mathsf{neg}\left(\left(\frac{z \cdot t}{16} + x \cdot y\right)\right)\right)\right)\right) \]

   13. distribute-neg-in N/A

       \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) + \color{blue}{\left(\mathsf{neg}\left(x \cdot y\right)\right)}\right)\right)\right) \]

   14. unsub-neg N/A

       \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right) - \color{blue}{x \cdot y}\right)\right)\right) \]

   15. --lowering--.f64 N/A

       \[\leadsto \mathsf{\_.f64}\left(c, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(a, b\right), 4\right), \mathsf{\_.f64}\left(\left(\mathsf{neg}\left(\frac{z \cdot t}{16}\right)\right), \color{blue}{\left(x \cdot y\right)}\right)\right)\right) \]

3. Simplified 98.8%

   \[\leadsto \color{blue}{c - \left(\frac{a \cdot b}{4} + \left(\frac{z \cdot t}{-16} - x \cdot y\right)\right)} \]
4. Add Preprocessing

5. Taylor expanded in c around inf

   \[\leadsto \color{blue}{c} \]
6. Step-by-step derivation

7. Simplified 24.4%

   \[\leadsto \color{blue}{c} \]
8. Add Preprocessing

Reproduce

herbie shell --seed 2024192 
(FPCore (x y z t a b c)
  :name "Diagrams.Solve.Polynomial:quartForm  from diagrams-solve-0.1, C"
  :precision binary64
  (+ (- (+ (* x y) (/ (* z t) 16.0)) (/ (* a b) 4.0)) c))