Data.Array.Repa.Algorithms.ColorRamp:rampColorHotToCold from repa-algorithms-3.4.0.1, A

Percentage Accurate: 99.8% → 100.0%
Time: 7.0s
Alternatives: 9
Speedup: 1.5×

Specification

?
\[\begin{array}{l} \\ 1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \end{array} \]
(FPCore (x y z)
 :precision binary64
 (+ 1.0 (/ (* 4.0 (- (+ x (* y 0.75)) z)) y)))
double code(double x, double y, double z) {
	return 1.0 + ((4.0 * ((x + (y * 0.75)) - z)) / y);
}
real(8) function code(x, y, z)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = 1.0d0 + ((4.0d0 * ((x + (y * 0.75d0)) - z)) / y)
end function
public static double code(double x, double y, double z) {
	return 1.0 + ((4.0 * ((x + (y * 0.75)) - z)) / y);
}
def code(x, y, z):
	return 1.0 + ((4.0 * ((x + (y * 0.75)) - z)) / y)
function code(x, y, z)
	return Float64(1.0 + Float64(Float64(4.0 * Float64(Float64(x + Float64(y * 0.75)) - z)) / y))
end
function tmp = code(x, y, z)
	tmp = 1.0 + ((4.0 * ((x + (y * 0.75)) - z)) / y);
end
code[x_, y_, z_] := N[(1.0 + N[(N[(4.0 * N[(N[(x + N[(y * 0.75), $MachinePrecision]), $MachinePrecision] - z), $MachinePrecision]), $MachinePrecision] / y), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

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

Accuracy vs Speed?

Herbie found 9 alternatives:

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

Initial Program: 99.8% accurate, 1.0× speedup?

\[\begin{array}{l} \\ 1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \end{array} \]
(FPCore (x y z)
 :precision binary64
 (+ 1.0 (/ (* 4.0 (- (+ x (* y 0.75)) z)) y)))
double code(double x, double y, double z) {
	return 1.0 + ((4.0 * ((x + (y * 0.75)) - z)) / y);
}
real(8) function code(x, y, z)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = 1.0d0 + ((4.0d0 * ((x + (y * 0.75d0)) - z)) / y)
end function
public static double code(double x, double y, double z) {
	return 1.0 + ((4.0 * ((x + (y * 0.75)) - z)) / y);
}
def code(x, y, z):
	return 1.0 + ((4.0 * ((x + (y * 0.75)) - z)) / y)
function code(x, y, z)
	return Float64(1.0 + Float64(Float64(4.0 * Float64(Float64(x + Float64(y * 0.75)) - z)) / y))
end
function tmp = code(x, y, z)
	tmp = 1.0 + ((4.0 * ((x + (y * 0.75)) - z)) / y);
end
code[x_, y_, z_] := N[(1.0 + N[(N[(4.0 * N[(N[(x + N[(y * 0.75), $MachinePrecision]), $MachinePrecision] - z), $MachinePrecision]), $MachinePrecision] / y), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}
\end{array}

Alternative 1: 100.0% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \mathsf{fma}\left(\frac{x - z}{y}, 4, 4\right) \end{array} \]
(FPCore (x y z) :precision binary64 (fma (/ (- x z) y) 4.0 4.0))
double code(double x, double y, double z) {
	return fma(((x - z) / y), 4.0, 4.0);
}
function code(x, y, z)
	return fma(Float64(Float64(x - z) / y), 4.0, 4.0)
end
code[x_, y_, z_] := N[(N[(N[(x - z), $MachinePrecision] / y), $MachinePrecision] * 4.0 + 4.0), $MachinePrecision]
\begin{array}{l}

\\
\mathsf{fma}\left(\frac{x - z}{y}, 4, 4\right)
\end{array}
Derivation
  1. Initial program 99.6%

    \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
  2. Add Preprocessing
  3. Taylor expanded in x around 0

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

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

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

      \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} + \left(4 \cdot \frac{\frac{3}{4} \cdot y - z}{y} + 1\right) \]
    4. div-subN/A

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

      \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) + 1\right) \]
    6. *-inversesN/A

      \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) + 1\right) \]
    7. metadata-evalN/A

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

      \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(1 + 4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right)\right)} \]
    9. sub-negN/A

      \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)}\right) \]
    10. distribute-rgt-inN/A

      \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \color{blue}{\left(\frac{3}{4} \cdot 4 + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)}\right) \]
    11. metadata-evalN/A

      \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \left(\color{blue}{3} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)\right) \]
    12. associate-+r+N/A

      \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(1 + 3\right) + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)} \]
    13. metadata-evalN/A

      \[\leadsto \frac{x}{y} \cdot 4 + \left(\color{blue}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right) \]
    14. distribute-rgt1-inN/A

      \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right) \cdot 4} \]
    15. distribute-rgt-inN/A

      \[\leadsto \color{blue}{4 \cdot \left(\frac{x}{y} + \left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right)\right)} \]
    16. associate-+l+N/A

      \[\leadsto 4 \cdot \color{blue}{\left(\left(\frac{x}{y} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right) + 1\right)} \]
    17. sub-negN/A

      \[\leadsto 4 \cdot \left(\color{blue}{\left(\frac{x}{y} - \frac{z}{y}\right)} + 1\right) \]
    18. div-subN/A

      \[\leadsto 4 \cdot \left(\color{blue}{\frac{x - z}{y}} + 1\right) \]
  5. Applied rewrites100.0%

    \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, 4, 4\right)} \]
  6. Add Preprocessing

Alternative 2: 65.2% accurate, 0.2× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{z}{y} \cdot -4\\ t_1 := \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}\\ t_2 := \frac{x}{y} \cdot 4\\ \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+255}:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;t\_1 \leq -4000000000000:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 1.25 \cdot 10^{+31}:\\ \;\;\;\;4\\ \mathbf{elif}\;t\_1 \leq 10^{+158}:\\ \;\;\;\;t\_2\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
(FPCore (x y z)
 :precision binary64
 (let* ((t_0 (* (/ z y) -4.0))
        (t_1 (/ (* 4.0 (- (+ x (* y 0.75)) z)) y))
        (t_2 (* (/ x y) 4.0)))
   (if (<= t_1 -1e+255)
     t_0
     (if (<= t_1 -4000000000000.0)
       t_2
       (if (<= t_1 1.25e+31) 4.0 (if (<= t_1 1e+158) t_2 t_0))))))
double code(double x, double y, double z) {
	double t_0 = (z / y) * -4.0;
	double t_1 = (4.0 * ((x + (y * 0.75)) - z)) / y;
	double t_2 = (x / y) * 4.0;
	double tmp;
	if (t_1 <= -1e+255) {
		tmp = t_0;
	} else if (t_1 <= -4000000000000.0) {
		tmp = t_2;
	} else if (t_1 <= 1.25e+31) {
		tmp = 4.0;
	} else if (t_1 <= 1e+158) {
		tmp = t_2;
	} else {
		tmp = t_0;
	}
	return tmp;
}
real(8) function code(x, y, z)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8) :: t_0
    real(8) :: t_1
    real(8) :: t_2
    real(8) :: tmp
    t_0 = (z / y) * (-4.0d0)
    t_1 = (4.0d0 * ((x + (y * 0.75d0)) - z)) / y
    t_2 = (x / y) * 4.0d0
    if (t_1 <= (-1d+255)) then
        tmp = t_0
    else if (t_1 <= (-4000000000000.0d0)) then
        tmp = t_2
    else if (t_1 <= 1.25d+31) then
        tmp = 4.0d0
    else if (t_1 <= 1d+158) then
        tmp = t_2
    else
        tmp = t_0
    end if
    code = tmp
end function
public static double code(double x, double y, double z) {
	double t_0 = (z / y) * -4.0;
	double t_1 = (4.0 * ((x + (y * 0.75)) - z)) / y;
	double t_2 = (x / y) * 4.0;
	double tmp;
	if (t_1 <= -1e+255) {
		tmp = t_0;
	} else if (t_1 <= -4000000000000.0) {
		tmp = t_2;
	} else if (t_1 <= 1.25e+31) {
		tmp = 4.0;
	} else if (t_1 <= 1e+158) {
		tmp = t_2;
	} else {
		tmp = t_0;
	}
	return tmp;
}
def code(x, y, z):
	t_0 = (z / y) * -4.0
	t_1 = (4.0 * ((x + (y * 0.75)) - z)) / y
	t_2 = (x / y) * 4.0
	tmp = 0
	if t_1 <= -1e+255:
		tmp = t_0
	elif t_1 <= -4000000000000.0:
		tmp = t_2
	elif t_1 <= 1.25e+31:
		tmp = 4.0
	elif t_1 <= 1e+158:
		tmp = t_2
	else:
		tmp = t_0
	return tmp
function code(x, y, z)
	t_0 = Float64(Float64(z / y) * -4.0)
	t_1 = Float64(Float64(4.0 * Float64(Float64(x + Float64(y * 0.75)) - z)) / y)
	t_2 = Float64(Float64(x / y) * 4.0)
	tmp = 0.0
	if (t_1 <= -1e+255)
		tmp = t_0;
	elseif (t_1 <= -4000000000000.0)
		tmp = t_2;
	elseif (t_1 <= 1.25e+31)
		tmp = 4.0;
	elseif (t_1 <= 1e+158)
		tmp = t_2;
	else
		tmp = t_0;
	end
	return tmp
end
function tmp_2 = code(x, y, z)
	t_0 = (z / y) * -4.0;
	t_1 = (4.0 * ((x + (y * 0.75)) - z)) / y;
	t_2 = (x / y) * 4.0;
	tmp = 0.0;
	if (t_1 <= -1e+255)
		tmp = t_0;
	elseif (t_1 <= -4000000000000.0)
		tmp = t_2;
	elseif (t_1 <= 1.25e+31)
		tmp = 4.0;
	elseif (t_1 <= 1e+158)
		tmp = t_2;
	else
		tmp = t_0;
	end
	tmp_2 = tmp;
end
code[x_, y_, z_] := Block[{t$95$0 = N[(N[(z / y), $MachinePrecision] * -4.0), $MachinePrecision]}, Block[{t$95$1 = N[(N[(4.0 * N[(N[(x + N[(y * 0.75), $MachinePrecision]), $MachinePrecision] - z), $MachinePrecision]), $MachinePrecision] / y), $MachinePrecision]}, Block[{t$95$2 = N[(N[(x / y), $MachinePrecision] * 4.0), $MachinePrecision]}, If[LessEqual[t$95$1, -1e+255], t$95$0, If[LessEqual[t$95$1, -4000000000000.0], t$95$2, If[LessEqual[t$95$1, 1.25e+31], 4.0, If[LessEqual[t$95$1, 1e+158], t$95$2, t$95$0]]]]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{z}{y} \cdot -4\\
t_1 := \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}\\
t_2 := \frac{x}{y} \cdot 4\\
\mathbf{if}\;t\_1 \leq -1 \cdot 10^{+255}:\\
\;\;\;\;t\_0\\

\mathbf{elif}\;t\_1 \leq -4000000000000:\\
\;\;\;\;t\_2\\

\mathbf{elif}\;t\_1 \leq 1.25 \cdot 10^{+31}:\\
\;\;\;\;4\\

\mathbf{elif}\;t\_1 \leq 10^{+158}:\\
\;\;\;\;t\_2\\

\mathbf{else}:\\
\;\;\;\;t\_0\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < -9.99999999999999988e254 or 9.99999999999999953e157 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y)

    1. Initial program 98.9%

      \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
    2. Add Preprocessing
    3. Taylor expanded in x around 0

      \[\leadsto \color{blue}{1 + 4 \cdot \frac{\frac{3}{4} \cdot y - z}{y}} \]
    4. Step-by-step derivation
      1. div-subN/A

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

        \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) \]
      3. *-inversesN/A

        \[\leadsto 1 + 4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) \]
      4. metadata-evalN/A

        \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4}} - \frac{z}{y}\right) \]
      5. +-commutativeN/A

        \[\leadsto \color{blue}{4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right) + 1} \]
      6. sub-negN/A

        \[\leadsto 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)} + 1 \]
      7. +-commutativeN/A

        \[\leadsto 4 \cdot \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + \frac{3}{4}\right)} + 1 \]
      8. distribute-rgt-inN/A

        \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4 + \frac{3}{4} \cdot 4\right)} + 1 \]
      9. *-commutativeN/A

        \[\leadsto \left(\color{blue}{4 \cdot \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
      10. *-lft-identityN/A

        \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\frac{\color{blue}{1 \cdot z}}{y}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
      11. associate-*l/N/A

        \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{y} \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
      12. distribute-rgt-neg-inN/A

        \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(\frac{1}{y} \cdot z\right)\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
      13. associate-*l*N/A

        \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\left(4 \cdot \frac{1}{y}\right) \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
      14. *-commutativeN/A

        \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{z \cdot \left(4 \cdot \frac{1}{y}\right)}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
      15. metadata-evalN/A

        \[\leadsto \left(\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{3}\right) + 1 \]
      16. associate-+l+N/A

        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \left(3 + 1\right)} \]
      17. metadata-evalN/A

        \[\leadsto \left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{4} \]
    5. Applied rewrites64.6%

      \[\leadsto \color{blue}{\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)} \]
    6. Taylor expanded in y around 0

      \[\leadsto -4 \cdot \color{blue}{\frac{z}{y}} \]
    7. Step-by-step derivation
      1. Applied rewrites63.4%

        \[\leadsto \frac{z}{y} \cdot \color{blue}{-4} \]

      if -9.99999999999999988e254 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < -4e12 or 1.25000000000000007e31 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < 9.99999999999999953e157

      1. Initial program 100.0%

        \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
      2. Add Preprocessing
      3. Taylor expanded in x around 0

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

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

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

          \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} + \left(4 \cdot \frac{\frac{3}{4} \cdot y - z}{y} + 1\right) \]
        4. div-subN/A

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

          \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) + 1\right) \]
        6. *-inversesN/A

          \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) + 1\right) \]
        7. metadata-evalN/A

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

          \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(1 + 4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right)\right)} \]
        9. sub-negN/A

          \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)}\right) \]
        10. distribute-rgt-inN/A

          \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \color{blue}{\left(\frac{3}{4} \cdot 4 + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)}\right) \]
        11. metadata-evalN/A

          \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \left(\color{blue}{3} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)\right) \]
        12. associate-+r+N/A

          \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(1 + 3\right) + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)} \]
        13. metadata-evalN/A

          \[\leadsto \frac{x}{y} \cdot 4 + \left(\color{blue}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right) \]
        14. distribute-rgt1-inN/A

          \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right) \cdot 4} \]
        15. distribute-rgt-inN/A

          \[\leadsto \color{blue}{4 \cdot \left(\frac{x}{y} + \left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right)\right)} \]
        16. associate-+l+N/A

          \[\leadsto 4 \cdot \color{blue}{\left(\left(\frac{x}{y} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right) + 1\right)} \]
        17. sub-negN/A

          \[\leadsto 4 \cdot \left(\color{blue}{\left(\frac{x}{y} - \frac{z}{y}\right)} + 1\right) \]
        18. div-subN/A

          \[\leadsto 4 \cdot \left(\color{blue}{\frac{x - z}{y}} + 1\right) \]
      5. Applied rewrites100.0%

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

        \[\leadsto \color{blue}{4 \cdot \frac{x}{y}} \]
      7. Step-by-step derivation
        1. *-commutativeN/A

          \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} \]
        2. lower-*.f64N/A

          \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} \]
        3. lower-/.f6464.3

          \[\leadsto \color{blue}{\frac{x}{y}} \cdot 4 \]
      8. Applied rewrites64.3%

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

      if -4e12 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < 1.25000000000000007e31

      1. Initial program 99.9%

        \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
      2. Add Preprocessing
      3. Taylor expanded in y around inf

        \[\leadsto \color{blue}{4} \]
      4. Step-by-step derivation
        1. Applied rewrites93.1%

          \[\leadsto \color{blue}{4} \]
      5. Recombined 3 regimes into one program.
      6. Add Preprocessing

      Alternative 3: 65.1% accurate, 0.2× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{z}{y} \cdot -4\\ t_1 := \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}\\ t_2 := x \cdot \frac{4}{y}\\ \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+255}:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;t\_1 \leq -4000000000000:\\ \;\;\;\;t\_2\\ \mathbf{elif}\;t\_1 \leq 1.25 \cdot 10^{+31}:\\ \;\;\;\;4\\ \mathbf{elif}\;t\_1 \leq 10^{+158}:\\ \;\;\;\;t\_2\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
      (FPCore (x y z)
       :precision binary64
       (let* ((t_0 (* (/ z y) -4.0))
              (t_1 (/ (* 4.0 (- (+ x (* y 0.75)) z)) y))
              (t_2 (* x (/ 4.0 y))))
         (if (<= t_1 -1e+255)
           t_0
           (if (<= t_1 -4000000000000.0)
             t_2
             (if (<= t_1 1.25e+31) 4.0 (if (<= t_1 1e+158) t_2 t_0))))))
      double code(double x, double y, double z) {
      	double t_0 = (z / y) * -4.0;
      	double t_1 = (4.0 * ((x + (y * 0.75)) - z)) / y;
      	double t_2 = x * (4.0 / y);
      	double tmp;
      	if (t_1 <= -1e+255) {
      		tmp = t_0;
      	} else if (t_1 <= -4000000000000.0) {
      		tmp = t_2;
      	} else if (t_1 <= 1.25e+31) {
      		tmp = 4.0;
      	} else if (t_1 <= 1e+158) {
      		tmp = t_2;
      	} else {
      		tmp = t_0;
      	}
      	return tmp;
      }
      
      real(8) function code(x, y, z)
          real(8), intent (in) :: x
          real(8), intent (in) :: y
          real(8), intent (in) :: z
          real(8) :: t_0
          real(8) :: t_1
          real(8) :: t_2
          real(8) :: tmp
          t_0 = (z / y) * (-4.0d0)
          t_1 = (4.0d0 * ((x + (y * 0.75d0)) - z)) / y
          t_2 = x * (4.0d0 / y)
          if (t_1 <= (-1d+255)) then
              tmp = t_0
          else if (t_1 <= (-4000000000000.0d0)) then
              tmp = t_2
          else if (t_1 <= 1.25d+31) then
              tmp = 4.0d0
          else if (t_1 <= 1d+158) then
              tmp = t_2
          else
              tmp = t_0
          end if
          code = tmp
      end function
      
      public static double code(double x, double y, double z) {
      	double t_0 = (z / y) * -4.0;
      	double t_1 = (4.0 * ((x + (y * 0.75)) - z)) / y;
      	double t_2 = x * (4.0 / y);
      	double tmp;
      	if (t_1 <= -1e+255) {
      		tmp = t_0;
      	} else if (t_1 <= -4000000000000.0) {
      		tmp = t_2;
      	} else if (t_1 <= 1.25e+31) {
      		tmp = 4.0;
      	} else if (t_1 <= 1e+158) {
      		tmp = t_2;
      	} else {
      		tmp = t_0;
      	}
      	return tmp;
      }
      
      def code(x, y, z):
      	t_0 = (z / y) * -4.0
      	t_1 = (4.0 * ((x + (y * 0.75)) - z)) / y
      	t_2 = x * (4.0 / y)
      	tmp = 0
      	if t_1 <= -1e+255:
      		tmp = t_0
      	elif t_1 <= -4000000000000.0:
      		tmp = t_2
      	elif t_1 <= 1.25e+31:
      		tmp = 4.0
      	elif t_1 <= 1e+158:
      		tmp = t_2
      	else:
      		tmp = t_0
      	return tmp
      
      function code(x, y, z)
      	t_0 = Float64(Float64(z / y) * -4.0)
      	t_1 = Float64(Float64(4.0 * Float64(Float64(x + Float64(y * 0.75)) - z)) / y)
      	t_2 = Float64(x * Float64(4.0 / y))
      	tmp = 0.0
      	if (t_1 <= -1e+255)
      		tmp = t_0;
      	elseif (t_1 <= -4000000000000.0)
      		tmp = t_2;
      	elseif (t_1 <= 1.25e+31)
      		tmp = 4.0;
      	elseif (t_1 <= 1e+158)
      		tmp = t_2;
      	else
      		tmp = t_0;
      	end
      	return tmp
      end
      
      function tmp_2 = code(x, y, z)
      	t_0 = (z / y) * -4.0;
      	t_1 = (4.0 * ((x + (y * 0.75)) - z)) / y;
      	t_2 = x * (4.0 / y);
      	tmp = 0.0;
      	if (t_1 <= -1e+255)
      		tmp = t_0;
      	elseif (t_1 <= -4000000000000.0)
      		tmp = t_2;
      	elseif (t_1 <= 1.25e+31)
      		tmp = 4.0;
      	elseif (t_1 <= 1e+158)
      		tmp = t_2;
      	else
      		tmp = t_0;
      	end
      	tmp_2 = tmp;
      end
      
      code[x_, y_, z_] := Block[{t$95$0 = N[(N[(z / y), $MachinePrecision] * -4.0), $MachinePrecision]}, Block[{t$95$1 = N[(N[(4.0 * N[(N[(x + N[(y * 0.75), $MachinePrecision]), $MachinePrecision] - z), $MachinePrecision]), $MachinePrecision] / y), $MachinePrecision]}, Block[{t$95$2 = N[(x * N[(4.0 / y), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$1, -1e+255], t$95$0, If[LessEqual[t$95$1, -4000000000000.0], t$95$2, If[LessEqual[t$95$1, 1.25e+31], 4.0, If[LessEqual[t$95$1, 1e+158], t$95$2, t$95$0]]]]]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_0 := \frac{z}{y} \cdot -4\\
      t_1 := \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}\\
      t_2 := x \cdot \frac{4}{y}\\
      \mathbf{if}\;t\_1 \leq -1 \cdot 10^{+255}:\\
      \;\;\;\;t\_0\\
      
      \mathbf{elif}\;t\_1 \leq -4000000000000:\\
      \;\;\;\;t\_2\\
      
      \mathbf{elif}\;t\_1 \leq 1.25 \cdot 10^{+31}:\\
      \;\;\;\;4\\
      
      \mathbf{elif}\;t\_1 \leq 10^{+158}:\\
      \;\;\;\;t\_2\\
      
      \mathbf{else}:\\
      \;\;\;\;t\_0\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 3 regimes
      2. if (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < -9.99999999999999988e254 or 9.99999999999999953e157 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y)

        1. Initial program 98.9%

          \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

          \[\leadsto \color{blue}{1 + 4 \cdot \frac{\frac{3}{4} \cdot y - z}{y}} \]
        4. Step-by-step derivation
          1. div-subN/A

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

            \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) \]
          3. *-inversesN/A

            \[\leadsto 1 + 4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) \]
          4. metadata-evalN/A

            \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4}} - \frac{z}{y}\right) \]
          5. +-commutativeN/A

            \[\leadsto \color{blue}{4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right) + 1} \]
          6. sub-negN/A

            \[\leadsto 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)} + 1 \]
          7. +-commutativeN/A

            \[\leadsto 4 \cdot \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + \frac{3}{4}\right)} + 1 \]
          8. distribute-rgt-inN/A

            \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4 + \frac{3}{4} \cdot 4\right)} + 1 \]
          9. *-commutativeN/A

            \[\leadsto \left(\color{blue}{4 \cdot \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
          10. *-lft-identityN/A

            \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\frac{\color{blue}{1 \cdot z}}{y}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
          11. associate-*l/N/A

            \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{y} \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
          12. distribute-rgt-neg-inN/A

            \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(\frac{1}{y} \cdot z\right)\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
          13. associate-*l*N/A

            \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\left(4 \cdot \frac{1}{y}\right) \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
          14. *-commutativeN/A

            \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{z \cdot \left(4 \cdot \frac{1}{y}\right)}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
          15. metadata-evalN/A

            \[\leadsto \left(\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{3}\right) + 1 \]
          16. associate-+l+N/A

            \[\leadsto \color{blue}{\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \left(3 + 1\right)} \]
          17. metadata-evalN/A

            \[\leadsto \left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{4} \]
        5. Applied rewrites64.6%

          \[\leadsto \color{blue}{\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)} \]
        6. Taylor expanded in y around 0

          \[\leadsto -4 \cdot \color{blue}{\frac{z}{y}} \]
        7. Step-by-step derivation
          1. Applied rewrites63.4%

            \[\leadsto \frac{z}{y} \cdot \color{blue}{-4} \]

          if -9.99999999999999988e254 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < -4e12 or 1.25000000000000007e31 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < 9.99999999999999953e157

          1. Initial program 100.0%

            \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
          2. Add Preprocessing
          3. Taylor expanded in x around 0

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

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

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

              \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} + \left(4 \cdot \frac{\frac{3}{4} \cdot y - z}{y} + 1\right) \]
            4. div-subN/A

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

              \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) + 1\right) \]
            6. *-inversesN/A

              \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) + 1\right) \]
            7. metadata-evalN/A

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

              \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(1 + 4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right)\right)} \]
            9. sub-negN/A

              \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)}\right) \]
            10. distribute-rgt-inN/A

              \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \color{blue}{\left(\frac{3}{4} \cdot 4 + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)}\right) \]
            11. metadata-evalN/A

              \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \left(\color{blue}{3} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)\right) \]
            12. associate-+r+N/A

              \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(1 + 3\right) + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)} \]
            13. metadata-evalN/A

              \[\leadsto \frac{x}{y} \cdot 4 + \left(\color{blue}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right) \]
            14. distribute-rgt1-inN/A

              \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right) \cdot 4} \]
            15. distribute-rgt-inN/A

              \[\leadsto \color{blue}{4 \cdot \left(\frac{x}{y} + \left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right)\right)} \]
            16. associate-+l+N/A

              \[\leadsto 4 \cdot \color{blue}{\left(\left(\frac{x}{y} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right) + 1\right)} \]
            17. sub-negN/A

              \[\leadsto 4 \cdot \left(\color{blue}{\left(\frac{x}{y} - \frac{z}{y}\right)} + 1\right) \]
            18. div-subN/A

              \[\leadsto 4 \cdot \left(\color{blue}{\frac{x - z}{y}} + 1\right) \]
          5. Applied rewrites100.0%

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

            \[\leadsto \color{blue}{4 \cdot \frac{x}{y}} \]
          7. Step-by-step derivation
            1. *-commutativeN/A

              \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} \]
            2. lower-*.f64N/A

              \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} \]
            3. lower-/.f6464.3

              \[\leadsto \color{blue}{\frac{x}{y}} \cdot 4 \]
          8. Applied rewrites64.3%

            \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} \]
          9. Step-by-step derivation
            1. Applied rewrites64.0%

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

            if -4e12 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < 1.25000000000000007e31

            1. Initial program 99.9%

              \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
            2. Add Preprocessing
            3. Taylor expanded in y around inf

              \[\leadsto \color{blue}{4} \]
            4. Step-by-step derivation
              1. Applied rewrites93.1%

                \[\leadsto \color{blue}{4} \]
            5. Recombined 3 regimes into one program.
            6. Add Preprocessing

            Alternative 4: 97.3% accurate, 0.4× speedup?

            \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}\\ \mathbf{if}\;t\_0 \leq -2 \cdot 10^{+40} \lor \neg \left(t\_0 \leq 20000\right):\\ \;\;\;\;\left(z - x\right) \cdot \frac{-4}{y}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{y}, 4, 4\right)\\ \end{array} \end{array} \]
            (FPCore (x y z)
             :precision binary64
             (let* ((t_0 (/ (* 4.0 (- (+ x (* y 0.75)) z)) y)))
               (if (or (<= t_0 -2e+40) (not (<= t_0 20000.0)))
                 (* (- z x) (/ -4.0 y))
                 (fma (/ x y) 4.0 4.0))))
            double code(double x, double y, double z) {
            	double t_0 = (4.0 * ((x + (y * 0.75)) - z)) / y;
            	double tmp;
            	if ((t_0 <= -2e+40) || !(t_0 <= 20000.0)) {
            		tmp = (z - x) * (-4.0 / y);
            	} else {
            		tmp = fma((x / y), 4.0, 4.0);
            	}
            	return tmp;
            }
            
            function code(x, y, z)
            	t_0 = Float64(Float64(4.0 * Float64(Float64(x + Float64(y * 0.75)) - z)) / y)
            	tmp = 0.0
            	if ((t_0 <= -2e+40) || !(t_0 <= 20000.0))
            		tmp = Float64(Float64(z - x) * Float64(-4.0 / y));
            	else
            		tmp = fma(Float64(x / y), 4.0, 4.0);
            	end
            	return tmp
            end
            
            code[x_, y_, z_] := Block[{t$95$0 = N[(N[(4.0 * N[(N[(x + N[(y * 0.75), $MachinePrecision]), $MachinePrecision] - z), $MachinePrecision]), $MachinePrecision] / y), $MachinePrecision]}, If[Or[LessEqual[t$95$0, -2e+40], N[Not[LessEqual[t$95$0, 20000.0]], $MachinePrecision]], N[(N[(z - x), $MachinePrecision] * N[(-4.0 / y), $MachinePrecision]), $MachinePrecision], N[(N[(x / y), $MachinePrecision] * 4.0 + 4.0), $MachinePrecision]]]
            
            \begin{array}{l}
            
            \\
            \begin{array}{l}
            t_0 := \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}\\
            \mathbf{if}\;t\_0 \leq -2 \cdot 10^{+40} \lor \neg \left(t\_0 \leq 20000\right):\\
            \;\;\;\;\left(z - x\right) \cdot \frac{-4}{y}\\
            
            \mathbf{else}:\\
            \;\;\;\;\mathsf{fma}\left(\frac{x}{y}, 4, 4\right)\\
            
            
            \end{array}
            \end{array}
            
            Derivation
            1. Split input into 2 regimes
            2. if (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < -2.00000000000000006e40 or 2e4 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y)

              1. Initial program 99.3%

                \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
              2. Add Preprocessing
              3. Taylor expanded in x around 0

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

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

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

                  \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} + \left(4 \cdot \frac{\frac{3}{4} \cdot y - z}{y} + 1\right) \]
                4. div-subN/A

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

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) + 1\right) \]
                6. *-inversesN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) + 1\right) \]
                7. metadata-evalN/A

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

                  \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(1 + 4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right)\right)} \]
                9. sub-negN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)}\right) \]
                10. distribute-rgt-inN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \color{blue}{\left(\frac{3}{4} \cdot 4 + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)}\right) \]
                11. metadata-evalN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \left(\color{blue}{3} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)\right) \]
                12. associate-+r+N/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(1 + 3\right) + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)} \]
                13. metadata-evalN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(\color{blue}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right) \]
                14. distribute-rgt1-inN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right) \cdot 4} \]
                15. distribute-rgt-inN/A

                  \[\leadsto \color{blue}{4 \cdot \left(\frac{x}{y} + \left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right)\right)} \]
                16. associate-+l+N/A

                  \[\leadsto 4 \cdot \color{blue}{\left(\left(\frac{x}{y} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right) + 1\right)} \]
                17. sub-negN/A

                  \[\leadsto 4 \cdot \left(\color{blue}{\left(\frac{x}{y} - \frac{z}{y}\right)} + 1\right) \]
                18. div-subN/A

                  \[\leadsto 4 \cdot \left(\color{blue}{\frac{x - z}{y}} + 1\right) \]
              5. Applied rewrites100.0%

                \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x - z}{y}, 4, 4\right)} \]
              6. Taylor expanded in y around 0

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

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

              if -2.00000000000000006e40 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < 2e4

              1. Initial program 99.9%

                \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
              2. Add Preprocessing
              3. Taylor expanded in x around 0

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

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

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

                  \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} + \left(4 \cdot \frac{\frac{3}{4} \cdot y - z}{y} + 1\right) \]
                4. div-subN/A

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

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) + 1\right) \]
                6. *-inversesN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) + 1\right) \]
                7. metadata-evalN/A

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

                  \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(1 + 4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right)\right)} \]
                9. sub-negN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)}\right) \]
                10. distribute-rgt-inN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \color{blue}{\left(\frac{3}{4} \cdot 4 + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)}\right) \]
                11. metadata-evalN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \left(\color{blue}{3} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)\right) \]
                12. associate-+r+N/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(1 + 3\right) + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)} \]
                13. metadata-evalN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \left(\color{blue}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right) \]
                14. distribute-rgt1-inN/A

                  \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right) \cdot 4} \]
                15. distribute-rgt-inN/A

                  \[\leadsto \color{blue}{4 \cdot \left(\frac{x}{y} + \left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right)\right)} \]
                16. associate-+l+N/A

                  \[\leadsto 4 \cdot \color{blue}{\left(\left(\frac{x}{y} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right) + 1\right)} \]
                17. sub-negN/A

                  \[\leadsto 4 \cdot \left(\color{blue}{\left(\frac{x}{y} - \frac{z}{y}\right)} + 1\right) \]
                18. div-subN/A

                  \[\leadsto 4 \cdot \left(\color{blue}{\frac{x - z}{y}} + 1\right) \]
              5. Applied rewrites100.0%

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

                \[\leadsto \mathsf{fma}\left(\frac{x}{y}, 4, 4\right) \]
              7. Step-by-step derivation
                1. Applied rewrites98.6%

                  \[\leadsto \mathsf{fma}\left(\frac{x}{y}, 4, 4\right) \]
              8. Recombined 2 regimes into one program.
              9. Final simplification98.7%

                \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \leq -2 \cdot 10^{+40} \lor \neg \left(\frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \leq 20000\right):\\ \;\;\;\;\left(z - x\right) \cdot \frac{-4}{y}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{y}, 4, 4\right)\\ \end{array} \]
              10. Add Preprocessing

              Alternative 5: 66.2% accurate, 0.4× speedup?

              \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}\\ \mathbf{if}\;t\_0 \leq -4000000000000 \lor \neg \left(t\_0 \leq 20000\right):\\ \;\;\;\;\frac{z}{y} \cdot -4\\ \mathbf{else}:\\ \;\;\;\;4\\ \end{array} \end{array} \]
              (FPCore (x y z)
               :precision binary64
               (let* ((t_0 (/ (* 4.0 (- (+ x (* y 0.75)) z)) y)))
                 (if (or (<= t_0 -4000000000000.0) (not (<= t_0 20000.0)))
                   (* (/ z y) -4.0)
                   4.0)))
              double code(double x, double y, double z) {
              	double t_0 = (4.0 * ((x + (y * 0.75)) - z)) / y;
              	double tmp;
              	if ((t_0 <= -4000000000000.0) || !(t_0 <= 20000.0)) {
              		tmp = (z / y) * -4.0;
              	} else {
              		tmp = 4.0;
              	}
              	return tmp;
              }
              
              real(8) function code(x, y, z)
                  real(8), intent (in) :: x
                  real(8), intent (in) :: y
                  real(8), intent (in) :: z
                  real(8) :: t_0
                  real(8) :: tmp
                  t_0 = (4.0d0 * ((x + (y * 0.75d0)) - z)) / y
                  if ((t_0 <= (-4000000000000.0d0)) .or. (.not. (t_0 <= 20000.0d0))) then
                      tmp = (z / y) * (-4.0d0)
                  else
                      tmp = 4.0d0
                  end if
                  code = tmp
              end function
              
              public static double code(double x, double y, double z) {
              	double t_0 = (4.0 * ((x + (y * 0.75)) - z)) / y;
              	double tmp;
              	if ((t_0 <= -4000000000000.0) || !(t_0 <= 20000.0)) {
              		tmp = (z / y) * -4.0;
              	} else {
              		tmp = 4.0;
              	}
              	return tmp;
              }
              
              def code(x, y, z):
              	t_0 = (4.0 * ((x + (y * 0.75)) - z)) / y
              	tmp = 0
              	if (t_0 <= -4000000000000.0) or not (t_0 <= 20000.0):
              		tmp = (z / y) * -4.0
              	else:
              		tmp = 4.0
              	return tmp
              
              function code(x, y, z)
              	t_0 = Float64(Float64(4.0 * Float64(Float64(x + Float64(y * 0.75)) - z)) / y)
              	tmp = 0.0
              	if ((t_0 <= -4000000000000.0) || !(t_0 <= 20000.0))
              		tmp = Float64(Float64(z / y) * -4.0);
              	else
              		tmp = 4.0;
              	end
              	return tmp
              end
              
              function tmp_2 = code(x, y, z)
              	t_0 = (4.0 * ((x + (y * 0.75)) - z)) / y;
              	tmp = 0.0;
              	if ((t_0 <= -4000000000000.0) || ~((t_0 <= 20000.0)))
              		tmp = (z / y) * -4.0;
              	else
              		tmp = 4.0;
              	end
              	tmp_2 = tmp;
              end
              
              code[x_, y_, z_] := Block[{t$95$0 = N[(N[(4.0 * N[(N[(x + N[(y * 0.75), $MachinePrecision]), $MachinePrecision] - z), $MachinePrecision]), $MachinePrecision] / y), $MachinePrecision]}, If[Or[LessEqual[t$95$0, -4000000000000.0], N[Not[LessEqual[t$95$0, 20000.0]], $MachinePrecision]], N[(N[(z / y), $MachinePrecision] * -4.0), $MachinePrecision], 4.0]]
              
              \begin{array}{l}
              
              \\
              \begin{array}{l}
              t_0 := \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}\\
              \mathbf{if}\;t\_0 \leq -4000000000000 \lor \neg \left(t\_0 \leq 20000\right):\\
              \;\;\;\;\frac{z}{y} \cdot -4\\
              
              \mathbf{else}:\\
              \;\;\;\;4\\
              
              
              \end{array}
              \end{array}
              
              Derivation
              1. Split input into 2 regimes
              2. if (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < -4e12 or 2e4 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y)

                1. Initial program 99.3%

                  \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
                2. Add Preprocessing
                3. Taylor expanded in x around 0

                  \[\leadsto \color{blue}{1 + 4 \cdot \frac{\frac{3}{4} \cdot y - z}{y}} \]
                4. Step-by-step derivation
                  1. div-subN/A

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

                    \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) \]
                  3. *-inversesN/A

                    \[\leadsto 1 + 4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) \]
                  4. metadata-evalN/A

                    \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4}} - \frac{z}{y}\right) \]
                  5. +-commutativeN/A

                    \[\leadsto \color{blue}{4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right) + 1} \]
                  6. sub-negN/A

                    \[\leadsto 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)} + 1 \]
                  7. +-commutativeN/A

                    \[\leadsto 4 \cdot \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + \frac{3}{4}\right)} + 1 \]
                  8. distribute-rgt-inN/A

                    \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4 + \frac{3}{4} \cdot 4\right)} + 1 \]
                  9. *-commutativeN/A

                    \[\leadsto \left(\color{blue}{4 \cdot \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
                  10. *-lft-identityN/A

                    \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\frac{\color{blue}{1 \cdot z}}{y}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                  11. associate-*l/N/A

                    \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{y} \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                  12. distribute-rgt-neg-inN/A

                    \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(\frac{1}{y} \cdot z\right)\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
                  13. associate-*l*N/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\left(4 \cdot \frac{1}{y}\right) \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                  14. *-commutativeN/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{z \cdot \left(4 \cdot \frac{1}{y}\right)}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                  15. metadata-evalN/A

                    \[\leadsto \left(\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{3}\right) + 1 \]
                  16. associate-+l+N/A

                    \[\leadsto \color{blue}{\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \left(3 + 1\right)} \]
                  17. metadata-evalN/A

                    \[\leadsto \left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{4} \]
                5. Applied rewrites54.9%

                  \[\leadsto \color{blue}{\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)} \]
                6. Taylor expanded in y around 0

                  \[\leadsto -4 \cdot \color{blue}{\frac{z}{y}} \]
                7. Step-by-step derivation
                  1. Applied rewrites53.7%

                    \[\leadsto \frac{z}{y} \cdot \color{blue}{-4} \]

                  if -4e12 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < 2e4

                  1. Initial program 99.9%

                    \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
                  2. Add Preprocessing
                  3. Taylor expanded in y around inf

                    \[\leadsto \color{blue}{4} \]
                  4. Step-by-step derivation
                    1. Applied rewrites96.2%

                      \[\leadsto \color{blue}{4} \]
                  5. Recombined 2 regimes into one program.
                  6. Final simplification71.5%

                    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \leq -4000000000000 \lor \neg \left(\frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \leq 20000\right):\\ \;\;\;\;\frac{z}{y} \cdot -4\\ \mathbf{else}:\\ \;\;\;\;4\\ \end{array} \]
                  7. Add Preprocessing

                  Alternative 6: 66.2% accurate, 0.4× speedup?

                  \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}\\ \mathbf{if}\;t\_0 \leq -4000000000000 \lor \neg \left(t\_0 \leq 20000\right):\\ \;\;\;\;z \cdot \frac{-4}{y}\\ \mathbf{else}:\\ \;\;\;\;4\\ \end{array} \end{array} \]
                  (FPCore (x y z)
                   :precision binary64
                   (let* ((t_0 (/ (* 4.0 (- (+ x (* y 0.75)) z)) y)))
                     (if (or (<= t_0 -4000000000000.0) (not (<= t_0 20000.0)))
                       (* z (/ -4.0 y))
                       4.0)))
                  double code(double x, double y, double z) {
                  	double t_0 = (4.0 * ((x + (y * 0.75)) - z)) / y;
                  	double tmp;
                  	if ((t_0 <= -4000000000000.0) || !(t_0 <= 20000.0)) {
                  		tmp = z * (-4.0 / y);
                  	} else {
                  		tmp = 4.0;
                  	}
                  	return tmp;
                  }
                  
                  real(8) function code(x, y, z)
                      real(8), intent (in) :: x
                      real(8), intent (in) :: y
                      real(8), intent (in) :: z
                      real(8) :: t_0
                      real(8) :: tmp
                      t_0 = (4.0d0 * ((x + (y * 0.75d0)) - z)) / y
                      if ((t_0 <= (-4000000000000.0d0)) .or. (.not. (t_0 <= 20000.0d0))) then
                          tmp = z * ((-4.0d0) / y)
                      else
                          tmp = 4.0d0
                      end if
                      code = tmp
                  end function
                  
                  public static double code(double x, double y, double z) {
                  	double t_0 = (4.0 * ((x + (y * 0.75)) - z)) / y;
                  	double tmp;
                  	if ((t_0 <= -4000000000000.0) || !(t_0 <= 20000.0)) {
                  		tmp = z * (-4.0 / y);
                  	} else {
                  		tmp = 4.0;
                  	}
                  	return tmp;
                  }
                  
                  def code(x, y, z):
                  	t_0 = (4.0 * ((x + (y * 0.75)) - z)) / y
                  	tmp = 0
                  	if (t_0 <= -4000000000000.0) or not (t_0 <= 20000.0):
                  		tmp = z * (-4.0 / y)
                  	else:
                  		tmp = 4.0
                  	return tmp
                  
                  function code(x, y, z)
                  	t_0 = Float64(Float64(4.0 * Float64(Float64(x + Float64(y * 0.75)) - z)) / y)
                  	tmp = 0.0
                  	if ((t_0 <= -4000000000000.0) || !(t_0 <= 20000.0))
                  		tmp = Float64(z * Float64(-4.0 / y));
                  	else
                  		tmp = 4.0;
                  	end
                  	return tmp
                  end
                  
                  function tmp_2 = code(x, y, z)
                  	t_0 = (4.0 * ((x + (y * 0.75)) - z)) / y;
                  	tmp = 0.0;
                  	if ((t_0 <= -4000000000000.0) || ~((t_0 <= 20000.0)))
                  		tmp = z * (-4.0 / y);
                  	else
                  		tmp = 4.0;
                  	end
                  	tmp_2 = tmp;
                  end
                  
                  code[x_, y_, z_] := Block[{t$95$0 = N[(N[(4.0 * N[(N[(x + N[(y * 0.75), $MachinePrecision]), $MachinePrecision] - z), $MachinePrecision]), $MachinePrecision] / y), $MachinePrecision]}, If[Or[LessEqual[t$95$0, -4000000000000.0], N[Not[LessEqual[t$95$0, 20000.0]], $MachinePrecision]], N[(z * N[(-4.0 / y), $MachinePrecision]), $MachinePrecision], 4.0]]
                  
                  \begin{array}{l}
                  
                  \\
                  \begin{array}{l}
                  t_0 := \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y}\\
                  \mathbf{if}\;t\_0 \leq -4000000000000 \lor \neg \left(t\_0 \leq 20000\right):\\
                  \;\;\;\;z \cdot \frac{-4}{y}\\
                  
                  \mathbf{else}:\\
                  \;\;\;\;4\\
                  
                  
                  \end{array}
                  \end{array}
                  
                  Derivation
                  1. Split input into 2 regimes
                  2. if (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < -4e12 or 2e4 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y)

                    1. Initial program 99.3%

                      \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
                    2. Add Preprocessing
                    3. Taylor expanded in x around 0

                      \[\leadsto \color{blue}{1 + 4 \cdot \frac{\frac{3}{4} \cdot y - z}{y}} \]
                    4. Step-by-step derivation
                      1. div-subN/A

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

                        \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) \]
                      3. *-inversesN/A

                        \[\leadsto 1 + 4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) \]
                      4. metadata-evalN/A

                        \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4}} - \frac{z}{y}\right) \]
                      5. +-commutativeN/A

                        \[\leadsto \color{blue}{4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right) + 1} \]
                      6. sub-negN/A

                        \[\leadsto 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)} + 1 \]
                      7. +-commutativeN/A

                        \[\leadsto 4 \cdot \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + \frac{3}{4}\right)} + 1 \]
                      8. distribute-rgt-inN/A

                        \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4 + \frac{3}{4} \cdot 4\right)} + 1 \]
                      9. *-commutativeN/A

                        \[\leadsto \left(\color{blue}{4 \cdot \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
                      10. *-lft-identityN/A

                        \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\frac{\color{blue}{1 \cdot z}}{y}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                      11. associate-*l/N/A

                        \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{y} \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                      12. distribute-rgt-neg-inN/A

                        \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(\frac{1}{y} \cdot z\right)\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
                      13. associate-*l*N/A

                        \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\left(4 \cdot \frac{1}{y}\right) \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                      14. *-commutativeN/A

                        \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{z \cdot \left(4 \cdot \frac{1}{y}\right)}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                      15. metadata-evalN/A

                        \[\leadsto \left(\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{3}\right) + 1 \]
                      16. associate-+l+N/A

                        \[\leadsto \color{blue}{\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \left(3 + 1\right)} \]
                      17. metadata-evalN/A

                        \[\leadsto \left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{4} \]
                    5. Applied rewrites54.9%

                      \[\leadsto \color{blue}{\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)} \]
                    6. Taylor expanded in y around 0

                      \[\leadsto -4 \cdot \color{blue}{\frac{z}{y}} \]
                    7. Step-by-step derivation
                      1. Applied rewrites53.7%

                        \[\leadsto \frac{z}{y} \cdot \color{blue}{-4} \]
                      2. Step-by-step derivation
                        1. Applied rewrites53.6%

                          \[\leadsto z \cdot \frac{-4}{\color{blue}{y}} \]

                        if -4e12 < (/.f64 (*.f64 #s(literal 4 binary64) (-.f64 (+.f64 x (*.f64 y #s(literal 3/4 binary64))) z)) y) < 2e4

                        1. Initial program 99.9%

                          \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
                        2. Add Preprocessing
                        3. Taylor expanded in y around inf

                          \[\leadsto \color{blue}{4} \]
                        4. Step-by-step derivation
                          1. Applied rewrites96.2%

                            \[\leadsto \color{blue}{4} \]
                        5. Recombined 2 regimes into one program.
                        6. Final simplification71.4%

                          \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \leq -4000000000000 \lor \neg \left(\frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \leq 20000\right):\\ \;\;\;\;z \cdot \frac{-4}{y}\\ \mathbf{else}:\\ \;\;\;\;4\\ \end{array} \]
                        7. Add Preprocessing

                        Alternative 7: 85.8% accurate, 1.0× speedup?

                        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -2.1 \cdot 10^{+24} \lor \neg \left(x \leq 1.65 \cdot 10^{+99}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{y}, 4, 4\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)\\ \end{array} \end{array} \]
                        (FPCore (x y z)
                         :precision binary64
                         (if (or (<= x -2.1e+24) (not (<= x 1.65e+99)))
                           (fma (/ x y) 4.0 4.0)
                           (fma -4.0 (/ z y) 4.0)))
                        double code(double x, double y, double z) {
                        	double tmp;
                        	if ((x <= -2.1e+24) || !(x <= 1.65e+99)) {
                        		tmp = fma((x / y), 4.0, 4.0);
                        	} else {
                        		tmp = fma(-4.0, (z / y), 4.0);
                        	}
                        	return tmp;
                        }
                        
                        function code(x, y, z)
                        	tmp = 0.0
                        	if ((x <= -2.1e+24) || !(x <= 1.65e+99))
                        		tmp = fma(Float64(x / y), 4.0, 4.0);
                        	else
                        		tmp = fma(-4.0, Float64(z / y), 4.0);
                        	end
                        	return tmp
                        end
                        
                        code[x_, y_, z_] := If[Or[LessEqual[x, -2.1e+24], N[Not[LessEqual[x, 1.65e+99]], $MachinePrecision]], N[(N[(x / y), $MachinePrecision] * 4.0 + 4.0), $MachinePrecision], N[(-4.0 * N[(z / y), $MachinePrecision] + 4.0), $MachinePrecision]]
                        
                        \begin{array}{l}
                        
                        \\
                        \begin{array}{l}
                        \mathbf{if}\;x \leq -2.1 \cdot 10^{+24} \lor \neg \left(x \leq 1.65 \cdot 10^{+99}\right):\\
                        \;\;\;\;\mathsf{fma}\left(\frac{x}{y}, 4, 4\right)\\
                        
                        \mathbf{else}:\\
                        \;\;\;\;\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)\\
                        
                        
                        \end{array}
                        \end{array}
                        
                        Derivation
                        1. Split input into 2 regimes
                        2. if x < -2.1000000000000001e24 or 1.65e99 < x

                          1. Initial program 100.0%

                            \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
                          2. Add Preprocessing
                          3. Taylor expanded in x around 0

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

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

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

                              \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} + \left(4 \cdot \frac{\frac{3}{4} \cdot y - z}{y} + 1\right) \]
                            4. div-subN/A

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

                              \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) + 1\right) \]
                            6. *-inversesN/A

                              \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) + 1\right) \]
                            7. metadata-evalN/A

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

                              \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(1 + 4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right)\right)} \]
                            9. sub-negN/A

                              \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)}\right) \]
                            10. distribute-rgt-inN/A

                              \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \color{blue}{\left(\frac{3}{4} \cdot 4 + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)}\right) \]
                            11. metadata-evalN/A

                              \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \left(\color{blue}{3} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)\right) \]
                            12. associate-+r+N/A

                              \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(1 + 3\right) + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)} \]
                            13. metadata-evalN/A

                              \[\leadsto \frac{x}{y} \cdot 4 + \left(\color{blue}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right) \]
                            14. distribute-rgt1-inN/A

                              \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right) \cdot 4} \]
                            15. distribute-rgt-inN/A

                              \[\leadsto \color{blue}{4 \cdot \left(\frac{x}{y} + \left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right)\right)} \]
                            16. associate-+l+N/A

                              \[\leadsto 4 \cdot \color{blue}{\left(\left(\frac{x}{y} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right) + 1\right)} \]
                            17. sub-negN/A

                              \[\leadsto 4 \cdot \left(\color{blue}{\left(\frac{x}{y} - \frac{z}{y}\right)} + 1\right) \]
                            18. div-subN/A

                              \[\leadsto 4 \cdot \left(\color{blue}{\frac{x - z}{y}} + 1\right) \]
                          5. Applied rewrites100.0%

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

                            \[\leadsto \mathsf{fma}\left(\frac{x}{y}, 4, 4\right) \]
                          7. Step-by-step derivation
                            1. Applied rewrites88.3%

                              \[\leadsto \mathsf{fma}\left(\frac{x}{y}, 4, 4\right) \]

                            if -2.1000000000000001e24 < x < 1.65e99

                            1. Initial program 99.4%

                              \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
                            2. Add Preprocessing
                            3. Taylor expanded in x around 0

                              \[\leadsto \color{blue}{1 + 4 \cdot \frac{\frac{3}{4} \cdot y - z}{y}} \]
                            4. Step-by-step derivation
                              1. div-subN/A

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

                                \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) \]
                              3. *-inversesN/A

                                \[\leadsto 1 + 4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) \]
                              4. metadata-evalN/A

                                \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4}} - \frac{z}{y}\right) \]
                              5. +-commutativeN/A

                                \[\leadsto \color{blue}{4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right) + 1} \]
                              6. sub-negN/A

                                \[\leadsto 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)} + 1 \]
                              7. +-commutativeN/A

                                \[\leadsto 4 \cdot \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + \frac{3}{4}\right)} + 1 \]
                              8. distribute-rgt-inN/A

                                \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4 + \frac{3}{4} \cdot 4\right)} + 1 \]
                              9. *-commutativeN/A

                                \[\leadsto \left(\color{blue}{4 \cdot \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
                              10. *-lft-identityN/A

                                \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\frac{\color{blue}{1 \cdot z}}{y}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                              11. associate-*l/N/A

                                \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{y} \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                              12. distribute-rgt-neg-inN/A

                                \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(\frac{1}{y} \cdot z\right)\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
                              13. associate-*l*N/A

                                \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\left(4 \cdot \frac{1}{y}\right) \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                              14. *-commutativeN/A

                                \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{z \cdot \left(4 \cdot \frac{1}{y}\right)}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                              15. metadata-evalN/A

                                \[\leadsto \left(\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{3}\right) + 1 \]
                              16. associate-+l+N/A

                                \[\leadsto \color{blue}{\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \left(3 + 1\right)} \]
                              17. metadata-evalN/A

                                \[\leadsto \left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{4} \]
                            5. Applied rewrites92.9%

                              \[\leadsto \color{blue}{\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)} \]
                          8. Recombined 2 regimes into one program.
                          9. Final simplification91.2%

                            \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -2.1 \cdot 10^{+24} \lor \neg \left(x \leq 1.65 \cdot 10^{+99}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{y}, 4, 4\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)\\ \end{array} \]
                          10. Add Preprocessing

                          Alternative 8: 81.2% accurate, 1.0× speedup?

                          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;x \leq -4.3 \cdot 10^{+108} \lor \neg \left(x \leq 1.62 \cdot 10^{+143}\right):\\ \;\;\;\;\frac{x}{y} \cdot 4\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)\\ \end{array} \end{array} \]
                          (FPCore (x y z)
                           :precision binary64
                           (if (or (<= x -4.3e+108) (not (<= x 1.62e+143)))
                             (* (/ x y) 4.0)
                             (fma -4.0 (/ z y) 4.0)))
                          double code(double x, double y, double z) {
                          	double tmp;
                          	if ((x <= -4.3e+108) || !(x <= 1.62e+143)) {
                          		tmp = (x / y) * 4.0;
                          	} else {
                          		tmp = fma(-4.0, (z / y), 4.0);
                          	}
                          	return tmp;
                          }
                          
                          function code(x, y, z)
                          	tmp = 0.0
                          	if ((x <= -4.3e+108) || !(x <= 1.62e+143))
                          		tmp = Float64(Float64(x / y) * 4.0);
                          	else
                          		tmp = fma(-4.0, Float64(z / y), 4.0);
                          	end
                          	return tmp
                          end
                          
                          code[x_, y_, z_] := If[Or[LessEqual[x, -4.3e+108], N[Not[LessEqual[x, 1.62e+143]], $MachinePrecision]], N[(N[(x / y), $MachinePrecision] * 4.0), $MachinePrecision], N[(-4.0 * N[(z / y), $MachinePrecision] + 4.0), $MachinePrecision]]
                          
                          \begin{array}{l}
                          
                          \\
                          \begin{array}{l}
                          \mathbf{if}\;x \leq -4.3 \cdot 10^{+108} \lor \neg \left(x \leq 1.62 \cdot 10^{+143}\right):\\
                          \;\;\;\;\frac{x}{y} \cdot 4\\
                          
                          \mathbf{else}:\\
                          \;\;\;\;\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)\\
                          
                          
                          \end{array}
                          \end{array}
                          
                          Derivation
                          1. Split input into 2 regimes
                          2. if x < -4.29999999999999996e108 or 1.62e143 < x

                            1. Initial program 100.0%

                              \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
                            2. Add Preprocessing
                            3. Taylor expanded in x around 0

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

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

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

                                \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} + \left(4 \cdot \frac{\frac{3}{4} \cdot y - z}{y} + 1\right) \]
                              4. div-subN/A

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

                                \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) + 1\right) \]
                              6. *-inversesN/A

                                \[\leadsto \frac{x}{y} \cdot 4 + \left(4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) + 1\right) \]
                              7. metadata-evalN/A

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

                                \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(1 + 4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right)\right)} \]
                              9. sub-negN/A

                                \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)}\right) \]
                              10. distribute-rgt-inN/A

                                \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \color{blue}{\left(\frac{3}{4} \cdot 4 + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)}\right) \]
                              11. metadata-evalN/A

                                \[\leadsto \frac{x}{y} \cdot 4 + \left(1 + \left(\color{blue}{3} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)\right) \]
                              12. associate-+r+N/A

                                \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(1 + 3\right) + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right)} \]
                              13. metadata-evalN/A

                                \[\leadsto \frac{x}{y} \cdot 4 + \left(\color{blue}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4\right) \]
                              14. distribute-rgt1-inN/A

                                \[\leadsto \frac{x}{y} \cdot 4 + \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right) \cdot 4} \]
                              15. distribute-rgt-inN/A

                                \[\leadsto \color{blue}{4 \cdot \left(\frac{x}{y} + \left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + 1\right)\right)} \]
                              16. associate-+l+N/A

                                \[\leadsto 4 \cdot \color{blue}{\left(\left(\frac{x}{y} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right) + 1\right)} \]
                              17. sub-negN/A

                                \[\leadsto 4 \cdot \left(\color{blue}{\left(\frac{x}{y} - \frac{z}{y}\right)} + 1\right) \]
                              18. div-subN/A

                                \[\leadsto 4 \cdot \left(\color{blue}{\frac{x - z}{y}} + 1\right) \]
                            5. Applied rewrites100.0%

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

                              \[\leadsto \color{blue}{4 \cdot \frac{x}{y}} \]
                            7. Step-by-step derivation
                              1. *-commutativeN/A

                                \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} \]
                              2. lower-*.f64N/A

                                \[\leadsto \color{blue}{\frac{x}{y} \cdot 4} \]
                              3. lower-/.f6472.9

                                \[\leadsto \color{blue}{\frac{x}{y}} \cdot 4 \]
                            8. Applied rewrites72.9%

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

                            if -4.29999999999999996e108 < x < 1.62e143

                            1. Initial program 99.4%

                              \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
                            2. Add Preprocessing
                            3. Taylor expanded in x around 0

                              \[\leadsto \color{blue}{1 + 4 \cdot \frac{\frac{3}{4} \cdot y - z}{y}} \]
                            4. Step-by-step derivation
                              1. div-subN/A

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

                                \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4} \cdot \frac{y}{y}} - \frac{z}{y}\right) \]
                              3. *-inversesN/A

                                \[\leadsto 1 + 4 \cdot \left(\frac{3}{4} \cdot \color{blue}{1} - \frac{z}{y}\right) \]
                              4. metadata-evalN/A

                                \[\leadsto 1 + 4 \cdot \left(\color{blue}{\frac{3}{4}} - \frac{z}{y}\right) \]
                              5. +-commutativeN/A

                                \[\leadsto \color{blue}{4 \cdot \left(\frac{3}{4} - \frac{z}{y}\right) + 1} \]
                              6. sub-negN/A

                                \[\leadsto 4 \cdot \color{blue}{\left(\frac{3}{4} + \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)\right)} + 1 \]
                              7. +-commutativeN/A

                                \[\leadsto 4 \cdot \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) + \frac{3}{4}\right)} + 1 \]
                              8. distribute-rgt-inN/A

                                \[\leadsto \color{blue}{\left(\left(\mathsf{neg}\left(\frac{z}{y}\right)\right) \cdot 4 + \frac{3}{4} \cdot 4\right)} + 1 \]
                              9. *-commutativeN/A

                                \[\leadsto \left(\color{blue}{4 \cdot \left(\mathsf{neg}\left(\frac{z}{y}\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
                              10. *-lft-identityN/A

                                \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\frac{\color{blue}{1 \cdot z}}{y}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                              11. associate-*l/N/A

                                \[\leadsto \left(4 \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{y} \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                              12. distribute-rgt-neg-inN/A

                                \[\leadsto \left(\color{blue}{\left(\mathsf{neg}\left(4 \cdot \left(\frac{1}{y} \cdot z\right)\right)\right)} + \frac{3}{4} \cdot 4\right) + 1 \]
                              13. associate-*l*N/A

                                \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{\left(4 \cdot \frac{1}{y}\right) \cdot z}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                              14. *-commutativeN/A

                                \[\leadsto \left(\left(\mathsf{neg}\left(\color{blue}{z \cdot \left(4 \cdot \frac{1}{y}\right)}\right)\right) + \frac{3}{4} \cdot 4\right) + 1 \]
                              15. metadata-evalN/A

                                \[\leadsto \left(\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{3}\right) + 1 \]
                              16. associate-+l+N/A

                                \[\leadsto \color{blue}{\left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \left(3 + 1\right)} \]
                              17. metadata-evalN/A

                                \[\leadsto \left(\mathsf{neg}\left(z \cdot \left(4 \cdot \frac{1}{y}\right)\right)\right) + \color{blue}{4} \]
                            5. Applied rewrites90.1%

                              \[\leadsto \color{blue}{\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)} \]
                          3. Recombined 2 regimes into one program.
                          4. Final simplification85.2%

                            \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -4.3 \cdot 10^{+108} \lor \neg \left(x \leq 1.62 \cdot 10^{+143}\right):\\ \;\;\;\;\frac{x}{y} \cdot 4\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-4, \frac{z}{y}, 4\right)\\ \end{array} \]
                          5. Add Preprocessing

                          Alternative 9: 34.0% accurate, 31.0× speedup?

                          \[\begin{array}{l} \\ 4 \end{array} \]
                          (FPCore (x y z) :precision binary64 4.0)
                          double code(double x, double y, double z) {
                          	return 4.0;
                          }
                          
                          real(8) function code(x, y, z)
                              real(8), intent (in) :: x
                              real(8), intent (in) :: y
                              real(8), intent (in) :: z
                              code = 4.0d0
                          end function
                          
                          public static double code(double x, double y, double z) {
                          	return 4.0;
                          }
                          
                          def code(x, y, z):
                          	return 4.0
                          
                          function code(x, y, z)
                          	return 4.0
                          end
                          
                          function tmp = code(x, y, z)
                          	tmp = 4.0;
                          end
                          
                          code[x_, y_, z_] := 4.0
                          
                          \begin{array}{l}
                          
                          \\
                          4
                          \end{array}
                          
                          Derivation
                          1. Initial program 99.6%

                            \[1 + \frac{4 \cdot \left(\left(x + y \cdot 0.75\right) - z\right)}{y} \]
                          2. Add Preprocessing
                          3. Taylor expanded in y around inf

                            \[\leadsto \color{blue}{4} \]
                          4. Step-by-step derivation
                            1. Applied rewrites42.2%

                              \[\leadsto \color{blue}{4} \]
                            2. Add Preprocessing

                            Reproduce

                            ?
                            herbie shell --seed 2024299 
                            (FPCore (x y z)
                              :name "Data.Array.Repa.Algorithms.ColorRamp:rampColorHotToCold from repa-algorithms-3.4.0.1, A"
                              :precision binary64
                              (+ 1.0 (/ (* 4.0 (- (+ x (* y 0.75)) z)) y)))