Graphics.Rasterific.Shading:$sradialGradientWithFocusShader from Rasterific-0.6.1, B

Percentage Accurate: 91.1% → 94.5%

Time: 6.2s

Alternatives: 9

Speedup: N/A×

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

Specification

Math

\[\begin{array}{l} \\ x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \end{array} \]

FPCore

(FPCore (x y z t) :precision binary64 (- (* x x) (* (* y 4.0) (- (* z z) t))))

C

double code(double x, double y, double z, double t) {
	return (x * x) - ((y * 4.0) * ((z * z) - t));
}

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z, t)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    code = (x * x) - ((y * 4.0d0) * ((z * z) - t))
end function

Java

public static double code(double x, double y, double z, double t) {
	return (x * x) - ((y * 4.0) * ((z * z) - t));
}

Python

def code(x, y, z, t):
	return (x * x) - ((y * 4.0) * ((z * z) - t))

Julia

function code(x, y, z, t)
	return Float64(Float64(x * x) - Float64(Float64(y * 4.0) * Float64(Float64(z * z) - t)))
end

MATLAB

function tmp = code(x, y, z, t)
	tmp = (x * x) - ((y * 4.0) * ((z * z) - t));
end

Wolfram

code[x_, y_, z_, t_] := N[(N[(x * x), $MachinePrecision] - N[(N[(y * 4.0), $MachinePrecision] * N[(N[(z * z), $MachinePrecision] - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Initial Program: 91.1% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \end{array} \]

FPCore

(FPCore (x y z t) :precision binary64 (- (* x x) (* (* y 4.0) (- (* z z) t))))

C

double code(double x, double y, double z, double t) {
	return (x * x) - ((y * 4.0) * ((z * z) - t));
}

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z, t)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    code = (x * x) - ((y * 4.0d0) * ((z * z) - t))
end function

Java

public static double code(double x, double y, double z, double t) {
	return (x * x) - ((y * 4.0) * ((z * z) - t));
}

Python

def code(x, y, z, t):
	return (x * x) - ((y * 4.0) * ((z * z) - t))

Julia

function code(x, y, z, t)
	return Float64(Float64(x * x) - Float64(Float64(y * 4.0) * Float64(Float64(z * z) - t)))
end

MATLAB

function tmp = code(x, y, z, t)
	tmp = (x * x) - ((y * 4.0) * ((z * z) - t));
end

Wolfram

code[x_, y_, z_, t_] := N[(N[(x * x), $MachinePrecision] - N[(N[(y * 4.0), $MachinePrecision] * N[(N[(z * z), $MachinePrecision] - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Alternative 1: 94.5% accurate, N/A× speedup

Math

\[\begin{array}{l} z_m = \left|z\right| \\ \begin{array}{l} t_1 := 1 \cdot \left(-z\_m\right)\\ \mathbf{if}\;z\_m \leq 5 \cdot 10^{+124}:\\ \;\;\;\;\mathsf{fma}\left(-4 \cdot \mathsf{fma}\left(t\_1, t\_1, -1 \cdot t\right), y, x \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot x - \mathsf{fma}\left(\left(\frac{z\_m}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z\_m}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t\\ \end{array} \end{array} \]

FPCore

z_m = (fabs.f64 z)
(FPCore (x y z_m t)
 :precision binary64
 (let* ((t_1 (* 1.0 (- z_m))))
   (if (<= z_m 5e+124)
     (fma (* -4.0 (fma t_1 t_1 (* -1.0 t))) y (* x x))
     (-
      (* x x)
      (*
       (fma (* (* (/ z_m t) -1.0) (* (/ (* -1.0 z_m) 1.0) y)) 4.0 (* y -4.0))
       t)))))

C

z_m = fabs(z);
double code(double x, double y, double z_m, double t) {
	double t_1 = 1.0 * -z_m;
	double tmp;
	if (z_m <= 5e+124) {
		tmp = fma((-4.0 * fma(t_1, t_1, (-1.0 * t))), y, (x * x));
	} else {
		tmp = (x * x) - (fma((((z_m / t) * -1.0) * (((-1.0 * z_m) / 1.0) * y)), 4.0, (y * -4.0)) * t);
	}
	return tmp;
}

Julia

z_m = abs(z)
function code(x, y, z_m, t)
	t_1 = Float64(1.0 * Float64(-z_m))
	tmp = 0.0
	if (z_m <= 5e+124)
		tmp = fma(Float64(-4.0 * fma(t_1, t_1, Float64(-1.0 * t))), y, Float64(x * x));
	else
		tmp = Float64(Float64(x * x) - Float64(fma(Float64(Float64(Float64(z_m / t) * -1.0) * Float64(Float64(Float64(-1.0 * z_m) / 1.0) * y)), 4.0, Float64(y * -4.0)) * t));
	end
	return tmp
end

Wolfram

z_m = N[Abs[z], $MachinePrecision]
code[x_, y_, z$95$m_, t_] := Block[{t$95$1 = N[(1.0 * (-z$95$m)), $MachinePrecision]}, If[LessEqual[z$95$m, 5e+124], N[(N[(-4.0 * N[(t$95$1 * t$95$1 + N[(-1.0 * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * y + N[(x * x), $MachinePrecision]), $MachinePrecision], N[(N[(x * x), $MachinePrecision] - N[(N[(N[(N[(N[(z$95$m / t), $MachinePrecision] * -1.0), $MachinePrecision] * N[(N[(N[(-1.0 * z$95$m), $MachinePrecision] / 1.0), $MachinePrecision] * y), $MachinePrecision]), $MachinePrecision] * 4.0 + N[(y * -4.0), $MachinePrecision]), $MachinePrecision] * t), $MachinePrecision]), $MachinePrecision]]]

Derivation

1. Split input into 2 regimes

2. if z < 4.9999999999999996e124

   1. Initial program 98.1%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. lift-*.f64 N/A

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

      4. lift-*.f64 N/A

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

      5. lift--.f64 N/A

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

      6. lift-*.f64 N/A

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

      7. pow2 N/A

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

      8. *-commutative N/A

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

      9. pow2 N/A

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

      10. associate-*r* N/A

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

      11. fp-cancel-sub-sign-inv N/A

          \[\leadsto \color{blue}{{x}^{2} + \left(\mathsf{neg}\left(4\right)\right) \cdot \left(y \cdot \left({z}^{2} - t\right)\right)} \]

      12. metadata-eval N/A

          \[\leadsto {x}^{2} + \color{blue}{-4} \cdot \left(y \cdot \left({z}^{2} - t\right)\right) \]

      13. +-commutative N/A

          \[\leadsto \color{blue}{-4 \cdot \left(y \cdot \left({z}^{2} - t\right)\right) + {x}^{2}} \]

      14. *-commutative N/A

          \[\leadsto -4 \cdot \color{blue}{\left(\left({z}^{2} - t\right) \cdot y\right)} + {x}^{2} \]

      15. pow2 N/A

          \[\leadsto -4 \cdot \left(\left(\color{blue}{z \cdot z} - t\right) \cdot y\right) + {x}^{2} \]

      16. associate-*r* N/A

          \[\leadsto \color{blue}{\left(-4 \cdot \left(z \cdot z - t\right)\right) \cdot y} + {x}^{2} \]

      17. pow2 N/A

          \[\leadsto \left(-4 \cdot \left(\color{blue}{{z}^{2}} - t\right)\right) \cdot y + {x}^{2} \]

   3. Applied rewrites 99.4%

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

   if 4.9999999999999996e124 < z

   1. Initial program 74.3%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. pow2 N/A

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

      4. *-lft-identity N/A

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

      5. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

      6. fp-cancel-sign-sub-inv N/A

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

      7. +-commutative N/A

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

      8. flip-+ N/A

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

      9. lower-/.f64 N/A

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

   3. Applied rewrites 7.6%

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

   4. Taylor expanded in t around inf

      \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
   5. Step-by-step derivation

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. +-commutative N/A

         \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

      4. *-commutative N/A

         \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

      5. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      6. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      7. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      8. pow2 N/A

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

      9. lift-/.f64 N/A

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

      10. lift-*.f64 N/A

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

      11. *-commutative N/A

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

      12. lower-*.f64 70.9

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

   6. Applied rewrites 70.9%

      \[\leadsto x \cdot x - \color{blue}{\mathsf{fma}\left(y \cdot \frac{z \cdot z}{t}, 4, y \cdot -4\right) \cdot t} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, y \cdot -4\right) \cdot t \]

      4. frac-2neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      5. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      6. distribute-lft-neg-out N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      7. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      8. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{-1 \cdot t}, 4, y \cdot -4\right) \cdot t \]

      9. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{t \cdot -1}, 4, y \cdot -4\right) \cdot t \]

      10. frac-times N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      12. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      13. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      14. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      15. lower-*.f64 76.4

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      16. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      17. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      18. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot \frac{z}{t}\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      19. *-commutative N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      20. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      21. lower-/.f64 76.4

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   8. Applied rewrites 76.4%

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]
   9. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      2. lift-/.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      3. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      4. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      5. lift-/.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      6. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1} \cdot y, 4, y \cdot -4\right) \cdot t \]

      7. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\left(\frac{z}{t} \cdot -1\right) \cdot \frac{z}{-1}\right) \cdot y, 4, y \cdot -4\right) \cdot t \]

      8. associate-*l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      9. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      10. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      12. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      13. frac-2neg N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{\mathsf{neg}\left(-1\right)} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      14. metadata-eval N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      15. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      16. mul-1-neg N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      17. lower-*.f64 82.8

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

   10. Applied rewrites 82.8%

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

Alternative 2: 93.6% accurate, N/A× speedup

Math

\[\begin{array}{l} z_m = \left|z\right| \\ \begin{array}{l} \mathbf{if}\;z\_m \leq 5 \cdot 10^{+124}:\\ \;\;\;\;x \cdot x - \left(y \cdot 4\right) \cdot \left(z\_m \cdot z\_m - t\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot x - \mathsf{fma}\left(\left(\frac{z\_m}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z\_m}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t\\ \end{array} \end{array} \]

FPCore

z_m = (fabs.f64 z)
(FPCore (x y z_m t)
 :precision binary64
 (if (<= z_m 5e+124)
   (- (* x x) (* (* y 4.0) (- (* z_m z_m) t)))
   (-
    (* x x)
    (*
     (fma (* (* (/ z_m t) -1.0) (* (/ (* -1.0 z_m) 1.0) y)) 4.0 (* y -4.0))
     t))))

C

z_m = fabs(z);
double code(double x, double y, double z_m, double t) {
	double tmp;
	if (z_m <= 5e+124) {
		tmp = (x * x) - ((y * 4.0) * ((z_m * z_m) - t));
	} else {
		tmp = (x * x) - (fma((((z_m / t) * -1.0) * (((-1.0 * z_m) / 1.0) * y)), 4.0, (y * -4.0)) * t);
	}
	return tmp;
}

Julia

z_m = abs(z)
function code(x, y, z_m, t)
	tmp = 0.0
	if (z_m <= 5e+124)
		tmp = Float64(Float64(x * x) - Float64(Float64(y * 4.0) * Float64(Float64(z_m * z_m) - t)));
	else
		tmp = Float64(Float64(x * x) - Float64(fma(Float64(Float64(Float64(z_m / t) * -1.0) * Float64(Float64(Float64(-1.0 * z_m) / 1.0) * y)), 4.0, Float64(y * -4.0)) * t));
	end
	return tmp
end

Wolfram

z_m = N[Abs[z], $MachinePrecision]
code[x_, y_, z$95$m_, t_] := If[LessEqual[z$95$m, 5e+124], N[(N[(x * x), $MachinePrecision] - N[(N[(y * 4.0), $MachinePrecision] * N[(N[(z$95$m * z$95$m), $MachinePrecision] - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x * x), $MachinePrecision] - N[(N[(N[(N[(N[(z$95$m / t), $MachinePrecision] * -1.0), $MachinePrecision] * N[(N[(N[(-1.0 * z$95$m), $MachinePrecision] / 1.0), $MachinePrecision] * y), $MachinePrecision]), $MachinePrecision] * 4.0 + N[(y * -4.0), $MachinePrecision]), $MachinePrecision] * t), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if z < 4.9999999999999996e124

   1. Initial program 98.1%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]

   if 4.9999999999999996e124 < z

   1. Initial program 74.3%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. pow2 N/A

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

      4. *-lft-identity N/A

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

      5. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

      6. fp-cancel-sign-sub-inv N/A

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

      7. +-commutative N/A

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

      8. flip-+ N/A

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

      9. lower-/.f64 N/A

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

   3. Applied rewrites 7.6%

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

   4. Taylor expanded in t around inf

      \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
   5. Step-by-step derivation

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. +-commutative N/A

         \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

      4. *-commutative N/A

         \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

      5. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      6. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      7. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      8. pow2 N/A

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

      9. lift-/.f64 N/A

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

      10. lift-*.f64 N/A

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

      11. *-commutative N/A

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

      12. lower-*.f64 70.9

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

   6. Applied rewrites 70.9%

      \[\leadsto x \cdot x - \color{blue}{\mathsf{fma}\left(y \cdot \frac{z \cdot z}{t}, 4, y \cdot -4\right) \cdot t} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, y \cdot -4\right) \cdot t \]

      4. frac-2neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      5. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      6. distribute-lft-neg-out N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      7. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      8. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{-1 \cdot t}, 4, y \cdot -4\right) \cdot t \]

      9. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{t \cdot -1}, 4, y \cdot -4\right) \cdot t \]

      10. frac-times N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      12. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      13. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      14. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      15. lower-*.f64 76.4

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      16. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      17. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      18. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot \frac{z}{t}\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      19. *-commutative N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      20. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      21. lower-/.f64 76.4

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   8. Applied rewrites 76.4%

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]
   9. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      2. lift-/.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      3. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      4. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      5. lift-/.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      6. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1} \cdot y, 4, y \cdot -4\right) \cdot t \]

      7. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\left(\frac{z}{t} \cdot -1\right) \cdot \frac{z}{-1}\right) \cdot y, 4, y \cdot -4\right) \cdot t \]

      8. associate-*l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      9. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      10. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      12. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      13. frac-2neg N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{\mathsf{neg}\left(-1\right)} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      14. metadata-eval N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      15. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      16. mul-1-neg N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      17. lower-*.f64 82.8

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

   10. Applied rewrites 82.8%

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

Alternative 3: 91.1% accurate, N/A× speedup

Math

\[\begin{array}{l} z_m = \left|z\right| \\ \begin{array}{l} \mathbf{if}\;z\_m \leq 1.9 \cdot 10^{+93}:\\ \;\;\;\;x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{z\_m \cdot z\_m}{t}, 1, -1\right) \cdot t\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot x - \mathsf{fma}\left(\left(\frac{z\_m}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z\_m}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t\\ \end{array} \end{array} \]

FPCore

z_m = (fabs.f64 z)
(FPCore (x y z_m t)
 :precision binary64
 (if (<= z_m 1.9e+93)
   (- (* x x) (* (* y 4.0) (* (fma (/ (* z_m z_m) t) 1.0 -1.0) t)))
   (-
    (* x x)
    (*
     (fma (* (* (/ z_m t) -1.0) (* (/ (* -1.0 z_m) 1.0) y)) 4.0 (* y -4.0))
     t))))

C

z_m = fabs(z);
double code(double x, double y, double z_m, double t) {
	double tmp;
	if (z_m <= 1.9e+93) {
		tmp = (x * x) - ((y * 4.0) * (fma(((z_m * z_m) / t), 1.0, -1.0) * t));
	} else {
		tmp = (x * x) - (fma((((z_m / t) * -1.0) * (((-1.0 * z_m) / 1.0) * y)), 4.0, (y * -4.0)) * t);
	}
	return tmp;
}

Julia

z_m = abs(z)
function code(x, y, z_m, t)
	tmp = 0.0
	if (z_m <= 1.9e+93)
		tmp = Float64(Float64(x * x) - Float64(Float64(y * 4.0) * Float64(fma(Float64(Float64(z_m * z_m) / t), 1.0, -1.0) * t)));
	else
		tmp = Float64(Float64(x * x) - Float64(fma(Float64(Float64(Float64(z_m / t) * -1.0) * Float64(Float64(Float64(-1.0 * z_m) / 1.0) * y)), 4.0, Float64(y * -4.0)) * t));
	end
	return tmp
end

Wolfram

z_m = N[Abs[z], $MachinePrecision]
code[x_, y_, z$95$m_, t_] := If[LessEqual[z$95$m, 1.9e+93], N[(N[(x * x), $MachinePrecision] - N[(N[(y * 4.0), $MachinePrecision] * N[(N[(N[(N[(z$95$m * z$95$m), $MachinePrecision] / t), $MachinePrecision] * 1.0 + -1.0), $MachinePrecision] * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x * x), $MachinePrecision] - N[(N[(N[(N[(N[(z$95$m / t), $MachinePrecision] * -1.0), $MachinePrecision] * N[(N[(N[(-1.0 * z$95$m), $MachinePrecision] / 1.0), $MachinePrecision] * y), $MachinePrecision]), $MachinePrecision] * 4.0 + N[(y * -4.0), $MachinePrecision]), $MachinePrecision] * t), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if z < 1.8999999999999999e93

   1. Initial program 98.3%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]

   2. Taylor expanded in t around inf

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

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} - 1 \cdot 1\right) \cdot t\right) \]

      4. fp-cancel-sub-sign-inv N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} + \left(\mathsf{neg}\left(1\right)\right) \cdot 1\right) \cdot t\right) \]

      5. *-rgt-identity N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} \cdot 1 + \left(\mathsf{neg}\left(1\right)\right) \cdot 1\right) \cdot t\right) \]

      6. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} \cdot 1 + -1 \cdot 1\right) \cdot t\right) \]

      7. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} \cdot 1 + -1\right) \cdot t\right) \]

      8. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{{z}^{2}}{t}, 1, -1\right) \cdot t\right) \]

      9. lower-/.f64 N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{{z}^{2}}{t}, 1, -1\right) \cdot t\right) \]

      10. pow2 N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{z \cdot z}{t}, 1, -1\right) \cdot t\right) \]

      11. lift-*.f64 95.8

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{z \cdot z}{t}, 1, -1\right) \cdot t\right) \]

   4. Applied rewrites 95.8%

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

   if 1.8999999999999999e93 < z

   1. Initial program 77.6%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. pow2 N/A

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

      4. *-lft-identity N/A

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

      5. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

      6. fp-cancel-sign-sub-inv N/A

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

      7. +-commutative N/A

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

      8. flip-+ N/A

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

      9. lower-/.f64 N/A

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

   3. Applied rewrites 12.6%

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

   4. Taylor expanded in t around inf

      \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
   5. Step-by-step derivation

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. +-commutative N/A

         \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

      4. *-commutative N/A

         \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

      5. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      6. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      7. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      8. pow2 N/A

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

      9. lift-/.f64 N/A

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

      10. lift-*.f64 N/A

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

      11. *-commutative N/A

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

      12. lower-*.f64 71.4

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

   6. Applied rewrites 71.4%

      \[\leadsto x \cdot x - \color{blue}{\mathsf{fma}\left(y \cdot \frac{z \cdot z}{t}, 4, y \cdot -4\right) \cdot t} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, y \cdot -4\right) \cdot t \]

      4. frac-2neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      5. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      6. distribute-lft-neg-out N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      7. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      8. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{-1 \cdot t}, 4, y \cdot -4\right) \cdot t \]

      9. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{t \cdot -1}, 4, y \cdot -4\right) \cdot t \]

      10. frac-times N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      12. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      13. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      14. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      15. lower-*.f64 76.0

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      16. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      17. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      18. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot \frac{z}{t}\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      19. *-commutative N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      20. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      21. lower-/.f64 76.0

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   8. Applied rewrites 76.0%

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]
   9. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      2. lift-/.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      3. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      4. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      5. lift-/.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      6. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1} \cdot y, 4, y \cdot -4\right) \cdot t \]

      7. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\left(\frac{z}{t} \cdot -1\right) \cdot \frac{z}{-1}\right) \cdot y, 4, y \cdot -4\right) \cdot t \]

      8. associate-*l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      9. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      10. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      12. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      13. frac-2neg N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{\mathsf{neg}\left(-1\right)} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      14. metadata-eval N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      15. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      16. mul-1-neg N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      17. lower-*.f64 82.2

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

   10. Applied rewrites 82.2%

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

Alternative 4: 91.1% accurate, N/A× speedup

Math

\[\begin{array}{l} z_m = \left|z\right| \\ \begin{array}{l} \mathbf{if}\;z\_m \leq 1.9 \cdot 10^{+93}:\\ \;\;\;\;x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{-1 \cdot z\_m}{t}, \frac{z\_m}{-1}, -1\right) \cdot t\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot x - \mathsf{fma}\left(\left(\frac{z\_m}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z\_m}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t\\ \end{array} \end{array} \]

FPCore

z_m = (fabs.f64 z)
(FPCore (x y z_m t)
 :precision binary64
 (if (<= z_m 1.9e+93)
   (- (* x x) (* (* y 4.0) (* (fma (/ (* -1.0 z_m) t) (/ z_m -1.0) -1.0) t)))
   (-
    (* x x)
    (*
     (fma (* (* (/ z_m t) -1.0) (* (/ (* -1.0 z_m) 1.0) y)) 4.0 (* y -4.0))
     t))))

C

z_m = fabs(z);
double code(double x, double y, double z_m, double t) {
	double tmp;
	if (z_m <= 1.9e+93) {
		tmp = (x * x) - ((y * 4.0) * (fma(((-1.0 * z_m) / t), (z_m / -1.0), -1.0) * t));
	} else {
		tmp = (x * x) - (fma((((z_m / t) * -1.0) * (((-1.0 * z_m) / 1.0) * y)), 4.0, (y * -4.0)) * t);
	}
	return tmp;
}

Julia

z_m = abs(z)
function code(x, y, z_m, t)
	tmp = 0.0
	if (z_m <= 1.9e+93)
		tmp = Float64(Float64(x * x) - Float64(Float64(y * 4.0) * Float64(fma(Float64(Float64(-1.0 * z_m) / t), Float64(z_m / -1.0), -1.0) * t)));
	else
		tmp = Float64(Float64(x * x) - Float64(fma(Float64(Float64(Float64(z_m / t) * -1.0) * Float64(Float64(Float64(-1.0 * z_m) / 1.0) * y)), 4.0, Float64(y * -4.0)) * t));
	end
	return tmp
end

Wolfram

z_m = N[Abs[z], $MachinePrecision]
code[x_, y_, z$95$m_, t_] := If[LessEqual[z$95$m, 1.9e+93], N[(N[(x * x), $MachinePrecision] - N[(N[(y * 4.0), $MachinePrecision] * N[(N[(N[(N[(-1.0 * z$95$m), $MachinePrecision] / t), $MachinePrecision] * N[(z$95$m / -1.0), $MachinePrecision] + -1.0), $MachinePrecision] * t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x * x), $MachinePrecision] - N[(N[(N[(N[(N[(z$95$m / t), $MachinePrecision] * -1.0), $MachinePrecision] * N[(N[(N[(-1.0 * z$95$m), $MachinePrecision] / 1.0), $MachinePrecision] * y), $MachinePrecision]), $MachinePrecision] * 4.0 + N[(y * -4.0), $MachinePrecision]), $MachinePrecision] * t), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if z < 1.8999999999999999e93

   1. Initial program 98.3%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]

   2. Taylor expanded in t around inf

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

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} - 1 \cdot 1\right) \cdot t\right) \]

      4. fp-cancel-sub-sign-inv N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} + \left(\mathsf{neg}\left(1\right)\right) \cdot 1\right) \cdot t\right) \]

      5. *-rgt-identity N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} \cdot 1 + \left(\mathsf{neg}\left(1\right)\right) \cdot 1\right) \cdot t\right) \]

      6. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} \cdot 1 + -1 \cdot 1\right) \cdot t\right) \]

      7. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} \cdot 1 + -1\right) \cdot t\right) \]

      8. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{{z}^{2}}{t}, 1, -1\right) \cdot t\right) \]

      9. lower-/.f64 N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{{z}^{2}}{t}, 1, -1\right) \cdot t\right) \]

      10. pow2 N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{z \cdot z}{t}, 1, -1\right) \cdot t\right) \]

      11. lift-*.f64 95.8

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{z \cdot z}{t}, 1, -1\right) \cdot t\right) \]

   4. Applied rewrites 95.8%

      \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \color{blue}{\left(\mathsf{fma}\left(\frac{z \cdot z}{t}, 1, -1\right) \cdot t\right)} \]
   5. Step-by-step derivation

      1. lift-fma.f64 N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{z \cdot z}{t} \cdot 1 + -1\right) \cdot t\right) \]

      2. lift-*.f64 N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{z \cdot z}{t} \cdot 1 + -1\right) \cdot t\right) \]

      3. lift-/.f64 N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{z \cdot z}{t} \cdot 1 + -1\right) \cdot t\right) \]

      4. *-rgt-identity N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{z \cdot z}{t} + -1\right) \cdot t\right) \]

      5. pow2 N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{{z}^{2}}{t} + -1\right) \cdot t\right) \]

      6. frac-2neg N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)} + -1\right) \cdot t\right) \]

      7. pow2 N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)} + -1\right) \cdot t\right) \]

      8. distribute-lft-neg-out N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)} + -1\right) \cdot t\right) \]

      9. *-lft-identity N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{\left(1 \cdot \left(\mathsf{neg}\left(z\right)\right)\right) \cdot z}{\mathsf{neg}\left(t\right)} + -1\right) \cdot t\right) \]

      10. lift-*.f64 N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{\left(1 \cdot \left(\mathsf{neg}\left(z\right)\right)\right) \cdot z}{\mathsf{neg}\left(t\right)} + -1\right) \cdot t\right) \]

      11. lift-neg.f64 N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{\left(1 \cdot \left(-z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)} + -1\right) \cdot t\right) \]

      12. mul-1-neg N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{\left(1 \cdot \left(-z\right)\right) \cdot z}{-1 \cdot t} + -1\right) \cdot t\right) \]

      13. *-commutative N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{\left(1 \cdot \left(-z\right)\right) \cdot z}{t \cdot -1} + -1\right) \cdot t\right) \]

      14. times-frac N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\left(\frac{1 \cdot \left(-z\right)}{t} \cdot \frac{z}{-1} + -1\right) \cdot t\right) \]

      15. lower-fma.f64 N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{1 \cdot \left(-z\right)}{t}, \frac{z}{-1}, -1\right) \cdot t\right) \]

      16. lower-/.f64 N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{1 \cdot \left(-z\right)}{t}, \frac{z}{-1}, -1\right) \cdot t\right) \]

      17. lift-neg.f64 N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{1 \cdot \left(\mathsf{neg}\left(z\right)\right)}{t}, \frac{z}{-1}, -1\right) \cdot t\right) \]

      18. lift-*.f64 N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{1 \cdot \left(\mathsf{neg}\left(z\right)\right)}{t}, \frac{z}{-1}, -1\right) \cdot t\right) \]

      19. *-lft-identity N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{\mathsf{neg}\left(z\right)}{t}, \frac{z}{-1}, -1\right) \cdot t\right) \]

      20. mul-1-neg N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{-1 \cdot z}{t}, \frac{z}{-1}, -1\right) \cdot t\right) \]

      21. lower-*.f64 N/A

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{-1 \cdot z}{t}, \frac{z}{-1}, -1\right) \cdot t\right) \]

      22. lower-/.f64 95.8

          \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{-1 \cdot z}{t}, \frac{z}{-1}, -1\right) \cdot t\right) \]

   6. Applied rewrites 95.8%

      \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left(\mathsf{fma}\left(\frac{-1 \cdot z}{t}, \frac{z}{-1}, -1\right) \cdot t\right) \]

   if 1.8999999999999999e93 < z

   1. Initial program 77.6%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. pow2 N/A

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

      4. *-lft-identity N/A

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

      5. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

      6. fp-cancel-sign-sub-inv N/A

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

      7. +-commutative N/A

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

      8. flip-+ N/A

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

      9. lower-/.f64 N/A

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

   3. Applied rewrites 12.6%

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

   4. Taylor expanded in t around inf

      \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
   5. Step-by-step derivation

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. +-commutative N/A

         \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

      4. *-commutative N/A

         \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

      5. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      6. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      7. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      8. pow2 N/A

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

      9. lift-/.f64 N/A

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

      10. lift-*.f64 N/A

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

      11. *-commutative N/A

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

      12. lower-*.f64 71.4

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

   6. Applied rewrites 71.4%

      \[\leadsto x \cdot x - \color{blue}{\mathsf{fma}\left(y \cdot \frac{z \cdot z}{t}, 4, y \cdot -4\right) \cdot t} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, y \cdot -4\right) \cdot t \]

      4. frac-2neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      5. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      6. distribute-lft-neg-out N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      7. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      8. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{-1 \cdot t}, 4, y \cdot -4\right) \cdot t \]

      9. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{t \cdot -1}, 4, y \cdot -4\right) \cdot t \]

      10. frac-times N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      12. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      13. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      14. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      15. lower-*.f64 76.0

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      16. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      17. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      18. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot \frac{z}{t}\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      19. *-commutative N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      20. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      21. lower-/.f64 76.0

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   8. Applied rewrites 76.0%

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]
   9. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      2. lift-/.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      3. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      4. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      5. lift-/.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      6. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1} \cdot y, 4, y \cdot -4\right) \cdot t \]

      7. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\left(\frac{z}{t} \cdot -1\right) \cdot \frac{z}{-1}\right) \cdot y, 4, y \cdot -4\right) \cdot t \]

      8. associate-*l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      9. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      10. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      12. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      13. frac-2neg N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{\mathsf{neg}\left(-1\right)} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      14. metadata-eval N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      15. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      16. mul-1-neg N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      17. lower-*.f64 82.2

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

   10. Applied rewrites 82.2%

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

Alternative 5: 90.4% accurate, N/A× speedup

Math

\[\begin{array}{l} z_m = \left|z\right| \\ \begin{array}{l} \mathbf{if}\;z\_m \cdot z\_m - t \leq 10^{+186}:\\ \;\;\;\;x \cdot x - \left(\left(-1 \cdot y\right) \cdot t\right) \cdot \mathsf{fma}\left(\frac{z\_m}{t} \cdot z\_m, -4, 4\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot x - \mathsf{fma}\left(\left(\frac{z\_m}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z\_m}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t\\ \end{array} \end{array} \]

FPCore

z_m = (fabs.f64 z)
(FPCore (x y z_m t)
 :precision binary64
 (if (<= (- (* z_m z_m) t) 1e+186)
   (- (* x x) (* (* (* -1.0 y) t) (fma (* (/ z_m t) z_m) -4.0 4.0)))
   (-
    (* x x)
    (*
     (fma (* (* (/ z_m t) -1.0) (* (/ (* -1.0 z_m) 1.0) y)) 4.0 (* y -4.0))
     t))))

C

z_m = fabs(z);
double code(double x, double y, double z_m, double t) {
	double tmp;
	if (((z_m * z_m) - t) <= 1e+186) {
		tmp = (x * x) - (((-1.0 * y) * t) * fma(((z_m / t) * z_m), -4.0, 4.0));
	} else {
		tmp = (x * x) - (fma((((z_m / t) * -1.0) * (((-1.0 * z_m) / 1.0) * y)), 4.0, (y * -4.0)) * t);
	}
	return tmp;
}

Julia

z_m = abs(z)
function code(x, y, z_m, t)
	tmp = 0.0
	if (Float64(Float64(z_m * z_m) - t) <= 1e+186)
		tmp = Float64(Float64(x * x) - Float64(Float64(Float64(-1.0 * y) * t) * fma(Float64(Float64(z_m / t) * z_m), -4.0, 4.0)));
	else
		tmp = Float64(Float64(x * x) - Float64(fma(Float64(Float64(Float64(z_m / t) * -1.0) * Float64(Float64(Float64(-1.0 * z_m) / 1.0) * y)), 4.0, Float64(y * -4.0)) * t));
	end
	return tmp
end

Wolfram

z_m = N[Abs[z], $MachinePrecision]
code[x_, y_, z$95$m_, t_] := If[LessEqual[N[(N[(z$95$m * z$95$m), $MachinePrecision] - t), $MachinePrecision], 1e+186], N[(N[(x * x), $MachinePrecision] - N[(N[(N[(-1.0 * y), $MachinePrecision] * t), $MachinePrecision] * N[(N[(N[(z$95$m / t), $MachinePrecision] * z$95$m), $MachinePrecision] * -4.0 + 4.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x * x), $MachinePrecision] - N[(N[(N[(N[(N[(z$95$m / t), $MachinePrecision] * -1.0), $MachinePrecision] * N[(N[(N[(-1.0 * z$95$m), $MachinePrecision] / 1.0), $MachinePrecision] * y), $MachinePrecision]), $MachinePrecision] * 4.0 + N[(y * -4.0), $MachinePrecision]), $MachinePrecision] * t), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if (-.f64 (*.f64 z z) t) < 9.9999999999999998e185

   1. Initial program 98.5%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. pow2 N/A

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

      4. *-lft-identity N/A

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

      5. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

      6. fp-cancel-sign-sub-inv N/A

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

      7. +-commutative N/A

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

      8. flip-+ N/A

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

      9. lower-/.f64 N/A

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

   3. Applied rewrites 82.7%

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

   4. Taylor expanded in t around inf

      \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
   5. Step-by-step derivation

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. +-commutative N/A

         \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

      4. *-commutative N/A

         \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

      5. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      6. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      7. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      8. pow2 N/A

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

      9. lift-/.f64 N/A

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

      10. lift-*.f64 N/A

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

      11. *-commutative N/A

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

      12. lower-*.f64 93.0

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

   6. Applied rewrites 93.0%

      \[\leadsto x \cdot x - \color{blue}{\mathsf{fma}\left(y \cdot \frac{z \cdot z}{t}, 4, y \cdot -4\right) \cdot t} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, y \cdot -4\right) \cdot t \]

      4. frac-2neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      5. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      6. distribute-lft-neg-out N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      7. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      8. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{-1 \cdot t}, 4, y \cdot -4\right) \cdot t \]

      9. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{t \cdot -1}, 4, y \cdot -4\right) \cdot t \]

      10. frac-times N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      12. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      13. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      14. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      15. lower-*.f64 93.0

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      16. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      17. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      18. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot \frac{z}{t}\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      19. *-commutative N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      20. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      21. lower-/.f64 93.0

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   8. Applied rewrites 93.0%

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   10. Applied rewrites 94.5%

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

   if 9.9999999999999998e185 < (-.f64 (*.f64 z z) t)

   1. Initial program 80.1%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. pow2 N/A

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

      4. *-lft-identity N/A

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

      5. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

      6. fp-cancel-sign-sub-inv N/A

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

      7. +-commutative N/A

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

      8. flip-+ N/A

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

      9. lower-/.f64 N/A

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

   3. Applied rewrites 17.4%

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

   4. Taylor expanded in t around inf

      \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
   5. Step-by-step derivation

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. +-commutative N/A

         \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

      4. *-commutative N/A

         \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

      5. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      6. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      7. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      8. pow2 N/A

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

      9. lift-/.f64 N/A

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

      10. lift-*.f64 N/A

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

      11. *-commutative N/A

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

      12. lower-*.f64 74.6

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

   6. Applied rewrites 74.6%

      \[\leadsto x \cdot x - \color{blue}{\mathsf{fma}\left(y \cdot \frac{z \cdot z}{t}, 4, y \cdot -4\right) \cdot t} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, y \cdot -4\right) \cdot t \]

      4. frac-2neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      5. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      6. distribute-lft-neg-out N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      7. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      8. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{-1 \cdot t}, 4, y \cdot -4\right) \cdot t \]

      9. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{t \cdot -1}, 4, y \cdot -4\right) \cdot t \]

      10. frac-times N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      12. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      13. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      14. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      15. lower-*.f64 78.6

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      16. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      17. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      18. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot \frac{z}{t}\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      19. *-commutative N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      20. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      21. lower-/.f64 78.6

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   8. Applied rewrites 78.6%

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]
   9. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      2. lift-/.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      3. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      4. lift-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      5. lift-/.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      6. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1} \cdot y, 4, y \cdot -4\right) \cdot t \]

      7. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\left(\frac{z}{t} \cdot -1\right) \cdot \frac{z}{-1}\right) \cdot y, 4, y \cdot -4\right) \cdot t \]

      8. associate-*l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      9. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      10. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      12. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{z}{-1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      13. frac-2neg N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{\mathsf{neg}\left(-1\right)} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      14. metadata-eval N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      15. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{\mathsf{neg}\left(z\right)}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      16. mul-1-neg N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

      17. lower-*.f64 84.2

          \[\leadsto x \cdot x - \mathsf{fma}\left(\left(\frac{z}{t} \cdot -1\right) \cdot \left(\frac{-1 \cdot z}{1} \cdot y\right), 4, y \cdot -4\right) \cdot t \]

   10. Applied rewrites 84.2%

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

Alternative 6: 88.2% accurate, N/A× speedup

Math

\[\begin{array}{l} z_m = \left|z\right| \\ \begin{array}{l} \mathbf{if}\;z\_m \cdot z\_m - t \leq 10^{+247}:\\ \;\;\;\;x \cdot x - \left(\left(-1 \cdot y\right) \cdot t\right) \cdot \mathsf{fma}\left(\frac{z\_m}{t} \cdot z\_m, -4, 4\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z\_m}{t} \cdot -1\right) \cdot z\_m}{-1}, 4, y \cdot -4\right) \cdot t\\ \end{array} \end{array} \]

FPCore

z_m = (fabs.f64 z)
(FPCore (x y z_m t)
 :precision binary64
 (if (<= (- (* z_m z_m) t) 1e+247)
   (- (* x x) (* (* (* -1.0 y) t) (fma (* (/ z_m t) z_m) -4.0 4.0)))
   (-
    (* x x)
    (* (fma (* y (/ (* (* (/ z_m t) -1.0) z_m) -1.0)) 4.0 (* y -4.0)) t))))

C

z_m = fabs(z);
double code(double x, double y, double z_m, double t) {
	double tmp;
	if (((z_m * z_m) - t) <= 1e+247) {
		tmp = (x * x) - (((-1.0 * y) * t) * fma(((z_m / t) * z_m), -4.0, 4.0));
	} else {
		tmp = (x * x) - (fma((y * ((((z_m / t) * -1.0) * z_m) / -1.0)), 4.0, (y * -4.0)) * t);
	}
	return tmp;
}

Julia

z_m = abs(z)
function code(x, y, z_m, t)
	tmp = 0.0
	if (Float64(Float64(z_m * z_m) - t) <= 1e+247)
		tmp = Float64(Float64(x * x) - Float64(Float64(Float64(-1.0 * y) * t) * fma(Float64(Float64(z_m / t) * z_m), -4.0, 4.0)));
	else
		tmp = Float64(Float64(x * x) - Float64(fma(Float64(y * Float64(Float64(Float64(Float64(z_m / t) * -1.0) * z_m) / -1.0)), 4.0, Float64(y * -4.0)) * t));
	end
	return tmp
end

Wolfram

z_m = N[Abs[z], $MachinePrecision]
code[x_, y_, z$95$m_, t_] := If[LessEqual[N[(N[(z$95$m * z$95$m), $MachinePrecision] - t), $MachinePrecision], 1e+247], N[(N[(x * x), $MachinePrecision] - N[(N[(N[(-1.0 * y), $MachinePrecision] * t), $MachinePrecision] * N[(N[(N[(z$95$m / t), $MachinePrecision] * z$95$m), $MachinePrecision] * -4.0 + 4.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x * x), $MachinePrecision] - N[(N[(N[(y * N[(N[(N[(N[(z$95$m / t), $MachinePrecision] * -1.0), $MachinePrecision] * z$95$m), $MachinePrecision] / -1.0), $MachinePrecision]), $MachinePrecision] * 4.0 + N[(y * -4.0), $MachinePrecision]), $MachinePrecision] * t), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if (-.f64 (*.f64 z z) t) < 9.99999999999999952e246

   1. Initial program 98.2%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. pow2 N/A

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

      4. *-lft-identity N/A

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

      5. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

      6. fp-cancel-sign-sub-inv N/A

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

      7. +-commutative N/A

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

      8. flip-+ N/A

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

      9. lower-/.f64 N/A

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

   3. Applied rewrites 78.3%

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

   4. Taylor expanded in t around inf

      \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
   5. Step-by-step derivation

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. +-commutative N/A

         \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

      4. *-commutative N/A

         \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

      5. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      6. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      7. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      8. pow2 N/A

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

      9. lift-/.f64 N/A

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

      10. lift-*.f64 N/A

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

      11. *-commutative N/A

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

      12. lower-*.f64 91.7

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

   6. Applied rewrites 91.7%

      \[\leadsto x \cdot x - \color{blue}{\mathsf{fma}\left(y \cdot \frac{z \cdot z}{t}, 4, y \cdot -4\right) \cdot t} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, y \cdot -4\right) \cdot t \]

      4. frac-2neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      5. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      6. distribute-lft-neg-out N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      7. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      8. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{-1 \cdot t}, 4, y \cdot -4\right) \cdot t \]

      9. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{t \cdot -1}, 4, y \cdot -4\right) \cdot t \]

      10. frac-times N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      12. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      13. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      14. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      15. lower-*.f64 91.7

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      16. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      17. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      18. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot \frac{z}{t}\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      19. *-commutative N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      20. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      21. lower-/.f64 91.7

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   8. Applied rewrites 91.7%

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   10. Applied rewrites 93.0%

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

   if 9.99999999999999952e246 < (-.f64 (*.f64 z z) t)

   1. Initial program 76.4%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. pow2 N/A

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

      4. *-lft-identity N/A

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

      5. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

      6. fp-cancel-sign-sub-inv N/A

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

      7. +-commutative N/A

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

      8. flip-+ N/A

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

      9. lower-/.f64 N/A

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

   3. Applied rewrites 11.9%

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

   4. Taylor expanded in t around inf

      \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
   5. Step-by-step derivation

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. +-commutative N/A

         \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

      4. *-commutative N/A

         \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

      5. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      6. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      7. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      8. pow2 N/A

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

      9. lift-/.f64 N/A

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

      10. lift-*.f64 N/A

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

      11. *-commutative N/A

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

      12. lower-*.f64 73.2

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

   6. Applied rewrites 73.2%

      \[\leadsto x \cdot x - \color{blue}{\mathsf{fma}\left(y \cdot \frac{z \cdot z}{t}, 4, y \cdot -4\right) \cdot t} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, y \cdot -4\right) \cdot t \]

      4. frac-2neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      5. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      6. distribute-lft-neg-out N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      7. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      8. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{-1 \cdot t}, 4, y \cdot -4\right) \cdot t \]

      9. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{t \cdot -1}, 4, y \cdot -4\right) \cdot t \]

      10. frac-times N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      12. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      13. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      14. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      15. lower-*.f64 78.1

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      16. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      17. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      18. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot \frac{z}{t}\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      19. *-commutative N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      20. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      21. lower-/.f64 78.1

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   8. Applied rewrites 78.1%

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

Alternative 7: 87.4% accurate, N/A× speedup

Math

\[\begin{array}{l} z_m = \left|z\right| \\ \begin{array}{l} \mathbf{if}\;z\_m \leq 3 \cdot 10^{+265}:\\ \;\;\;\;x \cdot x - \left(\left(-1 \cdot y\right) \cdot t\right) \cdot \mathsf{fma}\left(\frac{z\_m}{t} \cdot z\_m, -4, 4\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot x - \mathsf{fma}\left(y \cdot \frac{z\_m \cdot z\_m}{t}, 4, y \cdot -4\right) \cdot t\\ \end{array} \end{array} \]

FPCore

z_m = (fabs.f64 z)
(FPCore (x y z_m t)
 :precision binary64
 (if (<= z_m 3e+265)
   (- (* x x) (* (* (* -1.0 y) t) (fma (* (/ z_m t) z_m) -4.0 4.0)))
   (- (* x x) (* (fma (* y (/ (* z_m z_m) t)) 4.0 (* y -4.0)) t))))

C

z_m = fabs(z);
double code(double x, double y, double z_m, double t) {
	double tmp;
	if (z_m <= 3e+265) {
		tmp = (x * x) - (((-1.0 * y) * t) * fma(((z_m / t) * z_m), -4.0, 4.0));
	} else {
		tmp = (x * x) - (fma((y * ((z_m * z_m) / t)), 4.0, (y * -4.0)) * t);
	}
	return tmp;
}

Julia

z_m = abs(z)
function code(x, y, z_m, t)
	tmp = 0.0
	if (z_m <= 3e+265)
		tmp = Float64(Float64(x * x) - Float64(Float64(Float64(-1.0 * y) * t) * fma(Float64(Float64(z_m / t) * z_m), -4.0, 4.0)));
	else
		tmp = Float64(Float64(x * x) - Float64(fma(Float64(y * Float64(Float64(z_m * z_m) / t)), 4.0, Float64(y * -4.0)) * t));
	end
	return tmp
end

Wolfram

z_m = N[Abs[z], $MachinePrecision]
code[x_, y_, z$95$m_, t_] := If[LessEqual[z$95$m, 3e+265], N[(N[(x * x), $MachinePrecision] - N[(N[(N[(-1.0 * y), $MachinePrecision] * t), $MachinePrecision] * N[(N[(N[(z$95$m / t), $MachinePrecision] * z$95$m), $MachinePrecision] * -4.0 + 4.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x * x), $MachinePrecision] - N[(N[(N[(y * N[(N[(z$95$m * z$95$m), $MachinePrecision] / t), $MachinePrecision]), $MachinePrecision] * 4.0 + N[(y * -4.0), $MachinePrecision]), $MachinePrecision] * t), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if z < 3.00000000000000002e265

   1. Initial program 91.7%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. pow2 N/A

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

      4. *-lft-identity N/A

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

      5. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

      6. fp-cancel-sign-sub-inv N/A

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

      7. +-commutative N/A

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

      8. flip-+ N/A

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

      9. lower-/.f64 N/A

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

   3. Applied rewrites 61.0%

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

   4. Taylor expanded in t around inf

      \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
   5. Step-by-step derivation

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. +-commutative N/A

         \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

      4. *-commutative N/A

         \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

      5. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      6. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      7. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      8. pow2 N/A

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

      9. lift-/.f64 N/A

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

      10. lift-*.f64 N/A

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

      11. *-commutative N/A

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

      12. lower-*.f64 85.8

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

   6. Applied rewrites 85.8%

      \[\leadsto x \cdot x - \color{blue}{\mathsf{fma}\left(y \cdot \frac{z \cdot z}{t}, 4, y \cdot -4\right) \cdot t} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. lift-/.f64 N/A

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

      3. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, y \cdot -4\right) \cdot t \]

      4. frac-2neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      5. pow2 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      6. distribute-lft-neg-out N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      7. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

      8. mul-1-neg N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{-1 \cdot t}, 4, y \cdot -4\right) \cdot t \]

      9. *-commutative N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{t \cdot -1}, 4, y \cdot -4\right) \cdot t \]

      10. frac-times N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      11. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      12. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

      13. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      14. lower-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      15. lower-*.f64 87.5

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      16. lift-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      17. lift-/.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      18. associate-*r/ N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot \frac{z}{t}\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      19. *-commutative N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      20. lower-*.f64 N/A

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

      21. lower-/.f64 87.5

          \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   8. Applied rewrites 87.5%

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   10. Applied rewrites 87.7%

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

   if 3.00000000000000002e265 < z

   1. Initial program 84.0%

      \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
   2. Step-by-step derivation

      1. lift--.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. pow2 N/A

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

      4. *-lft-identity N/A

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

      5. metadata-eval N/A

         \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

      6. fp-cancel-sign-sub-inv N/A

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

      7. +-commutative N/A

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

      8. flip-+ N/A

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

      9. lower-/.f64 N/A

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

   3. Applied rewrites 0.0%

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

   4. Taylor expanded in t around inf

      \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
   5. Step-by-step derivation

      1. *-commutative N/A

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

      2. lower-*.f64 N/A

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

      3. +-commutative N/A

         \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

      4. *-commutative N/A

         \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

      5. lower-fma.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      6. associate-/l* N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      7. lower-*.f64 N/A

         \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

      8. pow2 N/A

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

      9. lift-/.f64 N/A

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

      10. lift-*.f64 N/A

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

      11. *-commutative N/A

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

      12. lower-*.f64 83.9

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

   6. Applied rewrites 83.9%

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

Alternative 8: 86.9% accurate, N/A× speedup

Math

\[\begin{array}{l} z_m = \left|z\right| \\ x \cdot x - \left(\left(-1 \cdot y\right) \cdot t\right) \cdot \mathsf{fma}\left(\frac{z\_m}{t} \cdot z\_m, -4, 4\right) \end{array} \]

FPCore

z_m = (fabs.f64 z)
(FPCore (x y z_m t)
 :precision binary64
 (- (* x x) (* (* (* -1.0 y) t) (fma (* (/ z_m t) z_m) -4.0 4.0))))

C

z_m = fabs(z);
double code(double x, double y, double z_m, double t) {
	return (x * x) - (((-1.0 * y) * t) * fma(((z_m / t) * z_m), -4.0, 4.0));
}

Julia

z_m = abs(z)
function code(x, y, z_m, t)
	return Float64(Float64(x * x) - Float64(Float64(Float64(-1.0 * y) * t) * fma(Float64(Float64(z_m / t) * z_m), -4.0, 4.0)))
end

Wolfram

z_m = N[Abs[z], $MachinePrecision]
code[x_, y_, z$95$m_, t_] := N[(N[(x * x), $MachinePrecision] - N[(N[(N[(-1.0 * y), $MachinePrecision] * t), $MachinePrecision] * N[(N[(N[(z$95$m / t), $MachinePrecision] * z$95$m), $MachinePrecision] * -4.0 + 4.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 91.1%

   \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]
2. Step-by-step derivation

   1. lift--.f64 N/A

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

   2. lift-*.f64 N/A

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

   3. pow2 N/A

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

   4. *-lft-identity N/A

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

   5. metadata-eval N/A

      \[\leadsto x \cdot x - \left(y \cdot 4\right) \cdot \left({z}^{2} - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot t\right) \]

   6. fp-cancel-sign-sub-inv N/A

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

   7. +-commutative N/A

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

   8. flip-+ N/A

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

   9. lower-/.f64 N/A

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

3. Applied rewrites 56.7%

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

4. Taylor expanded in t around inf

   \[\leadsto x \cdot x - \color{blue}{t \cdot \left(-4 \cdot y + 4 \cdot \frac{y \cdot {z}^{2}}{t}\right)} \]
5. Step-by-step derivation

   1. *-commutative N/A

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

   2. lower-*.f64 N/A

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

   3. +-commutative N/A

      \[\leadsto x \cdot x - \left(4 \cdot \frac{y \cdot {z}^{2}}{t} + -4 \cdot y\right) \cdot t \]

   4. *-commutative N/A

      \[\leadsto x \cdot x - \left(\frac{y \cdot {z}^{2}}{t} \cdot 4 + -4 \cdot y\right) \cdot t \]

   5. lower-fma.f64 N/A

      \[\leadsto x \cdot x - \mathsf{fma}\left(\frac{y \cdot {z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

   6. associate-/l* N/A

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

   7. lower-*.f64 N/A

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, -4 \cdot y\right) \cdot t \]

   8. pow2 N/A

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

   9. lift-/.f64 N/A

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

   10. lift-*.f64 N/A

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

   11. *-commutative N/A

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

   12. lower-*.f64 85.7

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

6. Applied rewrites 85.7%

   \[\leadsto x \cdot x - \color{blue}{\mathsf{fma}\left(y \cdot \frac{z \cdot z}{t}, 4, y \cdot -4\right) \cdot t} \]
7. Step-by-step derivation

   1. lift-*.f64 N/A

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

   2. lift-/.f64 N/A

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

   3. pow2 N/A

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{{z}^{2}}{t}, 4, y \cdot -4\right) \cdot t \]

   4. frac-2neg N/A

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left({z}^{2}\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

   5. pow2 N/A

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\mathsf{neg}\left(z \cdot z\right)}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

   6. distribute-lft-neg-out N/A

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\mathsf{neg}\left(z\right)\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

   7. mul-1-neg N/A

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{\mathsf{neg}\left(t\right)}, 4, y \cdot -4\right) \cdot t \]

   8. mul-1-neg N/A

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{-1 \cdot t}, 4, y \cdot -4\right) \cdot t \]

   9. *-commutative N/A

      \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot z\right) \cdot z}{t \cdot -1}, 4, y \cdot -4\right) \cdot t \]

   10. frac-times N/A

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

   11. lift-/.f64 N/A

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

   12. lift-*.f64 N/A

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \left(\frac{-1 \cdot z}{t} \cdot \frac{z}{-1}\right), 4, y \cdot -4\right) \cdot t \]

   13. associate-*r/ N/A

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   14. lower-/.f64 N/A

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   15. lower-*.f64 87.3

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   16. lift-*.f64 N/A

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   17. lift-/.f64 N/A

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\frac{-1 \cdot z}{t} \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   18. associate-*r/ N/A

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(-1 \cdot \frac{z}{t}\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   19. *-commutative N/A

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   20. lower-*.f64 N/A

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

   21. lower-/.f64 87.3

       \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

8. Applied rewrites 87.3%

   \[\leadsto x \cdot x - \mathsf{fma}\left(y \cdot \frac{\left(\frac{z}{t} \cdot -1\right) \cdot z}{-1}, 4, y \cdot -4\right) \cdot t \]

10. Applied rewrites 86.9%

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

Alternative 9: 43.8% accurate, N/A× speedup

Math

\[\begin{array}{l} z_m = \left|z\right| \\ \begin{array}{l} t_1 := 1 \cdot \left(-z\_m\right)\\ \mathsf{fma}\left(\left(x \cdot x\right) \cdot -4, \mathsf{fma}\left(t\_1, t\_1, -1 \cdot t\right) \cdot \frac{y}{x \cdot x}, x \cdot x\right) \end{array} \end{array} \]

FPCore

z_m = (fabs.f64 z)
(FPCore (x y z_m t)
 :precision binary64
 (let* ((t_1 (* 1.0 (- z_m))))
   (fma (* (* x x) -4.0) (* (fma t_1 t_1 (* -1.0 t)) (/ y (* x x))) (* x x))))

C

z_m = fabs(z);
double code(double x, double y, double z_m, double t) {
	double t_1 = 1.0 * -z_m;
	return fma(((x * x) * -4.0), (fma(t_1, t_1, (-1.0 * t)) * (y / (x * x))), (x * x));
}

Julia

z_m = abs(z)
function code(x, y, z_m, t)
	t_1 = Float64(1.0 * Float64(-z_m))
	return fma(Float64(Float64(x * x) * -4.0), Float64(fma(t_1, t_1, Float64(-1.0 * t)) * Float64(y / Float64(x * x))), Float64(x * x))
end

Wolfram

z_m = N[Abs[z], $MachinePrecision]
code[x_, y_, z$95$m_, t_] := Block[{t$95$1 = N[(1.0 * (-z$95$m)), $MachinePrecision]}, N[(N[(N[(x * x), $MachinePrecision] * -4.0), $MachinePrecision] * N[(N[(t$95$1 * t$95$1 + N[(-1.0 * t), $MachinePrecision]), $MachinePrecision] * N[(y / N[(x * x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(x * x), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Initial program 91.1%

   \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right) \]

2. Taylor expanded in x around inf

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

   1. +-commutative N/A

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

   2. distribute-lft-in N/A

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

   3. associate-*r* N/A

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

   4. *-rgt-identity N/A

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

   5. lower-fma.f64 N/A

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

4. Applied rewrites 43.8%

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

Reproduce

herbie shell --seed 2025093 
(FPCore (x y z t)
  :name "Graphics.Rasterific.Shading:$sradialGradientWithFocusShader from Rasterific-0.6.1, B"
  :precision binary64
  (- (* x x) (* (* y 4.0) (- (* z z) t))))