Beckmann Sample, near normal, slope_y

Percentage Accurate: 57.5% → 98.3%
Time: 4.8s
Alternatives: 11
Speedup: 4.5×

Specification

?
\[\left(\left(cosTheta\_i > 0.9999 \land cosTheta\_i \leq 1\right) \land \left(2.328306437 \cdot 10^{-10} \leq u1 \land u1 \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq u2 \land u2 \leq 1\right)\]
\[\begin{array}{l} \\ \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (* (sqrt (- (log (- 1.0 u1)))) (sin (* (* 2.0 PI) u2))))
float code(float cosTheta_i, float u1, float u2) {
	return sqrtf(-logf((1.0f - u1))) * sinf(((2.0f * ((float) M_PI)) * u2));
}
function code(cosTheta_i, u1, u2)
	return Float32(sqrt(Float32(-log(Float32(Float32(1.0) - u1)))) * sin(Float32(Float32(Float32(2.0) * Float32(pi)) * u2)))
end
function tmp = code(cosTheta_i, u1, u2)
	tmp = sqrt(-log((single(1.0) - u1))) * sin(((single(2.0) * single(pi)) * u2));
end
\begin{array}{l}

\\
\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\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 11 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.5% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (* (sqrt (- (log (- 1.0 u1)))) (sin (* (* 2.0 PI) u2))))
float code(float cosTheta_i, float u1, float u2) {
	return sqrtf(-logf((1.0f - u1))) * sinf(((2.0f * ((float) M_PI)) * u2));
}
function code(cosTheta_i, u1, u2)
	return Float32(sqrt(Float32(-log(Float32(Float32(1.0) - u1)))) * sin(Float32(Float32(Float32(2.0) * Float32(pi)) * u2)))
end
function tmp = code(cosTheta_i, u1, u2)
	tmp = sqrt(-log((single(1.0) - u1))) * sin(((single(2.0) * single(pi)) * u2));
end
\begin{array}{l}

\\
\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\end{array}

Alternative 1: 98.3% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \left(\mathsf{fma}\left(-u2, \pi, \pi \cdot 0.5\right)\right)\right)\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (*
  (sqrt (- (log1p (- u1))))
  (* 2.0 (* (sin (* PI u2)) (sin (fma (- u2) PI (* PI 0.5)))))))
float code(float cosTheta_i, float u1, float u2) {
	return sqrtf(-log1pf(-u1)) * (2.0f * (sinf((((float) M_PI) * u2)) * sinf(fmaf(-u2, ((float) M_PI), (((float) M_PI) * 0.5f)))));
}
function code(cosTheta_i, u1, u2)
	return Float32(sqrt(Float32(-log1p(Float32(-u1)))) * Float32(Float32(2.0) * Float32(sin(Float32(Float32(pi) * u2)) * sin(fma(Float32(-u2), Float32(pi), Float32(Float32(pi) * Float32(0.5)))))))
end
\begin{array}{l}

\\
\sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \left(\mathsf{fma}\left(-u2, \pi, \pi \cdot 0.5\right)\right)\right)\right)
\end{array}
Derivation
  1. Initial program 57.5%

    \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
  2. Step-by-step derivation
    1. lift-log.f32N/A

      \[\leadsto \sqrt{-\color{blue}{\log \left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    2. lift--.f32N/A

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    3. sub-flipN/A

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    4. lower-log1p.f32N/A

      \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    5. lower-neg.f3298.3

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{-u1}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
  3. Applied rewrites98.3%

    \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(-u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
  4. Step-by-step derivation
    1. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(2 \cdot \pi\right) \cdot u2\right)} \]
    2. *-commutativeN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(u2 \cdot \left(2 \cdot \pi\right)\right)} \]
    3. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(u2 \cdot \color{blue}{\left(2 \cdot \pi\right)}\right) \]
    4. associate-*r*N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 \cdot 2\right) \cdot \pi\right)} \]
    5. *-commutativeN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
    6. lower-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
    7. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(1 + 1\right)} \cdot u2\right) \cdot \pi\right) \]
    8. flip-+N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1}} \cdot u2\right) \cdot \pi\right) \]
    9. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{1} - 1 \cdot 1}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    10. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1 - \color{blue}{1}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    11. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{0}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    12. +-inversesN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi - \pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    13. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi} - \pi \cdot \pi}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    14. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \color{blue}{\pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    15. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{0}} \cdot u2\right) \cdot \pi\right) \]
    16. +-inversesN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{\pi - \pi}} \cdot u2\right) \cdot \pi\right) \]
    17. flip-+N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(\pi + \pi\right)} \cdot u2\right) \cdot \pi\right) \]
    18. count-2-revN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
    19. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
    20. lower-*.f3225.1

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(\left(2 \cdot \pi\right) \cdot u2\right) \cdot \pi\right)} \]
  5. Applied rewrites98.3%

    \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 + u2\right) \cdot \pi\right)} \]
  6. Step-by-step derivation
    1. lift-sin.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\sin \left(\left(u2 + u2\right) \cdot \pi\right)} \]
    2. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 + u2\right) \cdot \pi\right)} \]
    3. lift-+.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(u2 + u2\right)} \cdot \pi\right) \]
    4. count-2N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
    5. associate-*r*N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(2 \cdot \left(u2 \cdot \pi\right)\right)} \]
    6. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(2 \cdot \color{blue}{\left(u2 \cdot \pi\right)}\right) \]
    7. sin-2N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left(2 \cdot \left(\sin \left(u2 \cdot \pi\right) \cdot \cos \left(u2 \cdot \pi\right)\right)\right)} \]
    8. lower-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left(2 \cdot \left(\sin \left(u2 \cdot \pi\right) \cdot \cos \left(u2 \cdot \pi\right)\right)\right)} \]
    9. lower-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \color{blue}{\left(\sin \left(u2 \cdot \pi\right) \cdot \cos \left(u2 \cdot \pi\right)\right)}\right) \]
    10. lower-sin.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\color{blue}{\sin \left(u2 \cdot \pi\right)} \cdot \cos \left(u2 \cdot \pi\right)\right)\right) \]
    11. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \color{blue}{\left(u2 \cdot \pi\right)} \cdot \cos \left(u2 \cdot \pi\right)\right)\right) \]
    12. *-commutativeN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \color{blue}{\left(\pi \cdot u2\right)} \cdot \cos \left(u2 \cdot \pi\right)\right)\right) \]
    13. lower-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \color{blue}{\left(\pi \cdot u2\right)} \cdot \cos \left(u2 \cdot \pi\right)\right)\right) \]
    14. lower-cos.f3298.2

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \color{blue}{\cos \left(u2 \cdot \pi\right)}\right)\right) \]
    15. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \cos \color{blue}{\left(u2 \cdot \pi\right)}\right)\right) \]
    16. *-commutativeN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \cos \color{blue}{\left(\pi \cdot u2\right)}\right)\right) \]
    17. lower-*.f3298.2

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \cos \color{blue}{\left(\pi \cdot u2\right)}\right)\right) \]
  7. Applied rewrites98.2%

    \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \cos \left(\pi \cdot u2\right)\right)\right)} \]
  8. Step-by-step derivation
    1. lift-cos.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \color{blue}{\cos \left(\pi \cdot u2\right)}\right)\right) \]
    2. cos-neg-revN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \color{blue}{\cos \left(\mathsf{neg}\left(\pi \cdot u2\right)\right)}\right)\right) \]
    3. sin-+PI/2-revN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \color{blue}{\sin \left(\left(\mathsf{neg}\left(\pi \cdot u2\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right)}\right)\right) \]
    4. lower-sin.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \color{blue}{\sin \left(\left(\mathsf{neg}\left(\pi \cdot u2\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right)}\right)\right) \]
    5. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \left(\left(\mathsf{neg}\left(\color{blue}{\pi \cdot u2}\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right)\right)\right) \]
    6. *-commutativeN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \left(\left(\mathsf{neg}\left(\color{blue}{u2 \cdot \pi}\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right)\right)\right) \]
    7. distribute-lft-neg-inN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \left(\color{blue}{\left(\mathsf{neg}\left(u2\right)\right) \cdot \pi} + \frac{\mathsf{PI}\left(\right)}{2}\right)\right)\right) \]
    8. lower-fma.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \color{blue}{\left(\mathsf{fma}\left(\mathsf{neg}\left(u2\right), \pi, \frac{\mathsf{PI}\left(\right)}{2}\right)\right)}\right)\right) \]
    9. lower-neg.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \left(\mathsf{fma}\left(\color{blue}{-u2}, \pi, \frac{\mathsf{PI}\left(\right)}{2}\right)\right)\right)\right) \]
    10. lift-PI.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \left(\mathsf{fma}\left(-u2, \pi, \frac{\color{blue}{\pi}}{2}\right)\right)\right)\right) \]
    11. mult-flipN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \left(\mathsf{fma}\left(-u2, \pi, \color{blue}{\pi \cdot \frac{1}{2}}\right)\right)\right)\right) \]
    12. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \left(\mathsf{fma}\left(-u2, \pi, \pi \cdot \color{blue}{\frac{1}{2}}\right)\right)\right)\right) \]
    13. lower-*.f3298.3

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \sin \left(\mathsf{fma}\left(-u2, \pi, \color{blue}{\pi \cdot 0.5}\right)\right)\right)\right) \]
  9. Applied rewrites98.3%

    \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\sin \left(\pi \cdot u2\right) \cdot \color{blue}{\sin \left(\mathsf{fma}\left(-u2, \pi, \pi \cdot 0.5\right)\right)}\right)\right) \]
  10. Add Preprocessing

Alternative 2: 98.3% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (* (sqrt (- (log1p (- u1)))) (sin (* (+ u2 u2) PI))))
float code(float cosTheta_i, float u1, float u2) {
	return sqrtf(-log1pf(-u1)) * sinf(((u2 + u2) * ((float) M_PI)));
}
function code(cosTheta_i, u1, u2)
	return Float32(sqrt(Float32(-log1p(Float32(-u1)))) * sin(Float32(Float32(u2 + u2) * Float32(pi))))
end
\begin{array}{l}

\\
\sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right)
\end{array}
Derivation
  1. Initial program 57.5%

    \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
  2. Step-by-step derivation
    1. lift-log.f32N/A

      \[\leadsto \sqrt{-\color{blue}{\log \left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    2. lift--.f32N/A

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    3. sub-flipN/A

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    4. lower-log1p.f32N/A

      \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    5. lower-neg.f3298.3

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{-u1}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
  3. Applied rewrites98.3%

    \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(-u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
  4. Step-by-step derivation
    1. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(2 \cdot \pi\right) \cdot u2\right)} \]
    2. *-commutativeN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(u2 \cdot \left(2 \cdot \pi\right)\right)} \]
    3. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(u2 \cdot \color{blue}{\left(2 \cdot \pi\right)}\right) \]
    4. associate-*r*N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 \cdot 2\right) \cdot \pi\right)} \]
    5. *-commutativeN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
    6. lower-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
    7. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(1 + 1\right)} \cdot u2\right) \cdot \pi\right) \]
    8. flip-+N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1}} \cdot u2\right) \cdot \pi\right) \]
    9. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{1} - 1 \cdot 1}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    10. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1 - \color{blue}{1}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    11. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{0}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    12. +-inversesN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi - \pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    13. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi} - \pi \cdot \pi}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    14. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \color{blue}{\pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
    15. metadata-evalN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{0}} \cdot u2\right) \cdot \pi\right) \]
    16. +-inversesN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{\pi - \pi}} \cdot u2\right) \cdot \pi\right) \]
    17. flip-+N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(\pi + \pi\right)} \cdot u2\right) \cdot \pi\right) \]
    18. count-2-revN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
    19. lift-*.f32N/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
    20. lower-*.f3225.1

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(\left(2 \cdot \pi\right) \cdot u2\right) \cdot \pi\right)} \]
  5. Applied rewrites98.3%

    \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 + u2\right) \cdot \pi\right)} \]
  6. Add Preprocessing

Alternative 3: 96.9% accurate, 0.8× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \log \left(1 - u1\right)\\ \mathbf{if}\;t\_0 \leq -0.0024999999441206455:\\ \;\;\;\;\sqrt{-t\_0} \cdot \sin \left(\left(\pi + \pi\right) \cdot u2\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{u1 \cdot \left(1 + 0.5 \cdot u1\right)} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right)\\ \end{array} \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (let* ((t_0 (log (- 1.0 u1))))
   (if (<= t_0 -0.0024999999441206455)
     (* (sqrt (- t_0)) (sin (* (+ PI PI) u2)))
     (* (sqrt (* u1 (+ 1.0 (* 0.5 u1)))) (sin (* (+ u2 u2) PI))))))
float code(float cosTheta_i, float u1, float u2) {
	float t_0 = logf((1.0f - u1));
	float tmp;
	if (t_0 <= -0.0024999999441206455f) {
		tmp = sqrtf(-t_0) * sinf(((((float) M_PI) + ((float) M_PI)) * u2));
	} else {
		tmp = sqrtf((u1 * (1.0f + (0.5f * u1)))) * sinf(((u2 + u2) * ((float) M_PI)));
	}
	return tmp;
}
function code(cosTheta_i, u1, u2)
	t_0 = log(Float32(Float32(1.0) - u1))
	tmp = Float32(0.0)
	if (t_0 <= Float32(-0.0024999999441206455))
		tmp = Float32(sqrt(Float32(-t_0)) * sin(Float32(Float32(Float32(pi) + Float32(pi)) * u2)));
	else
		tmp = Float32(sqrt(Float32(u1 * Float32(Float32(1.0) + Float32(Float32(0.5) * u1)))) * sin(Float32(Float32(u2 + u2) * Float32(pi))));
	end
	return tmp
end
function tmp_2 = code(cosTheta_i, u1, u2)
	t_0 = log((single(1.0) - u1));
	tmp = single(0.0);
	if (t_0 <= single(-0.0024999999441206455))
		tmp = sqrt(-t_0) * sin(((single(pi) + single(pi)) * u2));
	else
		tmp = sqrt((u1 * (single(1.0) + (single(0.5) * u1)))) * sin(((u2 + u2) * single(pi)));
	end
	tmp_2 = tmp;
end
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \log \left(1 - u1\right)\\
\mathbf{if}\;t\_0 \leq -0.0024999999441206455:\\
\;\;\;\;\sqrt{-t\_0} \cdot \sin \left(\left(\pi + \pi\right) \cdot u2\right)\\

\mathbf{else}:\\
\;\;\;\;\sqrt{u1 \cdot \left(1 + 0.5 \cdot u1\right)} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (log.f32 (-.f32 #s(literal 1 binary32) u1)) < -0.00249999994

    1. Initial program 57.5%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    2. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
      2. count-2-revN/A

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\color{blue}{\left(\pi + \pi\right)} \cdot u2\right) \]
      3. lower-+.f3257.5

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\color{blue}{\left(\pi + \pi\right)} \cdot u2\right) \]
    3. Applied rewrites57.5%

      \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \color{blue}{\left(\left(\pi + \pi\right) \cdot u2\right)} \]

    if -0.00249999994 < (log.f32 (-.f32 #s(literal 1 binary32) u1))

    1. Initial program 57.5%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    2. Step-by-step derivation
      1. lift-log.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\log \left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      2. lift--.f32N/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      3. sub-flipN/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      4. lower-log1p.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      5. lower-neg.f3298.3

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{-u1}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    3. Applied rewrites98.3%

      \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(-u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    4. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(2 \cdot \pi\right) \cdot u2\right)} \]
      2. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(u2 \cdot \left(2 \cdot \pi\right)\right)} \]
      3. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(u2 \cdot \color{blue}{\left(2 \cdot \pi\right)}\right) \]
      4. associate-*r*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 \cdot 2\right) \cdot \pi\right)} \]
      5. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      6. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      7. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(1 + 1\right)} \cdot u2\right) \cdot \pi\right) \]
      8. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1}} \cdot u2\right) \cdot \pi\right) \]
      9. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{1} - 1 \cdot 1}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1 - \color{blue}{1}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      11. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{0}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      12. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi - \pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      13. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi} - \pi \cdot \pi}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      14. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \color{blue}{\pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      15. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{0}} \cdot u2\right) \cdot \pi\right) \]
      16. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{\pi - \pi}} \cdot u2\right) \cdot \pi\right) \]
      17. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(\pi + \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      18. count-2-revN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      19. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      20. lower-*.f3225.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(\left(2 \cdot \pi\right) \cdot u2\right) \cdot \pi\right)} \]
    5. Applied rewrites98.3%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 + u2\right) \cdot \pi\right)} \]
    6. Taylor expanded in u1 around 0

      \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + \frac{1}{2} \cdot u1\right)}} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
    7. Step-by-step derivation
      1. lower-*.f32N/A

        \[\leadsto \sqrt{u1 \cdot \color{blue}{\left(1 + \frac{1}{2} \cdot u1\right)}} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
      2. lower-+.f32N/A

        \[\leadsto \sqrt{u1 \cdot \left(1 + \color{blue}{\frac{1}{2} \cdot u1}\right)} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
      3. lower-*.f3288.0

        \[\leadsto \sqrt{u1 \cdot \left(1 + 0.5 \cdot \color{blue}{u1}\right)} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
    8. Applied rewrites88.0%

      \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + 0.5 \cdot u1\right)}} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 4: 94.2% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;u2 \leq 0.00018200000340584666:\\ \;\;\;\;\sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\pi + \pi\right) \cdot u2\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{u1 \cdot \left(1 + 0.5 \cdot u1\right)} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right)\\ \end{array} \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (if (<= u2 0.00018200000340584666)
   (* (sqrt (- (log1p (- u1)))) (* (+ PI PI) u2))
   (* (sqrt (* u1 (+ 1.0 (* 0.5 u1)))) (sin (* (+ u2 u2) PI)))))
float code(float cosTheta_i, float u1, float u2) {
	float tmp;
	if (u2 <= 0.00018200000340584666f) {
		tmp = sqrtf(-log1pf(-u1)) * ((((float) M_PI) + ((float) M_PI)) * u2);
	} else {
		tmp = sqrtf((u1 * (1.0f + (0.5f * u1)))) * sinf(((u2 + u2) * ((float) M_PI)));
	}
	return tmp;
}
function code(cosTheta_i, u1, u2)
	tmp = Float32(0.0)
	if (u2 <= Float32(0.00018200000340584666))
		tmp = Float32(sqrt(Float32(-log1p(Float32(-u1)))) * Float32(Float32(Float32(pi) + Float32(pi)) * u2));
	else
		tmp = Float32(sqrt(Float32(u1 * Float32(Float32(1.0) + Float32(Float32(0.5) * u1)))) * sin(Float32(Float32(u2 + u2) * Float32(pi))));
	end
	return tmp
end
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;u2 \leq 0.00018200000340584666:\\
\;\;\;\;\sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\pi + \pi\right) \cdot u2\right)\\

\mathbf{else}:\\
\;\;\;\;\sqrt{u1 \cdot \left(1 + 0.5 \cdot u1\right)} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if u2 < 1.82000003e-4

    1. Initial program 57.5%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    2. Step-by-step derivation
      1. lift-log.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\log \left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      2. lift--.f32N/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      3. sub-flipN/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      4. lower-log1p.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      5. lower-neg.f3298.3

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{-u1}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    3. Applied rewrites98.3%

      \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(-u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    4. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(2 \cdot \pi\right) \cdot u2\right)} \]
      2. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(u2 \cdot \left(2 \cdot \pi\right)\right)} \]
      3. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(u2 \cdot \color{blue}{\left(2 \cdot \pi\right)}\right) \]
      4. associate-*r*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 \cdot 2\right) \cdot \pi\right)} \]
      5. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      6. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      7. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(1 + 1\right)} \cdot u2\right) \cdot \pi\right) \]
      8. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1}} \cdot u2\right) \cdot \pi\right) \]
      9. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{1} - 1 \cdot 1}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1 - \color{blue}{1}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      11. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{0}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      12. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi - \pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      13. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi} - \pi \cdot \pi}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      14. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \color{blue}{\pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      15. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{0}} \cdot u2\right) \cdot \pi\right) \]
      16. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{\pi - \pi}} \cdot u2\right) \cdot \pi\right) \]
      17. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(\pi + \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      18. count-2-revN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      19. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      20. lower-*.f3225.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(\left(2 \cdot \pi\right) \cdot u2\right) \cdot \pi\right)} \]
    5. Applied rewrites98.3%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 + u2\right) \cdot \pi\right)} \]
    6. Taylor expanded in u2 around 0

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
    7. Step-by-step derivation
      1. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right)\right)}\right) \]
      2. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(u2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)\right) \]
      3. lower-PI.f3281.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right) \]
    8. Applied rewrites81.1%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left(2 \cdot \left(u2 \cdot \pi\right)\right)} \]
    9. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \color{blue}{\left(u2 \cdot \pi\right)}\right) \]
      2. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(u2 \cdot \color{blue}{\pi}\right)\right) \]
      3. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\pi \cdot \color{blue}{u2}\right)\right) \]
      4. associate-*l*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \pi\right) \cdot \color{blue}{u2}\right) \]
      5. lift-PI.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      6. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(1 + 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      7. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      8. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{1 - 1 \cdot 1}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      9. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{1 - 1}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{0}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      11. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{u2 \cdot u2 - u2 \cdot u2}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      12. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{u2 \cdot u2 - u2 \cdot u2}{0} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      13. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{u2 \cdot u2 - u2 \cdot u2}{u2 - u2} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      14. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(u2 + u2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      15. count-2N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(2 \cdot u2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      16. lift-PI.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(2 \cdot u2\right) \cdot \pi\right) \cdot u2\right) \]
      17. associate-*r*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot u2\right) \]
      18. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot u2\right) \]
      19. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot u2\right) \]
      20. lower-*.f3216.3

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot \color{blue}{u2}\right) \]
    10. Applied rewrites81.1%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\pi + \pi\right) \cdot \color{blue}{u2}\right) \]

    if 1.82000003e-4 < u2

    1. Initial program 57.5%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    2. Step-by-step derivation
      1. lift-log.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\log \left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      2. lift--.f32N/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      3. sub-flipN/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      4. lower-log1p.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      5. lower-neg.f3298.3

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{-u1}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    3. Applied rewrites98.3%

      \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(-u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    4. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(2 \cdot \pi\right) \cdot u2\right)} \]
      2. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(u2 \cdot \left(2 \cdot \pi\right)\right)} \]
      3. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(u2 \cdot \color{blue}{\left(2 \cdot \pi\right)}\right) \]
      4. associate-*r*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 \cdot 2\right) \cdot \pi\right)} \]
      5. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      6. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      7. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(1 + 1\right)} \cdot u2\right) \cdot \pi\right) \]
      8. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1}} \cdot u2\right) \cdot \pi\right) \]
      9. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{1} - 1 \cdot 1}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1 - \color{blue}{1}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      11. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{0}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      12. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi - \pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      13. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi} - \pi \cdot \pi}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      14. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \color{blue}{\pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      15. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{0}} \cdot u2\right) \cdot \pi\right) \]
      16. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{\pi - \pi}} \cdot u2\right) \cdot \pi\right) \]
      17. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(\pi + \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      18. count-2-revN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      19. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      20. lower-*.f3225.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(\left(2 \cdot \pi\right) \cdot u2\right) \cdot \pi\right)} \]
    5. Applied rewrites98.3%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 + u2\right) \cdot \pi\right)} \]
    6. Taylor expanded in u1 around 0

      \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + \frac{1}{2} \cdot u1\right)}} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
    7. Step-by-step derivation
      1. lower-*.f32N/A

        \[\leadsto \sqrt{u1 \cdot \color{blue}{\left(1 + \frac{1}{2} \cdot u1\right)}} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
      2. lower-+.f32N/A

        \[\leadsto \sqrt{u1 \cdot \left(1 + \color{blue}{\frac{1}{2} \cdot u1}\right)} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
      3. lower-*.f3288.0

        \[\leadsto \sqrt{u1 \cdot \left(1 + 0.5 \cdot \color{blue}{u1}\right)} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
    8. Applied rewrites88.0%

      \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + 0.5 \cdot u1\right)}} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 5: 90.7% accurate, 1.1× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;u2 \leq 0.0019000000320374966:\\ \;\;\;\;\sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\pi + \pi\right) \cdot u2\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{u1} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right)\\ \end{array} \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (if (<= u2 0.0019000000320374966)
   (* (sqrt (- (log1p (- u1)))) (* (+ PI PI) u2))
   (* (sqrt u1) (sin (* (+ u2 u2) PI)))))
float code(float cosTheta_i, float u1, float u2) {
	float tmp;
	if (u2 <= 0.0019000000320374966f) {
		tmp = sqrtf(-log1pf(-u1)) * ((((float) M_PI) + ((float) M_PI)) * u2);
	} else {
		tmp = sqrtf(u1) * sinf(((u2 + u2) * ((float) M_PI)));
	}
	return tmp;
}
function code(cosTheta_i, u1, u2)
	tmp = Float32(0.0)
	if (u2 <= Float32(0.0019000000320374966))
		tmp = Float32(sqrt(Float32(-log1p(Float32(-u1)))) * Float32(Float32(Float32(pi) + Float32(pi)) * u2));
	else
		tmp = Float32(sqrt(u1) * sin(Float32(Float32(u2 + u2) * Float32(pi))));
	end
	return tmp
end
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;u2 \leq 0.0019000000320374966:\\
\;\;\;\;\sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\pi + \pi\right) \cdot u2\right)\\

\mathbf{else}:\\
\;\;\;\;\sqrt{u1} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if u2 < 0.00190000003

    1. Initial program 57.5%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    2. Step-by-step derivation
      1. lift-log.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\log \left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      2. lift--.f32N/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      3. sub-flipN/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      4. lower-log1p.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      5. lower-neg.f3298.3

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{-u1}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    3. Applied rewrites98.3%

      \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(-u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    4. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(2 \cdot \pi\right) \cdot u2\right)} \]
      2. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(u2 \cdot \left(2 \cdot \pi\right)\right)} \]
      3. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(u2 \cdot \color{blue}{\left(2 \cdot \pi\right)}\right) \]
      4. associate-*r*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 \cdot 2\right) \cdot \pi\right)} \]
      5. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      6. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      7. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(1 + 1\right)} \cdot u2\right) \cdot \pi\right) \]
      8. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1}} \cdot u2\right) \cdot \pi\right) \]
      9. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{1} - 1 \cdot 1}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1 - \color{blue}{1}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      11. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{0}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      12. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi - \pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      13. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi} - \pi \cdot \pi}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      14. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \color{blue}{\pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      15. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{0}} \cdot u2\right) \cdot \pi\right) \]
      16. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{\pi - \pi}} \cdot u2\right) \cdot \pi\right) \]
      17. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(\pi + \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      18. count-2-revN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      19. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      20. lower-*.f3225.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(\left(2 \cdot \pi\right) \cdot u2\right) \cdot \pi\right)} \]
    5. Applied rewrites98.3%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 + u2\right) \cdot \pi\right)} \]
    6. Taylor expanded in u2 around 0

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
    7. Step-by-step derivation
      1. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right)\right)}\right) \]
      2. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(u2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)\right) \]
      3. lower-PI.f3281.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right) \]
    8. Applied rewrites81.1%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left(2 \cdot \left(u2 \cdot \pi\right)\right)} \]
    9. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \color{blue}{\left(u2 \cdot \pi\right)}\right) \]
      2. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(u2 \cdot \color{blue}{\pi}\right)\right) \]
      3. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\pi \cdot \color{blue}{u2}\right)\right) \]
      4. associate-*l*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \pi\right) \cdot \color{blue}{u2}\right) \]
      5. lift-PI.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      6. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(1 + 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      7. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      8. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{1 - 1 \cdot 1}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      9. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{1 - 1}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{0}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      11. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{u2 \cdot u2 - u2 \cdot u2}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      12. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{u2 \cdot u2 - u2 \cdot u2}{0} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      13. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{u2 \cdot u2 - u2 \cdot u2}{u2 - u2} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      14. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(u2 + u2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      15. count-2N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(2 \cdot u2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      16. lift-PI.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(2 \cdot u2\right) \cdot \pi\right) \cdot u2\right) \]
      17. associate-*r*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot u2\right) \]
      18. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot u2\right) \]
      19. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot u2\right) \]
      20. lower-*.f3216.3

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot \color{blue}{u2}\right) \]
    10. Applied rewrites81.1%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\pi + \pi\right) \cdot \color{blue}{u2}\right) \]

    if 0.00190000003 < u2

    1. Initial program 57.5%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    2. Step-by-step derivation
      1. lift-log.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\log \left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      2. lift--.f32N/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      3. sub-flipN/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      4. lower-log1p.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      5. lower-neg.f3298.3

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{-u1}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    3. Applied rewrites98.3%

      \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(-u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    4. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(2 \cdot \pi\right) \cdot u2\right)} \]
      2. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(u2 \cdot \left(2 \cdot \pi\right)\right)} \]
      3. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(u2 \cdot \color{blue}{\left(2 \cdot \pi\right)}\right) \]
      4. associate-*r*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 \cdot 2\right) \cdot \pi\right)} \]
      5. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      6. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      7. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(1 + 1\right)} \cdot u2\right) \cdot \pi\right) \]
      8. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1}} \cdot u2\right) \cdot \pi\right) \]
      9. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{1} - 1 \cdot 1}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1 - \color{blue}{1}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      11. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{0}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      12. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi - \pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      13. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi} - \pi \cdot \pi}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      14. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \color{blue}{\pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      15. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{0}} \cdot u2\right) \cdot \pi\right) \]
      16. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{\pi - \pi}} \cdot u2\right) \cdot \pi\right) \]
      17. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(\pi + \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      18. count-2-revN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      19. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      20. lower-*.f3225.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(\left(2 \cdot \pi\right) \cdot u2\right) \cdot \pi\right)} \]
    5. Applied rewrites98.3%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 + u2\right) \cdot \pi\right)} \]
    6. Taylor expanded in u1 around 0

      \[\leadsto \sqrt{\color{blue}{u1}} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
    7. Step-by-step derivation
      1. Applied rewrites76.6%

        \[\leadsto \sqrt{\color{blue}{u1}} \cdot \sin \left(\left(u2 + u2\right) \cdot \pi\right) \]
    8. Recombined 2 regimes into one program.
    9. Add Preprocessing

    Alternative 6: 81.1% accurate, 2.3× speedup?

    \[\begin{array}{l} \\ \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\pi + \pi\right) \cdot u2\right) \end{array} \]
    (FPCore (cosTheta_i u1 u2)
     :precision binary32
     (* (sqrt (- (log1p (- u1)))) (* (+ PI PI) u2)))
    float code(float cosTheta_i, float u1, float u2) {
    	return sqrtf(-log1pf(-u1)) * ((((float) M_PI) + ((float) M_PI)) * u2);
    }
    
    function code(cosTheta_i, u1, u2)
    	return Float32(sqrt(Float32(-log1p(Float32(-u1)))) * Float32(Float32(Float32(pi) + Float32(pi)) * u2))
    end
    
    \begin{array}{l}
    
    \\
    \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\pi + \pi\right) \cdot u2\right)
    \end{array}
    
    Derivation
    1. Initial program 57.5%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    2. Step-by-step derivation
      1. lift-log.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\log \left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      2. lift--.f32N/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      3. sub-flipN/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 + \left(\mathsf{neg}\left(u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      4. lower-log1p.f32N/A

        \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(\mathsf{neg}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      5. lower-neg.f3298.3

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{-u1}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    3. Applied rewrites98.3%

      \[\leadsto \sqrt{-\color{blue}{\mathsf{log1p}\left(-u1\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
    4. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(2 \cdot \pi\right) \cdot u2\right)} \]
      2. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(u2 \cdot \left(2 \cdot \pi\right)\right)} \]
      3. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(u2 \cdot \color{blue}{\left(2 \cdot \pi\right)}\right) \]
      4. associate-*r*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 \cdot 2\right) \cdot \pi\right)} \]
      5. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      6. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(2 \cdot u2\right)} \cdot \pi\right) \]
      7. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(1 + 1\right)} \cdot u2\right) \cdot \pi\right) \]
      8. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1}} \cdot u2\right) \cdot \pi\right) \]
      9. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{1} - 1 \cdot 1}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1 - \color{blue}{1}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      11. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{0}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      12. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi - \pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      13. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\color{blue}{\pi \cdot \pi} - \pi \cdot \pi}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      14. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \color{blue}{\pi \cdot \pi}}{1 - 1} \cdot u2\right) \cdot \pi\right) \]
      15. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{0}} \cdot u2\right) \cdot \pi\right) \]
      16. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{\pi \cdot \pi - \pi \cdot \pi}{\color{blue}{\pi - \pi}} \cdot u2\right) \cdot \pi\right) \]
      17. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(\pi + \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      18. count-2-revN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      19. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \cdot \pi\right) \]
      20. lower-*.f3225.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(\left(2 \cdot \pi\right) \cdot u2\right) \cdot \pi\right)} \]
    5. Applied rewrites98.3%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \color{blue}{\left(\left(u2 + u2\right) \cdot \pi\right)} \]
    6. Taylor expanded in u2 around 0

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
    7. Step-by-step derivation
      1. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right)\right)}\right) \]
      2. lower-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(u2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)\right) \]
      3. lower-PI.f3281.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right) \]
    8. Applied rewrites81.1%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \color{blue}{\left(2 \cdot \left(u2 \cdot \pi\right)\right)} \]
    9. Step-by-step derivation
      1. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \color{blue}{\left(u2 \cdot \pi\right)}\right) \]
      2. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(u2 \cdot \color{blue}{\pi}\right)\right) \]
      3. *-commutativeN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(2 \cdot \left(\pi \cdot \color{blue}{u2}\right)\right) \]
      4. associate-*l*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \pi\right) \cdot \color{blue}{u2}\right) \]
      5. lift-PI.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      6. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(1 + 1\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      7. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{1 \cdot 1 - 1 \cdot 1}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      8. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{1 - 1 \cdot 1}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      9. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{1 - 1}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      10. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{0}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      11. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{u2 \cdot u2 - u2 \cdot u2}{1 - 1} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      12. metadata-evalN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{u2 \cdot u2 - u2 \cdot u2}{0} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      13. +-inversesN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\frac{u2 \cdot u2 - u2 \cdot u2}{u2 - u2} \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      14. flip-+N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(u2 + u2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      15. count-2N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(2 \cdot u2\right) \cdot \mathsf{PI}\left(\right)\right) \cdot u2\right) \]
      16. lift-PI.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\left(2 \cdot u2\right) \cdot \pi\right) \cdot u2\right) \]
      17. associate-*r*N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot u2\right) \]
      18. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot u2\right) \]
      19. lift-*.f32N/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot u2\right) \]
      20. lower-*.f3216.3

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot \color{blue}{u2}\right) \]
    10. Applied rewrites81.1%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \left(\left(\pi + \pi\right) \cdot \color{blue}{u2}\right) \]
    11. Add Preprocessing

    Alternative 7: 80.2% accurate, 2.2× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;u1 \leq 0.0020000000949949026:\\ \;\;\;\;\sqrt{u1 \cdot \left(1 + u1 \cdot 0.5\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{-\log \left(1 - u1\right)} \cdot \left(u2 + u2\right)\right) \cdot \pi\\ \end{array} \end{array} \]
    (FPCore (cosTheta_i u1 u2)
     :precision binary32
     (if (<= u1 0.0020000000949949026)
       (* (sqrt (* u1 (+ 1.0 (* u1 0.5)))) (* 2.0 (* u2 PI)))
       (* (* (sqrt (- (log (- 1.0 u1)))) (+ u2 u2)) PI)))
    float code(float cosTheta_i, float u1, float u2) {
    	float tmp;
    	if (u1 <= 0.0020000000949949026f) {
    		tmp = sqrtf((u1 * (1.0f + (u1 * 0.5f)))) * (2.0f * (u2 * ((float) M_PI)));
    	} else {
    		tmp = (sqrtf(-logf((1.0f - u1))) * (u2 + u2)) * ((float) M_PI);
    	}
    	return tmp;
    }
    
    function code(cosTheta_i, u1, u2)
    	tmp = Float32(0.0)
    	if (u1 <= Float32(0.0020000000949949026))
    		tmp = Float32(sqrt(Float32(u1 * Float32(Float32(1.0) + Float32(u1 * Float32(0.5))))) * Float32(Float32(2.0) * Float32(u2 * Float32(pi))));
    	else
    		tmp = Float32(Float32(sqrt(Float32(-log(Float32(Float32(1.0) - u1)))) * Float32(u2 + u2)) * Float32(pi));
    	end
    	return tmp
    end
    
    function tmp_2 = code(cosTheta_i, u1, u2)
    	tmp = single(0.0);
    	if (u1 <= single(0.0020000000949949026))
    		tmp = sqrt((u1 * (single(1.0) + (u1 * single(0.5))))) * (single(2.0) * (u2 * single(pi)));
    	else
    		tmp = (sqrt(-log((single(1.0) - u1))) * (u2 + u2)) * single(pi);
    	end
    	tmp_2 = tmp;
    end
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;u1 \leq 0.0020000000949949026:\\
    \;\;\;\;\sqrt{u1 \cdot \left(1 + u1 \cdot 0.5\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\left(\sqrt{-\log \left(1 - u1\right)} \cdot \left(u2 + u2\right)\right) \cdot \pi\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if u1 < 0.00200000009

      1. Initial program 57.5%

        \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      2. Taylor expanded in u1 around 0

        \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      3. Step-by-step derivation
        1. lower-*.f32N/A

          \[\leadsto \sqrt{u1 \cdot \color{blue}{\left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        2. lower-+.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + \color{blue}{u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        3. lower-*.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \color{blue}{\left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        4. lower-+.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + \color{blue}{u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)}\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        5. lower-*.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \color{blue}{\left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)}\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        6. lower-+.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \color{blue}{\frac{1}{4} \cdot u1}\right)\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        7. lower-*.f3293.4

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(0.5 + u1 \cdot \left(0.3333333333333333 + 0.25 \cdot \color{blue}{u1}\right)\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      4. Applied rewrites93.4%

        \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + u1 \cdot \left(0.5 + u1 \cdot \left(0.3333333333333333 + 0.25 \cdot u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      5. Taylor expanded in u2 around 0

        \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)} \cdot \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
      6. Step-by-step derivation
        1. lower-*.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)} \cdot \left(2 \cdot \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right)\right)}\right) \]
        2. lower-*.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)} \cdot \left(2 \cdot \left(u2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)\right) \]
        3. lower-PI.f3277.7

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(0.5 + u1 \cdot \left(0.3333333333333333 + 0.25 \cdot u1\right)\right)\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right) \]
      7. Applied rewrites77.7%

        \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(0.5 + u1 \cdot \left(0.3333333333333333 + 0.25 \cdot u1\right)\right)\right)} \cdot \color{blue}{\left(2 \cdot \left(u2 \cdot \pi\right)\right)} \]
      8. Taylor expanded in u1 around 0

        \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \frac{1}{2}\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right) \]
      9. Step-by-step derivation
        1. Applied rewrites73.8%

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot 0.5\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right) \]

        if 0.00200000009 < u1

        1. Initial program 57.5%

          \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        2. Taylor expanded in u2 around 0

          \[\leadsto \color{blue}{2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right)} \]
        3. Step-by-step derivation
          1. lower-*.f32N/A

            \[\leadsto 2 \cdot \color{blue}{\left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right)} \]
          2. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)}\right) \]
          3. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}}\right)\right) \]
          4. lower-PI.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}}\right)\right) \]
          5. lower-sqrt.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right) \]
          6. lower-neg.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
          7. lower-log.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
          8. lower--.f3250.5

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
        4. Applied rewrites50.5%

          \[\leadsto \color{blue}{2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right)} \]
        5. Applied rewrites50.5%

          \[\leadsto \left(\sqrt{-\log \left(1 - u1\right)} \cdot \left(u2 + u2\right)\right) \cdot \color{blue}{\pi} \]
      10. Recombined 2 regimes into one program.
      11. Add Preprocessing

      Alternative 8: 73.8% accurate, 2.6× speedup?

      \[\begin{array}{l} \\ \sqrt{u1 \cdot \left(1 + u1 \cdot 0.5\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right) \end{array} \]
      (FPCore (cosTheta_i u1 u2)
       :precision binary32
       (* (sqrt (* u1 (+ 1.0 (* u1 0.5)))) (* 2.0 (* u2 PI))))
      float code(float cosTheta_i, float u1, float u2) {
      	return sqrtf((u1 * (1.0f + (u1 * 0.5f)))) * (2.0f * (u2 * ((float) M_PI)));
      }
      
      function code(cosTheta_i, u1, u2)
      	return Float32(sqrt(Float32(u1 * Float32(Float32(1.0) + Float32(u1 * Float32(0.5))))) * Float32(Float32(2.0) * Float32(u2 * Float32(pi))))
      end
      
      function tmp = code(cosTheta_i, u1, u2)
      	tmp = sqrt((u1 * (single(1.0) + (u1 * single(0.5))))) * (single(2.0) * (u2 * single(pi)));
      end
      
      \begin{array}{l}
      
      \\
      \sqrt{u1 \cdot \left(1 + u1 \cdot 0.5\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right)
      \end{array}
      
      Derivation
      1. Initial program 57.5%

        \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      2. Taylor expanded in u1 around 0

        \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      3. Step-by-step derivation
        1. lower-*.f32N/A

          \[\leadsto \sqrt{u1 \cdot \color{blue}{\left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        2. lower-+.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + \color{blue}{u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        3. lower-*.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \color{blue}{\left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        4. lower-+.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + \color{blue}{u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)}\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        5. lower-*.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \color{blue}{\left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)}\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        6. lower-+.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \color{blue}{\frac{1}{4} \cdot u1}\right)\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        7. lower-*.f3293.4

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(0.5 + u1 \cdot \left(0.3333333333333333 + 0.25 \cdot \color{blue}{u1}\right)\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      4. Applied rewrites93.4%

        \[\leadsto \sqrt{\color{blue}{u1 \cdot \left(1 + u1 \cdot \left(0.5 + u1 \cdot \left(0.3333333333333333 + 0.25 \cdot u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
      5. Taylor expanded in u2 around 0

        \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)} \cdot \color{blue}{\left(2 \cdot \left(u2 \cdot \mathsf{PI}\left(\right)\right)\right)} \]
      6. Step-by-step derivation
        1. lower-*.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)} \cdot \left(2 \cdot \color{blue}{\left(u2 \cdot \mathsf{PI}\left(\right)\right)}\right) \]
        2. lower-*.f32N/A

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(\frac{1}{2} + u1 \cdot \left(\frac{1}{3} + \frac{1}{4} \cdot u1\right)\right)\right)} \cdot \left(2 \cdot \left(u2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)\right) \]
        3. lower-PI.f3277.7

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(0.5 + u1 \cdot \left(0.3333333333333333 + 0.25 \cdot u1\right)\right)\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right) \]
      7. Applied rewrites77.7%

        \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \left(0.5 + u1 \cdot \left(0.3333333333333333 + 0.25 \cdot u1\right)\right)\right)} \cdot \color{blue}{\left(2 \cdot \left(u2 \cdot \pi\right)\right)} \]
      8. Taylor expanded in u1 around 0

        \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot \frac{1}{2}\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right) \]
      9. Step-by-step derivation
        1. Applied rewrites73.8%

          \[\leadsto \sqrt{u1 \cdot \left(1 + u1 \cdot 0.5\right)} \cdot \left(2 \cdot \left(u2 \cdot \pi\right)\right) \]
        2. Add Preprocessing

        Alternative 9: 66.0% accurate, 2.9× speedup?

        \[\begin{array}{l} \\ 2 \cdot \left(u2 \cdot \left(u1 \cdot \left(\pi \cdot \sqrt{\frac{1}{u1}}\right)\right)\right) \end{array} \]
        (FPCore (cosTheta_i u1 u2)
         :precision binary32
         (* 2.0 (* u2 (* u1 (* PI (sqrt (/ 1.0 u1)))))))
        float code(float cosTheta_i, float u1, float u2) {
        	return 2.0f * (u2 * (u1 * (((float) M_PI) * sqrtf((1.0f / u1)))));
        }
        
        function code(cosTheta_i, u1, u2)
        	return Float32(Float32(2.0) * Float32(u2 * Float32(u1 * Float32(Float32(pi) * sqrt(Float32(Float32(1.0) / u1))))))
        end
        
        function tmp = code(cosTheta_i, u1, u2)
        	tmp = single(2.0) * (u2 * (u1 * (single(pi) * sqrt((single(1.0) / u1)))));
        end
        
        \begin{array}{l}
        
        \\
        2 \cdot \left(u2 \cdot \left(u1 \cdot \left(\pi \cdot \sqrt{\frac{1}{u1}}\right)\right)\right)
        \end{array}
        
        Derivation
        1. Initial program 57.5%

          \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        2. Taylor expanded in u2 around 0

          \[\leadsto \color{blue}{2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right)} \]
        3. Step-by-step derivation
          1. lower-*.f32N/A

            \[\leadsto 2 \cdot \color{blue}{\left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right)} \]
          2. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)}\right) \]
          3. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}}\right)\right) \]
          4. lower-PI.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}}\right)\right) \]
          5. lower-sqrt.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right) \]
          6. lower-neg.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
          7. lower-log.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
          8. lower--.f3250.5

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
        4. Applied rewrites50.5%

          \[\leadsto \color{blue}{2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right)} \]
        5. Taylor expanded in u1 around 0

          \[\leadsto 2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\sqrt{u1}}\right)\right) \]
        6. Step-by-step derivation
          1. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{u1}\right)\right) \]
          2. lower-PI.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{u1}\right)\right) \]
          3. lower-sqrt.f3266.0

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{u1}\right)\right) \]
        7. Applied rewrites66.0%

          \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \color{blue}{\sqrt{u1}}\right)\right) \]
        8. Taylor expanded in u1 around inf

          \[\leadsto 2 \cdot \left(u2 \cdot \left(u1 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\sqrt{\frac{1}{u1}}}\right)\right)\right) \]
        9. Step-by-step derivation
          1. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(u1 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{\frac{1}{u1}}\right)\right)\right) \]
          2. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(u1 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{\frac{1}{u1}}\right)\right)\right) \]
          3. lower-PI.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(u1 \cdot \left(\pi \cdot \sqrt{\frac{1}{u1}}\right)\right)\right) \]
          4. lower-sqrt.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(u1 \cdot \left(\pi \cdot \sqrt{\frac{1}{u1}}\right)\right)\right) \]
          5. lower-/.f3266.0

            \[\leadsto 2 \cdot \left(u2 \cdot \left(u1 \cdot \left(\pi \cdot \sqrt{\frac{1}{u1}}\right)\right)\right) \]
        10. Applied rewrites66.0%

          \[\leadsto 2 \cdot \left(u2 \cdot \left(u1 \cdot \left(\pi \cdot \color{blue}{\sqrt{\frac{1}{u1}}}\right)\right)\right) \]
        11. Add Preprocessing

        Alternative 10: 66.0% accurate, 4.5× speedup?

        \[\begin{array}{l} \\ 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{u1}\right)\right) \end{array} \]
        (FPCore (cosTheta_i u1 u2) :precision binary32 (* 2.0 (* u2 (* PI (sqrt u1)))))
        float code(float cosTheta_i, float u1, float u2) {
        	return 2.0f * (u2 * (((float) M_PI) * sqrtf(u1)));
        }
        
        function code(cosTheta_i, u1, u2)
        	return Float32(Float32(2.0) * Float32(u2 * Float32(Float32(pi) * sqrt(u1))))
        end
        
        function tmp = code(cosTheta_i, u1, u2)
        	tmp = single(2.0) * (u2 * (single(pi) * sqrt(u1)));
        end
        
        \begin{array}{l}
        
        \\
        2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{u1}\right)\right)
        \end{array}
        
        Derivation
        1. Initial program 57.5%

          \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        2. Taylor expanded in u2 around 0

          \[\leadsto \color{blue}{2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right)} \]
        3. Step-by-step derivation
          1. lower-*.f32N/A

            \[\leadsto 2 \cdot \color{blue}{\left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right)} \]
          2. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)}\right) \]
          3. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}}\right)\right) \]
          4. lower-PI.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}}\right)\right) \]
          5. lower-sqrt.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right) \]
          6. lower-neg.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
          7. lower-log.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
          8. lower--.f3250.5

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
        4. Applied rewrites50.5%

          \[\leadsto \color{blue}{2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right)} \]
        5. Taylor expanded in u1 around 0

          \[\leadsto 2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\sqrt{u1}}\right)\right) \]
        6. Step-by-step derivation
          1. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{u1}\right)\right) \]
          2. lower-PI.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{u1}\right)\right) \]
          3. lower-sqrt.f3266.0

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{u1}\right)\right) \]
        7. Applied rewrites66.0%

          \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \color{blue}{\sqrt{u1}}\right)\right) \]
        8. Add Preprocessing

        Alternative 11: 16.0% accurate, 6.0× speedup?

        \[\begin{array}{l} \\ \left(\sqrt{u1} \cdot \pi\right) \cdot 2 \end{array} \]
        (FPCore (cosTheta_i u1 u2) :precision binary32 (* (* (sqrt u1) PI) 2.0))
        float code(float cosTheta_i, float u1, float u2) {
        	return (sqrtf(u1) * ((float) M_PI)) * 2.0f;
        }
        
        function code(cosTheta_i, u1, u2)
        	return Float32(Float32(sqrt(u1) * Float32(pi)) * Float32(2.0))
        end
        
        function tmp = code(cosTheta_i, u1, u2)
        	tmp = (sqrt(u1) * single(pi)) * single(2.0);
        end
        
        \begin{array}{l}
        
        \\
        \left(\sqrt{u1} \cdot \pi\right) \cdot 2
        \end{array}
        
        Derivation
        1. Initial program 57.5%

          \[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right) \]
        2. Taylor expanded in u2 around 0

          \[\leadsto \color{blue}{2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right)} \]
        3. Step-by-step derivation
          1. lower-*.f32N/A

            \[\leadsto 2 \cdot \color{blue}{\left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right)} \]
          2. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)}\right) \]
          3. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}}\right)\right) \]
          4. lower-PI.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{\color{blue}{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}}\right)\right) \]
          5. lower-sqrt.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}\right)\right) \]
          6. lower-neg.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
          7. lower-log.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
          8. lower--.f3250.5

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right) \]
        4. Applied rewrites50.5%

          \[\leadsto \color{blue}{2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{-\log \left(1 - u1\right)}\right)\right)} \]
        5. Taylor expanded in u1 around 0

          \[\leadsto 2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{\sqrt{u1}}\right)\right) \]
        6. Step-by-step derivation
          1. lower-*.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\mathsf{PI}\left(\right) \cdot \sqrt{u1}\right)\right) \]
          2. lower-PI.f32N/A

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{u1}\right)\right) \]
          3. lower-sqrt.f3266.0

            \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \sqrt{u1}\right)\right) \]
        7. Applied rewrites66.0%

          \[\leadsto 2 \cdot \left(u2 \cdot \left(\pi \cdot \color{blue}{\sqrt{u1}}\right)\right) \]
        8. Step-by-step derivation
          1. lift-*.f32N/A

            \[\leadsto 2 \cdot \color{blue}{\left(u2 \cdot \left(\pi \cdot \sqrt{u1}\right)\right)} \]
          2. count-2-revN/A

            \[\leadsto u2 \cdot \left(\pi \cdot \sqrt{u1}\right) + \color{blue}{u2 \cdot \left(\pi \cdot \sqrt{u1}\right)} \]
          3. lift-*.f32N/A

            \[\leadsto u2 \cdot \left(\pi \cdot \sqrt{u1}\right) + u2 \cdot \color{blue}{\left(\pi \cdot \sqrt{u1}\right)} \]
          4. lift-*.f32N/A

            \[\leadsto u2 \cdot \left(\pi \cdot \sqrt{u1}\right) + \color{blue}{u2} \cdot \left(\pi \cdot \sqrt{u1}\right) \]
          5. distribute-rgt-outN/A

            \[\leadsto \left(\pi \cdot \sqrt{u1}\right) \cdot \color{blue}{\left(u2 + u2\right)} \]
          6. flip-+N/A

            \[\leadsto \left(\pi \cdot \sqrt{u1}\right) \cdot \frac{u2 \cdot u2 - u2 \cdot u2}{\color{blue}{u2 - u2}} \]
          7. +-inversesN/A

            \[\leadsto \left(\pi \cdot \sqrt{u1}\right) \cdot \frac{0}{\color{blue}{u2} - u2} \]
          8. metadata-evalN/A

            \[\leadsto \left(\pi \cdot \sqrt{u1}\right) \cdot \frac{1 - 1}{\color{blue}{u2} - u2} \]
          9. metadata-evalN/A

            \[\leadsto \left(\pi \cdot \sqrt{u1}\right) \cdot \frac{1 \cdot 1 - 1}{u2 - u2} \]
          10. metadata-evalN/A

            \[\leadsto \left(\pi \cdot \sqrt{u1}\right) \cdot \frac{1 \cdot 1 - 1 \cdot 1}{u2 - u2} \]
          11. +-inversesN/A

            \[\leadsto \left(\pi \cdot \sqrt{u1}\right) \cdot \frac{1 \cdot 1 - 1 \cdot 1}{0} \]
          12. metadata-evalN/A

            \[\leadsto \left(\pi \cdot \sqrt{u1}\right) \cdot \frac{1 \cdot 1 - 1 \cdot 1}{1 - \color{blue}{1}} \]
          13. flip-+N/A

            \[\leadsto \left(\pi \cdot \sqrt{u1}\right) \cdot \left(1 + \color{blue}{1}\right) \]
          14. metadata-evalN/A

            \[\leadsto \left(\pi \cdot \sqrt{u1}\right) \cdot 2 \]
        9. Applied rewrites16.0%

          \[\leadsto \left(\sqrt{u1} \cdot \pi\right) \cdot \color{blue}{2} \]
        10. Add Preprocessing

        Reproduce

        ?
        herbie shell --seed 2025142 
        (FPCore (cosTheta_i u1 u2)
          :name "Beckmann Sample, near normal, slope_y"
          :precision binary32
          :pre (and (and (and (> cosTheta_i 0.9999) (<= cosTheta_i 1.0)) (and (<= 2.328306437e-10 u1) (<= u1 1.0))) (and (<= 2.328306437e-10 u2) (<= u2 1.0)))
          (* (sqrt (- (log (- 1.0 u1)))) (sin (* (* 2.0 PI) u2))))