UniformSampleCone 2

Percentage Accurate: 98.9% → 99.0%
Time: 8.5s
Alternatives: 19
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 19 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.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)\]
\[\mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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, \sin \left(\mathsf{fma}\left(-2 \cdot uy, \pi, \pi \cdot 0.5\right)\right) \cdot xi\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
 (* ux (- 1.0 ux))
 (* maxCos zi)
 (*
  (sqrt
   (fma
    (* (- ux 1.0) maxCos)
    (* (* (* maxCos (- 1.0 ux)) ux) ux)
    1.0))
  (fma
   (sin (* PI (+ uy uy)))
   yi
   (* (sin (fma (* -2.0 uy) PI (* PI 0.5))) xi)))))
float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
	return fmaf((ux * (1.0f - ux)), (maxCos * zi), (sqrtf(fmaf(((ux - 1.0f) * maxCos), (((maxCos * (1.0f - ux)) * ux) * ux), 1.0f)) * fmaf(sinf((((float) M_PI) * (uy + uy))), yi, (sinf(fmaf((-2.0f * uy), ((float) M_PI), (((float) M_PI) * 0.5f))) * xi))));
}
function code(xi, yi, zi, ux, uy, maxCos)
	return fma(Float32(ux * Float32(Float32(1.0) - ux)), Float32(maxCos * zi), 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(Float32(Float32(pi) * Float32(uy + uy))), yi, Float32(sin(fma(Float32(Float32(-2.0) * uy), Float32(pi), Float32(Float32(pi) * Float32(0.5)))) * xi))))
end
\mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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, \sin \left(\mathsf{fma}\left(-2 \cdot uy, \pi, \pi \cdot 0.5\right)\right) \cdot xi\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. Applied rewrites99.0%

    \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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. Step-by-step derivation
    1. Applied rewrites99.0%

      \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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, \sin \left(\mathsf{fma}\left(-2 \cdot uy, \pi, \pi \cdot 0.5\right)\right) \cdot xi\right)\right) \]
    2. 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(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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
       (* ux (- 1.0 ux))
       (* maxCos zi)
       (*
        (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((ux * (1.0f - ux)), (maxCos * zi), (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(ux * Float32(Float32(1.0) - ux)), Float32(maxCos * zi), 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(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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.8% accurate, 1.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)\]
    \[\begin{array}{l} t_0 := 2 \cdot \left(uy \cdot \pi\right)\\ \mathsf{fma}\left(xi, \cos t\_0, yi \cdot \sin t\_0\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \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 (* 2.0 (* uy PI))))
      (+
       (fma xi (cos t_0) (* yi (sin t_0)))
       (* (* (* (- 1.0 ux) maxCos) ux) zi))))
    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(xi, cosf(t_0), (yi * sinf(t_0))) + ((((1.0f - ux) * maxCos) * ux) * zi);
    }
    
    function code(xi, yi, zi, ux, uy, maxCos)
    	t_0 = Float32(Float32(2.0) * Float32(uy * Float32(pi)))
    	return Float32(fma(xi, cos(t_0), Float32(yi * sin(t_0))) + Float32(Float32(Float32(Float32(Float32(1.0) - ux) * maxCos) * ux) * zi))
    end
    
    \begin{array}{l}
    t_0 := 2 \cdot \left(uy \cdot \pi\right)\\
    \mathsf{fma}\left(xi, \cos t\_0, yi \cdot \sin t\_0\right) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi
    \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 \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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
    3. Step-by-step derivation
      1. Applied rewrites98.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) + \left(\left(\left(1 - ux\right) \cdot maxCos\right) \cdot ux\right) \cdot zi \]
      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 := 2 \cdot \left(uy \cdot \pi\right)\\ \mathsf{fma}\left(maxCos, ux \cdot \left(zi \cdot \left(1 - ux\right)\right), \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 (- 1.0 ux)))
         (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 * (1.0f - ux))), 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 * Float32(zi * Float32(Float32(1.0) - ux))), 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 \left(zi \cdot \left(1 - ux\right)\right), \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 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.2%

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

            \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\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. Add Preprocessing

            Alternative 5: 97.4% 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.018200000748038292:\\ \;\;\;\;\mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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(\left(yi + yi\right) \cdot uy, \pi, \mathsf{fma}\left(uy \cdot uy, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right), xi\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.018200000748038292)
                (fma
                 (* ux (- 1.0 ux))
                 (* maxCos zi)
                 (*
                  (sqrt
                   (fma
                    (* (- ux 1.0) maxCos)
                    (* (* (* maxCos (- 1.0 ux)) ux) ux)
                    1.0))
                  (fma
                   (* (+ yi yi) uy)
                   PI
                   (fma
                    (* uy uy)
                    (fma
                     (* (* PI PI) xi)
                     -2.0
                     (* (* (* (* (* PI PI) PI) yi) uy) -1.3333333333333333))
                    xi))))
                (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.018200000748038292f) {
            		tmp = fmaf((ux * (1.0f - ux)), (maxCos * zi), (sqrtf(fmaf(((ux - 1.0f) * maxCos), (((maxCos * (1.0f - ux)) * ux) * ux), 1.0f)) * fmaf(((yi + yi) * uy), ((float) M_PI), fmaf((uy * uy), fmaf(((((float) M_PI) * ((float) M_PI)) * xi), -2.0f, (((((((float) M_PI) * ((float) M_PI)) * ((float) M_PI)) * yi) * uy) * -1.3333333333333333f)), xi))));
            	} 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.018200000748038292))
            		tmp = fma(Float32(ux * Float32(Float32(1.0) - ux)), Float32(maxCos * zi), 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(Float32(Float32(yi + yi) * uy), Float32(pi), fma(Float32(uy * uy), fma(Float32(Float32(Float32(pi) * Float32(pi)) * xi), Float32(-2.0), Float32(Float32(Float32(Float32(Float32(Float32(pi) * Float32(pi)) * Float32(pi)) * yi) * uy) * Float32(-1.3333333333333333))), xi))));
            	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.018200000748038292:\\
            \;\;\;\;\mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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(\left(yi + yi\right) \cdot uy, \pi, \mathsf{fma}\left(uy \cdot uy, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right), xi\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.0182000007

              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(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 uy around 0

                \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(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)\right) \]
              4. Step-by-step derivation
                1. Applied rewrites89.4%

                  \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(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)\right) \]
                2. Applied rewrites89.4%

                  \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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(\left(yi + yi\right) \cdot uy, \pi, \mathsf{fma}\left(uy \cdot uy, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right), xi\right)\right)\right) \]

                if 0.0182000007 < 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 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.2%

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

                      \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\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.5%

                        \[\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.7% 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)\]
                    \[\mathsf{fma}\left(maxCos, ux \cdot zi, \mathsf{fma}\left(xi, \sin \left(\mathsf{fma}\left(-2, uy \cdot \pi, 0.5 \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \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)
                     (fma
                      xi
                      (sin (fma -2.0 (* uy PI) (* 0.5 PI)))
                      (* yi (sin (* 2.0 (* uy PI)))))))
                    float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                    	return fmaf(maxCos, (ux * zi), fmaf(xi, sinf(fmaf(-2.0f, (uy * ((float) M_PI)), (0.5f * ((float) M_PI)))), (yi * sinf((2.0f * (uy * ((float) M_PI)))))));
                    }
                    
                    function code(xi, yi, zi, ux, uy, maxCos)
                    	return fma(maxCos, Float32(ux * zi), fma(xi, sin(fma(Float32(-2.0), Float32(uy * Float32(pi)), Float32(Float32(0.5) * Float32(pi)))), Float32(yi * sin(Float32(Float32(2.0) * Float32(uy * Float32(pi)))))))
                    end
                    
                    \mathsf{fma}\left(maxCos, ux \cdot zi, \mathsf{fma}\left(xi, \sin \left(\mathsf{fma}\left(-2, uy \cdot \pi, 0.5 \cdot \pi\right)\right), yi \cdot \sin \left(2 \cdot \left(uy \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. Applied rewrites99.0%

                      \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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. Step-by-step derivation
                      1. Applied rewrites99.0%

                        \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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, \sin \left(\mathsf{fma}\left(-2 \cdot uy, \pi, \pi \cdot 0.5\right)\right) \cdot xi\right)\right) \]
                      2. Taylor expanded in ux around 0

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

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

                        Alternative 7: 95.7% 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)\\ \left(\cos t\_0 \cdot xi + \sin t\_0 \cdot yi\right) + \left(maxCos \cdot ux\right) \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 (* 2.0 (* uy PI))))
                          (+ (+ (* (cos t_0) xi) (* (sin t_0) yi)) (* (* maxCos ux) zi))))
                        float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                        	float t_0 = 2.0f * (uy * ((float) M_PI));
                        	return ((cosf(t_0) * xi) + (sinf(t_0) * yi)) + ((maxCos * ux) * zi);
                        }
                        
                        function code(xi, yi, zi, ux, uy, maxCos)
                        	t_0 = Float32(Float32(2.0) * Float32(uy * Float32(pi)))
                        	return Float32(Float32(Float32(cos(t_0) * xi) + Float32(sin(t_0) * yi)) + Float32(Float32(maxCos * ux) * zi))
                        end
                        
                        function tmp = code(xi, yi, zi, ux, uy, maxCos)
                        	t_0 = single(2.0) * (uy * single(pi));
                        	tmp = ((cos(t_0) * xi) + (sin(t_0) * yi)) + ((maxCos * ux) * zi);
                        end
                        
                        \begin{array}{l}
                        t_0 := 2 \cdot \left(uy \cdot \pi\right)\\
                        \left(\cos t\_0 \cdot xi + \sin t\_0 \cdot yi\right) + \left(maxCos \cdot ux\right) \cdot zi
                        \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 \left(\left(\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(maxCos \cdot ux\right) \cdot \left(maxCos \cdot ux\right)}\right) \cdot xi + \left(\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(maxCos \cdot ux\right) \cdot \left(maxCos \cdot ux\right)}\right) \cdot yi\right) + \left(maxCos \cdot ux\right) \cdot zi \]
                        3. Step-by-step derivation
                          1. Applied rewrites95.7%

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

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

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

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

                                \[\leadsto \left(\cos \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot xi + \sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot yi\right) + \left(maxCos \cdot ux\right) \cdot zi \]
                              2. Add Preprocessing

                              Alternative 8: 95.7% 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 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.2%

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

                                    \[\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 9: 89.5% accurate, 1.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)\]
                                  \[\mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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(\left(yi + yi\right) \cdot uy, \pi, \mathsf{fma}\left(uy \cdot uy, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right), xi\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
                                   (* ux (- 1.0 ux))
                                   (* maxCos zi)
                                   (*
                                    (sqrt
                                     (fma
                                      (* (- ux 1.0) maxCos)
                                      (* (* (* maxCos (- 1.0 ux)) ux) ux)
                                      1.0))
                                    (fma
                                     (* (+ yi yi) uy)
                                     PI
                                     (fma
                                      (* uy uy)
                                      (fma
                                       (* (* PI PI) xi)
                                       -2.0
                                       (* (* (* (* (* PI PI) PI) yi) uy) -1.3333333333333333))
                                      xi)))))
                                  float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                  	return fmaf((ux * (1.0f - ux)), (maxCos * zi), (sqrtf(fmaf(((ux - 1.0f) * maxCos), (((maxCos * (1.0f - ux)) * ux) * ux), 1.0f)) * fmaf(((yi + yi) * uy), ((float) M_PI), fmaf((uy * uy), fmaf(((((float) M_PI) * ((float) M_PI)) * xi), -2.0f, (((((((float) M_PI) * ((float) M_PI)) * ((float) M_PI)) * yi) * uy) * -1.3333333333333333f)), xi))));
                                  }
                                  
                                  function code(xi, yi, zi, ux, uy, maxCos)
                                  	return fma(Float32(ux * Float32(Float32(1.0) - ux)), Float32(maxCos * zi), 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(Float32(Float32(yi + yi) * uy), Float32(pi), fma(Float32(uy * uy), fma(Float32(Float32(Float32(pi) * Float32(pi)) * xi), Float32(-2.0), Float32(Float32(Float32(Float32(Float32(Float32(pi) * Float32(pi)) * Float32(pi)) * yi) * uy) * Float32(-1.3333333333333333))), xi))))
                                  end
                                  
                                  \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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(\left(yi + yi\right) \cdot uy, \pi, \mathsf{fma}\left(uy \cdot uy, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right), xi\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. Applied rewrites99.0%

                                    \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 uy around 0

                                    \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(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)\right) \]
                                  4. Step-by-step derivation
                                    1. Applied rewrites89.4%

                                      \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(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)\right) \]
                                    2. Applied rewrites89.4%

                                      \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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(\left(yi + yi\right) \cdot uy, \pi, \mathsf{fma}\left(uy \cdot uy, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right), xi\right)\right)\right) \]
                                    3. Add Preprocessing

                                    Alternative 10: 89.4% accurate, 1.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)\]
                                    \[\mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(xi + uy \cdot \mathsf{fma}\left(\pi, yi, \mathsf{fma}\left(yi, \pi, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right) \cdot uy\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
                                     (* ux (- 1.0 ux))
                                     (* maxCos zi)
                                     (*
                                      (sqrt
                                       (fma
                                        (* (- ux 1.0) maxCos)
                                        (* (* (* maxCos (- 1.0 ux)) ux) ux)
                                        1.0))
                                      (+
                                       xi
                                       (*
                                        uy
                                        (fma
                                         PI
                                         yi
                                         (fma
                                          yi
                                          PI
                                          (*
                                           (fma
                                            (* (* PI PI) xi)
                                            -2.0
                                            (* (* (* (* (* PI PI) PI) yi) uy) -1.3333333333333333))
                                           uy))))))))
                                    float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                    	return fmaf((ux * (1.0f - ux)), (maxCos * zi), (sqrtf(fmaf(((ux - 1.0f) * maxCos), (((maxCos * (1.0f - ux)) * ux) * ux), 1.0f)) * (xi + (uy * fmaf(((float) M_PI), yi, fmaf(yi, ((float) M_PI), (fmaf(((((float) M_PI) * ((float) M_PI)) * xi), -2.0f, (((((((float) M_PI) * ((float) M_PI)) * ((float) M_PI)) * yi) * uy) * -1.3333333333333333f)) * uy)))))));
                                    }
                                    
                                    function code(xi, yi, zi, ux, uy, maxCos)
                                    	return fma(Float32(ux * Float32(Float32(1.0) - ux)), Float32(maxCos * zi), Float32(sqrt(fma(Float32(Float32(ux - Float32(1.0)) * maxCos), Float32(Float32(Float32(maxCos * Float32(Float32(1.0) - ux)) * ux) * ux), Float32(1.0))) * Float32(xi + Float32(uy * fma(Float32(pi), yi, fma(yi, Float32(pi), Float32(fma(Float32(Float32(Float32(pi) * Float32(pi)) * xi), Float32(-2.0), Float32(Float32(Float32(Float32(Float32(Float32(pi) * Float32(pi)) * Float32(pi)) * yi) * uy) * Float32(-1.3333333333333333))) * uy)))))))
                                    end
                                    
                                    \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(xi + uy \cdot \mathsf{fma}\left(\pi, yi, \mathsf{fma}\left(yi, \pi, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right) \cdot uy\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. Applied rewrites99.0%

                                      \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 uy around 0

                                      \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(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)\right) \]
                                    4. Step-by-step derivation
                                      1. Applied rewrites89.4%

                                        \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(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)\right) \]
                                      2. Step-by-step derivation
                                        1. Applied rewrites89.4%

                                          \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(xi + uy \cdot \mathsf{fma}\left(\pi, yi, \mathsf{fma}\left(yi, \pi, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right) \cdot uy\right)\right)\right)\right) \]
                                        2. Add Preprocessing

                                        Alternative 11: 89.4% 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(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(xi + uy \cdot \mathsf{fma}\left(\mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right), uy, \left(\pi + \pi\right) \cdot yi\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
                                         (* ux (- 1.0 ux))
                                         (* maxCos zi)
                                         (*
                                          (sqrt
                                           (fma
                                            (* (- ux 1.0) maxCos)
                                            (* (* (* maxCos (- 1.0 ux)) ux) ux)
                                            1.0))
                                          (+
                                           xi
                                           (*
                                            uy
                                            (fma
                                             (fma
                                              (* (* PI PI) xi)
                                              -2.0
                                              (* (* (* (* (* PI PI) PI) yi) uy) -1.3333333333333333))
                                             uy
                                             (* (+ PI PI) yi)))))))
                                        float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                        	return fmaf((ux * (1.0f - ux)), (maxCos * zi), (sqrtf(fmaf(((ux - 1.0f) * maxCos), (((maxCos * (1.0f - ux)) * ux) * ux), 1.0f)) * (xi + (uy * fmaf(fmaf(((((float) M_PI) * ((float) M_PI)) * xi), -2.0f, (((((((float) M_PI) * ((float) M_PI)) * ((float) M_PI)) * yi) * uy) * -1.3333333333333333f)), uy, ((((float) M_PI) + ((float) M_PI)) * yi))))));
                                        }
                                        
                                        function code(xi, yi, zi, ux, uy, maxCos)
                                        	return fma(Float32(ux * Float32(Float32(1.0) - ux)), Float32(maxCos * zi), Float32(sqrt(fma(Float32(Float32(ux - Float32(1.0)) * maxCos), Float32(Float32(Float32(maxCos * Float32(Float32(1.0) - ux)) * ux) * ux), Float32(1.0))) * Float32(xi + Float32(uy * fma(fma(Float32(Float32(Float32(pi) * Float32(pi)) * xi), Float32(-2.0), Float32(Float32(Float32(Float32(Float32(Float32(pi) * Float32(pi)) * Float32(pi)) * yi) * uy) * Float32(-1.3333333333333333))), uy, Float32(Float32(Float32(pi) + Float32(pi)) * yi))))))
                                        end
                                        
                                        \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(xi + uy \cdot \mathsf{fma}\left(\mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right), uy, \left(\pi + \pi\right) \cdot yi\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. Applied rewrites99.0%

                                          \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 uy around 0

                                          \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(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)\right) \]
                                        4. Step-by-step derivation
                                          1. Applied rewrites89.4%

                                            \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(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)\right) \]
                                          2. Step-by-step derivation
                                            1. Applied rewrites89.4%

                                              \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(xi + uy \cdot \mathsf{fma}\left(\mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right), uy, \left(\pi + \pi\right) \cdot yi\right)\right)\right) \]
                                            2. Add Preprocessing

                                            Alternative 12: 89.4% 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)\]
                                            \[\begin{array}{l} t_0 := \left(1 - ux\right) \cdot ux\\ \mathsf{fma}\left(t\_0, zi \cdot maxCos, \sqrt{\mathsf{fma}\left(\left(\left(\left(ux - 1\right) \cdot maxCos\right) \cdot ux\right) \cdot maxCos, t\_0, 1\right)} \cdot \mathsf{fma}\left(\mathsf{fma}\left(\pi + \pi, yi, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right) \cdot uy\right), uy, 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 (* (- 1.0 ux) ux)))
                                              (fma
                                               t_0
                                               (* zi maxCos)
                                               (*
                                                (sqrt (fma (* (* (* (- ux 1.0) maxCos) ux) maxCos) t_0 1.0))
                                                (fma
                                                 (fma
                                                  (+ PI PI)
                                                  yi
                                                  (*
                                                   (fma
                                                    (* (* PI PI) xi)
                                                    -2.0
                                                    (* (* (* (* (* PI PI) PI) yi) uy) -1.3333333333333333))
                                                   uy))
                                                 uy
                                                 xi)))))
                                            float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                            	float t_0 = (1.0f - ux) * ux;
                                            	return fmaf(t_0, (zi * maxCos), (sqrtf(fmaf(((((ux - 1.0f) * maxCos) * ux) * maxCos), t_0, 1.0f)) * fmaf(fmaf((((float) M_PI) + ((float) M_PI)), yi, (fmaf(((((float) M_PI) * ((float) M_PI)) * xi), -2.0f, (((((((float) M_PI) * ((float) M_PI)) * ((float) M_PI)) * yi) * uy) * -1.3333333333333333f)) * uy)), uy, xi)));
                                            }
                                            
                                            function code(xi, yi, zi, ux, uy, maxCos)
                                            	t_0 = Float32(Float32(Float32(1.0) - ux) * ux)
                                            	return fma(t_0, Float32(zi * maxCos), Float32(sqrt(fma(Float32(Float32(Float32(Float32(ux - Float32(1.0)) * maxCos) * ux) * maxCos), t_0, Float32(1.0))) * fma(fma(Float32(Float32(pi) + Float32(pi)), yi, Float32(fma(Float32(Float32(Float32(pi) * Float32(pi)) * xi), Float32(-2.0), Float32(Float32(Float32(Float32(Float32(Float32(pi) * Float32(pi)) * Float32(pi)) * yi) * uy) * Float32(-1.3333333333333333))) * uy)), uy, xi)))
                                            end
                                            
                                            \begin{array}{l}
                                            t_0 := \left(1 - ux\right) \cdot ux\\
                                            \mathsf{fma}\left(t\_0, zi \cdot maxCos, \sqrt{\mathsf{fma}\left(\left(\left(\left(ux - 1\right) \cdot maxCos\right) \cdot ux\right) \cdot maxCos, t\_0, 1\right)} \cdot \mathsf{fma}\left(\mathsf{fma}\left(\pi + \pi, yi, \mathsf{fma}\left(\left(\pi \cdot \pi\right) \cdot xi, -2, \left(\left(\left(\left(\pi \cdot \pi\right) \cdot \pi\right) \cdot yi\right) \cdot uy\right) \cdot -1.3333333333333333\right) \cdot uy\right), uy, 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(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 uy around 0

                                              \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(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)\right) \]
                                            4. Step-by-step derivation
                                              1. Applied rewrites89.4%

                                                \[\leadsto \mathsf{fma}\left(ux \cdot \left(1 - ux\right), maxCos \cdot zi, \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 \left(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)\right) \]
                                              2. Applied rewrites89.5%

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

                                              Alternative 13: 83.0% accurate, 5.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)\]
                                              \[xi + \mathsf{fma}\left(maxCos, ux \cdot zi, uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(xi \cdot 9.869604110717773\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)
                                                (*
                                                 uy
                                                 (fma -2.0 (* uy (* xi 9.869604110717773)) (* 2.0 (* yi PI)))))))
                                              float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                              	return xi + fmaf(maxCos, (ux * zi), (uy * fmaf(-2.0f, (uy * (xi * 9.869604110717773f)), (2.0f * (yi * ((float) M_PI))))));
                                              }
                                              
                                              function code(xi, yi, zi, ux, uy, maxCos)
                                              	return Float32(xi + fma(maxCos, Float32(ux * zi), Float32(uy * fma(Float32(-2.0), Float32(uy * Float32(xi * Float32(9.869604110717773))), Float32(Float32(2.0) * Float32(yi * Float32(pi)))))))
                                              end
                                              
                                              xi + \mathsf{fma}\left(maxCos, ux \cdot zi, uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(xi \cdot 9.869604110717773\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 uy around 0

                                                \[\leadsto maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) + \left(uy \cdot \left(-2 \cdot \left(uy \cdot \left(xi \cdot \left({\pi}^{2} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right)\right) + 2 \cdot \left(yi \cdot \left(\pi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                              3. Applied rewrites85.9%

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

                                                \[\leadsto xi + \left(maxCos \cdot \left(ux \cdot zi\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) \]
                                              5. Step-by-step derivation
                                                1. Applied rewrites83.0%

                                                  \[\leadsto xi + \mathsf{fma}\left(maxCos, ux \cdot zi, uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(xi \cdot {\pi}^{2}\right), 2 \cdot \left(yi \cdot \pi\right)\right)\right) \]
                                                2. Evaluated real constant83.0%

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

                                                Alternative 14: 78.8% accurate, 7.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)\]
                                                \[xi + \mathsf{fma}\left(2, uy \cdot \left(yi \cdot \pi\right), maxCos \cdot \left(ux \cdot zi\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)))))
                                                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)));
                                                }
                                                
                                                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 * zi))))
                                                end
                                                
                                                xi + \mathsf{fma}\left(2, uy \cdot \left(yi \cdot \pi\right), maxCos \cdot \left(ux \cdot zi\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) + \left(uy \cdot \left(-2 \cdot \left(uy \cdot \left(xi \cdot \left({\pi}^{2} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right)\right) + 2 \cdot \left(yi \cdot \left(\pi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                                3. Applied rewrites85.9%

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

                                                  \[\leadsto xi + \left(maxCos \cdot \left(ux \cdot zi\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) \]
                                                5. Step-by-step derivation
                                                  1. Applied rewrites83.0%

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

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

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

                                                    Alternative 15: 61.0% accurate, 6.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 := \mathsf{fma}\left(2, uy \cdot \left(yi \cdot \pi\right), maxCos \cdot \left(ux \cdot zi\right)\right)\\ \mathbf{if}\;yi \leq -5.0000000843119176 \cdot 10^{-17}:\\ \;\;\;\;t\_0\\ \mathbf{elif}\;yi \leq 4.999999980020986 \cdot 10^{-13}:\\ \;\;\;\;xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \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 (fma 2.0 (* uy (* yi PI)) (* maxCos (* ux zi)))))
                                                      (if (<= yi -5.0000000843119176e-17)
                                                        t_0
                                                        (if (<= yi 4.999999980020986e-13)
                                                          (+ xi (* maxCos (* ux (* zi (- 1.0 ux)))))
                                                          t_0))))
                                                    float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                                    	float t_0 = fmaf(2.0f, (uy * (yi * ((float) M_PI))), (maxCos * (ux * zi)));
                                                    	float tmp;
                                                    	if (yi <= -5.0000000843119176e-17f) {
                                                    		tmp = t_0;
                                                    	} else if (yi <= 4.999999980020986e-13f) {
                                                    		tmp = xi + (maxCos * (ux * (zi * (1.0f - ux))));
                                                    	} else {
                                                    		tmp = t_0;
                                                    	}
                                                    	return tmp;
                                                    }
                                                    
                                                    function code(xi, yi, zi, ux, uy, maxCos)
                                                    	t_0 = fma(Float32(2.0), Float32(uy * Float32(yi * Float32(pi))), Float32(maxCos * Float32(ux * zi)))
                                                    	tmp = Float32(0.0)
                                                    	if (yi <= Float32(-5.0000000843119176e-17))
                                                    		tmp = t_0;
                                                    	elseif (yi <= Float32(4.999999980020986e-13))
                                                    		tmp = Float32(xi + Float32(maxCos * Float32(ux * Float32(zi * Float32(Float32(1.0) - ux)))));
                                                    	else
                                                    		tmp = t_0;
                                                    	end
                                                    	return tmp
                                                    end
                                                    
                                                    \begin{array}{l}
                                                    t_0 := \mathsf{fma}\left(2, uy \cdot \left(yi \cdot \pi\right), maxCos \cdot \left(ux \cdot zi\right)\right)\\
                                                    \mathbf{if}\;yi \leq -5.0000000843119176 \cdot 10^{-17}:\\
                                                    \;\;\;\;t\_0\\
                                                    
                                                    \mathbf{elif}\;yi \leq 4.999999980020986 \cdot 10^{-13}:\\
                                                    \;\;\;\;xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right)\\
                                                    
                                                    \mathbf{else}:\\
                                                    \;\;\;\;t\_0\\
                                                    
                                                    
                                                    \end{array}
                                                    
                                                    Derivation
                                                    1. Split input into 2 regimes
                                                    2. if yi < -5.00000008e-17 or 4.99999998e-13 < yi

                                                      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) + \left(uy \cdot \left(-2 \cdot \left(uy \cdot \left(xi \cdot \left({\pi}^{2} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right)\right) + 2 \cdot \left(yi \cdot \left(\pi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                                      3. Applied rewrites85.9%

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

                                                        \[\leadsto xi + \left(maxCos \cdot \left(ux \cdot zi\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) \]
                                                      5. Step-by-step derivation
                                                        1. Applied rewrites83.0%

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

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

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

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

                                                              \[\leadsto \mathsf{fma}\left(2, uy \cdot \left(yi \cdot \pi\right), maxCos \cdot \left(ux \cdot zi\right)\right) \]

                                                            if -5.00000008e-17 < yi < 4.99999998e-13

                                                            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.2%

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

                                                                  \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\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 rewrites52.2%

                                                                    \[\leadsto xi + maxCos \cdot \left(ux \cdot \left(zi \cdot \left(1 - ux\right)\right)\right) \]
                                                                4. Recombined 2 regimes into one program.
                                                                5. Add Preprocessing

                                                                Alternative 16: 52.2% 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.2%

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

                                                                      \[\leadsto xi + maxCos \cdot \left(ux \cdot zi\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 rewrites52.2%

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

                                                                      Alternative 17: 50.1% 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.2%

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

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

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

                                                                            Alternative 18: 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)\]
                                                                            \[zi \cdot \left(maxCos \cdot ux\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)))
                                                                              (* zi (* maxCos ux)))
                                                                            float code(float xi, float yi, float zi, float ux, float uy, float maxCos) {
                                                                            	return zi * (maxCos * 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 = zi * (maxcos * ux)
                                                                            end function
                                                                            
                                                                            function code(xi, yi, zi, ux, uy, maxCos)
                                                                            	return Float32(zi * Float32(maxCos * ux))
                                                                            end
                                                                            
                                                                            function tmp = code(xi, yi, zi, ux, uy, maxCos)
                                                                            	tmp = zi * (maxCos * ux);
                                                                            end
                                                                            
                                                                            zi \cdot \left(maxCos \cdot ux\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) + \left(uy \cdot \left(-2 \cdot \left(uy \cdot \left(xi \cdot \left({\pi}^{2} \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right)\right) + 2 \cdot \left(yi \cdot \left(\pi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right)\right)\right) + xi \cdot \sqrt{1 - {maxCos}^{2} \cdot \left({ux}^{2} \cdot {\left(1 - ux\right)}^{2}\right)}\right) \]
                                                                            3. Applied rewrites85.9%

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

                                                                              \[\leadsto xi + \left(maxCos \cdot \left(ux \cdot zi\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) \]
                                                                            5. Step-by-step derivation
                                                                              1. Applied rewrites83.0%

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

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

                                                                                  \[\leadsto zi \cdot \mathsf{fma}\left(maxCos, ux, \frac{xi}{zi} + \frac{uy \cdot \mathsf{fma}\left(-2, uy \cdot \left(xi \cdot {\pi}^{2}\right), 2 \cdot \left(yi \cdot \pi\right)\right)}{zi}\right) \]
                                                                                2. Taylor expanded in zi around inf

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

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

                                                                                  Alternative 19: 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.2%

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

                                                                                        \[\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 2026035 +o sampling:rival3
                                                                                        (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)))