Anisotropic x16 LOD (line direction, u)

Percentage Accurate: 76.5% → 76.7%

Time: 12.0s

Alternatives: 7

Speedup: 1.0×

Specification

\[\left(\left(\left(\left(\left(\left(1 \leq w \land w \leq 16384\right) \land \left(1 \leq h \land h \leq 16384\right)\right) \land \left(10^{-20} \leq \left|dX.u\right| \land \left|dX.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dX.v\right| \land \left|dX.v\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.u\right| \land \left|dY.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.v\right| \land \left|dY.v\right| \leq 10^{+20}\right)\right) \land maxAniso = 16\]

Math

\[\begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_2 := \left\lfloor w\right\rfloor \cdot dX.u\\ t_3 := t\_2 \cdot t\_2 + t\_0 \cdot t\_0\\ t_4 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_5 := t\_1 \cdot t\_1 + t\_4 \cdot t\_4\\ t_6 := \frac{1}{\sqrt{\mathsf{max}\left(t\_3, t\_5\right)}}\\ \mathbf{if}\;t\_3 \geq t\_5:\\ \;\;\;\;t\_6 \cdot t\_2\\ \mathbf{else}:\\ \;\;\;\;t\_6 \cdot t\_1\\ \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0))
                              (and (<= 1.0 h) (<= h 16384.0)))
                         (and (<= 1e-20 (fabs dX.u))
                              (<= (fabs dX.u) 1e+20)))
                    (and (<= 1e-20 (fabs dX.v))
                         (<= (fabs dX.v) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (== maxAniso 16.0))
  (let* ((t_0 (* (floor h) dX.v))
       (t_1 (* (floor w) dY.u))
       (t_2 (* (floor w) dX.u))
       (t_3 (+ (* t_2 t_2) (* t_0 t_0)))
       (t_4 (* (floor h) dY.v))
       (t_5 (+ (* t_1 t_1) (* t_4 t_4)))
       (t_6 (/ 1.0 (sqrt (fmax t_3 t_5)))))
  (if (>= t_3 t_5) (* t_6 t_2) (* t_6 t_1))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = floorf(w) * dY_46_u;
	float t_2 = floorf(w) * dX_46_u;
	float t_3 = (t_2 * t_2) + (t_0 * t_0);
	float t_4 = floorf(h) * dY_46_v;
	float t_5 = (t_1 * t_1) + (t_4 * t_4);
	float t_6 = 1.0f / sqrtf(fmaxf(t_3, t_5));
	float tmp;
	if (t_3 >= t_5) {
		tmp = t_6 * t_2;
	} else {
		tmp = t_6 * t_1;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = Float32(floor(w) * dY_46_u)
	t_2 = Float32(floor(w) * dX_46_u)
	t_3 = Float32(Float32(t_2 * t_2) + Float32(t_0 * t_0))
	t_4 = Float32(floor(h) * dY_46_v)
	t_5 = Float32(Float32(t_1 * t_1) + Float32(t_4 * t_4))
	t_6 = Float32(Float32(1.0) / sqrt(fmax(t_3, t_5)))
	tmp = Float32(0.0)
	if (t_3 >= t_5)
		tmp = Float32(t_6 * t_2);
	else
		tmp = Float32(t_6 * t_1);
	end
	return tmp
end

MATLAB

function tmp_2 = code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = floor(h) * dX_46_v;
	t_1 = floor(w) * dY_46_u;
	t_2 = floor(w) * dX_46_u;
	t_3 = (t_2 * t_2) + (t_0 * t_0);
	t_4 = floor(h) * dY_46_v;
	t_5 = (t_1 * t_1) + (t_4 * t_4);
	t_6 = single(1.0) / sqrt(max(t_3, t_5));
	tmp = single(0.0);
	if (t_3 >= t_5)
		tmp = t_6 * t_2;
	else
		tmp = t_6 * t_1;
	end
	tmp_2 = tmp;
end

Initial Program: 76.5% accurate, 1.0× speedup

\[\left(\left(\left(\left(\left(\left(1 \leq w \land w \leq 16384\right) \land \left(1 \leq h \land h \leq 16384\right)\right) \land \left(10^{-20} \leq \left|dX.u\right| \land \left|dX.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dX.v\right| \land \left|dX.v\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.u\right| \land \left|dY.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.v\right| \land \left|dY.v\right| \leq 10^{+20}\right)\right) \land maxAniso = 16\]

Math

\[\begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_2 := \left\lfloor w\right\rfloor \cdot dX.u\\ t_3 := t\_2 \cdot t\_2 + t\_0 \cdot t\_0\\ t_4 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_5 := t\_1 \cdot t\_1 + t\_4 \cdot t\_4\\ t_6 := \frac{1}{\sqrt{\mathsf{max}\left(t\_3, t\_5\right)}}\\ \mathbf{if}\;t\_3 \geq t\_5:\\ \;\;\;\;t\_6 \cdot t\_2\\ \mathbf{else}:\\ \;\;\;\;t\_6 \cdot t\_1\\ \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0))
                              (and (<= 1.0 h) (<= h 16384.0)))
                         (and (<= 1e-20 (fabs dX.u))
                              (<= (fabs dX.u) 1e+20)))
                    (and (<= 1e-20 (fabs dX.v))
                         (<= (fabs dX.v) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (== maxAniso 16.0))
  (let* ((t_0 (* (floor h) dX.v))
       (t_1 (* (floor w) dY.u))
       (t_2 (* (floor w) dX.u))
       (t_3 (+ (* t_2 t_2) (* t_0 t_0)))
       (t_4 (* (floor h) dY.v))
       (t_5 (+ (* t_1 t_1) (* t_4 t_4)))
       (t_6 (/ 1.0 (sqrt (fmax t_3 t_5)))))
  (if (>= t_3 t_5) (* t_6 t_2) (* t_6 t_1))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = floorf(w) * dY_46_u;
	float t_2 = floorf(w) * dX_46_u;
	float t_3 = (t_2 * t_2) + (t_0 * t_0);
	float t_4 = floorf(h) * dY_46_v;
	float t_5 = (t_1 * t_1) + (t_4 * t_4);
	float t_6 = 1.0f / sqrtf(fmaxf(t_3, t_5));
	float tmp;
	if (t_3 >= t_5) {
		tmp = t_6 * t_2;
	} else {
		tmp = t_6 * t_1;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = Float32(floor(w) * dY_46_u)
	t_2 = Float32(floor(w) * dX_46_u)
	t_3 = Float32(Float32(t_2 * t_2) + Float32(t_0 * t_0))
	t_4 = Float32(floor(h) * dY_46_v)
	t_5 = Float32(Float32(t_1 * t_1) + Float32(t_4 * t_4))
	t_6 = Float32(Float32(1.0) / sqrt(fmax(t_3, t_5)))
	tmp = Float32(0.0)
	if (t_3 >= t_5)
		tmp = Float32(t_6 * t_2);
	else
		tmp = Float32(t_6 * t_1);
	end
	return tmp
end

MATLAB

function tmp_2 = code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = floor(h) * dX_46_v;
	t_1 = floor(w) * dY_46_u;
	t_2 = floor(w) * dX_46_u;
	t_3 = (t_2 * t_2) + (t_0 * t_0);
	t_4 = floor(h) * dY_46_v;
	t_5 = (t_1 * t_1) + (t_4 * t_4);
	t_6 = single(1.0) / sqrt(max(t_3, t_5));
	tmp = single(0.0);
	if (t_3 >= t_5)
		tmp = t_6 * t_2;
	else
		tmp = t_6 * t_1;
	end
	tmp_2 = tmp;
end

Alternative 1: 76.7% accurate, 1.0× speedup

\[\left(\left(\left(\left(\left(\left(1 \leq w \land w \leq 16384\right) \land \left(1 \leq h \land h \leq 16384\right)\right) \land \left(10^{-20} \leq \left|dX.u\right| \land \left|dX.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dX.v\right| \land \left|dX.v\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.u\right| \land \left|dY.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.v\right| \land \left|dY.v\right| \leq 10^{+20}\right)\right) \land maxAniso = 16\]

Math

\[\begin{array}{l} t_0 := dY.v \cdot \left\lfloor h\right\rfloor \\ t_1 := dY.u \cdot \left\lfloor w\right\rfloor \\ t_2 := \mathsf{fma}\left(t\_0, t\_0, t\_1 \cdot t\_1\right)\\ t_3 := dX.u \cdot \left\lfloor w\right\rfloor \\ t_4 := dX.v \cdot \left\lfloor h\right\rfloor \\ t_5 := \mathsf{fma}\left(t\_4, t\_4, t\_3 \cdot t\_3\right)\\ t_6 := \sqrt{\mathsf{max}\left(t\_2, t\_5\right)}\\ \mathbf{if}\;t\_5 \geq t\_2:\\ \;\;\;\;\frac{t\_3}{t\_6}\\ \mathbf{else}:\\ \;\;\;\;\frac{t\_1}{t\_6}\\ \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0))
                              (and (<= 1.0 h) (<= h 16384.0)))
                         (and (<= 1e-20 (fabs dX.u))
                              (<= (fabs dX.u) 1e+20)))
                    (and (<= 1e-20 (fabs dX.v))
                         (<= (fabs dX.v) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (== maxAniso 16.0))
  (let* ((t_0 (* dY.v (floor h)))
       (t_1 (* dY.u (floor w)))
       (t_2 (fma t_0 t_0 (* t_1 t_1)))
       (t_3 (* dX.u (floor w)))
       (t_4 (* dX.v (floor h)))
       (t_5 (fma t_4 t_4 (* t_3 t_3)))
       (t_6 (sqrt (fmax t_2 t_5))))
  (if (>= t_5 t_2) (/ t_3 t_6) (/ t_1 t_6))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = dY_46_v * floorf(h);
	float t_1 = dY_46_u * floorf(w);
	float t_2 = fmaf(t_0, t_0, (t_1 * t_1));
	float t_3 = dX_46_u * floorf(w);
	float t_4 = dX_46_v * floorf(h);
	float t_5 = fmaf(t_4, t_4, (t_3 * t_3));
	float t_6 = sqrtf(fmaxf(t_2, t_5));
	float tmp;
	if (t_5 >= t_2) {
		tmp = t_3 / t_6;
	} else {
		tmp = t_1 / t_6;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(dY_46_v * floor(h))
	t_1 = Float32(dY_46_u * floor(w))
	t_2 = fma(t_0, t_0, Float32(t_1 * t_1))
	t_3 = Float32(dX_46_u * floor(w))
	t_4 = Float32(dX_46_v * floor(h))
	t_5 = fma(t_4, t_4, Float32(t_3 * t_3))
	t_6 = sqrt(fmax(t_2, t_5))
	tmp = Float32(0.0)
	if (t_5 >= t_2)
		tmp = Float32(t_3 / t_6);
	else
		tmp = Float32(t_1 / t_6);
	end
	return tmp
end

Derivation

1. Initial program 76.5%

   \[\begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

3. Applied rewrites 76.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right)\right) \geq \mathsf{fma}\left(dY.v \cdot \left\lfloor h\right\rfloor , dY.v \cdot \left\lfloor h\right\rfloor , \left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor w\right\rfloor \right)\right):\\ \;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.v \cdot \left\lfloor h\right\rfloor , dY.v \cdot \left\lfloor h\right\rfloor , \left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor w\right\rfloor \right)\right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right)\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.v \cdot \left\lfloor h\right\rfloor , dY.v \cdot \left\lfloor h\right\rfloor , \left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor w\right\rfloor \right)\right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right)\right)\right)}}\\ \end{array} \]
4. Add Preprocessing

Alternative 2: 76.6% accurate, 1.0× speedup

\[\left(\left(\left(\left(\left(\left(1 \leq w \land w \leq 16384\right) \land \left(1 \leq h \land h \leq 16384\right)\right) \land \left(10^{-20} \leq \left|dX.u\right| \land \left|dX.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dX.v\right| \land \left|dX.v\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.u\right| \land \left|dY.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.v\right| \land \left|dY.v\right| \leq 10^{+20}\right)\right) \land maxAniso = 16\]

Math

\[\begin{array}{l} t_0 := dY.v \cdot \left\lfloor h\right\rfloor \\ t_1 := \mathsf{fma}\left(\left\lfloor h\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)\right)\\ t_2 := dY.u \cdot \left\lfloor w\right\rfloor \\ t_3 := \mathsf{fma}\left(t\_0, t\_0, t\_2 \cdot t\_2\right)\\ t_4 := \sqrt{\mathsf{max}\left(t\_3, t\_1\right)}\\ \mathbf{if}\;t\_1 \geq t\_3:\\ \;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{t\_4}\\ \mathbf{else}:\\ \;\;\;\;\frac{t\_2}{t\_4}\\ \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0))
                              (and (<= 1.0 h) (<= h 16384.0)))
                         (and (<= 1e-20 (fabs dX.u))
                              (<= (fabs dX.u) 1e+20)))
                    (and (<= 1e-20 (fabs dX.v))
                         (<= (fabs dX.v) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (== maxAniso 16.0))
  (let* ((t_0 (* dY.v (floor h)))
       (t_1
        (fma
         (floor h)
         (* (* dX.v dX.v) (floor h))
         (* (* (floor w) (floor w)) (* dX.u dX.u))))
       (t_2 (* dY.u (floor w)))
       (t_3 (fma t_0 t_0 (* t_2 t_2)))
       (t_4 (sqrt (fmax t_3 t_1))))
  (if (>= t_1 t_3) (/ (* dX.u (floor w)) t_4) (/ t_2 t_4))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = dY_46_v * floorf(h);
	float t_1 = fmaf(floorf(h), ((dX_46_v * dX_46_v) * floorf(h)), ((floorf(w) * floorf(w)) * (dX_46_u * dX_46_u)));
	float t_2 = dY_46_u * floorf(w);
	float t_3 = fmaf(t_0, t_0, (t_2 * t_2));
	float t_4 = sqrtf(fmaxf(t_3, t_1));
	float tmp;
	if (t_1 >= t_3) {
		tmp = (dX_46_u * floorf(w)) / t_4;
	} else {
		tmp = t_2 / t_4;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(dY_46_v * floor(h))
	t_1 = fma(floor(h), Float32(Float32(dX_46_v * dX_46_v) * floor(h)), Float32(Float32(floor(w) * floor(w)) * Float32(dX_46_u * dX_46_u)))
	t_2 = Float32(dY_46_u * floor(w))
	t_3 = fma(t_0, t_0, Float32(t_2 * t_2))
	t_4 = sqrt(fmax(t_3, t_1))
	tmp = Float32(0.0)
	if (t_1 >= t_3)
		tmp = Float32(Float32(dX_46_u * floor(w)) / t_4);
	else
		tmp = Float32(t_2 / t_4);
	end
	return tmp
end

Derivation

1. Initial program 76.5%

   \[\begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

3. Applied rewrites 76.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right)\right) \geq \mathsf{fma}\left(dY.v \cdot \left\lfloor h\right\rfloor , dY.v \cdot \left\lfloor h\right\rfloor , \left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor w\right\rfloor \right)\right):\\ \;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.v \cdot \left\lfloor h\right\rfloor , dY.v \cdot \left\lfloor h\right\rfloor , \left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor w\right\rfloor \right)\right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right)\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.v \cdot \left\lfloor h\right\rfloor , dY.v \cdot \left\lfloor h\right\rfloor , \left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor w\right\rfloor \right)\right), \mathsf{fma}\left(dX.v \cdot \left\lfloor h\right\rfloor , dX.v \cdot \left\lfloor h\right\rfloor , \left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right)\right)\right)}}\\ \end{array} \]
4. Step-by-step derivation

5. Applied rewrites 76.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{fma}\left(\left\lfloor h\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)\right) \geq \mathsf{fma}\left(dY.v \cdot \left\lfloor h\right\rfloor , dY.v \cdot \left\lfloor h\right\rfloor , \left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor w\right\rfloor \right)\right):\\ \;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.v \cdot \left\lfloor h\right\rfloor , dY.v \cdot \left\lfloor h\right\rfloor , \left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor w\right\rfloor \right)\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.v \cdot \left\lfloor h\right\rfloor , dY.v \cdot \left\lfloor h\right\rfloor , \left(dY.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor w\right\rfloor \right)\right), \mathsf{fma}\left(\left\lfloor h\right\rfloor , \left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)\right)\right)}}\\ \end{array} \]
6. Add Preprocessing

Alternative 3: 46.4% accurate, 1.4× speedup

\[\left(\left(\left(\left(\left(\left(1 \leq w \land w \leq 16384\right) \land \left(1 \leq h \land h \leq 16384\right)\right) \land \left(10^{-20} \leq \left|dX.u\right| \land \left|dX.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dX.v\right| \land \left|dX.v\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.u\right| \land \left|dY.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.v\right| \land \left|dY.v\right| \leq 10^{+20}\right)\right) \land maxAniso = 16\]

Math

\[\begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_1 := \left\lfloor w\right\rfloor \cdot dX.u\\ t_2 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_3 := \left\lfloor w\right\rfloor \cdot dY.u\\ \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor w\right\rfloor \cdot \left(\frac{1}{\sqrt{\mathsf{max}\left(\frac{1}{\frac{1}{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}}, \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}} \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(t\_1 \cdot t\_1 + t\_2 \cdot t\_2, t\_3 \cdot t\_3 + t\_0 \cdot t\_0\right)}} \cdot t\_3\\ \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0))
                              (and (<= 1.0 h) (<= h 16384.0)))
                         (and (<= 1e-20 (fabs dX.u))
                              (<= (fabs dX.u) 1e+20)))
                    (and (<= 1e-20 (fabs dX.v))
                         (<= (fabs dX.v) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (== maxAniso 16.0))
  (let* ((t_0 (* (floor h) dY.v))
       (t_1 (* (floor w) dX.u))
       (t_2 (* (floor h) dX.v))
       (t_3 (* (floor w) dY.u)))
  (if 0
    (*
     (floor w)
     (*
      (/
       1.0
       (sqrt
        (fmax
         (/ 1.0 (/ 1.0 (* (pow dY.v 2.0) (pow (floor h) 2.0))))
         (fma
          (* (* (floor w) (floor w)) dX.u)
          dX.u
          (* (* (* (floor h) (floor h)) dX.v) dX.v)))))
      dX.u))
    (*
     (/
      1.0
      (sqrt
       (fmax
        (+ (* t_1 t_1) (* t_2 t_2))
        (+ (* t_3 t_3) (* t_0 t_0)))))
     t_3))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * dY_46_v;
	float t_1 = floorf(w) * dX_46_u;
	float t_2 = floorf(h) * dX_46_v;
	float t_3 = floorf(w) * dY_46_u;
	float tmp;
	if (0.0f) {
		tmp = floorf(w) * ((1.0f / sqrtf(fmaxf((1.0f / (1.0f / (powf(dY_46_v, 2.0f) * powf(floorf(h), 2.0f)))), fmaf(((floorf(w) * floorf(w)) * dX_46_u), dX_46_u, (((floorf(h) * floorf(h)) * dX_46_v) * dX_46_v))))) * dX_46_u);
	} else {
		tmp = (1.0f / sqrtf(fmaxf(((t_1 * t_1) + (t_2 * t_2)), ((t_3 * t_3) + (t_0 * t_0))))) * t_3;
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * dY_46_v)
	t_1 = Float32(floor(w) * dX_46_u)
	t_2 = Float32(floor(h) * dX_46_v)
	t_3 = Float32(floor(w) * dY_46_u)
	tmp = Float32(0.0)
	if (Float32(0.0))
		tmp = Float32(floor(w) * Float32(Float32(Float32(1.0) / sqrt(fmax(Float32(Float32(1.0) / Float32(Float32(1.0) / Float32((dY_46_v ^ Float32(2.0)) * (floor(h) ^ Float32(2.0))))), fma(Float32(Float32(floor(w) * floor(w)) * dX_46_u), dX_46_u, Float32(Float32(Float32(floor(h) * floor(h)) * dX_46_v) * dX_46_v))))) * dX_46_u));
	else
		tmp = Float32(Float32(Float32(1.0) / sqrt(fmax(Float32(Float32(t_1 * t_1) + Float32(t_2 * t_2)), Float32(Float32(t_3 * t_3) + Float32(t_0 * t_0))))) * t_3);
	end
	return tmp
end

Derivation

1. Initial program 76.5%

   \[\begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

2. Taylor expanded in undef-var around zero

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

6. Applied rewrites 42.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor w\right\rfloor \cdot \left(\frac{1}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}} \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]
7. Step-by-step derivation

8. Applied rewrites 42.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor w\right\rfloor \cdot \left(\frac{1}{\sqrt{\mathsf{max}\left(\frac{1}{{\left(\mathsf{fma}\left(dY.u \cdot \left\lfloor w\right\rfloor , dY.u \cdot \left\lfloor w\right\rfloor , \left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\right)\right)}^{-1}}, \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}} \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

9. Taylor expanded in dY.u around 0

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor w\right\rfloor \cdot \left(\frac{1}{\sqrt{\mathsf{max}\left(\frac{1}{\frac{1}{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}}, \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}} \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]
10. Step-by-step derivation

11. Applied rewrites 46.4%

    \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor w\right\rfloor \cdot \left(\frac{1}{\sqrt{\mathsf{max}\left(\frac{1}{\frac{1}{{dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2}}}, \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}} \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]
12. Add Preprocessing

Alternative 4: 43.1% accurate, 1.9× speedup

\[\left(\left(\left(\left(\left(\left(1 \leq w \land w \leq 16384\right) \land \left(1 \leq h \land h \leq 16384\right)\right) \land \left(10^{-20} \leq \left|dX.u\right| \land \left|dX.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dX.v\right| \land \left|dX.v\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.u\right| \land \left|dY.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.v\right| \land \left|dY.v\right| \leq 10^{+20}\right)\right) \land maxAniso = 16\]

Math

\[\begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \\ t_1 := \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\\ t_2 := dY.u \cdot \left\lfloor w\right\rfloor \\ t_3 := dY.v \cdot \left\lfloor h\right\rfloor \\ t_4 := t\_0 \cdot dX.v\\ \mathbf{if}\;0:\\ \;\;\;\;\frac{dX.u}{\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_4, dX.v, t\_1 \cdot dX.u\right), \mathsf{fma}\left(t\_2, t\_2, t\_3 \cdot t\_3\right)\right)}}{\left\lfloor w\right\rfloor }}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(t\_0 \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(t\_1, dX.u, t\_4 \cdot dX.v\right)\right)}} \cdot \left\lfloor w\right\rfloor \\ \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0))
                              (and (<= 1.0 h) (<= h 16384.0)))
                         (and (<= 1e-20 (fabs dX.u))
                              (<= (fabs dX.u) 1e+20)))
                    (and (<= 1e-20 (fabs dX.v))
                         (<= (fabs dX.v) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (== maxAniso 16.0))
  (let* ((t_0 (* (floor h) (floor h)))
       (t_1 (* (* (floor w) (floor w)) dX.u))
       (t_2 (* dY.u (floor w)))
       (t_3 (* dY.v (floor h)))
       (t_4 (* t_0 dX.v)))
  (if 0
    (/
     dX.u
     (/
      (sqrt
       (fmax (fma t_4 dX.v (* t_1 dX.u)) (fma t_2 t_2 (* t_3 t_3))))
      (floor w)))
    (*
     (/
      dY.u
      (sqrt
       (fmax
        (fma
         (* (* dY.u dY.u) (floor w))
         (floor w)
         (* (* t_0 dY.v) dY.v))
        (fma t_1 dX.u (* t_4 dX.v)))))
     (floor w)))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * floorf(h);
	float t_1 = (floorf(w) * floorf(w)) * dX_46_u;
	float t_2 = dY_46_u * floorf(w);
	float t_3 = dY_46_v * floorf(h);
	float t_4 = t_0 * dX_46_v;
	float tmp;
	if (0.0f) {
		tmp = dX_46_u / (sqrtf(fmaxf(fmaf(t_4, dX_46_v, (t_1 * dX_46_u)), fmaf(t_2, t_2, (t_3 * t_3)))) / floorf(w));
	} else {
		tmp = (dY_46_u / sqrtf(fmaxf(fmaf(((dY_46_u * dY_46_u) * floorf(w)), floorf(w), ((t_0 * dY_46_v) * dY_46_v)), fmaf(t_1, dX_46_u, (t_4 * dX_46_v))))) * floorf(w);
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * floor(h))
	t_1 = Float32(Float32(floor(w) * floor(w)) * dX_46_u)
	t_2 = Float32(dY_46_u * floor(w))
	t_3 = Float32(dY_46_v * floor(h))
	t_4 = Float32(t_0 * dX_46_v)
	tmp = Float32(0.0)
	if (Float32(0.0))
		tmp = Float32(dX_46_u / Float32(sqrt(fmax(fma(t_4, dX_46_v, Float32(t_1 * dX_46_u)), fma(t_2, t_2, Float32(t_3 * t_3)))) / floor(w)));
	else
		tmp = Float32(Float32(dY_46_u / sqrt(fmax(fma(Float32(Float32(dY_46_u * dY_46_u) * floor(w)), floor(w), Float32(Float32(t_0 * dY_46_v) * dY_46_v)), fma(t_1, dX_46_u, Float32(t_4 * dX_46_v))))) * floor(w));
	end
	return tmp
end

Derivation

1. Initial program 76.5%

   \[\begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

2. Taylor expanded in undef-var around zero

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

6. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}} \cdot \left\lfloor w\right\rfloor \\ \end{array} \]

8. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{dX.u}{\frac{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, dX.v, \left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot dX.u\right), \mathsf{fma}\left(dY.u \cdot \left\lfloor w\right\rfloor , dY.u \cdot \left\lfloor w\right\rfloor , \left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\right)\right)}}{\left\lfloor w\right\rfloor }}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}} \cdot \left\lfloor w\right\rfloor \\ \end{array} \]
9. Add Preprocessing

Alternative 5: 43.0% accurate, 1.9× speedup

\[\left(\left(\left(\left(\left(\left(1 \leq w \land w \leq 16384\right) \land \left(1 \leq h \land h \leq 16384\right)\right) \land \left(10^{-20} \leq \left|dX.u\right| \land \left|dX.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dX.v\right| \land \left|dX.v\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.u\right| \land \left|dY.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.v\right| \land \left|dY.v\right| \leq 10^{+20}\right)\right) \land maxAniso = 16\]

Math

\[\begin{array}{l} t_0 := dX.u \cdot \left\lfloor w\right\rfloor \\ t_1 := dX.v \cdot \left\lfloor h\right\rfloor \\ t_2 := \sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(t\_0, t\_0, t\_1 \cdot t\_1\right)\right)}\\ \mathbf{if}\;0:\\ \;\;\;\;\frac{t\_0}{t\_2}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u}{t\_2} \cdot \left\lfloor w\right\rfloor \\ \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0))
                              (and (<= 1.0 h) (<= h 16384.0)))
                         (and (<= 1e-20 (fabs dX.u))
                              (<= (fabs dX.u) 1e+20)))
                    (and (<= 1e-20 (fabs dX.v))
                         (<= (fabs dX.v) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (== maxAniso 16.0))
  (let* ((t_0 (* dX.u (floor w)))
       (t_1 (* dX.v (floor h)))
       (t_2
        (sqrt
         (fmax
          (fma
           (* (* dY.u dY.u) (floor w))
           (floor w)
           (* (* (* (floor h) (floor h)) dY.v) dY.v))
          (fma t_0 t_0 (* t_1 t_1))))))
  (if 0 (/ t_0 t_2) (* (/ dY.u t_2) (floor w)))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = dX_46_u * floorf(w);
	float t_1 = dX_46_v * floorf(h);
	float t_2 = sqrtf(fmaxf(fmaf(((dY_46_u * dY_46_u) * floorf(w)), floorf(w), (((floorf(h) * floorf(h)) * dY_46_v) * dY_46_v)), fmaf(t_0, t_0, (t_1 * t_1))));
	float tmp;
	if (0.0f) {
		tmp = t_0 / t_2;
	} else {
		tmp = (dY_46_u / t_2) * floorf(w);
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(dX_46_u * floor(w))
	t_1 = Float32(dX_46_v * floor(h))
	t_2 = sqrt(fmax(fma(Float32(Float32(dY_46_u * dY_46_u) * floor(w)), floor(w), Float32(Float32(Float32(floor(h) * floor(h)) * dY_46_v) * dY_46_v)), fma(t_0, t_0, Float32(t_1 * t_1))))
	tmp = Float32(0.0)
	if (Float32(0.0))
		tmp = Float32(t_0 / t_2);
	else
		tmp = Float32(Float32(dY_46_u / t_2) * floor(w));
	end
	return tmp
end

Derivation

1. Initial program 76.5%

   \[\begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

2. Taylor expanded in undef-var around zero

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

6. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}} \cdot \left\lfloor w\right\rfloor \\ \end{array} \]
7. Step-by-step derivation

8. Applied rewrites 43.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(dX.u \cdot \left\lfloor w\right\rfloor , dX.u \cdot \left\lfloor w\right\rfloor , \left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(dX.u \cdot \left\lfloor w\right\rfloor , dX.u \cdot \left\lfloor w\right\rfloor , \left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\right)\right)}} \cdot \left\lfloor w\right\rfloor \\ \end{array} \]
9. Add Preprocessing

Alternative 6: 43.0% accurate, 1.9× speedup

\[\left(\left(\left(\left(\left(\left(1 \leq w \land w \leq 16384\right) \land \left(1 \leq h \land h \leq 16384\right)\right) \land \left(10^{-20} \leq \left|dX.u\right| \land \left|dX.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dX.v\right| \land \left|dX.v\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.u\right| \land \left|dY.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.v\right| \land \left|dY.v\right| \leq 10^{+20}\right)\right) \land maxAniso = 16\]

Math

\[\begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \\ t_1 := t\_0 \cdot dX.v\\ t_2 := \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\\ t_3 := dY.u \cdot \left\lfloor w\right\rfloor \\ t_4 := dY.v \cdot \left\lfloor h\right\rfloor \\ \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor w\right\rfloor \cdot \frac{dX.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_1, dX.v, t\_2 \cdot dX.u\right), \mathsf{fma}\left(t\_3, t\_3, t\_4 \cdot t\_4\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(t\_0 \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(t\_2, dX.u, t\_1 \cdot dX.v\right)\right)}} \cdot \left\lfloor w\right\rfloor \\ \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0))
                              (and (<= 1.0 h) (<= h 16384.0)))
                         (and (<= 1e-20 (fabs dX.u))
                              (<= (fabs dX.u) 1e+20)))
                    (and (<= 1e-20 (fabs dX.v))
                         (<= (fabs dX.v) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (== maxAniso 16.0))
  (let* ((t_0 (* (floor h) (floor h)))
       (t_1 (* t_0 dX.v))
       (t_2 (* (* (floor w) (floor w)) dX.u))
       (t_3 (* dY.u (floor w)))
       (t_4 (* dY.v (floor h))))
  (if 0
    (*
     (floor w)
     (/
      dX.u
      (sqrt
       (fmax (fma t_1 dX.v (* t_2 dX.u)) (fma t_3 t_3 (* t_4 t_4))))))
    (*
     (/
      dY.u
      (sqrt
       (fmax
        (fma
         (* (* dY.u dY.u) (floor w))
         (floor w)
         (* (* t_0 dY.v) dY.v))
        (fma t_2 dX.u (* t_1 dX.v)))))
     (floor w)))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = floorf(h) * floorf(h);
	float t_1 = t_0 * dX_46_v;
	float t_2 = (floorf(w) * floorf(w)) * dX_46_u;
	float t_3 = dY_46_u * floorf(w);
	float t_4 = dY_46_v * floorf(h);
	float tmp;
	if (0.0f) {
		tmp = floorf(w) * (dX_46_u / sqrtf(fmaxf(fmaf(t_1, dX_46_v, (t_2 * dX_46_u)), fmaf(t_3, t_3, (t_4 * t_4)))));
	} else {
		tmp = (dY_46_u / sqrtf(fmaxf(fmaf(((dY_46_u * dY_46_u) * floorf(w)), floorf(w), ((t_0 * dY_46_v) * dY_46_v)), fmaf(t_2, dX_46_u, (t_1 * dX_46_v))))) * floorf(w);
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(floor(h) * floor(h))
	t_1 = Float32(t_0 * dX_46_v)
	t_2 = Float32(Float32(floor(w) * floor(w)) * dX_46_u)
	t_3 = Float32(dY_46_u * floor(w))
	t_4 = Float32(dY_46_v * floor(h))
	tmp = Float32(0.0)
	if (Float32(0.0))
		tmp = Float32(floor(w) * Float32(dX_46_u / sqrt(fmax(fma(t_1, dX_46_v, Float32(t_2 * dX_46_u)), fma(t_3, t_3, Float32(t_4 * t_4))))));
	else
		tmp = Float32(Float32(dY_46_u / sqrt(fmax(fma(Float32(Float32(dY_46_u * dY_46_u) * floor(w)), floor(w), Float32(Float32(t_0 * dY_46_v) * dY_46_v)), fma(t_2, dX_46_u, Float32(t_1 * dX_46_v))))) * floor(w));
	end
	return tmp
end

Derivation

1. Initial program 76.5%

   \[\begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

2. Taylor expanded in undef-var around zero

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

6. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{dX.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}} \cdot \left\lfloor w\right\rfloor \\ \end{array} \]

8. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor w\right\rfloor \cdot \frac{dX.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, dX.v, \left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot dX.u\right), \mathsf{fma}\left(dY.u \cdot \left\lfloor w\right\rfloor , dY.u \cdot \left\lfloor w\right\rfloor , \left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}} \cdot \left\lfloor w\right\rfloor \\ \end{array} \]
9. Add Preprocessing

Alternative 7: 43.0% accurate, 1.9× speedup

\[\left(\left(\left(\left(\left(\left(1 \leq w \land w \leq 16384\right) \land \left(1 \leq h \land h \leq 16384\right)\right) \land \left(10^{-20} \leq \left|dX.u\right| \land \left|dX.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dX.v\right| \land \left|dX.v\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.u\right| \land \left|dY.u\right| \leq 10^{+20}\right)\right) \land \left(10^{-20} \leq \left|dY.v\right| \land \left|dY.v\right| \leq 10^{+20}\right)\right) \land maxAniso = 16\]

Math

\[\begin{array}{l} t_0 := dY.u \cdot \left\lfloor w\right\rfloor \\ t_1 := \left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \\ t_2 := dY.v \cdot \left\lfloor h\right\rfloor \\ t_3 := \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\\ t_4 := t\_1 \cdot dX.v\\ \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor w\right\rfloor \cdot \frac{dX.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(t\_1 \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(t\_3, dX.u, t\_4 \cdot dX.v\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t\_0}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_4, dX.v, t\_3 \cdot dX.u\right), \mathsf{fma}\left(t\_0, t\_0, t\_2 \cdot t\_2\right)\right)}}\\ \end{array} \]

FPCore

(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0))
                              (and (<= 1.0 h) (<= h 16384.0)))
                         (and (<= 1e-20 (fabs dX.u))
                              (<= (fabs dX.u) 1e+20)))
                    (and (<= 1e-20 (fabs dX.v))
                         (<= (fabs dX.v) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (== maxAniso 16.0))
  (let* ((t_0 (* dY.u (floor w)))
       (t_1 (* (floor h) (floor h)))
       (t_2 (* dY.v (floor h)))
       (t_3 (* (* (floor w) (floor w)) dX.u))
       (t_4 (* t_1 dX.v)))
  (if 0
    (*
     (floor w)
     (/
      dX.u
      (sqrt
       (fmax
        (fma
         (* (* dY.u dY.u) (floor w))
         (floor w)
         (* (* t_1 dY.v) dY.v))
        (fma t_3 dX.u (* t_4 dX.v))))))
    (/
     t_0
     (sqrt
      (fmax (fma t_4 dX.v (* t_3 dX.u)) (fma t_0 t_0 (* t_2 t_2))))))))

C

float code(float w, float h, float dX_46_u, float dX_46_v, float dY_46_u, float dY_46_v, float maxAniso) {
	float t_0 = dY_46_u * floorf(w);
	float t_1 = floorf(h) * floorf(h);
	float t_2 = dY_46_v * floorf(h);
	float t_3 = (floorf(w) * floorf(w)) * dX_46_u;
	float t_4 = t_1 * dX_46_v;
	float tmp;
	if (0.0f) {
		tmp = floorf(w) * (dX_46_u / sqrtf(fmaxf(fmaf(((dY_46_u * dY_46_u) * floorf(w)), floorf(w), ((t_1 * dY_46_v) * dY_46_v)), fmaf(t_3, dX_46_u, (t_4 * dX_46_v)))));
	} else {
		tmp = t_0 / sqrtf(fmaxf(fmaf(t_4, dX_46_v, (t_3 * dX_46_u)), fmaf(t_0, t_0, (t_2 * t_2))));
	}
	return tmp;
}

Julia

function code(w, h, dX_46_u, dX_46_v, dY_46_u, dY_46_v, maxAniso)
	t_0 = Float32(dY_46_u * floor(w))
	t_1 = Float32(floor(h) * floor(h))
	t_2 = Float32(dY_46_v * floor(h))
	t_3 = Float32(Float32(floor(w) * floor(w)) * dX_46_u)
	t_4 = Float32(t_1 * dX_46_v)
	tmp = Float32(0.0)
	if (Float32(0.0))
		tmp = Float32(floor(w) * Float32(dX_46_u / sqrt(fmax(fma(Float32(Float32(dY_46_u * dY_46_u) * floor(w)), floor(w), Float32(Float32(t_1 * dY_46_v) * dY_46_v)), fma(t_3, dX_46_u, Float32(t_4 * dX_46_v))))));
	else
		tmp = Float32(t_0 / sqrt(fmax(fma(t_4, dX_46_v, Float32(t_3 * dX_46_u)), fma(t_0, t_0, Float32(t_2 * t_2)))));
	end
	return tmp
end

Derivation

1. Initial program 76.5%

   \[\begin{array}{l} \mathbf{if}\;\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \geq \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right):\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

2. Taylor expanded in undef-var around zero

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

6. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor w\right\rfloor \cdot \frac{dX.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor w\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dX.u\right) + \left(\left\lfloor h\right\rfloor \cdot dX.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right), \left(\left\lfloor w\right\rfloor \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right) + \left(\left\lfloor h\right\rfloor \cdot dY.v\right) \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\right)}} \cdot \left(\left\lfloor w\right\rfloor \cdot dY.u\right)\\ \end{array} \]

8. Applied rewrites 43.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor w\right\rfloor \cdot \frac{dX.u}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v\right) \cdot dY.v\right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, dX.u, \left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v\right) \cdot dX.v\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.u \cdot \left\lfloor w\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, dX.v, \left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot dX.u\right), \mathsf{fma}\left(dY.u \cdot \left\lfloor w\right\rfloor , dY.u \cdot \left\lfloor w\right\rfloor , \left(dY.v \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dY.v \cdot \left\lfloor h\right\rfloor \right)\right)\right)}}\\ \end{array} \]
9. Add Preprocessing

Reproduce

herbie shell --seed 2026084 
(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :name "Anisotropic x16 LOD (line direction, u)"
  :precision binary32
  :pre (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0)) (and (<= 1.0 h) (<= h 16384.0))) (and (<= 1e-20 (fabs dX.u)) (<= (fabs dX.u) 1e+20))) (and (<= 1e-20 (fabs dX.v)) (<= (fabs dX.v) 1e+20))) (and (<= 1e-20 (fabs dY.u)) (<= (fabs dY.u) 1e+20))) (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20))) (== maxAniso 16.0))
  (if (>= (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (* (/ 1.0 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))))) (* (floor w) dX.u)) (* (/ 1.0 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))))) (* (floor w) dY.u))))