Isotropic LOD (LOD)

Percentage Accurate: 68.2% → 70.9%

Time: 11.3s

Alternatives: 7

Speedup: 0.5×

Specification

\[\left(\left(\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(1 \leq d \land d \leq 4096\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|dX.w\right| \land \left|dX.w\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 \left(10^{-20} \leq \left|dY.w\right| \land \left|dY.w\right| \leq 10^{+20}\right)\]

Math

\[\begin{array}{l} t_0 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_1 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_2 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_3 := \left\lfloor d\right\rfloor \cdot dY.w\\ t_4 := \left\lfloor d\right\rfloor \cdot dX.w\\ t_5 := \left\lfloor w\right\rfloor \cdot dX.u\\ \log_{2} \left(\sqrt{\mathsf{max}\left(\left(t\_5 \cdot t\_5 + t\_2 \cdot t\_2\right) + t\_4 \cdot t\_4, \left(t\_0 \cdot t\_0 + t\_1 \cdot t\_1\right) + t\_3 \cdot t\_3\right)}\right) \end{array} \]

FPCore

(FPCore (w h d dX.u dX.v dX.w dY.u dY.v dY.w)
  :precision binary32
  :pre (and (and (and (and (and (and (and (and (and (<= 1.0 w)
                                             (<= w 16384.0))
                                        (and (<= 1.0 h)
                                             (<= h 16384.0)))
                                   (and (<= 1.0 d)
                                        (<= d 4096.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 dX.w))
                         (<= (fabs dX.w) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (and (<= 1e-20 (fabs dY.w)) (<= (fabs dY.w) 1e+20)))
  (let* ((t_0 (* (floor w) dY.u))
       (t_1 (* (floor h) dY.v))
       (t_2 (* (floor h) dX.v))
       (t_3 (* (floor d) dY.w))
       (t_4 (* (floor d) dX.w))
       (t_5 (* (floor w) dX.u)))
  (log2
   (sqrt
    (fmax
     (+ (+ (* t_5 t_5) (* t_2 t_2)) (* t_4 t_4))
     (+ (+ (* t_0 t_0) (* t_1 t_1)) (* t_3 t_3)))))))

C

float code(float w, float h, float d, float dX_46_u, float dX_46_v, float dX_46_w, float dY_46_u, float dY_46_v, float dY_46_w) {
	float t_0 = floorf(w) * dY_46_u;
	float t_1 = floorf(h) * dY_46_v;
	float t_2 = floorf(h) * dX_46_v;
	float t_3 = floorf(d) * dY_46_w;
	float t_4 = floorf(d) * dX_46_w;
	float t_5 = floorf(w) * dX_46_u;
	return log2f(sqrtf(fmaxf((((t_5 * t_5) + (t_2 * t_2)) + (t_4 * t_4)), (((t_0 * t_0) + (t_1 * t_1)) + (t_3 * t_3)))));
}

Julia

function code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	t_0 = Float32(floor(w) * dY_46_u)
	t_1 = Float32(floor(h) * dY_46_v)
	t_2 = Float32(floor(h) * dX_46_v)
	t_3 = Float32(floor(d) * dY_46_w)
	t_4 = Float32(floor(d) * dX_46_w)
	t_5 = Float32(floor(w) * dX_46_u)
	return log2(sqrt(fmax(Float32(Float32(Float32(t_5 * t_5) + Float32(t_2 * t_2)) + Float32(t_4 * t_4)), Float32(Float32(Float32(t_0 * t_0) + Float32(t_1 * t_1)) + Float32(t_3 * t_3)))))
end

MATLAB

function tmp = code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	t_0 = floor(w) * dY_46_u;
	t_1 = floor(h) * dY_46_v;
	t_2 = floor(h) * dX_46_v;
	t_3 = floor(d) * dY_46_w;
	t_4 = floor(d) * dX_46_w;
	t_5 = floor(w) * dX_46_u;
	tmp = log2(sqrt(max((((t_5 * t_5) + (t_2 * t_2)) + (t_4 * t_4)), (((t_0 * t_0) + (t_1 * t_1)) + (t_3 * t_3)))));
end

Initial Program: 68.2% accurate, 1.0× speedup

\[\left(\left(\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(1 \leq d \land d \leq 4096\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|dX.w\right| \land \left|dX.w\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 \left(10^{-20} \leq \left|dY.w\right| \land \left|dY.w\right| \leq 10^{+20}\right)\]

Math

\[\begin{array}{l} t_0 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_1 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_2 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_3 := \left\lfloor d\right\rfloor \cdot dY.w\\ t_4 := \left\lfloor d\right\rfloor \cdot dX.w\\ t_5 := \left\lfloor w\right\rfloor \cdot dX.u\\ \log_{2} \left(\sqrt{\mathsf{max}\left(\left(t\_5 \cdot t\_5 + t\_2 \cdot t\_2\right) + t\_4 \cdot t\_4, \left(t\_0 \cdot t\_0 + t\_1 \cdot t\_1\right) + t\_3 \cdot t\_3\right)}\right) \end{array} \]

FPCore

(FPCore (w h d dX.u dX.v dX.w dY.u dY.v dY.w)
  :precision binary32
  :pre (and (and (and (and (and (and (and (and (and (<= 1.0 w)
                                             (<= w 16384.0))
                                        (and (<= 1.0 h)
                                             (<= h 16384.0)))
                                   (and (<= 1.0 d)
                                        (<= d 4096.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 dX.w))
                         (<= (fabs dX.w) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (and (<= 1e-20 (fabs dY.w)) (<= (fabs dY.w) 1e+20)))
  (let* ((t_0 (* (floor w) dY.u))
       (t_1 (* (floor h) dY.v))
       (t_2 (* (floor h) dX.v))
       (t_3 (* (floor d) dY.w))
       (t_4 (* (floor d) dX.w))
       (t_5 (* (floor w) dX.u)))
  (log2
   (sqrt
    (fmax
     (+ (+ (* t_5 t_5) (* t_2 t_2)) (* t_4 t_4))
     (+ (+ (* t_0 t_0) (* t_1 t_1)) (* t_3 t_3)))))))

C

float code(float w, float h, float d, float dX_46_u, float dX_46_v, float dX_46_w, float dY_46_u, float dY_46_v, float dY_46_w) {
	float t_0 = floorf(w) * dY_46_u;
	float t_1 = floorf(h) * dY_46_v;
	float t_2 = floorf(h) * dX_46_v;
	float t_3 = floorf(d) * dY_46_w;
	float t_4 = floorf(d) * dX_46_w;
	float t_5 = floorf(w) * dX_46_u;
	return log2f(sqrtf(fmaxf((((t_5 * t_5) + (t_2 * t_2)) + (t_4 * t_4)), (((t_0 * t_0) + (t_1 * t_1)) + (t_3 * t_3)))));
}

Julia

function code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	t_0 = Float32(floor(w) * dY_46_u)
	t_1 = Float32(floor(h) * dY_46_v)
	t_2 = Float32(floor(h) * dX_46_v)
	t_3 = Float32(floor(d) * dY_46_w)
	t_4 = Float32(floor(d) * dX_46_w)
	t_5 = Float32(floor(w) * dX_46_u)
	return log2(sqrt(fmax(Float32(Float32(Float32(t_5 * t_5) + Float32(t_2 * t_2)) + Float32(t_4 * t_4)), Float32(Float32(Float32(t_0 * t_0) + Float32(t_1 * t_1)) + Float32(t_3 * t_3)))))
end

MATLAB

function tmp = code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	t_0 = floor(w) * dY_46_u;
	t_1 = floor(h) * dY_46_v;
	t_2 = floor(h) * dX_46_v;
	t_3 = floor(d) * dY_46_w;
	t_4 = floor(d) * dX_46_w;
	t_5 = floor(w) * dX_46_u;
	tmp = log2(sqrt(max((((t_5 * t_5) + (t_2 * t_2)) + (t_4 * t_4)), (((t_0 * t_0) + (t_1 * t_1)) + (t_3 * t_3)))));
end

Alternative 1: 70.9% accurate, 0.5× speedup

\[\left(\left(\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(1 \leq d \land d \leq 4096\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|dX.w\right| \land \left|dX.w\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 \left(10^{-20} \leq \left|dY.w\right| \land \left|dY.w\right| \leq 10^{+20}\right)\]

Math

\[\begin{array}{l} t_0 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_1 := \left\lfloor d\right\rfloor \cdot dY.w\\ t_2 := \left\lfloor d\right\rfloor \cdot dX.w\\ t_3 := \left\lfloor w\right\rfloor \cdot dX.u\\ t_4 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_5 := \left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w\\ t_6 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_7 := \left(t\_4 \cdot t\_4 + t\_6 \cdot t\_6\right) + t\_1 \cdot t\_1\\ t_8 := dX.u \cdot \left\lfloor w\right\rfloor \\ \mathbf{if}\;\mathsf{max}\left(\left(t\_3 \cdot t\_3 + t\_0 \cdot t\_0\right) + t\_2 \cdot t\_2, t\_7\right) \leq 3.0000000054977558 \cdot 10^{+38}:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dX.v, \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \mathsf{fma}\left(t\_5, dX.w, t\_8 \cdot t\_8\right)\right), t\_7\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_5, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right)\\ \end{array} \]

FPCore

(FPCore (w h d dX.u dX.v dX.w dY.u dY.v dY.w)
  :precision binary32
  :pre (and (and (and (and (and (and (and (and (and (<= 1.0 w)
                                             (<= w 16384.0))
                                        (and (<= 1.0 h)
                                             (<= h 16384.0)))
                                   (and (<= 1.0 d)
                                        (<= d 4096.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 dX.w))
                         (<= (fabs dX.w) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (and (<= 1e-20 (fabs dY.w)) (<= (fabs dY.w) 1e+20)))
  (let* ((t_0 (* (floor h) dX.v))
       (t_1 (* (floor d) dY.w))
       (t_2 (* (floor d) dX.w))
       (t_3 (* (floor w) dX.u))
       (t_4 (* (floor w) dY.u))
       (t_5 (* (* (floor d) (floor d)) dX.w))
       (t_6 (* (floor h) dY.v))
       (t_7 (+ (+ (* t_4 t_4) (* t_6 t_6)) (* t_1 t_1)))
       (t_8 (* dX.u (floor w))))
  (if (<=
       (fmax (+ (+ (* t_3 t_3) (* t_0 t_0)) (* t_2 t_2)) t_7)
       3.0000000054977558e+38)
    (log2
     (sqrt
      (fmax
       (fma
        dX.v
        (* (* (floor h) (floor h)) dX.v)
        (fma t_5 dX.w (* t_8 t_8)))
       t_7)))
    (log2
     (sqrt
      (fmax
       (fma t_5 dX.w (* (* (* dX.u dX.u) (floor w)) (floor w)))
       (* (pow dY.u 2.0) (pow (floor w) 2.0))))))))

C

float code(float w, float h, float d, float dX_46_u, float dX_46_v, float dX_46_w, float dY_46_u, float dY_46_v, float dY_46_w) {
	float t_0 = floorf(h) * dX_46_v;
	float t_1 = floorf(d) * dY_46_w;
	float t_2 = floorf(d) * dX_46_w;
	float t_3 = floorf(w) * dX_46_u;
	float t_4 = floorf(w) * dY_46_u;
	float t_5 = (floorf(d) * floorf(d)) * dX_46_w;
	float t_6 = floorf(h) * dY_46_v;
	float t_7 = ((t_4 * t_4) + (t_6 * t_6)) + (t_1 * t_1);
	float t_8 = dX_46_u * floorf(w);
	float tmp;
	if (fmaxf((((t_3 * t_3) + (t_0 * t_0)) + (t_2 * t_2)), t_7) <= 3.0000000054977558e+38f) {
		tmp = log2f(sqrtf(fmaxf(fmaf(dX_46_v, ((floorf(h) * floorf(h)) * dX_46_v), fmaf(t_5, dX_46_w, (t_8 * t_8))), t_7)));
	} else {
		tmp = log2f(sqrtf(fmaxf(fmaf(t_5, dX_46_w, (((dX_46_u * dX_46_u) * floorf(w)) * floorf(w))), (powf(dY_46_u, 2.0f) * powf(floorf(w), 2.0f)))));
	}
	return tmp;
}

Julia

function code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	t_0 = Float32(floor(h) * dX_46_v)
	t_1 = Float32(floor(d) * dY_46_w)
	t_2 = Float32(floor(d) * dX_46_w)
	t_3 = Float32(floor(w) * dX_46_u)
	t_4 = Float32(floor(w) * dY_46_u)
	t_5 = Float32(Float32(floor(d) * floor(d)) * dX_46_w)
	t_6 = Float32(floor(h) * dY_46_v)
	t_7 = Float32(Float32(Float32(t_4 * t_4) + Float32(t_6 * t_6)) + Float32(t_1 * t_1))
	t_8 = Float32(dX_46_u * floor(w))
	tmp = Float32(0.0)
	if (fmax(Float32(Float32(Float32(t_3 * t_3) + Float32(t_0 * t_0)) + Float32(t_2 * t_2)), t_7) <= Float32(3.0000000054977558e+38))
		tmp = log2(sqrt(fmax(fma(dX_46_v, Float32(Float32(floor(h) * floor(h)) * dX_46_v), fma(t_5, dX_46_w, Float32(t_8 * t_8))), t_7)));
	else
		tmp = log2(sqrt(fmax(fma(t_5, dX_46_w, Float32(Float32(Float32(dX_46_u * dX_46_u) * floor(w)) * floor(w))), Float32((dY_46_u ^ Float32(2.0)) * (floor(w) ^ Float32(2.0))))));
	end
	return tmp
end

Derivation

1. Split input into 2 regimes

2. if (fmax.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 (floor.f32 d) dX.w) (*.f32 (floor.f32 d) dX.w))) (+.f32 (+.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 (floor.f32 d) dY.w) (*.f32 (floor.f32 d) dY.w)))) < 3.00000001e38

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]
   2. Step-by-step derivation

   3. Applied rewrites 68.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dX.v, \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dX.v, \mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(dX.u \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot \left\lfloor w\right\rfloor \right)\right)\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   if 3.00000001e38 < (fmax.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 (floor.f32 d) dX.w) (*.f32 (floor.f32 d) dX.w))) (+.f32 (+.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 (floor.f32 d) dY.w) (*.f32 (floor.f32 d) dY.w))))

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   2. Taylor expanded in dX.v around 0

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}, \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left({dX.u}^{2}, {\left(\left\lfloor w\right\rfloor \right)}^{2}, {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   6. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)\right), \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\right)}\right) \]

   8. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, dY.u, \mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v, dY.v, \left(dY.w \cdot \left\lfloor d\right\rfloor \right) \cdot \left(dY.w \cdot \left\lfloor d\right\rfloor \right)\right)\right)\right)}\right) \]

   9. Taylor expanded in dY.u around inf

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right) \]
   10. Step-by-step derivation

   11. Applied rewrites 46.0%

       \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 2: 70.9% accurate, 0.5× speedup

\[\left(\left(\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(1 \leq d \land d \leq 4096\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|dX.w\right| \land \left|dX.w\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 \left(10^{-20} \leq \left|dY.w\right| \land \left|dY.w\right| \leq 10^{+20}\right)\]

Math

\[\begin{array}{l} t_0 := \left\lfloor w\right\rfloor \cdot dY.u\\ t_1 := dY.u \cdot \left\lfloor w\right\rfloor \\ t_2 := \left\lfloor h\right\rfloor \cdot dX.v\\ t_3 := dX.v \cdot \left\lfloor h\right\rfloor \\ t_4 := \left\lfloor d\right\rfloor \cdot dY.w\\ t_5 := dX.u \cdot \left\lfloor w\right\rfloor \\ t_6 := \left\lfloor d\right\rfloor \cdot dX.w\\ t_7 := dY.w \cdot \left\lfloor d\right\rfloor \\ t_8 := \left\lfloor h\right\rfloor \cdot dY.v\\ t_9 := dX.w \cdot \left\lfloor d\right\rfloor \\ t_10 := \left\lfloor w\right\rfloor \cdot dX.u\\ t_11 := dY.v \cdot \left\lfloor h\right\rfloor \\ \mathbf{if}\;\mathsf{max}\left(\left(t\_10 \cdot t\_10 + t\_2 \cdot t\_2\right) + t\_6 \cdot t\_6, \left(t\_0 \cdot t\_0 + t\_8 \cdot t\_8\right) + t\_4 \cdot t\_4\right) \leq 3.0000000054977558 \cdot 10^{+38}:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_7, t\_7, \mathsf{fma}\left(t\_11, t\_11, t\_1 \cdot t\_1\right)\right), \mathsf{fma}\left(t\_9, t\_9, \mathsf{fma}\left(t\_3, t\_3, t\_5 \cdot t\_5\right)\right)\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right)\\ \end{array} \]

FPCore

(FPCore (w h d dX.u dX.v dX.w dY.u dY.v dY.w)
  :precision binary32
  :pre (and (and (and (and (and (and (and (and (and (<= 1.0 w)
                                             (<= w 16384.0))
                                        (and (<= 1.0 h)
                                             (<= h 16384.0)))
                                   (and (<= 1.0 d)
                                        (<= d 4096.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 dX.w))
                         (<= (fabs dX.w) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (and (<= 1e-20 (fabs dY.w)) (<= (fabs dY.w) 1e+20)))
  (let* ((t_0 (* (floor w) dY.u))
       (t_1 (* dY.u (floor w)))
       (t_2 (* (floor h) dX.v))
       (t_3 (* dX.v (floor h)))
       (t_4 (* (floor d) dY.w))
       (t_5 (* dX.u (floor w)))
       (t_6 (* (floor d) dX.w))
       (t_7 (* dY.w (floor d)))
       (t_8 (* (floor h) dY.v))
       (t_9 (* dX.w (floor d)))
       (t_10 (* (floor w) dX.u))
       (t_11 (* dY.v (floor h))))
  (if (<=
       (fmax
        (+ (+ (* t_10 t_10) (* t_2 t_2)) (* t_6 t_6))
        (+ (+ (* t_0 t_0) (* t_8 t_8)) (* t_4 t_4)))
       3.0000000054977558e+38)
    (log2
     (sqrt
      (fmax
       (fma t_7 t_7 (fma t_11 t_11 (* t_1 t_1)))
       (fma t_9 t_9 (fma t_3 t_3 (* t_5 t_5))))))
    (log2
     (sqrt
      (fmax
       (fma
        (* (* (floor d) (floor d)) dX.w)
        dX.w
        (* (* (* dX.u dX.u) (floor w)) (floor w)))
       (* (pow dY.u 2.0) (pow (floor w) 2.0))))))))

C

float code(float w, float h, float d, float dX_46_u, float dX_46_v, float dX_46_w, float dY_46_u, float dY_46_v, float dY_46_w) {
	float t_0 = floorf(w) * dY_46_u;
	float t_1 = dY_46_u * floorf(w);
	float t_2 = floorf(h) * dX_46_v;
	float t_3 = dX_46_v * floorf(h);
	float t_4 = floorf(d) * dY_46_w;
	float t_5 = dX_46_u * floorf(w);
	float t_6 = floorf(d) * dX_46_w;
	float t_7 = dY_46_w * floorf(d);
	float t_8 = floorf(h) * dY_46_v;
	float t_9 = dX_46_w * floorf(d);
	float t_10 = floorf(w) * dX_46_u;
	float t_11 = dY_46_v * floorf(h);
	float tmp;
	if (fmaxf((((t_10 * t_10) + (t_2 * t_2)) + (t_6 * t_6)), (((t_0 * t_0) + (t_8 * t_8)) + (t_4 * t_4))) <= 3.0000000054977558e+38f) {
		tmp = log2f(sqrtf(fmaxf(fmaf(t_7, t_7, fmaf(t_11, t_11, (t_1 * t_1))), fmaf(t_9, t_9, fmaf(t_3, t_3, (t_5 * t_5))))));
	} else {
		tmp = log2f(sqrtf(fmaxf(fmaf(((floorf(d) * floorf(d)) * dX_46_w), dX_46_w, (((dX_46_u * dX_46_u) * floorf(w)) * floorf(w))), (powf(dY_46_u, 2.0f) * powf(floorf(w), 2.0f)))));
	}
	return tmp;
}

Julia

function code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	t_0 = Float32(floor(w) * dY_46_u)
	t_1 = Float32(dY_46_u * floor(w))
	t_2 = Float32(floor(h) * dX_46_v)
	t_3 = Float32(dX_46_v * floor(h))
	t_4 = Float32(floor(d) * dY_46_w)
	t_5 = Float32(dX_46_u * floor(w))
	t_6 = Float32(floor(d) * dX_46_w)
	t_7 = Float32(dY_46_w * floor(d))
	t_8 = Float32(floor(h) * dY_46_v)
	t_9 = Float32(dX_46_w * floor(d))
	t_10 = Float32(floor(w) * dX_46_u)
	t_11 = Float32(dY_46_v * floor(h))
	tmp = Float32(0.0)
	if (fmax(Float32(Float32(Float32(t_10 * t_10) + Float32(t_2 * t_2)) + Float32(t_6 * t_6)), Float32(Float32(Float32(t_0 * t_0) + Float32(t_8 * t_8)) + Float32(t_4 * t_4))) <= Float32(3.0000000054977558e+38))
		tmp = log2(sqrt(fmax(fma(t_7, t_7, fma(t_11, t_11, Float32(t_1 * t_1))), fma(t_9, t_9, fma(t_3, t_3, Float32(t_5 * t_5))))));
	else
		tmp = log2(sqrt(fmax(fma(Float32(Float32(floor(d) * floor(d)) * dX_46_w), dX_46_w, Float32(Float32(Float32(dX_46_u * dX_46_u) * floor(w)) * floor(w))), Float32((dY_46_u ^ Float32(2.0)) * (floor(w) ^ Float32(2.0))))));
	end
	return tmp
end

Derivation

1. Split input into 2 regimes

2. if (fmax.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 (floor.f32 d) dX.w) (*.f32 (floor.f32 d) dX.w))) (+.f32 (+.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 (floor.f32 d) dY.w) (*.f32 (floor.f32 d) dY.w)))) < 3.00000001e38

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   3. Applied rewrites 68.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.w \cdot \left\lfloor d\right\rfloor , dY.w \cdot \left\lfloor d\right\rfloor , \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)\right), \mathsf{fma}\left(dX.w \cdot \left\lfloor d\right\rfloor , dX.w \cdot \left\lfloor d\right\rfloor , \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)\right)}\right) \]

   if 3.00000001e38 < (fmax.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 (floor.f32 d) dX.w) (*.f32 (floor.f32 d) dX.w))) (+.f32 (+.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 (floor.f32 d) dY.w) (*.f32 (floor.f32 d) dY.w))))

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   2. Taylor expanded in dX.v around 0

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}, \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left({dX.u}^{2}, {\left(\left\lfloor w\right\rfloor \right)}^{2}, {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   6. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)\right), \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\right)}\right) \]

   8. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, dY.u, \mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v, dY.v, \left(dY.w \cdot \left\lfloor d\right\rfloor \right) \cdot \left(dY.w \cdot \left\lfloor d\right\rfloor \right)\right)\right)\right)}\right) \]

   9. Taylor expanded in dY.u around inf

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right) \]
   10. Step-by-step derivation

   11. Applied rewrites 46.0%

       \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 3: 66.2% accurate, 1.1× speedup

\[\left(\left(\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(1 \leq d \land d \leq 4096\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|dX.w\right| \land \left|dX.w\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 \left(10^{-20} \leq \left|dY.w\right| \land \left|dY.w\right| \leq 10^{+20}\right)\]

Math

\[\begin{array}{l} t_0 := \left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \\ t_1 := \mathsf{fma}\left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \mathsf{fma}\left(\left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , t\_0 \cdot \left(dX.w \cdot dX.w\right)\right)\right)\\ \mathbf{if}\;\left|dY.v\right| \leq 0.12039202451705933:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.u \cdot dY.u, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor , \left(dY.w \cdot dY.w\right) \cdot t\_0\right), t\_1\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \left(\left|dY.v\right| \cdot \left|dY.v\right|\right) \cdot \left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right)\right), t\_1\right)}\right)\\ \end{array} \]

FPCore

(FPCore (w h d dX.u dX.v dX.w dY.u dY.v dY.w)
  :precision binary32
  :pre (and (and (and (and (and (and (and (and (and (<= 1.0 w)
                                             (<= w 16384.0))
                                        (and (<= 1.0 h)
                                             (<= h 16384.0)))
                                   (and (<= 1.0 d)
                                        (<= d 4096.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 dX.w))
                         (<= (fabs dX.w) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (and (<= 1e-20 (fabs dY.w)) (<= (fabs dY.w) 1e+20)))
  (let* ((t_0 (* (floor d) (floor d)))
       (t_1
        (fma
         (* (* dX.u dX.u) (floor w))
         (floor w)
         (fma
          (* (* dX.v dX.v) (floor h))
          (floor h)
          (* t_0 (* dX.w dX.w))))))
  (if (<= (fabs dY.v) 0.12039202451705933)
    (log2
     (sqrt
      (fmax
       (fma
        (* dY.u dY.u)
        (* (floor w) (floor w))
        (* (* dY.w dY.w) t_0))
       t_1)))
    (log2
     (sqrt
      (fmax
       (fma
        (* (* dY.w dY.w) (floor d))
        (floor d)
        (* (* (fabs dY.v) (fabs dY.v)) (* (floor h) (floor h))))
       t_1))))))

C

float code(float w, float h, float d, float dX_46_u, float dX_46_v, float dX_46_w, float dY_46_u, float dY_46_v, float dY_46_w) {
	float t_0 = floorf(d) * floorf(d);
	float t_1 = fmaf(((dX_46_u * dX_46_u) * floorf(w)), floorf(w), fmaf(((dX_46_v * dX_46_v) * floorf(h)), floorf(h), (t_0 * (dX_46_w * dX_46_w))));
	float tmp;
	if (fabsf(dY_46_v) <= 0.12039202451705933f) {
		tmp = log2f(sqrtf(fmaxf(fmaf((dY_46_u * dY_46_u), (floorf(w) * floorf(w)), ((dY_46_w * dY_46_w) * t_0)), t_1)));
	} else {
		tmp = log2f(sqrtf(fmaxf(fmaf(((dY_46_w * dY_46_w) * floorf(d)), floorf(d), ((fabsf(dY_46_v) * fabsf(dY_46_v)) * (floorf(h) * floorf(h)))), t_1)));
	}
	return tmp;
}

Julia

function code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	t_0 = Float32(floor(d) * floor(d))
	t_1 = fma(Float32(Float32(dX_46_u * dX_46_u) * floor(w)), floor(w), fma(Float32(Float32(dX_46_v * dX_46_v) * floor(h)), floor(h), Float32(t_0 * Float32(dX_46_w * dX_46_w))))
	tmp = Float32(0.0)
	if (abs(dY_46_v) <= Float32(0.12039202451705933))
		tmp = log2(sqrt(fmax(fma(Float32(dY_46_u * dY_46_u), Float32(floor(w) * floor(w)), Float32(Float32(dY_46_w * dY_46_w) * t_0)), t_1)));
	else
		tmp = log2(sqrt(fmax(fma(Float32(Float32(dY_46_w * dY_46_w) * floor(d)), floor(d), Float32(Float32(abs(dY_46_v) * abs(dY_46_v)) * Float32(floor(h) * floor(h)))), t_1)));
	end
	return tmp
end

Derivation

1. Split input into 2 regimes

2. if dY.v < 0.120392025

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   2. Taylor expanded in dY.v around 0

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {dY.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right)}\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 61.3%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \mathsf{fma}\left({dY.u}^{2}, {\left(\left\lfloor w\right\rfloor \right)}^{2}, {dY.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right)\right)}\right) \]

   6. Applied rewrites 61.3%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.u \cdot dY.u, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor , \left(dY.w \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right)\right), \mathsf{fma}\left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \mathsf{fma}\left(\left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot \left(dX.w \cdot dX.w\right)\right)\right)\right)}\right) \]

   if 0.120392025 < dY.v

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   2. Taylor expanded in dY.u around 0

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), {dY.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} + {dY.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right)}\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 61.0%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \mathsf{fma}\left({dY.v}^{2}, {\left(\left\lfloor h\right\rfloor \right)}^{2}, {dY.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right)\right)}\right) \]

   6. Applied rewrites 61.0%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \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(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \mathsf{fma}\left(\left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot \left(dX.w \cdot dX.w\right)\right)\right)\right)}\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 4: 65.8% accurate, 1.1× speedup

\[\left(\left(\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(1 \leq d \land d \leq 4096\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|dX.w\right| \land \left|dX.w\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 \left(10^{-20} \leq \left|dY.w\right| \land \left|dY.w\right| \leq 10^{+20}\right)\]

Math

\[\begin{array}{l} t_0 := \left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \\ t_1 := \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \\ \mathbf{if}\;\left|dX.v\right| \leq 2842.50634765625:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_0 \cdot dX.w, dX.w, t\_1 \cdot \left(dX.u \cdot dX.u\right)\right), \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.u \cdot dY.u, t\_1, \left(dY.w \cdot dY.w\right) \cdot t\_0\right), \mathsf{fma}\left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \mathsf{fma}\left(\left(\left|dX.v\right| \cdot \left|dX.v\right|\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , t\_0 \cdot \left(dX.w \cdot dX.w\right)\right)\right)\right)}\right)\\ \end{array} \]

FPCore

(FPCore (w h d dX.u dX.v dX.w dY.u dY.v dY.w)
  :precision binary32
  :pre (and (and (and (and (and (and (and (and (and (<= 1.0 w)
                                             (<= w 16384.0))
                                        (and (<= 1.0 h)
                                             (<= h 16384.0)))
                                   (and (<= 1.0 d)
                                        (<= d 4096.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 dX.w))
                         (<= (fabs dX.w) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (and (<= 1e-20 (fabs dY.w)) (<= (fabs dY.w) 1e+20)))
  (let* ((t_0 (* (floor d) (floor d))) (t_1 (* (floor w) (floor w))))
  (if (<= (fabs dX.v) 2842.50634765625)
    (log2
     (sqrt
      (fmax
       (fma (* t_0 dX.w) dX.w (* t_1 (* dX.u dX.u)))
       (fma
        (* (* dY.w dY.w) (floor d))
        (floor d)
        (fma
         (* (* dY.u dY.u) (floor w))
         (floor w)
         (* (* dY.v dY.v) (* (floor h) (floor h))))))))
    (log2
     (sqrt
      (fmax
       (fma (* dY.u dY.u) t_1 (* (* dY.w dY.w) t_0))
       (fma
        (* (* dX.u dX.u) (floor w))
        (floor w)
        (fma
         (* (* (fabs dX.v) (fabs dX.v)) (floor h))
         (floor h)
         (* t_0 (* dX.w dX.w))))))))))

C

float code(float w, float h, float d, float dX_46_u, float dX_46_v, float dX_46_w, float dY_46_u, float dY_46_v, float dY_46_w) {
	float t_0 = floorf(d) * floorf(d);
	float t_1 = floorf(w) * floorf(w);
	float tmp;
	if (fabsf(dX_46_v) <= 2842.50634765625f) {
		tmp = log2f(sqrtf(fmaxf(fmaf((t_0 * dX_46_w), dX_46_w, (t_1 * (dX_46_u * dX_46_u))), fmaf(((dY_46_w * dY_46_w) * floorf(d)), floorf(d), fmaf(((dY_46_u * dY_46_u) * floorf(w)), floorf(w), ((dY_46_v * dY_46_v) * (floorf(h) * floorf(h))))))));
	} else {
		tmp = log2f(sqrtf(fmaxf(fmaf((dY_46_u * dY_46_u), t_1, ((dY_46_w * dY_46_w) * t_0)), fmaf(((dX_46_u * dX_46_u) * floorf(w)), floorf(w), fmaf(((fabsf(dX_46_v) * fabsf(dX_46_v)) * floorf(h)), floorf(h), (t_0 * (dX_46_w * dX_46_w)))))));
	}
	return tmp;
}

Julia

function code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	t_0 = Float32(floor(d) * floor(d))
	t_1 = Float32(floor(w) * floor(w))
	tmp = Float32(0.0)
	if (abs(dX_46_v) <= Float32(2842.50634765625))
		tmp = log2(sqrt(fmax(fma(Float32(t_0 * dX_46_w), dX_46_w, Float32(t_1 * Float32(dX_46_u * dX_46_u))), fma(Float32(Float32(dY_46_w * dY_46_w) * floor(d)), floor(d), fma(Float32(Float32(dY_46_u * dY_46_u) * floor(w)), floor(w), Float32(Float32(dY_46_v * dY_46_v) * Float32(floor(h) * floor(h))))))));
	else
		tmp = log2(sqrt(fmax(fma(Float32(dY_46_u * dY_46_u), t_1, Float32(Float32(dY_46_w * dY_46_w) * t_0)), fma(Float32(Float32(dX_46_u * dX_46_u) * floor(w)), floor(w), fma(Float32(Float32(abs(dX_46_v) * abs(dX_46_v)) * floor(h)), floor(h), Float32(t_0 * Float32(dX_46_w * dX_46_w)))))));
	end
	return tmp
end

Derivation

1. Split input into 2 regimes

2. if dX.v < 2842.50635

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   2. Taylor expanded in dX.v around 0

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}, \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left({dX.u}^{2}, {\left(\left\lfloor w\right\rfloor \right)}^{2}, {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   6. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)\right), \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\right)}\right) \]

   if 2842.50635 < dX.v

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   2. Taylor expanded in dY.v around 0

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {dY.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right)}\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 61.3%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \mathsf{fma}\left({dY.u}^{2}, {\left(\left\lfloor w\right\rfloor \right)}^{2}, {dY.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right)\right)}\right) \]

   6. Applied rewrites 61.3%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(dY.u \cdot dY.u, \left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor , \left(dY.w \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right)\right), \mathsf{fma}\left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor , \left\lfloor w\right\rfloor , \mathsf{fma}\left(\left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot \left(dX.w \cdot dX.w\right)\right)\right)\right)}\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 5: 65.3% accurate, 1.1× speedup

\[\left(\left(\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(1 \leq d \land d \leq 4096\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|dX.w\right| \land \left|dX.w\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 \left(10^{-20} \leq \left|dY.w\right| \land \left|dY.w\right| \leq 10^{+20}\right)\]

Math

\[\begin{array}{l} t_0 := \left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \\ t_1 := \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\\ \mathbf{if}\;\left|dX.u\right| \leq 54774.28125:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , t\_0 \cdot \left(dX.w \cdot dX.w\right)\right), t\_1\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_0 \cdot dX.w, dX.w, \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(\left|dX.u\right| \cdot \left|dX.u\right|\right)\right), t\_1\right)}\right)\\ \end{array} \]

FPCore

(FPCore (w h d dX.u dX.v dX.w dY.u dY.v dY.w)
  :precision binary32
  :pre (and (and (and (and (and (and (and (and (and (<= 1.0 w)
                                             (<= w 16384.0))
                                        (and (<= 1.0 h)
                                             (<= h 16384.0)))
                                   (and (<= 1.0 d)
                                        (<= d 4096.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 dX.w))
                         (<= (fabs dX.w) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (and (<= 1e-20 (fabs dY.w)) (<= (fabs dY.w) 1e+20)))
  (let* ((t_0 (* (floor d) (floor d)))
       (t_1
        (fma
         (* (* dY.w dY.w) (floor d))
         (floor d)
         (fma
          (* (* dY.u dY.u) (floor w))
          (floor w)
          (* (* dY.v dY.v) (* (floor h) (floor h)))))))
  (if (<= (fabs dX.u) 54774.28125)
    (log2
     (sqrt
      (fmax
       (fma
        (* (* dX.v dX.v) (floor h))
        (floor h)
        (* t_0 (* dX.w dX.w)))
       t_1)))
    (log2
     (sqrt
      (fmax
       (fma
        (* t_0 dX.w)
        dX.w
        (* (* (floor w) (floor w)) (* (fabs dX.u) (fabs dX.u))))
       t_1))))))

C

float code(float w, float h, float d, float dX_46_u, float dX_46_v, float dX_46_w, float dY_46_u, float dY_46_v, float dY_46_w) {
	float t_0 = floorf(d) * floorf(d);
	float t_1 = fmaf(((dY_46_w * dY_46_w) * floorf(d)), floorf(d), fmaf(((dY_46_u * dY_46_u) * floorf(w)), floorf(w), ((dY_46_v * dY_46_v) * (floorf(h) * floorf(h)))));
	float tmp;
	if (fabsf(dX_46_u) <= 54774.28125f) {
		tmp = log2f(sqrtf(fmaxf(fmaf(((dX_46_v * dX_46_v) * floorf(h)), floorf(h), (t_0 * (dX_46_w * dX_46_w))), t_1)));
	} else {
		tmp = log2f(sqrtf(fmaxf(fmaf((t_0 * dX_46_w), dX_46_w, ((floorf(w) * floorf(w)) * (fabsf(dX_46_u) * fabsf(dX_46_u)))), t_1)));
	}
	return tmp;
}

Julia

function code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	t_0 = Float32(floor(d) * floor(d))
	t_1 = fma(Float32(Float32(dY_46_w * dY_46_w) * floor(d)), floor(d), fma(Float32(Float32(dY_46_u * dY_46_u) * floor(w)), floor(w), Float32(Float32(dY_46_v * dY_46_v) * Float32(floor(h) * floor(h)))))
	tmp = Float32(0.0)
	if (abs(dX_46_u) <= Float32(54774.28125))
		tmp = log2(sqrt(fmax(fma(Float32(Float32(dX_46_v * dX_46_v) * floor(h)), floor(h), Float32(t_0 * Float32(dX_46_w * dX_46_w))), t_1)));
	else
		tmp = log2(sqrt(fmax(fma(Float32(t_0 * dX_46_w), dX_46_w, Float32(Float32(floor(w) * floor(w)) * Float32(abs(dX_46_u) * abs(dX_46_u)))), t_1)));
	end
	return tmp
end

Derivation

1. Split input into 2 regimes

2. if dX.u < 54774.2812

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   2. Taylor expanded in dX.u around 0

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} + {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}, \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 60.9%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left({dX.v}^{2}, {\left(\left\lfloor h\right\rfloor \right)}^{2}, {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   6. Applied rewrites 60.9%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot \left(dX.w \cdot dX.w\right)\right), \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\right)}\right) \]

   if 54774.2812 < dX.u

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   2. Taylor expanded in dX.v around 0

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}, \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left({dX.u}^{2}, {\left(\left\lfloor w\right\rfloor \right)}^{2}, {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   6. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)\right), \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\right)}\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 6: 64.0% accurate, 1.1× speedup

\[\left(\left(\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(1 \leq d \land d \leq 4096\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|dX.w\right| \land \left|dX.w\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 \left(10^{-20} \leq \left|dY.w\right| \land \left|dY.w\right| \leq 10^{+20}\right)\]

Math

\[\begin{array}{l} t_0 := \left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \\ \mathbf{if}\;\left|dX.u\right| \leq 8183726.5:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , t\_0 \cdot \left(dX.w \cdot dX.w\right)\right), \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(t\_0 \cdot dX.w, dX.w, \left(\left(\left|dX.u\right| \cdot \left|dX.u\right|\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right)\\ \end{array} \]

FPCore

(FPCore (w h d dX.u dX.v dX.w dY.u dY.v dY.w)
  :precision binary32
  :pre (and (and (and (and (and (and (and (and (and (<= 1.0 w)
                                             (<= w 16384.0))
                                        (and (<= 1.0 h)
                                             (<= h 16384.0)))
                                   (and (<= 1.0 d)
                                        (<= d 4096.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 dX.w))
                         (<= (fabs dX.w) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (and (<= 1e-20 (fabs dY.w)) (<= (fabs dY.w) 1e+20)))
  (let* ((t_0 (* (floor d) (floor d))))
  (if (<= (fabs dX.u) 8183726.5)
    (log2
     (sqrt
      (fmax
       (fma
        (* (* dX.v dX.v) (floor h))
        (floor h)
        (* t_0 (* dX.w dX.w)))
       (fma
        (* (* dY.w dY.w) (floor d))
        (floor d)
        (fma
         (* (* dY.u dY.u) (floor w))
         (floor w)
         (* (* dY.v dY.v) (* (floor h) (floor h))))))))
    (log2
     (sqrt
      (fmax
       (fma
        (* t_0 dX.w)
        dX.w
        (* (* (* (fabs dX.u) (fabs dX.u)) (floor w)) (floor w)))
       (* (pow dY.u 2.0) (pow (floor w) 2.0))))))))

C

float code(float w, float h, float d, float dX_46_u, float dX_46_v, float dX_46_w, float dY_46_u, float dY_46_v, float dY_46_w) {
	float t_0 = floorf(d) * floorf(d);
	float tmp;
	if (fabsf(dX_46_u) <= 8183726.5f) {
		tmp = log2f(sqrtf(fmaxf(fmaf(((dX_46_v * dX_46_v) * floorf(h)), floorf(h), (t_0 * (dX_46_w * dX_46_w))), fmaf(((dY_46_w * dY_46_w) * floorf(d)), floorf(d), fmaf(((dY_46_u * dY_46_u) * floorf(w)), floorf(w), ((dY_46_v * dY_46_v) * (floorf(h) * floorf(h))))))));
	} else {
		tmp = log2f(sqrtf(fmaxf(fmaf((t_0 * dX_46_w), dX_46_w, (((fabsf(dX_46_u) * fabsf(dX_46_u)) * floorf(w)) * floorf(w))), (powf(dY_46_u, 2.0f) * powf(floorf(w), 2.0f)))));
	}
	return tmp;
}

Julia

function code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	t_0 = Float32(floor(d) * floor(d))
	tmp = Float32(0.0)
	if (abs(dX_46_u) <= Float32(8183726.5))
		tmp = log2(sqrt(fmax(fma(Float32(Float32(dX_46_v * dX_46_v) * floor(h)), floor(h), Float32(t_0 * Float32(dX_46_w * dX_46_w))), fma(Float32(Float32(dY_46_w * dY_46_w) * floor(d)), floor(d), fma(Float32(Float32(dY_46_u * dY_46_u) * floor(w)), floor(w), Float32(Float32(dY_46_v * dY_46_v) * Float32(floor(h) * floor(h))))))));
	else
		tmp = log2(sqrt(fmax(fma(Float32(t_0 * dX_46_w), dX_46_w, Float32(Float32(Float32(abs(dX_46_u) * abs(dX_46_u)) * floor(w)) * floor(w))), Float32((dY_46_u ^ Float32(2.0)) * (floor(w) ^ Float32(2.0))))));
	end
	return tmp
end

Derivation

1. Split input into 2 regimes

2. if dX.u < 8183726.5

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   2. Taylor expanded in dX.u around 0

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left({dX.v}^{2} \cdot {\left(\left\lfloor h\right\rfloor \right)}^{2} + {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}, \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 60.9%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left({dX.v}^{2}, {\left(\left\lfloor h\right\rfloor \right)}^{2}, {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   6. Applied rewrites 60.9%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(dX.v \cdot dX.v\right) \cdot \left\lfloor h\right\rfloor , \left\lfloor h\right\rfloor , \left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot \left(dX.w \cdot dX.w\right)\right), \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\right)}\right) \]

   if 8183726.5 < dX.u

   1. Initial program 68.2%

      \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   2. Taylor expanded in dX.v around 0

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}, \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]
   3. Step-by-step derivation

   4. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left({dX.u}^{2}, {\left(\left\lfloor w\right\rfloor \right)}^{2}, {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

   6. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)\right), \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\right)}\right) \]

   8. Applied rewrites 61.2%

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, dY.u, \mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v, dY.v, \left(dY.w \cdot \left\lfloor d\right\rfloor \right) \cdot \left(dY.w \cdot \left\lfloor d\right\rfloor \right)\right)\right)\right)}\right) \]

   9. Taylor expanded in dY.u around inf

      \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right) \]
   10. Step-by-step derivation

   11. Applied rewrites 46.0%

       \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 7: 46.0% accurate, 1.3× speedup

\[\left(\left(\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(1 \leq d \land d \leq 4096\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|dX.w\right| \land \left|dX.w\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 \left(10^{-20} \leq \left|dY.w\right| \land \left|dY.w\right| \leq 10^{+20}\right)\]

Math

\[\log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right) \]

FPCore

(FPCore (w h d dX.u dX.v dX.w dY.u dY.v dY.w)
  :precision binary32
  :pre (and (and (and (and (and (and (and (and (and (<= 1.0 w)
                                             (<= w 16384.0))
                                        (and (<= 1.0 h)
                                             (<= h 16384.0)))
                                   (and (<= 1.0 d)
                                        (<= d 4096.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 dX.w))
                         (<= (fabs dX.w) 1e+20)))
               (and (<= 1e-20 (fabs dY.u))
                    (<= (fabs dY.u) 1e+20)))
          (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20)))
     (and (<= 1e-20 (fabs dY.w)) (<= (fabs dY.w) 1e+20)))
  (log2
 (sqrt
  (fmax
   (fma
    (* (* (floor d) (floor d)) dX.w)
    dX.w
    (* (* (* dX.u dX.u) (floor w)) (floor w)))
   (* (pow dY.u 2.0) (pow (floor w) 2.0))))))

C

float code(float w, float h, float d, float dX_46_u, float dX_46_v, float dX_46_w, float dY_46_u, float dY_46_v, float dY_46_w) {
	return log2f(sqrtf(fmaxf(fmaf(((floorf(d) * floorf(d)) * dX_46_w), dX_46_w, (((dX_46_u * dX_46_u) * floorf(w)) * floorf(w))), (powf(dY_46_u, 2.0f) * powf(floorf(w), 2.0f)))));
}

Julia

function code(w, h, d, dX_46_u, dX_46_v, dX_46_w, dY_46_u, dY_46_v, dY_46_w)
	return log2(sqrt(fmax(fma(Float32(Float32(floor(d) * floor(d)) * dX_46_w), dX_46_w, Float32(Float32(Float32(dX_46_u * dX_46_u) * floor(w)) * floor(w))), Float32((dY_46_u ^ Float32(2.0)) * (floor(w) ^ Float32(2.0))))))
end

Derivation

1. Initial program 68.2%

   \[\log_{2} \left(\sqrt{\mathsf{max}\left(\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)\right) + \left(\left\lfloor d\right\rfloor \cdot dX.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dX.w\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

2. Taylor expanded in dX.v around 0

   \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left({dX.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2} + {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}, \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]
3. Step-by-step derivation

4. Applied rewrites 61.2%

   \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left({dX.u}^{2}, {\left(\left\lfloor w\right\rfloor \right)}^{2}, {dX.w}^{2} \cdot {\left(\left\lfloor d\right\rfloor \right)}^{2}\right), \left(\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) + \left(\left\lfloor d\right\rfloor \cdot dY.w\right) \cdot \left(\left\lfloor d\right\rfloor \cdot dY.w\right)\right)}\right) \]

6. Applied rewrites 61.2%

   \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot \left(dX.u \cdot dX.u\right)\right), \mathsf{fma}\left(\left(dY.w \cdot dY.w\right) \cdot \left\lfloor d\right\rfloor , \left\lfloor d\right\rfloor , \mathsf{fma}\left(\left(dY.u \cdot dY.u\right) \cdot \left\lfloor w\right\rfloor , \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)\right)\right)\right)}\right) \]

8. Applied rewrites 61.2%

   \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), \mathsf{fma}\left(\left(\left\lfloor w\right\rfloor \cdot \left\lfloor w\right\rfloor \right) \cdot dY.u, dY.u, \mathsf{fma}\left(\left(\left\lfloor h\right\rfloor \cdot \left\lfloor h\right\rfloor \right) \cdot dY.v, dY.v, \left(dY.w \cdot \left\lfloor d\right\rfloor \right) \cdot \left(dY.w \cdot \left\lfloor d\right\rfloor \right)\right)\right)\right)}\right) \]

9. Taylor expanded in dY.u around inf

   \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right) \]
10. Step-by-step derivation

11. Applied rewrites 46.0%

    \[\leadsto \log_{2} \left(\sqrt{\mathsf{max}\left(\mathsf{fma}\left(\left(\left\lfloor d\right\rfloor \cdot \left\lfloor d\right\rfloor \right) \cdot dX.w, dX.w, \left(\left(dX.u \cdot dX.u\right) \cdot \left\lfloor w\right\rfloor \right) \cdot \left\lfloor w\right\rfloor \right), {dY.u}^{2} \cdot {\left(\left\lfloor w\right\rfloor \right)}^{2}\right)}\right) \]
12. Add Preprocessing

Reproduce

herbie shell --seed 2026084 
(FPCore (w h d dX.u dX.v dX.w dY.u dY.v dY.w)
  :name "Isotropic LOD (LOD)"
  :precision binary32
  :pre (and (and (and (and (and (and (and (and (and (<= 1.0 w) (<= w 16384.0)) (and (<= 1.0 h) (<= h 16384.0))) (and (<= 1.0 d) (<= d 4096.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 dX.w)) (<= (fabs dX.w) 1e+20))) (and (<= 1e-20 (fabs dY.u)) (<= (fabs dY.u) 1e+20))) (and (<= 1e-20 (fabs dY.v)) (<= (fabs dY.v) 1e+20))) (and (<= 1e-20 (fabs dY.w)) (<= (fabs dY.w) 1e+20)))
  (log2 (sqrt (fmax (+ (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (* (* (floor d) dX.w) (* (floor d) dX.w))) (+ (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v))) (* (* (floor d) dY.w) (* (floor d) dY.w)))))))