UniformSampleCone, x

Percentage Accurate: 57.4% → 99.1%
Time: 5.9s
Alternatives: 13
Speedup: 12.1×

Specification

?
\[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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) + ux \cdot maxCos\\ \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - t\_0 \cdot t\_0} \end{array} \]
(FPCore (ux uy maxCos)
  :precision binary32
  :pre (and (and (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 maxCos))))
  (* (cos (* (* uy 2.0) PI)) (sqrt (- 1.0 (* t_0 t_0))))))
float code(float ux, float uy, float maxCos) {
	float t_0 = (1.0f - ux) + (ux * maxCos);
	return cosf(((uy * 2.0f) * ((float) M_PI))) * sqrtf((1.0f - (t_0 * t_0)));
}
function code(ux, uy, maxCos)
	t_0 = Float32(Float32(Float32(1.0) - ux) + Float32(ux * maxCos))
	return Float32(cos(Float32(Float32(uy * Float32(2.0)) * Float32(pi))) * sqrt(Float32(Float32(1.0) - Float32(t_0 * t_0))))
end
function tmp = code(ux, uy, maxCos)
	t_0 = (single(1.0) - ux) + (ux * maxCos);
	tmp = cos(((uy * single(2.0)) * single(pi))) * sqrt((single(1.0) - (t_0 * t_0)));
end
\begin{array}{l}
t_0 := \left(1 - ux\right) + ux \cdot maxCos\\
\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - t\_0 \cdot t\_0}
\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 13 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: 57.4% accurate, 1.0× speedup?

\[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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) + ux \cdot maxCos\\ \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - t\_0 \cdot t\_0} \end{array} \]
(FPCore (ux uy maxCos)
  :precision binary32
  :pre (and (and (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 maxCos))))
  (* (cos (* (* uy 2.0) PI)) (sqrt (- 1.0 (* t_0 t_0))))))
float code(float ux, float uy, float maxCos) {
	float t_0 = (1.0f - ux) + (ux * maxCos);
	return cosf(((uy * 2.0f) * ((float) M_PI))) * sqrtf((1.0f - (t_0 * t_0)));
}
function code(ux, uy, maxCos)
	t_0 = Float32(Float32(Float32(1.0) - ux) + Float32(ux * maxCos))
	return Float32(cos(Float32(Float32(uy * Float32(2.0)) * Float32(pi))) * sqrt(Float32(Float32(1.0) - Float32(t_0 * t_0))))
end
function tmp = code(ux, uy, maxCos)
	t_0 = (single(1.0) - ux) + (ux * maxCos);
	tmp = cos(((uy * single(2.0)) * single(pi))) * sqrt((single(1.0) - (t_0 * t_0)));
end
\begin{array}{l}
t_0 := \left(1 - ux\right) + ux \cdot maxCos\\
\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - t\_0 \cdot t\_0}
\end{array}

Alternative 1: 99.1% accurate, 0.9× speedup?

\[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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 := ux - maxCos \cdot ux\\ \sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 0.5 \cdot \pi\right)\right) \cdot \sqrt{\left(t\_0 - 0\right) \cdot \left(-\left(t\_0 - 2\right)\right)} \end{array} \]
(FPCore (ux uy maxCos)
  :precision binary32
  :pre (and (and (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 (- ux (* maxCos ux))))
  (*
   (sin (fma (- uy) (+ PI PI) (* 0.5 PI)))
   (sqrt (* (- t_0 0.0) (- (- t_0 2.0)))))))
float code(float ux, float uy, float maxCos) {
	float t_0 = ux - (maxCos * ux);
	return sinf(fmaf(-uy, (((float) M_PI) + ((float) M_PI)), (0.5f * ((float) M_PI)))) * sqrtf(((t_0 - 0.0f) * -(t_0 - 2.0f)));
}
function code(ux, uy, maxCos)
	t_0 = Float32(ux - Float32(maxCos * ux))
	return Float32(sin(fma(Float32(-uy), Float32(Float32(pi) + Float32(pi)), Float32(Float32(0.5) * Float32(pi)))) * sqrt(Float32(Float32(t_0 - Float32(0.0)) * Float32(-Float32(t_0 - Float32(2.0))))))
end
\begin{array}{l}
t_0 := ux - maxCos \cdot ux\\
\sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 0.5 \cdot \pi\right)\right) \cdot \sqrt{\left(t\_0 - 0\right) \cdot \left(-\left(t\_0 - 2\right)\right)}
\end{array}
Derivation
  1. Initial program 57.4%

    \[\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)} \]
  2. Step-by-step derivation
    1. Applied rewrites98.9%

      \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(\left(ux - maxCos \cdot ux\right) - 0\right) \cdot \left(-\left(\left(ux - maxCos \cdot ux\right) - 2\right)\right)} \]
    2. Step-by-step derivation
      1. Applied rewrites99.1%

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

      Alternative 2: 99.1% accurate, 1.0× speedup?

      \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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)\]
      \[\sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 0.5 \cdot \pi\right)\right) \cdot \sqrt{\left(\left(\mathsf{fma}\left(maxCos, ux, 1\right) + 1\right) - ux\right) \cdot \left(ux - maxCos \cdot ux\right)} \]
      (FPCore (ux uy maxCos)
        :precision binary32
        :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0))
                (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
           (and (<= 0.0 maxCos) (<= maxCos 1.0)))
        (*
       (sin (fma (- uy) (+ PI PI) (* 0.5 PI)))
       (sqrt (* (- (+ (fma maxCos ux 1.0) 1.0) ux) (- ux (* maxCos ux))))))
      float code(float ux, float uy, float maxCos) {
      	return sinf(fmaf(-uy, (((float) M_PI) + ((float) M_PI)), (0.5f * ((float) M_PI)))) * sqrtf((((fmaf(maxCos, ux, 1.0f) + 1.0f) - ux) * (ux - (maxCos * ux))));
      }
      
      function code(ux, uy, maxCos)
      	return Float32(sin(fma(Float32(-uy), Float32(Float32(pi) + Float32(pi)), Float32(Float32(0.5) * Float32(pi)))) * sqrt(Float32(Float32(Float32(fma(maxCos, ux, Float32(1.0)) + Float32(1.0)) - ux) * Float32(ux - Float32(maxCos * ux)))))
      end
      
      \sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 0.5 \cdot \pi\right)\right) \cdot \sqrt{\left(\left(\mathsf{fma}\left(maxCos, ux, 1\right) + 1\right) - ux\right) \cdot \left(ux - maxCos \cdot ux\right)}
      
      Derivation
      1. Initial program 57.4%

        \[\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)} \]
      2. Step-by-step derivation
        1. Applied rewrites98.9%

          \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(\left(ux - maxCos \cdot ux\right) - 0\right) \cdot \left(-\left(\left(ux - maxCos \cdot ux\right) - 2\right)\right)} \]
        2. Step-by-step derivation
          1. Applied rewrites99.1%

            \[\leadsto \sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 0.5 \cdot \pi\right)\right) \cdot \sqrt{\left(\left(ux - maxCos \cdot ux\right) - 0\right) \cdot \left(-\left(\left(ux - maxCos \cdot ux\right) - 2\right)\right)} \]
          2. Step-by-step derivation
            1. Applied rewrites99.1%

              \[\leadsto \sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 0.5 \cdot \pi\right)\right) \cdot \sqrt{\left(\mathsf{fma}\left(maxCos, ux, 2\right) - ux\right) \cdot \left(ux - maxCos \cdot ux\right)} \]
            2. Step-by-step derivation
              1. Applied rewrites99.1%

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

              Alternative 3: 99.1% accurate, 1.0× speedup?

              \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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)\]
              \[\sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 1.5707963705062866\right)\right) \cdot \sqrt{\left(\mathsf{fma}\left(maxCos, ux, 2\right) - ux\right) \cdot \left(ux - maxCos \cdot ux\right)} \]
              (FPCore (ux uy maxCos)
                :precision binary32
                :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0))
                        (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                   (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                (*
               (sin (fma (- uy) (+ PI PI) 1.5707963705062866))
               (sqrt (* (- (fma maxCos ux 2.0) ux) (- ux (* maxCos ux))))))
              float code(float ux, float uy, float maxCos) {
              	return sinf(fmaf(-uy, (((float) M_PI) + ((float) M_PI)), 1.5707963705062866f)) * sqrtf(((fmaf(maxCos, ux, 2.0f) - ux) * (ux - (maxCos * ux))));
              }
              
              function code(ux, uy, maxCos)
              	return Float32(sin(fma(Float32(-uy), Float32(Float32(pi) + Float32(pi)), Float32(1.5707963705062866))) * sqrt(Float32(Float32(fma(maxCos, ux, Float32(2.0)) - ux) * Float32(ux - Float32(maxCos * ux)))))
              end
              
              \sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 1.5707963705062866\right)\right) \cdot \sqrt{\left(\mathsf{fma}\left(maxCos, ux, 2\right) - ux\right) \cdot \left(ux - maxCos \cdot ux\right)}
              
              Derivation
              1. Initial program 57.4%

                \[\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)} \]
              2. Step-by-step derivation
                1. Applied rewrites98.9%

                  \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(\left(ux - maxCos \cdot ux\right) - 0\right) \cdot \left(-\left(\left(ux - maxCos \cdot ux\right) - 2\right)\right)} \]
                2. Step-by-step derivation
                  1. Applied rewrites99.1%

                    \[\leadsto \sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 0.5 \cdot \pi\right)\right) \cdot \sqrt{\left(\left(ux - maxCos \cdot ux\right) - 0\right) \cdot \left(-\left(\left(ux - maxCos \cdot ux\right) - 2\right)\right)} \]
                  2. Step-by-step derivation
                    1. Applied rewrites99.1%

                      \[\leadsto \sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 0.5 \cdot \pi\right)\right) \cdot \sqrt{\left(\mathsf{fma}\left(maxCos, ux, 2\right) - ux\right) \cdot \left(ux - maxCos \cdot ux\right)} \]
                    2. Evaluated real constant99.1%

                      \[\leadsto \sin \left(\mathsf{fma}\left(-uy, \pi + \pi, 1.5707963705062866\right)\right) \cdot \sqrt{\left(\mathsf{fma}\left(maxCos, ux, 2\right) - ux\right) \cdot \left(ux - maxCos \cdot ux\right)} \]
                    3. Add Preprocessing

                    Alternative 4: 98.9% accurate, 1.1× speedup?

                    \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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)\]
                    \[\sqrt{\left(maxCos \cdot ux - ux\right) \cdot \left(ux - \mathsf{fma}\left(maxCos, ux, 2\right)\right)} \cdot \cos \left(\left(uy + uy\right) \cdot \pi\right) \]
                    (FPCore (ux uy maxCos)
                      :precision binary32
                      :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0))
                              (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                         (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                      (*
                     (sqrt (* (- (* maxCos ux) ux) (- ux (fma maxCos ux 2.0))))
                     (cos (* (+ uy uy) PI))))
                    float code(float ux, float uy, float maxCos) {
                    	return sqrtf((((maxCos * ux) - ux) * (ux - fmaf(maxCos, ux, 2.0f)))) * cosf(((uy + uy) * ((float) M_PI)));
                    }
                    
                    function code(ux, uy, maxCos)
                    	return Float32(sqrt(Float32(Float32(Float32(maxCos * ux) - ux) * Float32(ux - fma(maxCos, ux, Float32(2.0))))) * cos(Float32(Float32(uy + uy) * Float32(pi))))
                    end
                    
                    \sqrt{\left(maxCos \cdot ux - ux\right) \cdot \left(ux - \mathsf{fma}\left(maxCos, ux, 2\right)\right)} \cdot \cos \left(\left(uy + uy\right) \cdot \pi\right)
                    
                    Derivation
                    1. Initial program 57.4%

                      \[\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)} \]
                    2. Step-by-step derivation
                      1. Applied rewrites98.9%

                        \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(\left(ux - maxCos \cdot ux\right) - 0\right) \cdot \left(-\left(\left(ux - maxCos \cdot ux\right) - 2\right)\right)} \]
                      2. Step-by-step derivation
                        1. Applied rewrites98.9%

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

                        Alternative 5: 97.5% accurate, 1.2× speedup?

                        \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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)\]
                        \[\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(ux - maxCos \cdot ux\right) \cdot \left(2 - ux\right)} \]
                        (FPCore (ux uy maxCos)
                          :precision binary32
                          :pre (and (and (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 (* (- ux (* maxCos ux)) (- 2.0 ux)))))
                        float code(float ux, float uy, float maxCos) {
                        	return cosf(((uy * 2.0f) * ((float) M_PI))) * sqrtf(((ux - (maxCos * ux)) * (2.0f - ux)));
                        }
                        
                        function code(ux, uy, maxCos)
                        	return Float32(cos(Float32(Float32(uy * Float32(2.0)) * Float32(pi))) * sqrt(Float32(Float32(ux - Float32(maxCos * ux)) * Float32(Float32(2.0) - ux))))
                        end
                        
                        function tmp = code(ux, uy, maxCos)
                        	tmp = cos(((uy * single(2.0)) * single(pi))) * sqrt(((ux - (maxCos * ux)) * (single(2.0) - ux)));
                        end
                        
                        \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(ux - maxCos \cdot ux\right) \cdot \left(2 - ux\right)}
                        
                        Derivation
                        1. Initial program 57.4%

                          \[\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)} \]
                        2. Step-by-step derivation
                          1. Applied rewrites98.9%

                            \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(\left(ux - maxCos \cdot ux\right) - 0\right) \cdot \left(\mathsf{fma}\left(maxCos, ux, 1 - ux\right) - -1\right)} \]
                          2. Step-by-step derivation
                            1. Applied rewrites98.9%

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

                              \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(ux - maxCos \cdot ux\right) \cdot \left(2 - ux\right)} \]
                            3. Step-by-step derivation
                              1. Applied rewrites97.5%

                                \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(ux - maxCos \cdot ux\right) \cdot \left(2 - ux\right)} \]
                              2. Add Preprocessing

                              Alternative 6: 96.3% accurate, 1.1× speedup?

                              \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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} \mathbf{if}\;uy \leq 0.0001500000071246177:\\ \;\;\;\;\sqrt{ux \cdot \left(\left(2 + -1 \cdot \left(ux \cdot {\left(maxCos - 1\right)}^{2}\right)\right) - 2 \cdot maxCos\right)}\\ \mathbf{else}:\\ \;\;\;\;\sin \left(\mathsf{fma}\left(-2, uy \cdot \pi, 0.5 \cdot \pi\right)\right) \cdot \sqrt{ux \cdot \left(2 - ux\right)}\\ \end{array} \]
                              (FPCore (ux uy maxCos)
                                :precision binary32
                                :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0))
                                        (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                   (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                (if (<= uy 0.0001500000071246177)
                                (sqrt
                                 (*
                                  ux
                                  (-
                                   (+ 2.0 (* -1.0 (* ux (pow (- maxCos 1.0) 2.0))))
                                   (* 2.0 maxCos))))
                                (* (sin (fma -2.0 (* uy PI) (* 0.5 PI))) (sqrt (* ux (- 2.0 ux))))))
                              float code(float ux, float uy, float maxCos) {
                              	float tmp;
                              	if (uy <= 0.0001500000071246177f) {
                              		tmp = sqrtf((ux * ((2.0f + (-1.0f * (ux * powf((maxCos - 1.0f), 2.0f)))) - (2.0f * maxCos))));
                              	} else {
                              		tmp = sinf(fmaf(-2.0f, (uy * ((float) M_PI)), (0.5f * ((float) M_PI)))) * sqrtf((ux * (2.0f - ux)));
                              	}
                              	return tmp;
                              }
                              
                              function code(ux, uy, maxCos)
                              	tmp = Float32(0.0)
                              	if (uy <= Float32(0.0001500000071246177))
                              		tmp = sqrt(Float32(ux * Float32(Float32(Float32(2.0) + Float32(Float32(-1.0) * Float32(ux * (Float32(maxCos - Float32(1.0)) ^ Float32(2.0))))) - Float32(Float32(2.0) * maxCos))));
                              	else
                              		tmp = Float32(sin(fma(Float32(-2.0), Float32(uy * Float32(pi)), Float32(Float32(0.5) * Float32(pi)))) * sqrt(Float32(ux * Float32(Float32(2.0) - ux))));
                              	end
                              	return tmp
                              end
                              
                              \begin{array}{l}
                              \mathbf{if}\;uy \leq 0.0001500000071246177:\\
                              \;\;\;\;\sqrt{ux \cdot \left(\left(2 + -1 \cdot \left(ux \cdot {\left(maxCos - 1\right)}^{2}\right)\right) - 2 \cdot maxCos\right)}\\
                              
                              \mathbf{else}:\\
                              \;\;\;\;\sin \left(\mathsf{fma}\left(-2, uy \cdot \pi, 0.5 \cdot \pi\right)\right) \cdot \sqrt{ux \cdot \left(2 - ux\right)}\\
                              
                              
                              \end{array}
                              
                              Derivation
                              1. Split input into 2 regimes
                              2. if uy < 1.50000007e-4

                                1. Initial program 57.4%

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

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

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

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

                                      \[\leadsto \sqrt{ux \cdot \left(\left(2 + -1 \cdot \left(ux \cdot {\left(maxCos - 1\right)}^{2}\right)\right) - 2 \cdot maxCos\right)} \]

                                    if 1.50000007e-4 < uy

                                    1. Initial program 57.4%

                                      \[\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)} \]
                                    2. Step-by-step derivation
                                      1. Applied rewrites98.9%

                                        \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(\left(ux - maxCos \cdot ux\right) - 0\right) \cdot \left(-\left(\left(ux - maxCos \cdot ux\right) - 2\right)\right)} \]
                                      2. Step-by-step derivation
                                        1. Applied rewrites99.1%

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

                                          \[\leadsto \sin \left(-2 \cdot \left(uy \cdot \pi\right) + \frac{1}{2} \cdot \pi\right) \cdot \sqrt{ux \cdot \left(2 - ux\right)} \]
                                        3. Step-by-step derivation
                                          1. Applied rewrites92.5%

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

                                        Alternative 7: 96.2% accurate, 1.2× speedup?

                                        \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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} \mathbf{if}\;uy \leq 0.0001500000071246177:\\ \;\;\;\;\sqrt{ux \cdot \left(\left(2 + -1 \cdot \left(ux \cdot {\left(maxCos - 1\right)}^{2}\right)\right) - 2 \cdot maxCos\right)}\\ \mathbf{else}:\\ \;\;\;\;\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{ux \cdot \left(2 - ux\right)}\\ \end{array} \]
                                        (FPCore (ux uy maxCos)
                                          :precision binary32
                                          :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0))
                                                  (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                             (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                          (if (<= uy 0.0001500000071246177)
                                          (sqrt
                                           (*
                                            ux
                                            (-
                                             (+ 2.0 (* -1.0 (* ux (pow (- maxCos 1.0) 2.0))))
                                             (* 2.0 maxCos))))
                                          (* (cos (* (* uy 2.0) PI)) (sqrt (* ux (- 2.0 ux))))))
                                        float code(float ux, float uy, float maxCos) {
                                        	float tmp;
                                        	if (uy <= 0.0001500000071246177f) {
                                        		tmp = sqrtf((ux * ((2.0f + (-1.0f * (ux * powf((maxCos - 1.0f), 2.0f)))) - (2.0f * maxCos))));
                                        	} else {
                                        		tmp = cosf(((uy * 2.0f) * ((float) M_PI))) * sqrtf((ux * (2.0f - ux)));
                                        	}
                                        	return tmp;
                                        }
                                        
                                        function code(ux, uy, maxCos)
                                        	tmp = Float32(0.0)
                                        	if (uy <= Float32(0.0001500000071246177))
                                        		tmp = sqrt(Float32(ux * Float32(Float32(Float32(2.0) + Float32(Float32(-1.0) * Float32(ux * (Float32(maxCos - Float32(1.0)) ^ Float32(2.0))))) - Float32(Float32(2.0) * maxCos))));
                                        	else
                                        		tmp = Float32(cos(Float32(Float32(uy * Float32(2.0)) * Float32(pi))) * sqrt(Float32(ux * Float32(Float32(2.0) - ux))));
                                        	end
                                        	return tmp
                                        end
                                        
                                        function tmp_2 = code(ux, uy, maxCos)
                                        	tmp = single(0.0);
                                        	if (uy <= single(0.0001500000071246177))
                                        		tmp = sqrt((ux * ((single(2.0) + (single(-1.0) * (ux * ((maxCos - single(1.0)) ^ single(2.0))))) - (single(2.0) * maxCos))));
                                        	else
                                        		tmp = cos(((uy * single(2.0)) * single(pi))) * sqrt((ux * (single(2.0) - ux)));
                                        	end
                                        	tmp_2 = tmp;
                                        end
                                        
                                        \begin{array}{l}
                                        \mathbf{if}\;uy \leq 0.0001500000071246177:\\
                                        \;\;\;\;\sqrt{ux \cdot \left(\left(2 + -1 \cdot \left(ux \cdot {\left(maxCos - 1\right)}^{2}\right)\right) - 2 \cdot maxCos\right)}\\
                                        
                                        \mathbf{else}:\\
                                        \;\;\;\;\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{ux \cdot \left(2 - ux\right)}\\
                                        
                                        
                                        \end{array}
                                        
                                        Derivation
                                        1. Split input into 2 regimes
                                        2. if uy < 1.50000007e-4

                                          1. Initial program 57.4%

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

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

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

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

                                                \[\leadsto \sqrt{ux \cdot \left(\left(2 + -1 \cdot \left(ux \cdot {\left(maxCos - 1\right)}^{2}\right)\right) - 2 \cdot maxCos\right)} \]

                                              if 1.50000007e-4 < uy

                                              1. Initial program 57.4%

                                                \[\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)} \]
                                              2. Step-by-step derivation
                                                1. Applied rewrites98.9%

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

                                                  \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{ux \cdot \left(2 - ux\right)} \]
                                                3. Step-by-step derivation
                                                  1. Applied rewrites92.4%

                                                    \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{ux \cdot \left(2 - ux\right)} \]
                                                4. Recombined 2 regimes into one program.
                                                5. Add Preprocessing

                                                Alternative 8: 80.0% accurate, 1.7× speedup?

                                                \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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)\]
                                                \[\sqrt{ux \cdot \left(\left(2 + -1 \cdot \left(ux \cdot {\left(maxCos - 1\right)}^{2}\right)\right) - 2 \cdot maxCos\right)} \]
                                                (FPCore (ux uy maxCos)
                                                  :precision binary32
                                                  :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0))
                                                          (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                                     (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                                  (sqrt
                                                 (*
                                                  ux
                                                  (-
                                                   (+ 2.0 (* -1.0 (* ux (pow (- maxCos 1.0) 2.0))))
                                                   (* 2.0 maxCos)))))
                                                float code(float ux, float uy, float maxCos) {
                                                	return sqrtf((ux * ((2.0f + (-1.0f * (ux * powf((maxCos - 1.0f), 2.0f)))) - (2.0f * maxCos))));
                                                }
                                                
                                                real(4) function code(ux, uy, maxcos)
                                                use fmin_fmax_functions
                                                    real(4), intent (in) :: ux
                                                    real(4), intent (in) :: uy
                                                    real(4), intent (in) :: maxcos
                                                    code = sqrt((ux * ((2.0e0 + ((-1.0e0) * (ux * ((maxcos - 1.0e0) ** 2.0e0)))) - (2.0e0 * maxcos))))
                                                end function
                                                
                                                function code(ux, uy, maxCos)
                                                	return sqrt(Float32(ux * Float32(Float32(Float32(2.0) + Float32(Float32(-1.0) * Float32(ux * (Float32(maxCos - Float32(1.0)) ^ Float32(2.0))))) - Float32(Float32(2.0) * maxCos))))
                                                end
                                                
                                                function tmp = code(ux, uy, maxCos)
                                                	tmp = sqrt((ux * ((single(2.0) + (single(-1.0) * (ux * ((maxCos - single(1.0)) ^ single(2.0))))) - (single(2.0) * maxCos))));
                                                end
                                                
                                                \sqrt{ux \cdot \left(\left(2 + -1 \cdot \left(ux \cdot {\left(maxCos - 1\right)}^{2}\right)\right) - 2 \cdot maxCos\right)}
                                                
                                                Derivation
                                                1. Initial program 57.4%

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

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

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

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

                                                      \[\leadsto \sqrt{ux \cdot \left(\left(2 + -1 \cdot \left(ux \cdot {\left(maxCos - 1\right)}^{2}\right)\right) - 2 \cdot maxCos\right)} \]
                                                    2. Add Preprocessing

                                                    Alternative 9: 79.9% accurate, 3.4× speedup?

                                                    \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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)\]
                                                    \[\sqrt{\left(ux - maxCos \cdot ux\right) \cdot \left(\left(2 + maxCos \cdot ux\right) - ux\right)} \]
                                                    (FPCore (ux uy maxCos)
                                                      :precision binary32
                                                      :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0))
                                                              (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                                         (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                                      (sqrt (* (- ux (* maxCos ux)) (- (+ 2.0 (* maxCos ux)) ux))))
                                                    float code(float ux, float uy, float maxCos) {
                                                    	return sqrtf(((ux - (maxCos * ux)) * ((2.0f + (maxCos * ux)) - ux)));
                                                    }
                                                    
                                                    real(4) function code(ux, uy, maxcos)
                                                    use fmin_fmax_functions
                                                        real(4), intent (in) :: ux
                                                        real(4), intent (in) :: uy
                                                        real(4), intent (in) :: maxcos
                                                        code = sqrt(((ux - (maxcos * ux)) * ((2.0e0 + (maxcos * ux)) - ux)))
                                                    end function
                                                    
                                                    function code(ux, uy, maxCos)
                                                    	return sqrt(Float32(Float32(ux - Float32(maxCos * ux)) * Float32(Float32(Float32(2.0) + Float32(maxCos * ux)) - ux)))
                                                    end
                                                    
                                                    function tmp = code(ux, uy, maxCos)
                                                    	tmp = sqrt(((ux - (maxCos * ux)) * ((single(2.0) + (maxCos * ux)) - ux)));
                                                    end
                                                    
                                                    \sqrt{\left(ux - maxCos \cdot ux\right) \cdot \left(\left(2 + maxCos \cdot ux\right) - ux\right)}
                                                    
                                                    Derivation
                                                    1. Initial program 57.4%

                                                      \[\cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)} \]
                                                    2. Step-by-step derivation
                                                      1. Applied rewrites98.9%

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

                                                        \[\leadsto \cos \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(\left(ux - maxCos \cdot ux\right) - 0\right) \cdot 2} \]
                                                      3. Step-by-step derivation
                                                        1. Applied rewrites76.8%

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

                                                          \[\leadsto \sqrt{\left(ux - maxCos \cdot ux\right) \cdot \left(\left(2 + maxCos \cdot ux\right) - ux\right)} \]
                                                        3. Step-by-step derivation
                                                          1. Applied rewrites79.9%

                                                            \[\leadsto \sqrt{\left(ux - maxCos \cdot ux\right) \cdot \left(\left(2 + maxCos \cdot ux\right) - ux\right)} \]
                                                          2. Add Preprocessing

                                                          Alternative 10: 74.2% accurate, 1.7× speedup?

                                                          \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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) + ux \cdot maxCos\\ \mathbf{if}\;t\_0 \cdot t\_0 \leq 0.9997000098228455:\\ \;\;\;\;\sqrt{\left(1 - \left(1 + -2 \cdot ux\right)\right) - ux \cdot ux}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(ux, 2, ux \cdot \left(-2 \cdot maxCos\right)\right)}\\ \end{array} \]
                                                          (FPCore (ux uy maxCos)
                                                            :precision binary32
                                                            :pre (and (and (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 maxCos))))
                                                            (if (<= (* t_0 t_0) 0.9997000098228455)
                                                              (sqrt (- (- 1.0 (+ 1.0 (* -2.0 ux))) (* ux ux)))
                                                              (sqrt (fma ux 2.0 (* ux (* -2.0 maxCos)))))))
                                                          float code(float ux, float uy, float maxCos) {
                                                          	float t_0 = (1.0f - ux) + (ux * maxCos);
                                                          	float tmp;
                                                          	if ((t_0 * t_0) <= 0.9997000098228455f) {
                                                          		tmp = sqrtf(((1.0f - (1.0f + (-2.0f * ux))) - (ux * ux)));
                                                          	} else {
                                                          		tmp = sqrtf(fmaf(ux, 2.0f, (ux * (-2.0f * maxCos))));
                                                          	}
                                                          	return tmp;
                                                          }
                                                          
                                                          function code(ux, uy, maxCos)
                                                          	t_0 = Float32(Float32(Float32(1.0) - ux) + Float32(ux * maxCos))
                                                          	tmp = Float32(0.0)
                                                          	if (Float32(t_0 * t_0) <= Float32(0.9997000098228455))
                                                          		tmp = sqrt(Float32(Float32(Float32(1.0) - Float32(Float32(1.0) + Float32(Float32(-2.0) * ux))) - Float32(ux * ux)));
                                                          	else
                                                          		tmp = sqrt(fma(ux, Float32(2.0), Float32(ux * Float32(Float32(-2.0) * maxCos))));
                                                          	end
                                                          	return tmp
                                                          end
                                                          
                                                          \begin{array}{l}
                                                          t_0 := \left(1 - ux\right) + ux \cdot maxCos\\
                                                          \mathbf{if}\;t\_0 \cdot t\_0 \leq 0.9997000098228455:\\
                                                          \;\;\;\;\sqrt{\left(1 - \left(1 + -2 \cdot ux\right)\right) - ux \cdot ux}\\
                                                          
                                                          \mathbf{else}:\\
                                                          \;\;\;\;\sqrt{\mathsf{fma}\left(ux, 2, ux \cdot \left(-2 \cdot maxCos\right)\right)}\\
                                                          
                                                          
                                                          \end{array}
                                                          
                                                          Derivation
                                                          1. Split input into 2 regimes
                                                          2. if (*.f32 (+.f32 (-.f32 #s(literal 1 binary32) ux) (*.f32 ux maxCos)) (+.f32 (-.f32 #s(literal 1 binary32) ux) (*.f32 ux maxCos))) < 0.99970001

                                                            1. Initial program 57.4%

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

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

                                                                \[\leadsto \sqrt{1 - {\left(\left(1 + maxCos \cdot ux\right) - ux\right)}^{2}} \]
                                                              2. Step-by-step derivation
                                                                1. Applied rewrites49.9%

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

                                                                  \[\leadsto \sqrt{\left(1 - \left(1 + -2 \cdot ux\right)\right) - ux \cdot ux} \]
                                                                3. Step-by-step derivation
                                                                  1. Applied rewrites48.3%

                                                                    \[\leadsto \sqrt{\left(1 - \left(1 + -2 \cdot ux\right)\right) - ux \cdot ux} \]

                                                                  if 0.99970001 < (*.f32 (+.f32 (-.f32 #s(literal 1 binary32) ux) (*.f32 ux maxCos)) (+.f32 (-.f32 #s(literal 1 binary32) ux) (*.f32 ux maxCos)))

                                                                  1. Initial program 57.4%

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

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

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

                                                                      \[\leadsto \sqrt{ux \cdot \left(2 - 2 \cdot maxCos\right)} \]
                                                                    3. Step-by-step derivation
                                                                      1. Applied rewrites64.8%

                                                                        \[\leadsto \sqrt{ux \cdot \left(2 - 2 \cdot maxCos\right)} \]
                                                                      2. Step-by-step derivation
                                                                        1. Applied rewrites64.8%

                                                                          \[\leadsto \sqrt{\mathsf{fma}\left(ux, 2, ux \cdot \left(-2 \cdot maxCos\right)\right)} \]
                                                                      3. Recombined 2 regimes into one program.
                                                                      4. Add Preprocessing

                                                                      Alternative 11: 64.8% accurate, 4.9× speedup?

                                                                      \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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)\]
                                                                      \[\sqrt{\mathsf{fma}\left(ux, 2, ux \cdot \left(-2 \cdot maxCos\right)\right)} \]
                                                                      (FPCore (ux uy maxCos)
                                                                        :precision binary32
                                                                        :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0))
                                                                                (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                                                           (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                                                        (sqrt (fma ux 2.0 (* ux (* -2.0 maxCos)))))
                                                                      float code(float ux, float uy, float maxCos) {
                                                                      	return sqrtf(fmaf(ux, 2.0f, (ux * (-2.0f * maxCos))));
                                                                      }
                                                                      
                                                                      function code(ux, uy, maxCos)
                                                                      	return sqrt(fma(ux, Float32(2.0), Float32(ux * Float32(Float32(-2.0) * maxCos))))
                                                                      end
                                                                      
                                                                      \sqrt{\mathsf{fma}\left(ux, 2, ux \cdot \left(-2 \cdot maxCos\right)\right)}
                                                                      
                                                                      Derivation
                                                                      1. Initial program 57.4%

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

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

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

                                                                          \[\leadsto \sqrt{ux \cdot \left(2 - 2 \cdot maxCos\right)} \]
                                                                        3. Step-by-step derivation
                                                                          1. Applied rewrites64.8%

                                                                            \[\leadsto \sqrt{ux \cdot \left(2 - 2 \cdot maxCos\right)} \]
                                                                          2. Step-by-step derivation
                                                                            1. Applied rewrites64.8%

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

                                                                            Alternative 12: 64.8% accurate, 6.2× speedup?

                                                                            \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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)\]
                                                                            \[\sqrt{\mathsf{fma}\left(-2, maxCos, 2\right) \cdot ux} \]
                                                                            (FPCore (ux uy maxCos)
                                                                              :precision binary32
                                                                              :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0))
                                                                                      (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                                                                 (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                                                              (sqrt (* (fma -2.0 maxCos 2.0) ux)))
                                                                            float code(float ux, float uy, float maxCos) {
                                                                            	return sqrtf((fmaf(-2.0f, maxCos, 2.0f) * ux));
                                                                            }
                                                                            
                                                                            function code(ux, uy, maxCos)
                                                                            	return sqrt(Float32(fma(Float32(-2.0), maxCos, Float32(2.0)) * ux))
                                                                            end
                                                                            
                                                                            \sqrt{\mathsf{fma}\left(-2, maxCos, 2\right) \cdot ux}
                                                                            
                                                                            Derivation
                                                                            1. Initial program 57.4%

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

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

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

                                                                                \[\leadsto \sqrt{ux \cdot \left(2 - 2 \cdot maxCos\right)} \]
                                                                              3. Step-by-step derivation
                                                                                1. Applied rewrites64.8%

                                                                                  \[\leadsto \sqrt{ux \cdot \left(2 - 2 \cdot maxCos\right)} \]
                                                                                2. Step-by-step derivation
                                                                                  1. Applied rewrites64.8%

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

                                                                                  Alternative 13: 62.0% accurate, 12.1× speedup?

                                                                                  \[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\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)\]
                                                                                  \[\sqrt{ux + ux} \]
                                                                                  (FPCore (ux uy maxCos)
                                                                                    :precision binary32
                                                                                    :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0))
                                                                                            (and (<= 2.328306437e-10 uy) (<= uy 1.0)))
                                                                                       (and (<= 0.0 maxCos) (<= maxCos 1.0)))
                                                                                    (sqrt (+ ux ux)))
                                                                                  float code(float ux, float uy, float maxCos) {
                                                                                  	return sqrtf((ux + ux));
                                                                                  }
                                                                                  
                                                                                  real(4) function code(ux, uy, maxcos)
                                                                                  use fmin_fmax_functions
                                                                                      real(4), intent (in) :: ux
                                                                                      real(4), intent (in) :: uy
                                                                                      real(4), intent (in) :: maxcos
                                                                                      code = sqrt((ux + ux))
                                                                                  end function
                                                                                  
                                                                                  function code(ux, uy, maxCos)
                                                                                  	return sqrt(Float32(ux + ux))
                                                                                  end
                                                                                  
                                                                                  function tmp = code(ux, uy, maxCos)
                                                                                  	tmp = sqrt((ux + ux));
                                                                                  end
                                                                                  
                                                                                  \sqrt{ux + ux}
                                                                                  
                                                                                  Derivation
                                                                                  1. Initial program 57.4%

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

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

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

                                                                                      \[\leadsto \sqrt{ux \cdot \left(2 - 2 \cdot maxCos\right)} \]
                                                                                    3. Step-by-step derivation
                                                                                      1. Applied rewrites64.8%

                                                                                        \[\leadsto \sqrt{ux \cdot \left(2 - 2 \cdot maxCos\right)} \]
                                                                                      2. Taylor expanded in maxCos around 0

                                                                                        \[\leadsto \sqrt{2 \cdot ux} \]
                                                                                      3. Step-by-step derivation
                                                                                        1. Applied rewrites62.0%

                                                                                          \[\leadsto \sqrt{2 \cdot ux} \]
                                                                                        2. Step-by-step derivation
                                                                                          1. Applied rewrites62.0%

                                                                                            \[\leadsto \sqrt{ux + ux} \]
                                                                                          2. Add Preprocessing

                                                                                          Reproduce

                                                                                          ?
                                                                                          herbie shell --seed 2025359 
                                                                                          (FPCore (ux uy maxCos)
                                                                                            :name "UniformSampleCone, x"
                                                                                            :precision binary32
                                                                                            :pre (and (and (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) (* ux maxCos)) (+ (- 1.0 ux) (* ux maxCos)))))))