Anisotropic x16 LOD (line direction, v)

Percentage Accurate: 77.2% → 77.5%

Time: 11.4s

Alternatives: 10

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\_0\\ \mathbf{else}:\\ \;\;\;\;t\_6 \cdot 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 (* (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_0) (* t_6 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 = 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_0;
	} else {
		tmp = t_6 * 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(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_0);
	else
		tmp = Float32(t_6 * t_4);
	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_0;
	else
		tmp = t_6 * t_4;
	end
	tmp_2 = tmp;
end

Initial Program: 77.2% 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\_0\\ \mathbf{else}:\\ \;\;\;\;t\_6 \cdot 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 (* (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_0) (* t_6 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 = 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_0;
	} else {
		tmp = t_6 * 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(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_0);
	else
		tmp = Float32(t_6 * t_4);
	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_0;
	else
		tmp = t_6 * t_4;
	end
	tmp_2 = tmp;
end

Alternative 1: 77.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 := 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\_4}{t\_6}\\ \mathbf{else}:\\ \;\;\;\;\frac{t\_0}{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_4 t_6) (/ t_0 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_4 / t_6;
	} else {
		tmp = t_0 / 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_4 / t_6);
	else
		tmp = Float32(t_0 / t_6);
	end
	return tmp
end

Derivation

1. Initial program 77.2%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

3. Applied rewrites 77.5%

   \[\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.v \cdot \left\lfloor h\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.v \cdot \left\lfloor h\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: 77.3% 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 := \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \\ 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 := dX.v \cdot \left\lfloor h\right\rfloor \\ t_5 := dX.u \cdot \left\lfloor w\right\rfloor \\ t_6 := \mathsf{fma}\left(t\_4, t\_4, t\_5 \cdot t\_5\right)\\ \mathbf{if}\;t\_6 \geq t\_3:\\ \;\;\;\;\frac{t\_4}{\sqrt{\mathsf{max}\left(t\_3, t\_6\right)}}\\ \mathbf{else}:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dY.v}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot t\_1\right), \mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, dX.v, \left(t\_1 \cdot dX.u\right) \cdot dX.u\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.v (floor h)))
       (t_1 (* (floor w) (floor w)))
       (t_2 (* dY.u (floor w)))
       (t_3 (fma t_0 t_0 (* t_2 t_2)))
       (t_4 (* dX.v (floor h)))
       (t_5 (* dX.u (floor w)))
       (t_6 (fma t_4 t_4 (* t_5 t_5))))
  (if (>= t_6 t_3)
    (/ t_4 (sqrt (fmax t_3 t_6)))
    (*
     (floor h)
     (/
      dY.v
      (sqrt
       (fmax
        (fma
         (* (* dY.v dY.v) (floor h))
         (floor h)
         (* (* dY.u dY.u) t_1))
        (fma
         (* (* (floor h) (floor h)) dX.v)
         dX.v
         (* (* t_1 dX.u) dX.u)))))))))

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 = floorf(w) * floorf(w);
	float t_2 = dY_46_u * floorf(w);
	float t_3 = fmaf(t_0, t_0, (t_2 * t_2));
	float t_4 = dX_46_v * floorf(h);
	float t_5 = dX_46_u * floorf(w);
	float t_6 = fmaf(t_4, t_4, (t_5 * t_5));
	float tmp;
	if (t_6 >= t_3) {
		tmp = t_4 / sqrtf(fmaxf(t_3, t_6));
	} else {
		tmp = floorf(h) * (dY_46_v / sqrtf(fmaxf(fmaf(((dY_46_v * dY_46_v) * floorf(h)), floorf(h), ((dY_46_u * dY_46_u) * t_1)), fmaf(((floorf(h) * floorf(h)) * dX_46_v), dX_46_v, ((t_1 * dX_46_u) * dX_46_u)))));
	}
	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(floor(w) * floor(w))
	t_2 = Float32(dY_46_u * floor(w))
	t_3 = fma(t_0, t_0, Float32(t_2 * t_2))
	t_4 = Float32(dX_46_v * floor(h))
	t_5 = Float32(dX_46_u * floor(w))
	t_6 = fma(t_4, t_4, Float32(t_5 * t_5))
	tmp = Float32(0.0)
	if (t_6 >= t_3)
		tmp = Float32(t_4 / sqrt(fmax(t_3, t_6)));
	else
		tmp = Float32(floor(h) * Float32(dY_46_v / sqrt(fmax(fma(Float32(Float32(dY_46_v * dY_46_v) * floor(h)), floor(h), Float32(Float32(dY_46_u * dY_46_u) * t_1)), fma(Float32(Float32(floor(h) * floor(h)) * dX_46_v), dX_46_v, Float32(Float32(t_1 * dX_46_u) * dX_46_u))))));
	end
	return tmp
end

Derivation

1. Initial program 77.2%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

3. Applied rewrites 77.5%

   \[\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.v \cdot \left\lfloor h\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.v \cdot \left\lfloor h\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} \]

5. Applied rewrites 77.3%

   \[\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.v \cdot \left\lfloor h\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}:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dY.v}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)\right), \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)\right)}}\\ \end{array} \]
6. Add Preprocessing

Alternative 3: 77.3% 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 := \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \\ 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 := dX.v \cdot \left\lfloor h\right\rfloor \\ t_5 := dX.u \cdot \left\lfloor w\right\rfloor \\ t_6 := \mathsf{fma}\left(t\_4, t\_4, t\_5 \cdot t\_5\right)\\ \mathbf{if}\;t\_6 \geq t\_3:\\ \;\;\;\;\frac{t\_4}{\sqrt{\mathsf{max}\left(t\_3, t\_6\right)}}\\ \mathbf{else}:\\ \;\;\;\;dY.v \cdot \frac{\left\lfloor h\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot t\_1\right), \mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, dX.v, \left(t\_1 \cdot dX.u\right) \cdot dX.u\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.v (floor h)))
       (t_1 (* (floor w) (floor w)))
       (t_2 (* dY.u (floor w)))
       (t_3 (fma t_0 t_0 (* t_2 t_2)))
       (t_4 (* dX.v (floor h)))
       (t_5 (* dX.u (floor w)))
       (t_6 (fma t_4 t_4 (* t_5 t_5))))
  (if (>= t_6 t_3)
    (/ t_4 (sqrt (fmax t_3 t_6)))
    (*
     dY.v
     (/
      (floor h)
      (sqrt
       (fmax
        (fma
         (* (* dY.v dY.v) (floor h))
         (floor h)
         (* (* dY.u dY.u) t_1))
        (fma
         (* (* (floor h) (floor h)) dX.v)
         dX.v
         (* (* t_1 dX.u) dX.u)))))))))

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 = floorf(w) * floorf(w);
	float t_2 = dY_46_u * floorf(w);
	float t_3 = fmaf(t_0, t_0, (t_2 * t_2));
	float t_4 = dX_46_v * floorf(h);
	float t_5 = dX_46_u * floorf(w);
	float t_6 = fmaf(t_4, t_4, (t_5 * t_5));
	float tmp;
	if (t_6 >= t_3) {
		tmp = t_4 / sqrtf(fmaxf(t_3, t_6));
	} else {
		tmp = dY_46_v * (floorf(h) / sqrtf(fmaxf(fmaf(((dY_46_v * dY_46_v) * floorf(h)), floorf(h), ((dY_46_u * dY_46_u) * t_1)), fmaf(((floorf(h) * floorf(h)) * dX_46_v), dX_46_v, ((t_1 * dX_46_u) * dX_46_u)))));
	}
	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(floor(w) * floor(w))
	t_2 = Float32(dY_46_u * floor(w))
	t_3 = fma(t_0, t_0, Float32(t_2 * t_2))
	t_4 = Float32(dX_46_v * floor(h))
	t_5 = Float32(dX_46_u * floor(w))
	t_6 = fma(t_4, t_4, Float32(t_5 * t_5))
	tmp = Float32(0.0)
	if (t_6 >= t_3)
		tmp = Float32(t_4 / sqrt(fmax(t_3, t_6)));
	else
		tmp = Float32(dY_46_v * Float32(floor(h) / sqrt(fmax(fma(Float32(Float32(dY_46_v * dY_46_v) * floor(h)), floor(h), Float32(Float32(dY_46_u * dY_46_u) * t_1)), fma(Float32(Float32(floor(h) * floor(h)) * dX_46_v), dX_46_v, Float32(Float32(t_1 * dX_46_u) * dX_46_u))))));
	end
	return tmp
end

Derivation

1. Initial program 77.2%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

3. Applied rewrites 77.5%

   \[\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.v \cdot \left\lfloor h\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.v \cdot \left\lfloor h\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} \]

5. Applied rewrites 77.3%

   \[\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.v \cdot \left\lfloor h\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}:\\ \;\;\;\;dY.v \cdot \frac{\left\lfloor h\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)\right), \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)\right)}}\\ \end{array} \]
6. Add Preprocessing

Alternative 4: 59.1% accurate, 0.3× 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 0\right\rfloor \\ t_1 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_2 := dX.v \cdot \left\lfloor h\right\rfloor \\ t_3 := \left\lfloor 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \\ t_4 := \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \\ t_5 := \mathsf{fma}\left(t\_2, t\_2, \left(dX.u \cdot dX.u\right) \cdot t\_3\right)\\ t_6 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_7 := \left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \\ t_8 := \sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_7, \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot t\_4\right), \mathsf{fma}\left(dX.u, t\_4 \cdot dX.u, t\_2 \cdot t\_2\right)\right)}\\ t_9 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_10 := t\_6 \cdot t\_6 + t\_9 \cdot t\_9\\ t_11 := \left\lfloor w\right\rfloor \cdot dX.u\\ t_12 := t\_11 \cdot t\_11 + t\_1 \cdot t\_1\\ t_13 := \frac{1}{\sqrt{\mathsf{max}\left(t\_12, t\_10\right)}}\\ t_14 := \begin{array}{l} \mathbf{if}\;t\_12 \geq t\_10:\\ \;\;\;\;t\_13 \cdot t\_1\\ \mathbf{else}:\\ \;\;\;\;t\_13 \cdot t\_9\\ \end{array}\\ t_15 := dY.v \cdot \left\lfloor h\right\rfloor \\ t_16 := \mathsf{fma}\left(t\_15, t\_15, t\_0 \cdot t\_0\right)\\ t_17 := \begin{array}{l} \mathbf{if}\;t\_5 \geq t\_16:\\ \;\;\;\;\frac{t\_2}{\sqrt{\mathsf{max}\left(t\_16, t\_5\right)}}\\ \mathbf{else}:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dY.v}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_7, \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot t\_3\right), \mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, dX.v, \left(t\_3 \cdot dX.u\right) \cdot dX.u\right)\right)}}\\ \end{array}\\ \mathbf{if}\;t\_14 \leq -0.9980000257492065:\\ \;\;\;\;t\_17\\ \mathbf{elif}\;t\_14 \leq 0.9999899864196777:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{t\_2}{t\_8}\\ \mathbf{else}:\\ \;\;\;\;\frac{t\_15}{t\_8}\\ \end{array}\\ \mathbf{else}:\\ \;\;\;\;t\_17\\ \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 0.0)))
       (t_1 (* (floor h) dX.v))
       (t_2 (* dX.v (floor h)))
       (t_3 (* (floor 0.0) (floor 0.0)))
       (t_4 (* (floor w) (floor w)))
       (t_5 (fma t_2 t_2 (* (* dX.u dX.u) t_3)))
       (t_6 (* (floor w) dY.u))
       (t_7 (* (* dY.v dY.v) (floor h)))
       (t_8
        (sqrt
         (fmax
          (fma t_7 (floor h) (* (* dY.u dY.u) t_4))
          (fma dX.u (* t_4 dX.u) (* t_2 t_2)))))
       (t_9 (* (floor h) dY.v))
       (t_10 (+ (* t_6 t_6) (* t_9 t_9)))
       (t_11 (* (floor w) dX.u))
       (t_12 (+ (* t_11 t_11) (* t_1 t_1)))
       (t_13 (/ 1.0 (sqrt (fmax t_12 t_10))))
       (t_14 (if (>= t_12 t_10) (* t_13 t_1) (* t_13 t_9)))
       (t_15 (* dY.v (floor h)))
       (t_16 (fma t_15 t_15 (* t_0 t_0)))
       (t_17
        (if (>= t_5 t_16)
          (/ t_2 (sqrt (fmax t_16 t_5)))
          (*
           (floor h)
           (/
            dY.v
            (sqrt
             (fmax
              (fma t_7 (floor h) (* (* dY.u dY.u) t_3))
              (fma
               (* (* (floor h) (floor h)) dX.v)
               dX.v
               (* (* t_3 dX.u) dX.u)))))))))
  (if (<= t_14 -0.9980000257492065)
    t_17
    (if (<= t_14 0.9999899864196777)
      (if 0 (/ t_2 t_8) (/ t_15 t_8))
      t_17))))

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(0.0f);
	float t_1 = floorf(h) * dX_46_v;
	float t_2 = dX_46_v * floorf(h);
	float t_3 = floorf(0.0f) * floorf(0.0f);
	float t_4 = floorf(w) * floorf(w);
	float t_5 = fmaf(t_2, t_2, ((dX_46_u * dX_46_u) * t_3));
	float t_6 = floorf(w) * dY_46_u;
	float t_7 = (dY_46_v * dY_46_v) * floorf(h);
	float t_8 = sqrtf(fmaxf(fmaf(t_7, floorf(h), ((dY_46_u * dY_46_u) * t_4)), fmaf(dX_46_u, (t_4 * dX_46_u), (t_2 * t_2))));
	float t_9 = floorf(h) * dY_46_v;
	float t_10 = (t_6 * t_6) + (t_9 * t_9);
	float t_11 = floorf(w) * dX_46_u;
	float t_12 = (t_11 * t_11) + (t_1 * t_1);
	float t_13 = 1.0f / sqrtf(fmaxf(t_12, t_10));
	float tmp;
	if (t_12 >= t_10) {
		tmp = t_13 * t_1;
	} else {
		tmp = t_13 * t_9;
	}
	float t_14 = tmp;
	float t_15 = dY_46_v * floorf(h);
	float t_16 = fmaf(t_15, t_15, (t_0 * t_0));
	float tmp_1;
	if (t_5 >= t_16) {
		tmp_1 = t_2 / sqrtf(fmaxf(t_16, t_5));
	} else {
		tmp_1 = floorf(h) * (dY_46_v / sqrtf(fmaxf(fmaf(t_7, floorf(h), ((dY_46_u * dY_46_u) * t_3)), fmaf(((floorf(h) * floorf(h)) * dX_46_v), dX_46_v, ((t_3 * dX_46_u) * dX_46_u)))));
	}
	float t_17 = tmp_1;
	float tmp_2;
	if (t_14 <= -0.9980000257492065f) {
		tmp_2 = t_17;
	} else if (t_14 <= 0.9999899864196777f) {
		float tmp_3;
		if (0.0f) {
			tmp_3 = t_2 / t_8;
		} else {
			tmp_3 = t_15 / t_8;
		}
		tmp_2 = tmp_3;
	} else {
		tmp_2 = t_17;
	}
	return tmp_2;
}

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(Float32(0.0)))
	t_1 = Float32(floor(h) * dX_46_v)
	t_2 = Float32(dX_46_v * floor(h))
	t_3 = Float32(floor(Float32(0.0)) * floor(Float32(0.0)))
	t_4 = Float32(floor(w) * floor(w))
	t_5 = fma(t_2, t_2, Float32(Float32(dX_46_u * dX_46_u) * t_3))
	t_6 = Float32(floor(w) * dY_46_u)
	t_7 = Float32(Float32(dY_46_v * dY_46_v) * floor(h))
	t_8 = sqrt(fmax(fma(t_7, floor(h), Float32(Float32(dY_46_u * dY_46_u) * t_4)), fma(dX_46_u, Float32(t_4 * dX_46_u), Float32(t_2 * t_2))))
	t_9 = Float32(floor(h) * dY_46_v)
	t_10 = Float32(Float32(t_6 * t_6) + Float32(t_9 * t_9))
	t_11 = Float32(floor(w) * dX_46_u)
	t_12 = Float32(Float32(t_11 * t_11) + Float32(t_1 * t_1))
	t_13 = Float32(Float32(1.0) / sqrt(fmax(t_12, t_10)))
	tmp = Float32(0.0)
	if (t_12 >= t_10)
		tmp = Float32(t_13 * t_1);
	else
		tmp = Float32(t_13 * t_9);
	end
	t_14 = tmp
	t_15 = Float32(dY_46_v * floor(h))
	t_16 = fma(t_15, t_15, Float32(t_0 * t_0))
	tmp_1 = Float32(0.0)
	if (t_5 >= t_16)
		tmp_1 = Float32(t_2 / sqrt(fmax(t_16, t_5)));
	else
		tmp_1 = Float32(floor(h) * Float32(dY_46_v / sqrt(fmax(fma(t_7, floor(h), Float32(Float32(dY_46_u * dY_46_u) * t_3)), fma(Float32(Float32(floor(h) * floor(h)) * dX_46_v), dX_46_v, Float32(Float32(t_3 * dX_46_u) * dX_46_u))))));
	end
	t_17 = tmp_1
	tmp_2 = Float32(0.0)
	if (t_14 <= Float32(-0.9980000257492065))
		tmp_2 = t_17;
	elseif (t_14 <= Float32(0.9999899864196777))
		tmp_3 = Float32(0.0)
		if (Float32(0.0))
			tmp_3 = Float32(t_2 / t_8);
		else
			tmp_3 = Float32(t_15 / t_8);
		end
		tmp_2 = tmp_3;
	else
		tmp_2 = t_17;
	end
	return tmp_2
end

Derivation

1. Split input into 2 regimes

2. if (if.f32 (>=.f32 (+.f32 (*.f32 (*.f32 (floor.f32 w) dX.u) (*.f32 (floor.f32 w) dX.u)) (*.f32 (*.f32 (floor.f32 h) dX.v) (*.f32 (floor.f32 h) dX.v))) (+.f32 (*.f32 (*.f32 (floor.f32 w) dY.u) (*.f32 (floor.f32 w) dY.u)) (*.f32 (*.f32 (floor.f32 h) dY.v) (*.f32 (floor.f32 h) dY.v)))) (*.f32 (/.f32 #s(literal 1 binary32) (sqrt.f32 (fmax.f32 (+.f32 (*.f32 (*.f32 (floor.f32 w) dX.u) (*.f32 (floor.f32 w) dX.u)) (*.f32 (*.f32 (floor.f32 h) dX.v) (*.f32 (floor.f32 h) dX.v))) (+.f32 (*.f32 (*.f32 (floor.f32 w) dY.u) (*.f32 (floor.f32 w) dY.u)) (*.f32 (*.f32 (floor.f32 h) dY.v) (*.f32 (floor.f32 h) dY.v)))))) (*.f32 (floor.f32 h) dX.v)) (*.f32 (/.f32 #s(literal 1 binary32) (sqrt.f32 (fmax.f32 (+.f32 (*.f32 (*.f32 (floor.f32 w) dX.u) (*.f32 (floor.f32 w) dX.u)) (*.f32 (*.f32 (floor.f32 h) dX.v) (*.f32 (floor.f32 h) dX.v))) (+.f32 (*.f32 (*.f32 (floor.f32 w) dY.u) (*.f32 (floor.f32 w) dY.u)) (*.f32 (*.f32 (floor.f32 h) dY.v) (*.f32 (floor.f32 h) dY.v)))))) (*.f32 (floor.f32 h) dY.v))) < -0.998000026 or 0.999989986 < (if.f32 (>=.f32 (+.f32 (*.f32 (*.f32 (floor.f32 w) dX.u) (*.f32 (floor.f32 w) dX.u)) (*.f32 (*.f32 (floor.f32 h) dX.v) (*.f32 (floor.f32 h) dX.v))) (+.f32 (*.f32 (*.f32 (floor.f32 w) dY.u) (*.f32 (floor.f32 w) dY.u)) (*.f32 (*.f32 (floor.f32 h) dY.v) (*.f32 (floor.f32 h) dY.v)))) (*.f32 (/.f32 #s(literal 1 binary32) (sqrt.f32 (fmax.f32 (+.f32 (*.f32 (*.f32 (floor.f32 w) dX.u) (*.f32 (floor.f32 w) dX.u)) (*.f32 (*.f32 (floor.f32 h) dX.v) (*.f32 (floor.f32 h) dX.v))) (+.f32 (*.f32 (*.f32 (floor.f32 w) dY.u) (*.f32 (floor.f32 w) dY.u)) (*.f32 (*.f32 (floor.f32 h) dY.v) (*.f32 (floor.f32 h) dY.v)))))) (*.f32 (floor.f32 h) dX.v)) (*.f32 (/.f32 #s(literal 1 binary32) (sqrt.f32 (fmax.f32 (+.f32 (*.f32 (*.f32 (floor.f32 w) dX.u) (*.f32 (floor.f32 w) dX.u)) (*.f32 (*.f32 (floor.f32 h) dX.v) (*.f32 (floor.f32 h) dX.v))) (+.f32 (*.f32 (*.f32 (floor.f32 w) dY.u) (*.f32 (floor.f32 w) dY.u)) (*.f32 (*.f32 (floor.f32 h) dY.v) (*.f32 (floor.f32 h) dY.v)))))) (*.f32 (floor.f32 h) dY.v)))

   1. Initial program 77.2%

      \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

   3. Applied rewrites 77.5%

      \[\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.v \cdot \left\lfloor h\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.v \cdot \left\lfloor h\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} \]

   5. Applied rewrites 77.3%

      \[\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.v \cdot \left\lfloor h\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}:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dY.v}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)\right), \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)\right)}}\\ \end{array} \]

   6. Taylor expanded in undef-var around zero

      \[\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 0\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor 0\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 0\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor 0\right\rfloor \right)\right):\\ \;\;\;\;\frac{dX.v \cdot \left\lfloor h\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 0\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor 0\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 0\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor 0\right\rfloor \right)\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dY.v}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right)\right), \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 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot dX.u\right)\right)}}\\ \end{array} \]
   7. Step-by-step derivation

   8. Applied rewrites 42.4%

      \[\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 0\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor 0\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 0\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor 0\right\rfloor \right)\right):\\ \;\;\;\;\frac{dX.v \cdot \left\lfloor h\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 0\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor 0\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 0\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor 0\right\rfloor \right)\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dY.v}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right)\right), \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 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot dX.u\right)\right)}}\\ \end{array} \]
   9. Step-by-step derivation

   10. Applied rewrites 42.3%

       \[\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 dX.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot \left\lfloor 0\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 0\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor 0\right\rfloor \right)\right):\\ \;\;\;\;\frac{dX.v \cdot \left\lfloor h\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 0\right\rfloor \right) \cdot \left(dY.u \cdot \left\lfloor 0\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 dX.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right)\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dY.v}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right)\right), \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 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot dX.u\right)\right)}}\\ \end{array} \]

   if -0.998000026 < (if.f32 (>=.f32 (+.f32 (*.f32 (*.f32 (floor.f32 w) dX.u) (*.f32 (floor.f32 w) dX.u)) (*.f32 (*.f32 (floor.f32 h) dX.v) (*.f32 (floor.f32 h) dX.v))) (+.f32 (*.f32 (*.f32 (floor.f32 w) dY.u) (*.f32 (floor.f32 w) dY.u)) (*.f32 (*.f32 (floor.f32 h) dY.v) (*.f32 (floor.f32 h) dY.v)))) (*.f32 (/.f32 #s(literal 1 binary32) (sqrt.f32 (fmax.f32 (+.f32 (*.f32 (*.f32 (floor.f32 w) dX.u) (*.f32 (floor.f32 w) dX.u)) (*.f32 (*.f32 (floor.f32 h) dX.v) (*.f32 (floor.f32 h) dX.v))) (+.f32 (*.f32 (*.f32 (floor.f32 w) dY.u) (*.f32 (floor.f32 w) dY.u)) (*.f32 (*.f32 (floor.f32 h) dY.v) (*.f32 (floor.f32 h) dY.v)))))) (*.f32 (floor.f32 h) dX.v)) (*.f32 (/.f32 #s(literal 1 binary32) (sqrt.f32 (fmax.f32 (+.f32 (*.f32 (*.f32 (floor.f32 w) dX.u) (*.f32 (floor.f32 w) dX.u)) (*.f32 (*.f32 (floor.f32 h) dX.v) (*.f32 (floor.f32 h) dX.v))) (+.f32 (*.f32 (*.f32 (floor.f32 w) dY.u) (*.f32 (floor.f32 w) dY.u)) (*.f32 (*.f32 (floor.f32 h) dY.v) (*.f32 (floor.f32 h) dY.v)))))) (*.f32 (floor.f32 h) dY.v))) < 0.999989986

   1. Initial program 77.2%

      \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
   3. Step-by-step derivation

   4. Applied rewrites 42.9%

      \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

   6. Applied rewrites 42.9%

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

   8. Applied rewrites 43.0%

      \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{dX.v \cdot \left\lfloor h\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)\right), \mathsf{fma}\left(dX.u, \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \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.v \cdot \left\lfloor h\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)\right), \mathsf{fma}\left(dX.u, \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u, \left(dX.v \cdot \left\lfloor h\right\rfloor \right) \cdot \left(dX.v \cdot \left\lfloor h\right\rfloor \right)\right)\right)}}\\ \end{array} \]
3. Recombined 2 regimes into one program.
4. 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 := \left\lfloor w\right\rfloor \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.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot t\_0\right), \mathsf{fma}\left(dX.u, t\_0 \cdot dX.u, t\_1 \cdot t\_1\right)\right)}\\ \mathbf{if}\;0:\\ \;\;\;\;\frac{t\_1}{t\_2}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.v \cdot \left\lfloor h\right\rfloor }{t\_2}\\ \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 w) (floor w)))
       (t_1 (* dX.v (floor h)))
       (t_2
        (sqrt
         (fmax
          (fma
           (* (* dY.v dY.v) (floor h))
           (floor h)
           (* (* dY.u dY.u) t_0))
          (fma dX.u (* t_0 dX.u) (* t_1 t_1))))))
  (if 0 (/ t_1 t_2) (/ (* dY.v (floor h)) 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 = floorf(w) * floorf(w);
	float t_1 = dX_46_v * floorf(h);
	float t_2 = sqrtf(fmaxf(fmaf(((dY_46_v * dY_46_v) * floorf(h)), floorf(h), ((dY_46_u * dY_46_u) * t_0)), fmaf(dX_46_u, (t_0 * dX_46_u), (t_1 * t_1))));
	float tmp;
	if (0.0f) {
		tmp = t_1 / t_2;
	} else {
		tmp = (dY_46_v * floorf(h)) / 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(floor(w) * floor(w))
	t_1 = Float32(dX_46_v * floor(h))
	t_2 = sqrt(fmax(fma(Float32(Float32(dY_46_v * dY_46_v) * floor(h)), floor(h), Float32(Float32(dY_46_u * dY_46_u) * t_0)), fma(dX_46_u, Float32(t_0 * dX_46_u), Float32(t_1 * t_1))))
	tmp = Float32(0.0)
	if (Float32(0.0))
		tmp = Float32(t_1 / t_2);
	else
		tmp = Float32(Float32(dY_46_v * floor(h)) / t_2);
	end
	return tmp
end

Derivation

1. Initial program 77.2%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 42.9%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

6. Applied rewrites 42.9%

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

8. Applied rewrites 43.0%

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

Alternative 6: 42.9% 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 := \sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , dY.u \cdot \left(\left\lfloor w\right\rfloor \cdot \left(dY.u \cdot \left\lfloor w\right\rfloor \right)\right)\right), \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)\right)}\\ \mathbf{if}\;0:\\ \;\;\;\;\frac{dX.v \cdot \left\lfloor h\right\rfloor }{t\_0}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.v \cdot \left\lfloor h\right\rfloor }{t\_0}\\ \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
        (sqrt
         (fmax
          (fma
           (* (* dY.v dY.v) (floor h))
           (floor h)
           (* dY.u (* (floor w) (* dY.u (floor w)))))
          (fma
           (* (* (floor h) (floor h)) dX.v)
           dX.v
           (* (* (* (floor w) (floor w)) dX.u) dX.u))))))
  (if 0 (/ (* dX.v (floor h)) t_0) (/ (* dY.v (floor h)) t_0))))

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 = sqrtf(fmaxf(fmaf(((dY_46_v * dY_46_v) * floorf(h)), floorf(h), (dY_46_u * (floorf(w) * (dY_46_u * floorf(w))))), fmaf(((floorf(h) * floorf(h)) * dX_46_v), dX_46_v, (((floorf(w) * floorf(w)) * dX_46_u) * dX_46_u))));
	float tmp;
	if (0.0f) {
		tmp = (dX_46_v * floorf(h)) / t_0;
	} else {
		tmp = (dY_46_v * floorf(h)) / t_0;
	}
	return tmp;
}

Julia

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

Derivation

1. Initial program 77.2%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 42.9%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

6. Applied rewrites 42.9%

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

8. Applied rewrites 42.9%

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

Alternative 7: 42.9% 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 := \sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.v, t\_0 \cdot dY.v, \left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), \mathsf{fma}\left(t\_0 \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)\right)}\\ \mathbf{if}\;0:\\ \;\;\;\;\frac{dX.v \cdot \left\lfloor h\right\rfloor }{t\_1}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.v \cdot \left\lfloor h\right\rfloor }{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) (floor h)))
       (t_1
        (sqrt
         (fmax
          (fma
           dY.v
           (* t_0 dY.v)
           (* (* (* dY.u dY.u) (floor w)) (floor w)))
          (fma
           (* t_0 dX.v)
           dX.v
           (* (* (* (floor w) (floor w)) dX.u) dX.u))))))
  (if 0 (/ (* dX.v (floor h)) t_1) (/ (* dY.v (floor h)) 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) * floorf(h);
	float t_1 = sqrtf(fmaxf(fmaf(dY_46_v, (t_0 * dY_46_v), (((dY_46_u * dY_46_u) * floorf(w)) * floorf(w))), fmaf((t_0 * dX_46_v), dX_46_v, (((floorf(w) * floorf(w)) * dX_46_u) * dX_46_u))));
	float tmp;
	if (0.0f) {
		tmp = (dX_46_v * floorf(h)) / t_1;
	} else {
		tmp = (dY_46_v * floorf(h)) / 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) * floor(h))
	t_1 = sqrt(fmax(fma(dY_46_v, Float32(t_0 * dY_46_v), Float32(Float32(Float32(dY_46_u * dY_46_u) * floor(w)) * floor(w))), fma(Float32(t_0 * dX_46_v), dX_46_v, Float32(Float32(Float32(floor(w) * floor(w)) * dX_46_u) * dX_46_u))))
	tmp = Float32(0.0)
	if (Float32(0.0))
		tmp = Float32(Float32(dX_46_v * floor(h)) / t_1);
	else
		tmp = Float32(Float32(dY_46_v * floor(h)) / t_1);
	end
	return tmp
end

Derivation

1. Initial program 77.2%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 42.9%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

6. Applied rewrites 42.9%

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

8. Applied rewrites 42.9%

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

Alternative 8: 42.8% 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.v \cdot \left\lfloor h\right\rfloor \\ t_1 := \sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_0 \cdot \left\lfloor h\right\rfloor , dY.v, \left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), \mathsf{fma}\left(dX.v \cdot dX.v, \left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor , \left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dX.u\right) \cdot dX.u\right)\right)}\\ \mathbf{if}\;0:\\ \;\;\;\;\frac{\left\lfloor h\right\rfloor }{t\_1} \cdot dX.v\\ \mathbf{else}:\\ \;\;\;\;\frac{t\_0}{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 (* dY.v (floor h)))
       (t_1
        (sqrt
         (fmax
          (fma
           (* t_0 (floor h))
           dY.v
           (* (* (* dY.u dY.u) (floor w)) (floor w)))
          (fma
           (* dX.v dX.v)
           (* (floor h) (floor h))
           (* (* (* (floor w) (floor w)) dX.u) dX.u))))))
  (if 0 (* (/ (floor h) t_1) dX.v) (/ t_0 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 = dY_46_v * floorf(h);
	float t_1 = sqrtf(fmaxf(fmaf((t_0 * floorf(h)), dY_46_v, (((dY_46_u * dY_46_u) * floorf(w)) * floorf(w))), fmaf((dX_46_v * dX_46_v), (floorf(h) * floorf(h)), (((floorf(w) * floorf(w)) * dX_46_u) * dX_46_u))));
	float tmp;
	if (0.0f) {
		tmp = (floorf(h) / t_1) * dX_46_v;
	} else {
		tmp = t_0 / 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(dY_46_v * floor(h))
	t_1 = sqrt(fmax(fma(Float32(t_0 * floor(h)), dY_46_v, Float32(Float32(Float32(dY_46_u * dY_46_u) * floor(w)) * floor(w))), fma(Float32(dX_46_v * dX_46_v), Float32(floor(h) * floor(h)), Float32(Float32(Float32(floor(w) * floor(w)) * dX_46_u) * dX_46_u))))
	tmp = Float32(0.0)
	if (Float32(0.0))
		tmp = Float32(Float32(floor(h) / t_1) * dX_46_v);
	else
		tmp = Float32(t_0 / t_1);
	end
	return tmp
end

Derivation

1. Initial program 77.2%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 42.9%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
5. Step-by-step derivation

6. Applied rewrites 42.8%

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

8. Applied rewrites 42.8%

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

10. Applied rewrites 42.8%

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

Alternative 9: 42.8% 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.v \cdot \left\lfloor h\right\rfloor \\ t_1 := \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \\ t_2 := dX.v \cdot \left\lfloor h\right\rfloor \\ t_3 := dX.u \cdot \left\lfloor w\right\rfloor \\ \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dX.v}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_0 \cdot \left\lfloor h\right\rfloor , dY.v, \left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), \mathsf{fma}\left(t\_2, t\_2, t\_3 \cdot t\_3\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t\_0}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot t\_1\right), \mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, dX.v, \left(t\_1 \cdot dX.u\right) \cdot dX.u\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.v (floor h)))
       (t_1 (* (floor w) (floor w)))
       (t_2 (* dX.v (floor h)))
       (t_3 (* dX.u (floor w))))
  (if 0
    (*
     (floor h)
     (/
      dX.v
      (sqrt
       (fmax
        (fma
         (* t_0 (floor h))
         dY.v
         (* (* (* dY.u dY.u) (floor w)) (floor w)))
        (fma t_2 t_2 (* t_3 t_3))))))
    (/
     t_0
     (sqrt
      (fmax
       (fma
        (* (* dY.v dY.v) (floor h))
        (floor h)
        (* (* dY.u dY.u) t_1))
       (fma
        (* (* (floor h) (floor h)) dX.v)
        dX.v
        (* (* t_1 dX.u) dX.u))))))))

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 = floorf(w) * floorf(w);
	float t_2 = dX_46_v * floorf(h);
	float t_3 = dX_46_u * floorf(w);
	float tmp;
	if (0.0f) {
		tmp = floorf(h) * (dX_46_v / sqrtf(fmaxf(fmaf((t_0 * floorf(h)), dY_46_v, (((dY_46_u * dY_46_u) * floorf(w)) * floorf(w))), fmaf(t_2, t_2, (t_3 * t_3)))));
	} else {
		tmp = t_0 / sqrtf(fmaxf(fmaf(((dY_46_v * dY_46_v) * floorf(h)), floorf(h), ((dY_46_u * dY_46_u) * t_1)), fmaf(((floorf(h) * floorf(h)) * dX_46_v), dX_46_v, ((t_1 * dX_46_u) * dX_46_u))));
	}
	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(floor(w) * floor(w))
	t_2 = Float32(dX_46_v * floor(h))
	t_3 = Float32(dX_46_u * floor(w))
	tmp = Float32(0.0)
	if (Float32(0.0))
		tmp = Float32(floor(h) * Float32(dX_46_v / sqrt(fmax(fma(Float32(t_0 * floor(h)), dY_46_v, Float32(Float32(Float32(dY_46_u * dY_46_u) * floor(w)) * floor(w))), fma(t_2, t_2, Float32(t_3 * t_3))))));
	else
		tmp = Float32(t_0 / sqrt(fmax(fma(Float32(Float32(dY_46_v * dY_46_v) * floor(h)), floor(h), Float32(Float32(dY_46_u * dY_46_u) * t_1)), fma(Float32(Float32(floor(h) * floor(h)) * dX_46_v), dX_46_v, Float32(Float32(t_1 * dX_46_u) * dX_46_u)))));
	end
	return tmp
end

Derivation

1. Initial program 77.2%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 42.9%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

6. Applied rewrites 42.9%

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

8. Applied rewrites 42.8%

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

Alternative 10: 25.8% 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 0\right\rfloor \cdot dY.u\\ t_1 := \left\lfloor 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \\ t_2 := \left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \\ t_3 := \left\lfloor 0\right\rfloor \cdot dX.u\\ t_4 := dX.v \cdot \left\lfloor h\right\rfloor \\ \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dX.v}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_0, t\_0, t\_2 \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(t\_3, t\_3, t\_4 \cdot t\_4\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.v \cdot \left\lfloor h\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_2, \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot t\_1\right), \mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, dX.v, \left(t\_1 \cdot dX.u\right) \cdot dX.u\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 (* (floor 0.0) dY.u))
       (t_1 (* (floor 0.0) (floor 0.0)))
       (t_2 (* (* dY.v dY.v) (floor h)))
       (t_3 (* (floor 0.0) dX.u))
       (t_4 (* dX.v (floor h))))
  (if 0
    (*
     (floor h)
     (/
      dX.v
      (sqrt
       (fmax
        (fma t_0 t_0 (* t_2 (floor h)))
        (fma t_3 t_3 (* t_4 t_4))))))
    (/
     (* dY.v (floor h))
     (sqrt
      (fmax
       (fma t_2 (floor h) (* (* dY.u dY.u) t_1))
       (fma
        (* (* (floor h) (floor h)) dX.v)
        dX.v
        (* (* t_1 dX.u) dX.u))))))))

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(0.0f) * dY_46_u;
	float t_1 = floorf(0.0f) * floorf(0.0f);
	float t_2 = (dY_46_v * dY_46_v) * floorf(h);
	float t_3 = floorf(0.0f) * dX_46_u;
	float t_4 = dX_46_v * floorf(h);
	float tmp;
	if (0.0f) {
		tmp = floorf(h) * (dX_46_v / sqrtf(fmaxf(fmaf(t_0, t_0, (t_2 * floorf(h))), fmaf(t_3, t_3, (t_4 * t_4)))));
	} else {
		tmp = (dY_46_v * floorf(h)) / sqrtf(fmaxf(fmaf(t_2, floorf(h), ((dY_46_u * dY_46_u) * t_1)), fmaf(((floorf(h) * floorf(h)) * dX_46_v), dX_46_v, ((t_1 * dX_46_u) * dX_46_u))));
	}
	return tmp;
}

Julia

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

Derivation

1. Initial program 77.2%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
3. Step-by-step derivation

4. Applied rewrites 42.9%

   \[\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 h\right\rfloor \cdot dX.v\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 h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

6. Applied rewrites 42.9%

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

7. Taylor expanded in undef-var around zero

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

9. Applied rewrites 25.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{dX.v \cdot \left\lfloor h\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right)\right), \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 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot dX.u\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.v \cdot \left\lfloor h\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right)\right), \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 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot dX.u\right)\right)}}\\ \end{array} \]

11. Applied rewrites 25.8%

    \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\left\lfloor h\right\rfloor \cdot \frac{dX.v}{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left\lfloor 0\right\rfloor \cdot dY.u, \left\lfloor 0\right\rfloor \cdot dY.u, \left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor \right) \cdot \left\lfloor h\right\rfloor \right), \mathsf{fma}\left(\left\lfloor 0\right\rfloor \cdot dX.u, \left\lfloor 0\right\rfloor \cdot dX.u, \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.v \cdot \left\lfloor h\right\rfloor }{\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.v \cdot dY.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right)\right), \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 0\right\rfloor \cdot \left\lfloor 0\right\rfloor \right) \cdot dX.u\right) \cdot dX.u\right)\right)}}\\ \end{array} \]
12. Add Preprocessing

Reproduce

herbie shell --seed 2026086 
(FPCore (w h dX.u dX.v dY.u dY.v maxAniso)
  :name "Anisotropic x16 LOD (line direction, v)"
  :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 h) dX.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 h) dY.v))))