UniformSampleCone 2

Percentage Accurate: 98.9% → 99.0%
Time: 8.4s
Alternatives: 15
Speedup: 1.2×

Specification

?
\[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
\[\begin{array}{l} t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\ t_1 := \sqrt{1 - t\_0 \cdot t\_0}\\ t_2 := \left(uy \cdot 2\right) \cdot \pi\\ \left(\left(\cos t\_2 \cdot t\_1\right) \cdot xi + \left(\sin t\_2 \cdot t\_1\right) \cdot yi\right) + t\_0 \cdot zi \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
  :precision binary32
  :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                         (and (<= -10000.0 yi) (<= yi 10000.0)))
                    (and (<= -10000.0 zi) (<= zi 10000.0)))
               (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
          (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
     (and (<= 0.0 maxCos) (<= maxCos 1.0)))
  (let* ((t_0 (* (* (- 1.0 ux) maxCos) ux))
       (t_1 (sqrt (- 1.0 (* t_0 t_0))))
       (t_2 (* (* uy 2.0) PI)))
  (+
   (+ (* (* (cos t_2) t_1) xi) (* (* (sin t_2) t_1) yi))
   (* t_0 zi))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = ((1.0f - ux) * maxCos) * ux;
	float t_1 = sqrtf((1.0f - (t_0 * t_0)));
	float t_2 = (uy * 2.0f) * ((float) M_PI);
	return (((cosf(t_2) * t_1) * xi) + ((sinf(t_2) * t_1) * yi)) + (t_0 * zi);
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux)
	t_1 = sqrt(Float32(Float32(1.0) - Float32(t_0 * t_0)))
	t_2 = Float32(Float32(uy * Float32(2.0)) * Float32(pi))
	return Float32(Float32(Float32(Float32(cos(t_2) * t_1) * xi) + Float32(Float32(sin(t_2) * t_1) * yi)) + Float32(t_0 * zi))
end
function tmp = code(xi, yi, zi, ux, uy, maxCos)
	t_0 = ((single(1.0) - ux) * maxCos) * ux;
	t_1 = sqrt((single(1.0) - (t_0 * t_0)));
	t_2 = (uy * single(2.0)) * single(pi);
	tmp = (((cos(t_2) * t_1) * xi) + ((sin(t_2) * t_1) * yi)) + (t_0 * zi);
end
\begin{array}{l}
t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\
t_1 := \sqrt{1 - t\_0 \cdot t\_0}\\
t_2 := \left(uy \cdot 2\right) \cdot \pi\\
\left(\left(\cos t\_2 \cdot t\_1\right) \cdot xi + \left(\sin t\_2 \cdot t\_1\right) \cdot yi\right) + t\_0 \cdot zi
\end{array}

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 15 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 98.9% accurate, 1.0× speedup?

\[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
\[\begin{array}{l} t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\ t_1 := \sqrt{1 - t\_0 \cdot t\_0}\\ t_2 := \left(uy \cdot 2\right) \cdot \pi\\ \left(\left(\cos t\_2 \cdot t\_1\right) \cdot xi + \left(\sin t\_2 \cdot t\_1\right) \cdot yi\right) + t\_0 \cdot zi \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
  :precision binary32
  :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                         (and (<= -10000.0 yi) (<= yi 10000.0)))
                    (and (<= -10000.0 zi) (<= zi 10000.0)))
               (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
          (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
     (and (<= 0.0 maxCos) (<= maxCos 1.0)))
  (let* ((t_0 (* (* (- 1.0 ux) maxCos) ux))
       (t_1 (sqrt (- 1.0 (* t_0 t_0))))
       (t_2 (* (* uy 2.0) PI)))
  (+
   (+ (* (* (cos t_2) t_1) xi) (* (* (sin t_2) t_1) yi))
   (* t_0 zi))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = ((1.0f - ux) * maxCos) * ux;
	float t_1 = sqrtf((1.0f - (t_0 * t_0)));
	float t_2 = (uy * 2.0f) * ((float) M_PI);
	return (((cosf(t_2) * t_1) * xi) + ((sinf(t_2) * t_1) * yi)) + (t_0 * zi);
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux)
	t_1 = sqrt(Float32(Float32(1.0) - Float32(t_0 * t_0)))
	t_2 = Float32(Float32(uy * Float32(2.0)) * Float32(pi))
	return Float32(Float32(Float32(Float32(cos(t_2) * t_1) * xi) + Float32(Float32(sin(t_2) * t_1) * yi)) + Float32(t_0 * zi))
end
function tmp = code(xi, yi, zi, ux, uy, maxCos)
	t_0 = ((single(1.0) - ux) * maxCos) * ux;
	t_1 = sqrt((single(1.0) - (t_0 * t_0)));
	t_2 = (uy * single(2.0)) * single(pi);
	tmp = (((cos(t_2) * t_1) * xi) + ((sin(t_2) * t_1) * yi)) + (t_0 * zi);
end
\begin{array}{l}
t_0 := \left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\\
t_1 := \sqrt{1 - t\_0 \cdot t\_0}\\
t_2 := \left(uy \cdot 2\right) \cdot \pi\\
\left(\left(\cos t\_2 \cdot t\_1\right) \cdot xi + \left(\sin t\_2 \cdot t\_1\right) \cdot yi\right) + t\_0 \cdot zi
\end{array}

Alternative 1: 99.0% accurate, 1.0× speedup?

\[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
\[\begin{array}{l} t_0 := \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\\ t_1 := \pi \cdot \left(uy + uy\right)\\ t_2 := \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, t\_0 \cdot ux, 1\right)}\\ \mathsf{fma}\left(t\_2 \cdot \cos t\_1, xi, \mathsf{fma}\left(yi \cdot t\_2, \sin t\_1, zi \cdot t\_0\right)\right) \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
  :precision binary32
  :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                         (and (<= -10000.0 yi) (<= yi 10000.0)))
                    (and (<= -10000.0 zi) (<= zi 10000.0)))
               (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
          (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
     (and (<= 0.0 maxCos) (<= maxCos 1.0)))
  (let* ((t_0 (* (* maxCos (- 1.0 ux)) ux))
       (t_1 (* PI (+ uy uy)))
       (t_2 (sqrt (fma (* (- ux 1.0) maxCos) (* t_0 ux) 1.0))))
  (fma (* t_2 (cos t_1)) xi (fma (* yi t_2) (sin t_1) (* zi t_0)))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = (maxCos * (1.0f - ux)) * ux;
	float t_1 = ((float) M_PI) * (uy + uy);
	float t_2 = sqrtf(fmaf(((ux - 1.0f) * maxCos), (t_0 * ux), 1.0f));
	return fmaf((t_2 * cosf(t_1)), xi, fmaf((yi * t_2), sinf(t_1), (zi * t_0)));
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(maxCos * Float32(Float32(1.0) - ux)) * ux)
	t_1 = Float32(Float32(pi) * Float32(uy + uy))
	t_2 = sqrt(fma(Float32(Float32(ux - Float32(1.0)) * maxCos), Float32(t_0 * ux), Float32(1.0)))
	return fma(Float32(t_2 * cos(t_1)), xi, fma(Float32(yi * t_2), sin(t_1), Float32(zi * t_0)))
end
\begin{array}{l}
t_0 := \left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\\
t_1 := \pi \cdot \left(uy + uy\right)\\
t_2 := \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, t\_0 \cdot ux, 1\right)}\\
\mathsf{fma}\left(t\_2 \cdot \cos t\_1, xi, \mathsf{fma}\left(yi \cdot t\_2, \sin t\_1, zi \cdot t\_0\right)\right)
\end{array}
Derivation
  1. Initial program 98.9%

    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  2. Applied rewrites99.0%

    \[\leadsto \mathsf{fma}\left(\sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, \left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot ux, 1\right)} \cdot \cos \left(\pi \cdot \left(uy + uy\right)\right), xi, \mathsf{fma}\left(yi \cdot \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, \left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot ux, 1\right)}, \sin \left(\pi \cdot \left(uy + uy\right)\right), zi \cdot \left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right)\right)\right) \]
  3. Add Preprocessing

Alternative 2: 99.0% accurate, 1.2× speedup?

\[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
\[\begin{array}{l} t_0 := \pi \cdot \left(uy + uy\right)\\ \mathsf{fma}\left(zi \cdot \left(1 - ux\right), maxCos \cdot ux, \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, \left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot ux, 1\right)} \cdot \mathsf{fma}\left(\sin t\_0, yi, \cos t\_0 \cdot xi\right)\right) \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
  :precision binary32
  :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                         (and (<= -10000.0 yi) (<= yi 10000.0)))
                    (and (<= -10000.0 zi) (<= zi 10000.0)))
               (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
          (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
     (and (<= 0.0 maxCos) (<= maxCos 1.0)))
  (let* ((t_0 (* PI (+ uy uy))))
  (fma
   (* zi (- 1.0 ux))
   (* maxCos ux)
   (*
    (sqrt
     (fma
      (* (- ux 1.0) maxCos)
      (* (* (* maxCos (- 1.0 ux)) ux) ux)
      1.0))
    (fma (sin t_0) yi (* (cos t_0) xi))))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = ((float) M_PI) * (uy + uy);
	return fmaf((zi * (1.0f - ux)), (maxCos * ux), (sqrtf(fmaf(((ux - 1.0f) * maxCos), (((maxCos * (1.0f - ux)) * ux) * ux), 1.0f)) * fmaf(sinf(t_0), yi, (cosf(t_0) * xi))));
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(pi) * Float32(uy + uy))
	return fma(Float32(zi * Float32(Float32(1.0) - ux)), Float32(maxCos * ux), Float32(sqrt(fma(Float32(Float32(ux - Float32(1.0)) * maxCos), Float32(Float32(Float32(maxCos * Float32(Float32(1.0) - ux)) * ux) * ux), Float32(1.0))) * fma(sin(t_0), yi, Float32(cos(t_0) * xi))))
end
\begin{array}{l}
t_0 := \pi \cdot \left(uy + uy\right)\\
\mathsf{fma}\left(zi \cdot \left(1 - ux\right), maxCos \cdot ux, \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, \left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot ux, 1\right)} \cdot \mathsf{fma}\left(\sin t\_0, yi, \cos t\_0 \cdot xi\right)\right)
\end{array}
Derivation
  1. Initial program 98.9%

    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  2. Applied rewrites99.0%

    \[\leadsto \mathsf{fma}\left(zi \cdot \left(1 - ux\right), maxCos \cdot ux, \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, \left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot ux, 1\right)} \cdot \mathsf{fma}\left(\sin \left(\pi \cdot \left(uy + uy\right)\right), yi, \cos \left(\pi \cdot \left(uy + uy\right)\right) \cdot xi\right)\right) \]
  3. Add Preprocessing

Alternative 3: 98.9% accurate, 1.3× speedup?

\[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
\[\begin{array}{l} t_0 := \pi \cdot \left(uy + uy\right)\\ \mathsf{fma}\left(zi \cdot \left(1 - ux\right), maxCos \cdot ux, \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, \left(maxCos \cdot ux\right) \cdot ux, 1\right)} \cdot \mathsf{fma}\left(\sin t\_0, yi, \cos t\_0 \cdot xi\right)\right) \end{array} \]
(FPCore (xi yi zi ux uy maxCos)
  :precision binary32
  :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                         (and (<= -10000.0 yi) (<= yi 10000.0)))
                    (and (<= -10000.0 zi) (<= zi 10000.0)))
               (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
          (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
     (and (<= 0.0 maxCos) (<= maxCos 1.0)))
  (let* ((t_0 (* PI (+ uy uy))))
  (fma
   (* zi (- 1.0 ux))
   (* maxCos ux)
   (*
    (sqrt (fma (* (- ux 1.0) maxCos) (* (* maxCos ux) ux) 1.0))
    (fma (sin t_0) yi (* (cos t_0) xi))))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	float t_0 = ((float) M_PI) * (uy + uy);
	return fmaf((zi * (1.0f - ux)), (maxCos * ux), (sqrtf(fmaf(((ux - 1.0f) * maxCos), ((maxCos * ux) * ux), 1.0f)) * fmaf(sinf(t_0), yi, (cosf(t_0) * xi))));
}
function code(xi, yi, zi, ux, uy, maxCos)
	t_0 = Float32(Float32(pi) * Float32(uy + uy))
	return fma(Float32(zi * Float32(Float32(1.0) - ux)), Float32(maxCos * ux), Float32(sqrt(fma(Float32(Float32(ux - Float32(1.0)) * maxCos), Float32(Float32(maxCos * ux) * ux), Float32(1.0))) * fma(sin(t_0), yi, Float32(cos(t_0) * xi))))
end
\begin{array}{l}
t_0 := \pi \cdot \left(uy + uy\right)\\
\mathsf{fma}\left(zi \cdot \left(1 - ux\right), maxCos \cdot ux, \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, \left(maxCos \cdot ux\right) \cdot ux, 1\right)} \cdot \mathsf{fma}\left(\sin t\_0, yi, \cos t\_0 \cdot xi\right)\right)
\end{array}
Derivation
  1. Initial program 98.9%

    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
  2. Applied rewrites99.0%

    \[\leadsto \mathsf{fma}\left(zi \cdot \left(1 - ux\right), maxCos \cdot ux, \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, \left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux\right) \cdot ux, 1\right)} \cdot \mathsf{fma}\left(\sin \left(\pi \cdot \left(uy + uy\right)\right), yi, \cos \left(\pi \cdot \left(uy + uy\right)\right) \cdot xi\right)\right) \]
  3. Taylor expanded in ux around 0

    \[\leadsto \mathsf{fma}\left(zi \cdot \left(1 - ux\right), maxCos \cdot ux, \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, \left(maxCos \cdot ux\right) \cdot ux, 1\right)} \cdot \mathsf{fma}\left(\sin \left(\pi \cdot \left(uy + uy\right)\right), yi, \cos \left(\pi \cdot \left(uy + uy\right)\right) \cdot xi\right)\right) \]
  4. Step-by-step derivation
    1. Applied rewrites98.9%

      \[\leadsto \mathsf{fma}\left(zi \cdot \left(1 - ux\right), maxCos \cdot ux, \sqrt{\mathsf{fma}\left(\left(ux - 1\right) \cdot maxCos, \left(maxCos \cdot ux\right) \cdot ux, 1\right)} \cdot \mathsf{fma}\left(\sin \left(\pi \cdot \left(uy + uy\right)\right), yi, \cos \left(\pi \cdot \left(uy + uy\right)\right) \cdot xi\right)\right) \]
    2. Add Preprocessing

    Alternative 4: 98.8% accurate, 1.6× speedup?

    \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
    \[\begin{array}{l} t_0 := \left(\pi + \pi\right) \cdot uy\\ \mathsf{fma}\left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux, zi, \mathsf{fma}\left(\sin t\_0, yi, \cos t\_0 \cdot xi\right)\right) \end{array} \]
    (FPCore (xi yi zi ux uy maxCos)
      :precision binary32
      :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                             (and (<= -10000.0 yi) (<= yi 10000.0)))
                        (and (<= -10000.0 zi) (<= zi 10000.0)))
                   (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
              (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
         (and (<= 0.0 maxCos) (<= maxCos 1.0)))
      (let* ((t_0 (* (+ PI PI) uy)))
      (fma
       (* (* maxCos (- 1.0 ux)) ux)
       zi
       (fma (sin t_0) yi (* (cos t_0) xi)))))
    float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
    	float t_0 = (((float) M_PI) + ((float) M_PI)) * uy;
    	return fmaf(((maxCos * (1.0f - ux)) * ux), zi, fmaf(sinf(t_0), yi, (cosf(t_0) * xi)));
    }
    
    function code(xi, yi, zi, ux, uy, maxCos)
    	t_0 = Float32(Float32(Float32(pi) + Float32(pi)) * uy)
    	return fma(Float32(Float32(maxCos * Float32(Float32(1.0) - ux)) * ux), zi, fma(sin(t_0), yi, Float32(cos(t_0) * xi)))
    end
    
    \begin{array}{l}
    t_0 := \left(\pi + \pi\right) \cdot uy\\
    \mathsf{fma}\left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux, zi, \mathsf{fma}\left(\sin t\_0, yi, \cos t\_0 \cdot xi\right)\right)
    \end{array}
    
    Derivation
    1. Initial program 98.9%

      \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    2. Taylor expanded in xi around 0

      \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
    3. Step-by-step derivation
      1. Applied rewrites44.0%

        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right) \]
      2. Taylor expanded in maxCos around 0

        \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + \left(xi \cdot \cos \left(2 \cdot \left(uy \cdot \pi\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right) \]
      3. Step-by-step derivation
        1. Applied rewrites98.8%

          \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right)\right) \]
        2. Applied rewrites98.8%

          \[\leadsto \mathsf{fma}\left(\left(maxCos \cdot \left(1 - ux\right)\right) \cdot ux, zi, \mathsf{fma}\left(\sin \left(\left(\pi + \pi\right) \cdot uy\right), yi, \cos \left(\left(\pi + \pi\right) \cdot uy\right) \cdot xi\right)\right) \]
        3. Add Preprocessing

        Alternative 5: 97.3% accurate, 1.7× speedup?

        \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
        \[\begin{array}{l} t_0 := 2 \cdot \left(uy \cdot \pi\right)\\ \mathbf{if}\;uy \leq 0.007000000216066837:\\ \;\;\;\;\mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + uy \cdot \mathsf{fma}\left(2, yi \cdot \pi, uy \cdot \mathsf{fma}\left(-2, xi \cdot {\pi}^{2}, -1.3333333333333333 \cdot \left(uy \cdot \left(yi \cdot {\pi}^{3}\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(xi, \cos t\_0, yi \cdot \sin t\_0\right)\\ \end{array} \]
        (FPCore (xi yi zi ux uy maxCos)
          :precision binary32
          :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                 (and (<= -10000.0 yi) (<= yi 10000.0)))
                            (and (<= -10000.0 zi) (<= zi 10000.0)))
                       (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                  (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
             (and (<= 0.0 maxCos) (<= maxCos 1.0)))
          (let* ((t_0 (* 2.0 (* uy PI))))
          (if (<= uy 0.007000000216066837)
            (fma
             maxCos
             (* ux (* zi (- 1.0 ux)))
             (+
              xi
              (*
               uy
               (fma
                2.0
                (* yi PI)
                (*
                 uy
                 (fma
                  -2.0
                  (* xi (pow PI 2.0))
                  (* -1.3333333333333333 (* uy (* yi (pow PI 3.0))))))))))
            (fma xi (cos t_0) (* yi (sin t_0))))))
        float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
        	float t_0 = 2.0f * (uy * ((float) M_PI));
        	float tmp;
        	if (uy <= 0.007000000216066837f) {
        		tmp = fmaf(maxCos, (ux * (zi * (1.0f - ux))), (xi + (uy * fmaf(2.0f, (yi * ((float) M_PI)), (uy * fmaf(-2.0f, (xi * powf(((float) M_PI), 2.0f)), (-1.3333333333333333f * (uy * (yi * powf(((float) M_PI), 3.0f))))))))));
        	} else {
        		tmp = fmaf(xi, cosf(t_0), (yi * sinf(t_0)));
        	}
        	return tmp;
        }
        
        function code(xi, yi, zi, ux, uy, maxCos)
        	t_0 = Float32(Float32(2.0) * Float32(uy * Float32(pi)))
        	tmp = Float32(0.0)
        	if (uy <= Float32(0.007000000216066837))
        		tmp = fma(maxCos, Float32(ux * Float32(zi * Float32(Float32(1.0) - ux))), Float32(xi + Float32(uy * fma(Float32(2.0), Float32(yi * Float32(pi)), Float32(uy * fma(Float32(-2.0), Float32(xi * (Float32(pi) ^ Float32(2.0))), Float32(Float32(-1.3333333333333333) * Float32(uy * Float32(yi * (Float32(pi) ^ Float32(3.0)))))))))));
        	else
        		tmp = fma(xi, cos(t_0), Float32(yi * sin(t_0)));
        	end
        	return tmp
        end
        
        \begin{array}{l}
        t_0 := 2 \cdot \left(uy \cdot \pi\right)\\
        \mathbf{if}\;uy \leq 0.007000000216066837:\\
        \;\;\;\;\mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + uy \cdot \mathsf{fma}\left(2, yi \cdot \pi, uy \cdot \mathsf{fma}\left(-2, xi \cdot {\pi}^{2}, -1.3333333333333333 \cdot \left(uy \cdot \left(yi \cdot {\pi}^{3}\right)\right)\right)\right)\right)\\
        
        \mathbf{else}:\\
        \;\;\;\;\mathsf{fma}\left(xi, \cos t\_0, yi \cdot \sin t\_0\right)\\
        
        
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if uy < 0.00700000022

          1. Initial program 98.9%

            \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
          2. Taylor expanded in xi around 0

            \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
          3. Step-by-step derivation
            1. Applied rewrites44.0%

              \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right) \]
            2. Taylor expanded in maxCos around 0

              \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + \left(xi \cdot \cos \left(2 \cdot \left(uy \cdot \pi\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right) \]
            3. Step-by-step derivation
              1. Applied rewrites98.8%

                \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right)\right) \]
              2. Taylor expanded in uy around 0

                \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + uy \cdot \left(2 \cdot \left(yi \cdot \pi\right) + uy \cdot \left(-2 \cdot \left(xi \cdot {\pi}^{2}\right) + \frac{-4}{3} \cdot \left(uy \cdot \left(yi \cdot {\pi}^{3}\right)\right)\right)\right)\right) \]
              3. Step-by-step derivation
                1. Applied rewrites89.6%

                  \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + uy \cdot \mathsf{fma}\left(2, yi \cdot \pi, uy \cdot \mathsf{fma}\left(-2, xi \cdot {\pi}^{2}, -1.3333333333333333 \cdot \left(uy \cdot \left(yi \cdot {\pi}^{3}\right)\right)\right)\right)\right) \]

                if 0.00700000022 < uy

                1. Initial program 98.9%

                  \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                2. Taylor expanded in xi around 0

                  \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                3. Step-by-step derivation
                  1. Applied rewrites44.0%

                    \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right) \]
                  2. Taylor expanded in ux around 0

                    \[\leadsto xi \cdot \cos \left(2 \cdot \left(uy \cdot \pi\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \]
                  3. Step-by-step derivation
                    1. Applied rewrites90.8%

                      \[\leadsto \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right) \]
                  4. Recombined 2 regimes into one program.
                  5. Add Preprocessing

                  Alternative 6: 95.8% accurate, 1.6× speedup?

                  \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
                  \[\begin{array}{l} t_0 := 2 \cdot \left(uy \cdot \pi\right)\\ \mathsf{fma}\left(maxCos, ux \cdot zi, \mathsf{fma}\left(xi, \cos t\_0, yi \cdot \sin t\_0\right)\right) \end{array} \]
                  (FPCore (xi yi zi ux uy maxCos)
                    :precision binary32
                    :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                           (and (<= -10000.0 yi) (<= yi 10000.0)))
                                      (and (<= -10000.0 zi) (<= zi 10000.0)))
                                 (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                            (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                       (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                    (let* ((t_0 (* 2.0 (* uy PI))))
                    (fma maxCos (* ux zi) (fma xi (cos t_0) (* yi (sin t_0))))))
                  float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                  	float t_0 = 2.0f * (uy * ((float) M_PI));
                  	return fmaf(maxCos, (ux * zi), fmaf(xi, cosf(t_0), (yi * sinf(t_0))));
                  }
                  
                  function code(xi, yi, zi, ux, uy, maxCos)
                  	t_0 = Float32(Float32(2.0) * Float32(uy * Float32(pi)))
                  	return fma(maxCos, Float32(ux * zi), fma(xi, cos(t_0), Float32(yi * sin(t_0))))
                  end
                  
                  \begin{array}{l}
                  t_0 := 2 \cdot \left(uy \cdot \pi\right)\\
                  \mathsf{fma}\left(maxCos, ux \cdot zi, \mathsf{fma}\left(xi, \cos t\_0, yi \cdot \sin t\_0\right)\right)
                  \end{array}
                  
                  Derivation
                  1. Initial program 98.9%

                    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                  2. Taylor expanded in ux around 0

                    \[\leadsto maxCos \cdot \left(ux \cdot zi\right) + \left(xi \cdot \cos \left(2 \cdot \left(uy \cdot \pi\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right) \]
                  3. Step-by-step derivation
                    1. Applied rewrites95.8%

                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot zi, \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right)\right) \]
                    2. Add Preprocessing

                    Alternative 7: 90.2% accurate, 1.9× speedup?

                    \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
                    \[\mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + uy \cdot \mathsf{fma}\left(2, yi \cdot \pi, uy \cdot \mathsf{fma}\left(-2, xi \cdot {\pi}^{2}, -1.3333333333333333 \cdot \left(uy \cdot \left(yi \cdot {\pi}^{3}\right)\right)\right)\right)\right) \]
                    (FPCore (xi yi zi ux uy maxCos)
                      :precision binary32
                      :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                             (and (<= -10000.0 yi) (<= yi 10000.0)))
                                        (and (<= -10000.0 zi) (<= zi 10000.0)))
                                   (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                              (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                         (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                      (fma
                     maxCos
                     (* ux (* zi (- 1.0 ux)))
                     (+
                      xi
                      (*
                       uy
                       (fma
                        2.0
                        (* yi PI)
                        (*
                         uy
                         (fma
                          -2.0
                          (* xi (pow PI 2.0))
                          (* -1.3333333333333333 (* uy (* yi (pow PI 3.0)))))))))))
                    float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                    	return fmaf(maxCos, (ux * (zi * (1.0f - ux))), (xi + (uy * fmaf(2.0f, (yi * ((float) M_PI)), (uy * fmaf(-2.0f, (xi * powf(((float) M_PI), 2.0f)), (-1.3333333333333333f * (uy * (yi * powf(((float) M_PI), 3.0f))))))))));
                    }
                    
                    function code(xi, yi, zi, ux, uy, maxCos)
                    	return fma(maxCos, Float32(ux * Float32(zi * Float32(Float32(1.0) - ux))), Float32(xi + Float32(uy * fma(Float32(2.0), Float32(yi * Float32(pi)), Float32(uy * fma(Float32(-2.0), Float32(xi * (Float32(pi) ^ Float32(2.0))), Float32(Float32(-1.3333333333333333) * Float32(uy * Float32(yi * (Float32(pi) ^ Float32(3.0)))))))))))
                    end
                    
                    \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + uy \cdot \mathsf{fma}\left(2, yi \cdot \pi, uy \cdot \mathsf{fma}\left(-2, xi \cdot {\pi}^{2}, -1.3333333333333333 \cdot \left(uy \cdot \left(yi \cdot {\pi}^{3}\right)\right)\right)\right)\right)
                    
                    Derivation
                    1. Initial program 98.9%

                      \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                    2. Taylor expanded in xi around 0

                      \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                    3. Step-by-step derivation
                      1. Applied rewrites44.0%

                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right) \]
                      2. Taylor expanded in maxCos around 0

                        \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + \left(xi \cdot \cos \left(2 \cdot \left(uy \cdot \pi\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right) \]
                      3. Step-by-step derivation
                        1. Applied rewrites98.8%

                          \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right)\right) \]
                        2. Taylor expanded in uy around 0

                          \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + uy \cdot \left(2 \cdot \left(yi \cdot \pi\right) + uy \cdot \left(-2 \cdot \left(xi \cdot {\pi}^{2}\right) + \frac{-4}{3} \cdot \left(uy \cdot \left(yi \cdot {\pi}^{3}\right)\right)\right)\right)\right) \]
                        3. Step-by-step derivation
                          1. Applied rewrites89.6%

                            \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + uy \cdot \mathsf{fma}\left(2, yi \cdot \pi, uy \cdot \mathsf{fma}\left(-2, xi \cdot {\pi}^{2}, -1.3333333333333333 \cdot \left(uy \cdot \left(yi \cdot {\pi}^{3}\right)\right)\right)\right)\right) \]
                          2. Add Preprocessing

                          Alternative 8: 89.6% accurate, 2.3× speedup?

                          \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
                          \[\mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)\right)\right) \]
                          (FPCore (xi yi zi ux uy maxCos)
                            :precision binary32
                            :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                                   (and (<= -10000.0 yi) (<= yi 10000.0)))
                                              (and (<= -10000.0 zi) (<= zi 10000.0)))
                                         (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                                    (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                               (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                            (fma
                           maxCos
                           (* ux (* zi (- 1.0 ux)))
                           (fma xi (cos (* 2.0 (* uy PI))) (* 2.0 (* uy (* yi PI))))))
                          float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                          	return fmaf(maxCos, (ux * (zi * (1.0f - ux))), fmaf(xi, cosf((2.0f * (uy * ((float) M_PI)))), (2.0f * (uy * (yi * ((float) M_PI))))));
                          }
                          
                          function code(xi, yi, zi, ux, uy, maxCos)
                          	return fma(maxCos, Float32(ux * Float32(zi * Float32(Float32(1.0) - ux))), fma(xi, cos(Float32(Float32(2.0) * Float32(uy * Float32(pi)))), Float32(Float32(2.0) * Float32(uy * Float32(yi * Float32(pi))))))
                          end
                          
                          \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)\right)\right)
                          
                          Derivation
                          1. Initial program 98.9%

                            \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                          2. Taylor expanded in xi around 0

                            \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                          3. Step-by-step derivation
                            1. Applied rewrites44.0%

                              \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right) \]
                            2. Taylor expanded in maxCos around 0

                              \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + \left(xi \cdot \cos \left(2 \cdot \left(uy \cdot \pi\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right) \]
                            3. Step-by-step derivation
                              1. Applied rewrites98.8%

                                \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right)\right) \]
                              2. Taylor expanded in uy around 0

                                \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)\right)\right) \]
                              3. Step-by-step derivation
                                1. Applied rewrites90.2%

                                  \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)\right)\right) \]
                                2. Add Preprocessing

                                Alternative 9: 86.1% accurate, 2.9× speedup?

                                \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
                                \[xi + \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(xi \cdot {\pi}^{2}\right), 2 \cdot \left(yi \cdot \pi\right)\right)\right) \]
                                (FPCore (xi yi zi ux uy maxCos)
                                  :precision binary32
                                  :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                                         (and (<= -10000.0 yi) (<= yi 10000.0)))
                                                    (and (<= -10000.0 zi) (<= zi 10000.0)))
                                               (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                                          (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                     (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                  (+
                                 xi
                                 (fma
                                  maxCos
                                  (* ux (* zi (- 1.0 ux)))
                                  (* uy (fma -2.0 (* uy (* xi (pow PI 2.0))) (* 2.0 (* yi PI)))))))
                                float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                	return xi + fmaf(maxCos, (ux * (zi * (1.0f - ux))), (uy * fmaf(-2.0f, (uy * (xi * powf(((float) M_PI), 2.0f))), (2.0f * (yi * ((float) M_PI))))));
                                }
                                
                                function code(xi, yi, zi, ux, uy, maxCos)
                                	return Float32(xi + fma(maxCos, Float32(ux * Float32(zi * Float32(Float32(1.0) - ux))), Float32(uy * fma(Float32(-2.0), Float32(uy * Float32(xi * (Float32(pi) ^ Float32(2.0)))), Float32(Float32(2.0) * Float32(yi * Float32(pi)))))))
                                end
                                
                                xi + \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(xi \cdot {\pi}^{2}\right), 2 \cdot \left(yi \cdot \pi\right)\right)\right)
                                
                                Derivation
                                1. Initial program 98.9%

                                  \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                2. Taylor expanded in xi around 0

                                  \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                3. Step-by-step derivation
                                  1. Applied rewrites44.0%

                                    \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right) \]
                                  2. Taylor expanded in maxCos around 0

                                    \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + \left(xi \cdot \cos \left(2 \cdot \left(uy \cdot \pi\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right) \]
                                  3. Step-by-step derivation
                                    1. Applied rewrites98.8%

                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right)\right) \]
                                    2. Taylor expanded in uy around 0

                                      \[\leadsto xi + \left(maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + uy \cdot \left(-2 \cdot \left(uy \cdot \left(xi \cdot {\pi}^{2}\right)\right) + 2 \cdot \left(yi \cdot \pi\right)\right)\right) \]
                                    3. Step-by-step derivation
                                      1. Applied rewrites86.1%

                                        \[\leadsto xi + \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(xi \cdot {\pi}^{2}\right), 2 \cdot \left(yi \cdot \pi\right)\right)\right) \]
                                      2. Add Preprocessing

                                      Alternative 10: 81.8% accurate, 6.1× speedup?

                                      \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
                                      \[xi + \mathsf{fma}\left(2, uy \cdot \left(yi \cdot \pi\right), maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)\right) \]
                                      (FPCore (xi yi zi ux uy maxCos)
                                        :precision binary32
                                        :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                                               (and (<= -10000.0 yi) (<= yi 10000.0)))
                                                          (and (<= -10000.0 zi) (<= zi 10000.0)))
                                                     (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                                                (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                           (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                        (+ xi (fma 2.0 (* uy (* yi PI)) (* maxCos (* ux (* zi (- 1.0 ux)))))))
                                      float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                      	return xi + fmaf(2.0f, (uy * (yi * ((float) M_PI))), (maxCos * (ux * (zi * (1.0f - ux)))));
                                      }
                                      
                                      function code(xi, yi, zi, ux, uy, maxCos)
                                      	return Float32(xi + fma(Float32(2.0), Float32(uy * Float32(yi * Float32(pi))), Float32(maxCos * Float32(ux * Float32(zi * Float32(Float32(1.0) - ux))))))
                                      end
                                      
                                      xi + \mathsf{fma}\left(2, uy \cdot \left(yi \cdot \pi\right), maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)\right)
                                      
                                      Derivation
                                      1. Initial program 98.9%

                                        \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                      2. Taylor expanded in xi around 0

                                        \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                      3. Step-by-step derivation
                                        1. Applied rewrites44.0%

                                          \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right) \]
                                        2. Taylor expanded in maxCos around 0

                                          \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + \left(xi \cdot \cos \left(2 \cdot \left(uy \cdot \pi\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right) \]
                                        3. Step-by-step derivation
                                          1. Applied rewrites98.8%

                                            \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right)\right) \]
                                          2. Taylor expanded in uy around 0

                                            \[\leadsto xi + \left(2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right) + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)\right) \]
                                          3. Step-by-step derivation
                                            1. Applied rewrites81.8%

                                              \[\leadsto xi + \mathsf{fma}\left(2, uy \cdot \left(yi \cdot \pi\right), maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)\right) \]
                                            2. Add Preprocessing

                                            Alternative 11: 81.8% accurate, 6.1× speedup?

                                            \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
                                            \[\mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)\right) \]
                                            (FPCore (xi yi zi ux uy maxCos)
                                              :precision binary32
                                              :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                                                     (and (<= -10000.0 yi) (<= yi 10000.0)))
                                                                (and (<= -10000.0 zi) (<= zi 10000.0)))
                                                           (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                                                      (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                                 (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                              (fma maxCos (* ux (* zi (- 1.0 ux))) (+ xi (* 2.0 (* uy (* yi PI))))))
                                            float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                            	return fmaf(maxCos, (ux * (zi * (1.0f - ux))), (xi + (2.0f * (uy * (yi * ((float) M_PI))))));
                                            }
                                            
                                            function code(xi, yi, zi, ux, uy, maxCos)
                                            	return fma(maxCos, Float32(ux * Float32(zi * Float32(Float32(1.0) - ux))), Float32(xi + Float32(Float32(2.0) * Float32(uy * Float32(yi * Float32(pi))))))
                                            end
                                            
                                            \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)\right)
                                            
                                            Derivation
                                            1. Initial program 98.9%

                                              \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                            2. Taylor expanded in xi around 0

                                              \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                            3. Step-by-step derivation
                                              1. Applied rewrites44.0%

                                                \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), yi \cdot \left(\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right) \]
                                              2. Taylor expanded in maxCos around 0

                                                \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + \left(xi \cdot \cos \left(2 \cdot \left(uy \cdot \pi\right)\right) + yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right) \]
                                              3. Step-by-step derivation
                                                1. Applied rewrites98.8%

                                                  \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \mathsf{fma}\left(xi, \cos \left(2 \cdot \left(uy \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \cdot \pi\right)\right)\right)\right) \]
                                                2. Taylor expanded in uy around 0

                                                  \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)\right) \]
                                                3. Step-by-step derivation
                                                  1. Applied rewrites81.8%

                                                    \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi + 2 \cdot \left(uy \cdot \left(yi \cdot \pi\right)\right)\right) \]
                                                  2. Add Preprocessing

                                                  Alternative 12: 51.9% accurate, 10.5× speedup?

                                                  \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
                                                  \[xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) \]
                                                  (FPCore (xi yi zi ux uy maxCos)
                                                    :precision binary32
                                                    :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                                                           (and (<= -10000.0 yi) (<= yi 10000.0)))
                                                                      (and (<= -10000.0 zi) (<= zi 10000.0)))
                                                                 (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                                                            (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                                       (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                                    (+ xi (* maxCos (* ux (* zi (- 1.0 ux))))))
                                                  float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                                  	return xi + (maxCos * (ux * (zi * (1.0f - ux))));
                                                  }
                                                  
                                                  real(4) function code(xi, yi, zi, ux, uy, maxcos)
                                                  use fmin_fmax_functions
                                                      real(4), intent (in) :: xi
                                                      real(4), intent (in) :: yi
                                                      real(4), intent (in) :: zi
                                                      real(4), intent (in) :: ux
                                                      real(4), intent (in) :: uy
                                                      real(4), intent (in) :: maxcos
                                                      code = xi + (maxcos * (ux * (zi * (1.0e0 - ux))))
                                                  end function
                                                  
                                                  function code(xi, yi, zi, ux, uy, maxCos)
                                                  	return Float32(xi + Float32(maxCos * Float32(ux * Float32(zi * Float32(Float32(1.0) - ux)))))
                                                  end
                                                  
                                                  function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                                  	tmp = xi + (maxCos * (ux * (zi * (single(1.0) - ux))));
                                                  end
                                                  
                                                  xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)
                                                  
                                                  Derivation
                                                  1. Initial program 98.9%

                                                    \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                                  2. Taylor expanded in uy around 0

                                                    \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} \]
                                                  3. Step-by-step derivation
                                                    1. Applied rewrites52.0%

                                                      \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                                    2. Taylor expanded in maxCos around 0

                                                      \[\leadsto xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) \]
                                                    3. Step-by-step derivation
                                                      1. Applied rewrites51.9%

                                                        \[\leadsto xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) \]
                                                      2. Add Preprocessing

                                                      Alternative 13: 49.8% accurate, 17.7× speedup?

                                                      \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
                                                      \[\mathsf{fma}\left(maxCos \cdot ux, zi, xi\right) \]
                                                      (FPCore (xi yi zi ux uy maxCos)
                                                        :precision binary32
                                                        :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                                                               (and (<= -10000.0 yi) (<= yi 10000.0)))
                                                                          (and (<= -10000.0 zi) (<= zi 10000.0)))
                                                                     (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                                                                (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                                           (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                                        (fma (* maxCos ux) zi xi))
                                                      float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                                      	return fmaf((maxCos * ux), zi, xi);
                                                      }
                                                      
                                                      function code(xi, yi, zi, ux, uy, maxCos)
                                                      	return fma(Float32(maxCos * ux), zi, xi)
                                                      end
                                                      
                                                      \mathsf{fma}\left(maxCos \cdot ux, zi, xi\right)
                                                      
                                                      Derivation
                                                      1. Initial program 98.9%

                                                        \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                                      2. Taylor expanded in uy around 0

                                                        \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} \]
                                                      3. Step-by-step derivation
                                                        1. Applied rewrites52.0%

                                                          \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                                        2. Taylor expanded in ux around 0

                                                          \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\right) \]
                                                        3. Step-by-step derivation
                                                          1. Applied rewrites49.8%

                                                            \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\right) \]
                                                          2. Step-by-step derivation
                                                            1. Applied rewrites49.8%

                                                              \[\leadsto \mathsf{fma}\left(maxCos \cdot ux, zi, xi\right) \]
                                                            2. Add Preprocessing

                                                            Alternative 14: 11.8% accurate, 22.8× speedup?

                                                            \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
                                                            \[\left(maxCos \cdot ux\right) \cdot zi \]
                                                            (FPCore (xi yi zi ux uy maxCos)
                                                              :precision binary32
                                                              :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                                                                     (and (<= -10000.0 yi) (<= yi 10000.0)))
                                                                                (and (<= -10000.0 zi) (<= zi 10000.0)))
                                                                           (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                                                                      (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                                                 (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                                              (* (* maxCos ux) zi))
                                                            float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                                            	return (maxCos * ux) * zi;
                                                            }
                                                            
                                                            real(4) function code(xi, yi, zi, ux, uy, maxcos)
                                                            use fmin_fmax_functions
                                                                real(4), intent (in) :: xi
                                                                real(4), intent (in) :: yi
                                                                real(4), intent (in) :: zi
                                                                real(4), intent (in) :: ux
                                                                real(4), intent (in) :: uy
                                                                real(4), intent (in) :: maxcos
                                                                code = (maxcos * ux) * zi
                                                            end function
                                                            
                                                            function code(xi, yi, zi, ux, uy, maxCos)
                                                            	return Float32(Float32(maxCos * ux) * zi)
                                                            end
                                                            
                                                            function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                                            	tmp = (maxCos * ux) * zi;
                                                            end
                                                            
                                                            \left(maxCos \cdot ux\right) \cdot zi
                                                            
                                                            Derivation
                                                            1. Initial program 98.9%

                                                              \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                                            2. Taylor expanded in uy around 0

                                                              \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} \]
                                                            3. Step-by-step derivation
                                                              1. Applied rewrites52.0%

                                                                \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                                              2. Taylor expanded in ux around 0

                                                                \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\right) \]
                                                              3. Step-by-step derivation
                                                                1. Applied rewrites49.8%

                                                                  \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\right) \]
                                                                2. Taylor expanded in xi around 0

                                                                  \[\leadsto maxCos \cdot \left(ux \cdot zi\right) \]
                                                                3. Step-by-step derivation
                                                                  1. Applied rewrites11.8%

                                                                    \[\leadsto maxCos \cdot \left(ux \cdot zi\right) \]
                                                                  2. Step-by-step derivation
                                                                    1. Applied rewrites11.8%

                                                                      \[\leadsto \left(maxCos \cdot ux\right) \cdot zi \]
                                                                    2. Add Preprocessing

                                                                    Alternative 15: 11.8% accurate, 22.8× speedup?

                                                                    \[\left(\left(\left(\left(\left(-10000 \leq xi \land xi \leq 10000\right) \land \left(-10000 \leq yi \land yi \leq 10000\right)\right) \land \left(-10000 \leq zi \land zi \leq 10000\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
                                                                    \[maxCos \cdot \left(ux \cdot zi\right) \]
                                                                    (FPCore (xi yi zi ux uy maxCos)
                                                                      :precision binary32
                                                                      :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0))
                                                                                             (and (<= -10000.0 yi) (<= yi 10000.0)))
                                                                                        (and (<= -10000.0 zi) (<= zi 10000.0)))
                                                                                   (and (<= 2.328306437e-10 ux) (<= ux 1.0)))
                                                                              (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                                                         (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                                                      (* maxCos (* ux zi)))
                                                                    float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                                                    	return maxCos * (ux * zi);
                                                                    }
                                                                    
                                                                    real(4) function code(xi, yi, zi, ux, uy, maxcos)
                                                                    use fmin_fmax_functions
                                                                        real(4), intent (in) :: xi
                                                                        real(4), intent (in) :: yi
                                                                        real(4), intent (in) :: zi
                                                                        real(4), intent (in) :: ux
                                                                        real(4), intent (in) :: uy
                                                                        real(4), intent (in) :: maxcos
                                                                        code = maxcos * (ux * zi)
                                                                    end function
                                                                    
                                                                    function code(xi, yi, zi, ux, uy, maxCos)
                                                                    	return Float32(maxCos * Float32(ux * zi))
                                                                    end
                                                                    
                                                                    function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                                                    	tmp = maxCos * (ux * zi);
                                                                    end
                                                                    
                                                                    maxCos \cdot \left(ux \cdot zi\right)
                                                                    
                                                                    Derivation
                                                                    1. Initial program 98.9%

                                                                      \[\left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right)}\right) \cdot yi\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
                                                                    2. Taylor expanded in uy around 0

                                                                      \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)} \]
                                                                    3. Step-by-step derivation
                                                                      1. Applied rewrites52.0%

                                                                        \[\leadsto \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                                                      2. Taylor expanded in ux around 0

                                                                        \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\right) \]
                                                                      3. Step-by-step derivation
                                                                        1. Applied rewrites49.8%

                                                                          \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\right) \]
                                                                        2. Taylor expanded in xi around 0

                                                                          \[\leadsto maxCos \cdot \left(ux \cdot zi\right) \]
                                                                        3. Step-by-step derivation
                                                                          1. Applied rewrites11.8%

                                                                            \[\leadsto maxCos \cdot \left(ux \cdot zi\right) \]
                                                                          2. Add Preprocessing

                                                                          Reproduce

                                                                          ?
                                                                          herbie shell --seed 2025359 
                                                                          (FPCore (xi yi zi ux uy maxCos)
                                                                            :name "UniformSampleCone 2"
                                                                            :precision binary32
                                                                            :pre (and (and (and (and (and (and (<= -10000.0 xi) (<= xi 10000.0)) (and (<= -10000.0 yi) (<= yi 10000.0))) (and (<= -10000.0 zi) (<= zi 10000.0))) (and (<= 2.328306437e-10 ux) (<= ux 1.0))) (and (<= 2.328306437e-10 uy) (<= uy 1.0))) (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                                                            (+ (+ (* (* (cos (* (* uy 2.0) PI)) (sqrt (- 1.0 (* (* (* (- 1.0 ux) maxCos) ux) (* (* (- 1.0 ux) maxCos) ux))))) xi) (* (* (sin (* (* uy 2.0) PI)) (sqrt (- 1.0 (* (* (* (- 1.0 ux) maxCos) ux) (* (* (- 1.0 ux) maxCos) ux))))) yi)) (* (* (* (- 1.0 ux) maxCos) ux) zi)))