Anisotropic x16 LOD (line direction, v)

Percentage Accurate: 75.7% → 75.9%

Time: 11.6s

Alternatives: 7

Speedup: 1.0×

Specification

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

Math

\[\begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_2 := \left\lfloor w\right\rfloor \cdot dX.u\\ t_3 := t\_2 \cdot t\_2 + t\_0 \cdot t\_0\\ t_4 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_5 := t\_1 \cdot t\_1 + t\_4 \cdot t\_4\\ t_6 := \frac{1}{\sqrt{\mathsf{max}\left(t\_3, t\_5\right)}}\\ \mathbf{if}\;t\_3 \geq t\_5:\\ \;\;\;\;t\_6 \cdot t\_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: 75.7% accurate, 1.0× speedup

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

Math

\[\begin{array}{l} t_0 := \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: 75.9% accurate, 0.8× 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 := dX.u \cdot \left\lfloor w\right\rfloor \\ t_2 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_3 := \mathsf{fma}\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor , dX.u \cdot dX.u, t\_0 \cdot \left(dX.v \cdot dX.v\right)\right)\\ t_4 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_5 := t\_2 \cdot t\_2 + t\_4 \cdot t\_4\\ t_6 := \left(dY.v \cdot dY.v\right) \cdot t\_0\\ \mathbf{if}\;t\_3 \geq t\_5:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(t\_3, t\_5\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{dY.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, \frac{\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor }{t\_6 \cdot \frac{1}{t\_6}}\right), \mathsf{fma}\left(dX.v \cdot dX.v, t\_0, t\_1 \cdot t\_1\right)\right)}} \cdot \left\lfloor h\right\rfloor \\ \end{array} \]

FPCore

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

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

Julia

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

Derivation

1. Initial program 75.7%

   \[\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. Step-by-step derivation

3. Applied rewrites 75.7%

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

5. Applied rewrites 75.6%

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

7. Applied rewrites 70.5%

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

9. Applied rewrites 75.8%

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

Alternative 2: 75.8% 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 := dX.u \cdot \left\lfloor w\right\rfloor \\ t_1 := dY.v \cdot \left\lfloor h\right\rfloor \\ t_2 := dY.u \cdot \left\lfloor w\right\rfloor \\ t_3 := \mathsf{fma}\left(t\_1, t\_1, t\_2 \cdot t\_2\right)\\ t_4 := dX.v \cdot \left\lfloor h\right\rfloor \\ t_5 := \mathsf{fma}\left(t\_4, t\_4, t\_0 \cdot t\_0\right)\\ t_6 := \sqrt{\mathsf{max}\left(t\_3, t\_5\right)}\\ 1 \cdot \begin{array}{l} \mathbf{if}\;t\_5 \geq t\_3:\\ \;\;\;\;\frac{t\_4}{t\_6}\\ \mathbf{else}:\\ \;\;\;\;\frac{t\_1}{t\_6}\\ \end{array} \end{array} \]

FPCore

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

C

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

Julia

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

Derivation

1. Initial program 75.7%

   \[\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 75.9%

   \[\leadsto 1 \cdot \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 3: 75.6% accurate, 1.0× speedup

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

Math

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

FPCore

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

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

Julia

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

Derivation

1. Initial program 75.7%

   \[\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. Step-by-step derivation

3. Applied rewrites 75.7%

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

5. Applied rewrites 75.6%

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

7. Applied rewrites 75.6%

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

9. Applied rewrites 75.6%

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

Alternative 4: 75.6% accurate, 1.0× speedup

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

Math

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

FPCore

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

C

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

Julia

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

Derivation

1. Initial program 75.7%

   \[\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. Step-by-step derivation

3. Applied rewrites 75.7%

   \[\leadsto \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{dX.v}{\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)}} \cdot \left\lfloor h\right\rfloor \\ \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. Applied rewrites 75.6%

   \[\leadsto \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{dX.v}{\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)}} \cdot \left\lfloor h\right\rfloor \\ \mathbf{else}:\\ \;\;\;\;\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(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)}} \cdot dY.v\\ \end{array} \]

7. Applied rewrites 75.6%

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

9. Applied rewrites 75.6%

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

Alternative 5: 47.4% accurate, 0.6× 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 := t\_0 \cdot t\_0\\ t_2 := \left\lfloor 0\right\rfloor \cdot dX.u\\ t_3 := \frac{1}{\sqrt{\mathsf{max}\left(t\_2 \cdot t\_2 + t\_1, {\left(\left|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor 0\right\rfloor \right)}^{2}\right)}}\\ t_4 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_5 := \left\lfloor w\right\rfloor \cdot dX.u\\ t_6 := t\_5 \cdot t\_5 + t\_1\\ t_7 := \frac{1}{\sqrt{\mathsf{max}\left(t\_6, \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)\right)}}\\ t_8 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_9 := t\_4 \cdot t\_4 + t\_8 \cdot t\_8\\ t_10 := \frac{1}{\sqrt{\mathsf{max}\left(t\_6, t\_9\right)}}\\ \mathbf{if}\;\begin{array}{l} \mathbf{if}\;t\_6 \geq t\_9:\\ \;\;\;\;t\_10 \cdot t\_0\\ \mathbf{else}:\\ \;\;\;\;t\_10 \cdot t\_8\\ \end{array} \leq 0.0020000000949949026:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;t\_7 \cdot t\_0\\ \mathbf{else}:\\ \;\;\;\;t\_7 \cdot t\_8\\ \end{array}\\ \mathbf{elif}\;0:\\ \;\;\;\;t\_3 \cdot t\_0\\ \mathbf{else}:\\ \;\;\;\;t\_3 \cdot t\_8\\ \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 (* t_0 t_0))
       (t_2 (* (floor 0.0) dX.u))
       (t_3
        (/
         1.0
         (sqrt
          (fmax
           (+ (* t_2 t_2) t_1)
           (* (pow (fabs dY.u) 2.0) (pow (floor 0.0) 2.0))))))
       (t_4 (* (floor w) dY.u))
       (t_5 (* (floor w) dX.u))
       (t_6 (+ (* t_5 t_5) t_1))
       (t_7
        (/
         1.0
         (sqrt (fmax t_6 (* (* dY.u dY.u) (* (floor w) (floor w)))))))
       (t_8 (* (floor h) dY.v))
       (t_9 (+ (* t_4 t_4) (* t_8 t_8)))
       (t_10 (/ 1.0 (sqrt (fmax t_6 t_9)))))
  (if (<=
       (if (>= t_6 t_9) (* t_10 t_0) (* t_10 t_8))
       0.0020000000949949026)
    (if 0 (* t_7 t_0) (* t_7 t_8))
    (if 0 (* t_3 t_0) (* t_3 t_8)))))

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 = t_0 * t_0;
	float t_2 = floorf(0.0f) * dX_46_u;
	float t_3 = 1.0f / sqrtf(fmaxf(((t_2 * t_2) + t_1), (powf(fabsf(dY_46_u), 2.0f) * powf(floorf(0.0f), 2.0f))));
	float t_4 = floorf(w) * dY_46_u;
	float t_5 = floorf(w) * dX_46_u;
	float t_6 = (t_5 * t_5) + t_1;
	float t_7 = 1.0f / sqrtf(fmaxf(t_6, ((dY_46_u * dY_46_u) * (floorf(w) * floorf(w)))));
	float t_8 = floorf(h) * dY_46_v;
	float t_9 = (t_4 * t_4) + (t_8 * t_8);
	float t_10 = 1.0f / sqrtf(fmaxf(t_6, t_9));
	float tmp;
	if (t_6 >= t_9) {
		tmp = t_10 * t_0;
	} else {
		tmp = t_10 * t_8;
	}
	float tmp_2;
	if (tmp <= 0.0020000000949949026f) {
		float tmp_3;
		if (0.0f) {
			tmp_3 = t_7 * t_0;
		} else {
			tmp_3 = t_7 * t_8;
		}
		tmp_2 = tmp_3;
	} else if (0.0f) {
		tmp_2 = t_3 * t_0;
	} else {
		tmp_2 = t_3 * t_8;
	}
	return tmp_2;
}

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(t_0 * t_0)
	t_2 = Float32(floor(Float32(0.0)) * dX_46_u)
	t_3 = Float32(Float32(1.0) / sqrt(fmax(Float32(Float32(t_2 * t_2) + t_1), Float32((abs(dY_46_u) ^ Float32(2.0)) * (floor(Float32(0.0)) ^ Float32(2.0))))))
	t_4 = Float32(floor(w) * dY_46_u)
	t_5 = Float32(floor(w) * dX_46_u)
	t_6 = Float32(Float32(t_5 * t_5) + t_1)
	t_7 = Float32(Float32(1.0) / sqrt(fmax(t_6, Float32(Float32(dY_46_u * dY_46_u) * Float32(floor(w) * floor(w))))))
	t_8 = Float32(floor(h) * dY_46_v)
	t_9 = Float32(Float32(t_4 * t_4) + Float32(t_8 * t_8))
	t_10 = Float32(Float32(1.0) / sqrt(fmax(t_6, t_9)))
	tmp = Float32(0.0)
	if (t_6 >= t_9)
		tmp = Float32(t_10 * t_0);
	else
		tmp = Float32(t_10 * t_8);
	end
	tmp_2 = Float32(0.0)
	if (tmp <= Float32(0.0020000000949949026))
		tmp_3 = Float32(0.0)
		if (Float32(0.0))
			tmp_3 = Float32(t_7 * t_0);
		else
			tmp_3 = Float32(t_7 * t_8);
		end
		tmp_2 = tmp_3;
	elseif (Float32(0.0))
		tmp_2 = Float32(t_3 * t_0);
	else
		tmp_2 = Float32(t_3 * t_8);
	end
	return tmp_2
end

MATLAB

function tmp_5 = 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 = t_0 * t_0;
	t_2 = floor(single(0.0)) * dX_46_u;
	t_3 = single(1.0) / sqrt(max(((t_2 * t_2) + t_1), ((abs(dY_46_u) ^ single(2.0)) * (floor(single(0.0)) ^ single(2.0)))));
	t_4 = floor(w) * dY_46_u;
	t_5 = floor(w) * dX_46_u;
	t_6 = (t_5 * t_5) + t_1;
	t_7 = single(1.0) / sqrt(max(t_6, ((dY_46_u * dY_46_u) * (floor(w) * floor(w)))));
	t_8 = floor(h) * dY_46_v;
	t_9 = (t_4 * t_4) + (t_8 * t_8);
	t_10 = single(1.0) / sqrt(max(t_6, t_9));
	tmp = single(0.0);
	if (t_6 >= t_9)
		tmp = t_10 * t_0;
	else
		tmp = t_10 * t_8;
	end
	tmp_3 = single(0.0);
	if (tmp <= single(0.0020000000949949026))
		tmp_4 = single(0.0);
		if (single(0.0))
			tmp_4 = t_7 * t_0;
		else
			tmp_4 = t_7 * t_8;
		end
		tmp_3 = tmp_4;
	elseif (single(0.0))
		tmp_3 = t_3 * t_0;
	else
		tmp_3 = t_3 * t_8;
	end
	tmp_5 = tmp_3;
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.00200000009

   1. Initial program 75.7%

      \[\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.5%

      \[\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.5%

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

   7. Taylor expanded in dY.v around 0

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

   9. Applied rewrites 46.1%

      \[\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|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\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|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
   10. Step-by-step derivation

   11. Applied rewrites 46.1%

       \[\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(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \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(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

   if 0.00200000009 < (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 75.7%

      \[\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.5%

      \[\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.5%

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

   7. Taylor expanded in dY.v around 0

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

   9. Applied rewrites 46.1%

      \[\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|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\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|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

   10. Taylor expanded in undef-var around zero

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

   12. Applied rewrites 35.9%

       \[\leadsto \begin{array}{l} \mathbf{if}\;0:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor 0\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor 0\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|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor 0\right\rfloor \right)}^{2}\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dX.v\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{\mathsf{max}\left(\left(\left\lfloor 0\right\rfloor \cdot dX.u\right) \cdot \left(\left\lfloor 0\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|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor 0\right\rfloor \right)}^{2}\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 6: 46.1% accurate, 2.2× 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 dX.u\\ t_1 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_2 := \frac{1}{\sqrt{\mathsf{max}\left(t\_0 \cdot t\_0 + t\_1 \cdot t\_1, \left(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)\right)}}\\ \mathbf{if}\;0:\\ \;\;\;\;t\_2 \cdot t\_1\\ \mathbf{else}:\\ \;\;\;\;t\_2 \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\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 w) dX.u))
       (t_1 (* (floor h) dX.v))
       (t_2
        (/
         1.0
         (sqrt
          (fmax
           (+ (* t_0 t_0) (* t_1 t_1))
           (* (* dY.u dY.u) (* (floor w) (floor w))))))))
  (if 0 (* t_2 t_1) (* t_2 (* (floor h) dY.v)))))

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

Derivation

1. Initial program 75.7%

   \[\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.5%

   \[\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.5%

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

7. Taylor expanded in dY.v around 0

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

9. Applied rewrites 46.1%

   \[\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|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\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|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
10. Step-by-step derivation

11. Applied rewrites 46.1%

    \[\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(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \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(dY.u \cdot dY.u\right) \cdot \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right)\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]
12. Add Preprocessing

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

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

Derivation

1. Initial program 75.7%

   \[\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.5%

   \[\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.5%

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

7. Taylor expanded in dY.v around 0

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

9. Applied rewrites 46.1%

   \[\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|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\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|dY.u\right|\right)}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}} \cdot \left(\left\lfloor h\right\rfloor \cdot dY.v\right)\\ \end{array} \]

11. Applied rewrites 46.0%

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

Reproduce

herbie shell --seed 2026070 
(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))))