Beckmann Sample, near normal, slope_x

Percentage Accurate: 57.6% → 99.2%
Time: 4.4s
Alternatives: 13
Speedup: 1.6×

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 \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (* (sqrt (- (log (- 1.0 u1)))) (cos (* (* 2.0 PI) u2))))
float code(float cosTheta_i, float u1, float u2) {
	return sqrtf(-logf((1.0f - u1))) * cosf(((2.0f * ((float) M_PI)) * u2));
}
function code(cosTheta_i, u1, u2)
	return Float32(sqrt(Float32(-log(Float32(Float32(1.0) - u1)))) * cos(Float32(Float32(Float32(2.0) * Float32(pi)) * u2)))
end
function tmp = code(cosTheta_i, u1, u2)
	tmp = sqrt(-log((single(1.0) - u1))) * cos(((single(2.0) * single(pi)) * u2));
end
\begin{array}{l}

\\
\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 13 alternatives:

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

Initial Program: 57.6% accurate, 1.0× speedup?

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

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

Alternative 1: 99.2% accurate, 0.9× speedup?

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

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

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

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

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

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

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

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

      \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(\mathsf{neg}\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right) \]
    7. associate-*l*N/A

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

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

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

      \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(\color{blue}{-2}, \pi \cdot u2, \frac{\mathsf{PI}\left(\right)}{2}\right)\right) \]
    11. *-commutativeN/A

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

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

      \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\color{blue}{\pi}}{2}\right)\right) \]
    14. lower-/.f3257.6

      \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \color{blue}{\frac{\pi}{2}}\right)\right) \]
  3. Applied rewrites57.6%

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

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

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    3. flip--N/A

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

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

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

      \[\leadsto \sqrt{-\log \left(\frac{\color{blue}{1 - u1 \cdot u1}}{1 + u1}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    7. +-commutativeN/A

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

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

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

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

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

      \[\leadsto \sqrt{-\log \left(\frac{1 \cdot 1 - u1 \cdot u1}{\color{blue}{u1 + 1}}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    13. +-commutativeN/A

      \[\leadsto \sqrt{-\log \left(\frac{1 \cdot 1 - u1 \cdot u1}{\color{blue}{1 + u1}}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    14. flip--N/A

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    15. *-rgt-identityN/A

      \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    16. fp-cancel-sub-sign-invN/A

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

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

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

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
  5. Applied rewrites99.1%

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

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

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

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

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

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

Alternative 2: 99.1% accurate, 0.9× speedup?

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

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

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

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

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

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

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

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

      \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(\mathsf{neg}\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right) \]
    7. associate-*l*N/A

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

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

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

      \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(\color{blue}{-2}, \pi \cdot u2, \frac{\mathsf{PI}\left(\right)}{2}\right)\right) \]
    11. *-commutativeN/A

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

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

      \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\color{blue}{\pi}}{2}\right)\right) \]
    14. lower-/.f3257.6

      \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \color{blue}{\frac{\pi}{2}}\right)\right) \]
  3. Applied rewrites57.6%

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

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

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    3. flip--N/A

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

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

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

      \[\leadsto \sqrt{-\log \left(\frac{\color{blue}{1 - u1 \cdot u1}}{1 + u1}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    7. +-commutativeN/A

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

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

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

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

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

      \[\leadsto \sqrt{-\log \left(\frac{1 \cdot 1 - u1 \cdot u1}{\color{blue}{u1 + 1}}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    13. +-commutativeN/A

      \[\leadsto \sqrt{-\log \left(\frac{1 \cdot 1 - u1 \cdot u1}{\color{blue}{1 + u1}}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    14. flip--N/A

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    15. *-rgt-identityN/A

      \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    16. fp-cancel-sub-sign-invN/A

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

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

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

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
  5. Applied rewrites99.1%

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

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

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{-u1}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
  7. Applied rewrites99.1%

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

Alternative 3: 99.1% accurate, 1.0× speedup?

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

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

    \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
    2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    15. *-rgt-identityN/A

      \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    16. fp-cancel-sub-sign-invN/A

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

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

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    19. lower-neg.f3299.1

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
  5. Applied rewrites99.1%

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

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    2. *-rgt-identity99.1

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

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

Alternative 4: 97.3% accurate, 0.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) \leq 0.006500000134110451:\\ \;\;\;\;\sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\mathsf{fma}\left(\left(\left(\pi \cdot \pi\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \left(u2 \cdot u2\right), 0.6666666666666666, \left(\pi \cdot \pi\right) \cdot -2\right), u2 \cdot u2, 1\right)\\ \end{array} \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (if (<=
      (* (sqrt (- (log (- 1.0 u1)))) (cos (* (* 2.0 PI) u2)))
      0.006500000134110451)
   (* (sqrt (* (fma 0.5 u1 1.0) u1)) (cos (* (+ PI PI) u2)))
   (*
    (sqrt (- (log1p (* (- u1) 1.0))))
    (fma
     (fma
      (* (* (* PI PI) (* PI PI)) (* u2 u2))
      0.6666666666666666
      (* (* PI PI) -2.0))
     (* u2 u2)
     1.0))))
float code(float cosTheta_i, float u1, float u2) {
	float tmp;
	if ((sqrtf(-logf((1.0f - u1))) * cosf(((2.0f * ((float) M_PI)) * u2))) <= 0.006500000134110451f) {
		tmp = sqrtf((fmaf(0.5f, u1, 1.0f) * u1)) * cosf(((((float) M_PI) + ((float) M_PI)) * u2));
	} else {
		tmp = sqrtf(-log1pf((-u1 * 1.0f))) * fmaf(fmaf((((((float) M_PI) * ((float) M_PI)) * (((float) M_PI) * ((float) M_PI))) * (u2 * u2)), 0.6666666666666666f, ((((float) M_PI) * ((float) M_PI)) * -2.0f)), (u2 * u2), 1.0f);
	}
	return tmp;
}
function code(cosTheta_i, u1, u2)
	tmp = Float32(0.0)
	if (Float32(sqrt(Float32(-log(Float32(Float32(1.0) - u1)))) * cos(Float32(Float32(Float32(2.0) * Float32(pi)) * u2))) <= Float32(0.006500000134110451))
		tmp = Float32(sqrt(Float32(fma(Float32(0.5), u1, Float32(1.0)) * u1)) * cos(Float32(Float32(Float32(pi) + Float32(pi)) * u2)));
	else
		tmp = Float32(sqrt(Float32(-log1p(Float32(Float32(-u1) * Float32(1.0))))) * fma(fma(Float32(Float32(Float32(Float32(pi) * Float32(pi)) * Float32(Float32(pi) * Float32(pi))) * Float32(u2 * u2)), Float32(0.6666666666666666), Float32(Float32(Float32(pi) * Float32(pi)) * Float32(-2.0))), Float32(u2 * u2), Float32(1.0)));
	end
	return tmp
end
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right) \leq 0.006500000134110451:\\
\;\;\;\;\sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right)\\

\mathbf{else}:\\
\;\;\;\;\sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\mathsf{fma}\left(\left(\left(\pi \cdot \pi\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \left(u2 \cdot u2\right), 0.6666666666666666, \left(\pi \cdot \pi\right) \cdot -2\right), u2 \cdot u2, 1\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (*.f32 (sqrt.f32 (neg.f32 (log.f32 (-.f32 #s(literal 1 binary32) u1)))) (cos.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u2))) < 0.00650000013

    1. Initial program 57.6%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
      2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      15. *-rgt-identityN/A

        \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      16. fp-cancel-sub-sign-invN/A

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      19. lower-neg.f3299.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    5. Applied rewrites99.1%

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

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

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

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

        \[\leadsto \sqrt{\left(\frac{1}{2} \cdot u1 + 1\right) \cdot u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      4. lower-fma.f3288.2

        \[\leadsto \sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    8. Applied rewrites88.2%

      \[\leadsto \sqrt{\color{blue}{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]

    if 0.00650000013 < (*.f32 (sqrt.f32 (neg.f32 (log.f32 (-.f32 #s(literal 1 binary32) u1)))) (cos.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u2)))

    1. Initial program 57.6%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
      2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      15. *-rgt-identityN/A

        \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      16. fp-cancel-sub-sign-invN/A

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      19. lower-neg.f3299.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    5. Applied rewrites99.1%

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(-2 \cdot {\mathsf{PI}\left(\right)}^{2} + \frac{2}{3} \cdot \left({u2}^{2} \cdot {\mathsf{PI}\left(\right)}^{4}\right), \color{blue}{{u2}^{2}}, 1\right) \]
    8. Applied rewrites91.7%

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\left(\left(\pi \cdot \pi\right) \cdot \left(\pi \cdot \pi\right)\right) \cdot \left(u2 \cdot u2\right), 0.6666666666666666, \left(\pi \cdot \pi\right) \cdot -2\right), u2 \cdot u2, 1\right)} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 5: 97.1% accurate, 0.8× speedup?

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

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

\mathbf{else}:\\
\;\;\;\;\sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot t\_1\\


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

    1. Initial program 57.6%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
      2. count-2-revN/A

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

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

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

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

    1. Initial program 57.6%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
      2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      15. *-rgt-identityN/A

        \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      16. fp-cancel-sub-sign-invN/A

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      19. lower-neg.f3299.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    5. Applied rewrites99.1%

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

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

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

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

        \[\leadsto \sqrt{\left(\frac{1}{2} \cdot u1 + 1\right) \cdot u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      4. lower-fma.f3288.2

        \[\leadsto \sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    8. Applied rewrites88.2%

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

Alternative 6: 96.8% accurate, 1.0× speedup?

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

\\
\begin{array}{l}
\mathbf{if}\;u2 \leq 0.007000000216066837:\\
\;\;\;\;\sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \pi, 1\right)\\

\mathbf{else}:\\
\;\;\;\;\sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right)\\


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

    1. Initial program 57.6%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
      2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      15. *-rgt-identityN/A

        \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      16. fp-cancel-sub-sign-invN/A

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      19. lower-neg.f3299.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    5. Applied rewrites99.1%

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \left(-2 \cdot \left({u2}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + \color{blue}{1}\right) \]
      2. associate-*r*N/A

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(-2 \cdot {u2}^{2}, \color{blue}{{\mathsf{PI}\left(\right)}^{2}}, 1\right) \]
      4. *-commutativeN/A

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left({u2}^{2} \cdot -2, {\color{blue}{\mathsf{PI}\left(\right)}}^{2}, 1\right) \]
      6. unpow2N/A

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
      8. unpow2N/A

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \mathsf{PI}\left(\right), 1\right) \]
      11. lift-PI.f3288.5

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

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

    if 0.00700000022 < u2

    1. Initial program 57.6%

      \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
      2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      15. *-rgt-identityN/A

        \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      16. fp-cancel-sub-sign-invN/A

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      19. lower-neg.f3299.1

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    5. Applied rewrites99.1%

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

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

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

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

        \[\leadsto \sqrt{\left(\frac{1}{2} \cdot u1 + 1\right) \cdot u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      4. lower-fma.f3288.2

        \[\leadsto \sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
    8. Applied rewrites88.2%

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

Alternative 7: 94.6% accurate, 0.6× speedup?

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

\\
\begin{array}{l}
\mathbf{if}\;\cos \left(\left(2 \cdot \pi\right) \cdot u2\right) \leq 0.9900000095367432:\\
\;\;\;\;\sqrt{u1} \cdot \sin \left(\mathsf{fma}\left(u2 \cdot -2, \pi, \frac{\pi}{2}\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \pi, 1\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (cos.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u2)) < 0.99000001

    1. Initial program 57.6%

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

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

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

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

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

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

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(\mathsf{neg}\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right) \]
      7. associate-*l*N/A

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

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

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

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(\color{blue}{-2}, \pi \cdot u2, \frac{\mathsf{PI}\left(\right)}{2}\right)\right) \]
      11. *-commutativeN/A

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

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

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\color{blue}{\pi}}{2}\right)\right) \]
      14. lower-/.f3257.6

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \color{blue}{\frac{\pi}{2}}\right)\right) \]
    3. Applied rewrites57.6%

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

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

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
      3. flip--N/A

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

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

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

        \[\leadsto \sqrt{-\log \left(\frac{\color{blue}{1 - u1 \cdot u1}}{1 + u1}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
      7. +-commutativeN/A

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

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

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

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

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

        \[\leadsto \sqrt{-\log \left(\frac{1 \cdot 1 - u1 \cdot u1}{\color{blue}{u1 + 1}}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
      13. +-commutativeN/A

        \[\leadsto \sqrt{-\log \left(\frac{1 \cdot 1 - u1 \cdot u1}{\color{blue}{1 + u1}}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
      14. flip--N/A

        \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
      15. *-rgt-identityN/A

        \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
      16. fp-cancel-sub-sign-invN/A

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
    5. Applied rewrites99.1%

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

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

      \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \sin \color{blue}{\left(\mathsf{fma}\left(u2 \cdot -2, \pi, \frac{\pi}{2}\right)\right)} \]
    8. Taylor expanded in u1 around 0

      \[\leadsto \sqrt{\color{blue}{u1}} \cdot \sin \left(\mathsf{fma}\left(u2 \cdot -2, \pi, \frac{\pi}{2}\right)\right) \]
    9. Step-by-step derivation
      1. Applied rewrites76.7%

        \[\leadsto \sqrt{\color{blue}{u1}} \cdot \sin \left(\mathsf{fma}\left(u2 \cdot -2, \pi, \frac{\pi}{2}\right)\right) \]

      if 0.99000001 < (cos.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u2))

      1. Initial program 57.6%

        \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
        2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        15. *-rgt-identityN/A

          \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        16. fp-cancel-sub-sign-invN/A

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        19. lower-neg.f3299.1

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      5. Applied rewrites99.1%

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \left(-2 \cdot \left({u2}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + \color{blue}{1}\right) \]
        2. associate-*r*N/A

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(-2 \cdot {u2}^{2}, \color{blue}{{\mathsf{PI}\left(\right)}^{2}}, 1\right) \]
        4. *-commutativeN/A

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left({u2}^{2} \cdot -2, {\color{blue}{\mathsf{PI}\left(\right)}}^{2}, 1\right) \]
        6. unpow2N/A

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        8. unpow2N/A

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \mathsf{PI}\left(\right), 1\right) \]
        11. lift-PI.f3288.5

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

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

    Alternative 8: 94.6% accurate, 0.6× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\cos \left(\left(2 \cdot \pi\right) \cdot u2\right) \leq 0.9900000095367432:\\ \;\;\;\;\sqrt{u1} \cdot \sin \left(\mathsf{fma}\left(\pi \cdot u2, -2, 0.5 \cdot \pi\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \pi, 1\right)\\ \end{array} \end{array} \]
    (FPCore (cosTheta_i u1 u2)
     :precision binary32
     (if (<= (cos (* (* 2.0 PI) u2)) 0.9900000095367432)
       (* (sqrt u1) (sin (fma (* PI u2) -2.0 (* 0.5 PI))))
       (*
        (sqrt (- (log1p (* (- u1) 1.0))))
        (fma (* (* u2 u2) -2.0) (* PI PI) 1.0))))
    float code(float cosTheta_i, float u1, float u2) {
    	float tmp;
    	if (cosf(((2.0f * ((float) M_PI)) * u2)) <= 0.9900000095367432f) {
    		tmp = sqrtf(u1) * sinf(fmaf((((float) M_PI) * u2), -2.0f, (0.5f * ((float) M_PI))));
    	} else {
    		tmp = sqrtf(-log1pf((-u1 * 1.0f))) * fmaf(((u2 * u2) * -2.0f), (((float) M_PI) * ((float) M_PI)), 1.0f);
    	}
    	return tmp;
    }
    
    function code(cosTheta_i, u1, u2)
    	tmp = Float32(0.0)
    	if (cos(Float32(Float32(Float32(2.0) * Float32(pi)) * u2)) <= Float32(0.9900000095367432))
    		tmp = Float32(sqrt(u1) * sin(fma(Float32(Float32(pi) * u2), Float32(-2.0), Float32(Float32(0.5) * Float32(pi)))));
    	else
    		tmp = Float32(sqrt(Float32(-log1p(Float32(Float32(-u1) * Float32(1.0))))) * fma(Float32(Float32(u2 * u2) * Float32(-2.0)), Float32(Float32(pi) * Float32(pi)), Float32(1.0)));
    	end
    	return tmp
    end
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;\cos \left(\left(2 \cdot \pi\right) \cdot u2\right) \leq 0.9900000095367432:\\
    \;\;\;\;\sqrt{u1} \cdot \sin \left(\mathsf{fma}\left(\pi \cdot u2, -2, 0.5 \cdot \pi\right)\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \pi, 1\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (cos.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u2)) < 0.99000001

      1. Initial program 57.6%

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

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

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

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(\mathsf{neg}\left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right)\right) + \frac{\mathsf{PI}\left(\right)}{2}\right) \]
        7. associate-*l*N/A

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(\color{blue}{-2}, \pi \cdot u2, \frac{\mathsf{PI}\left(\right)}{2}\right)\right) \]
        11. *-commutativeN/A

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\color{blue}{\pi}}{2}\right)\right) \]
        14. lower-/.f3257.6

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \color{blue}{\frac{\pi}{2}}\right)\right) \]
      3. Applied rewrites57.6%

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

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

          \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
        3. flip--N/A

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

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

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

          \[\leadsto \sqrt{-\log \left(\frac{\color{blue}{1 - u1 \cdot u1}}{1 + u1}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
        7. +-commutativeN/A

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

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

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

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

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

          \[\leadsto \sqrt{-\log \left(\frac{1 \cdot 1 - u1 \cdot u1}{\color{blue}{u1 + 1}}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
        13. +-commutativeN/A

          \[\leadsto \sqrt{-\log \left(\frac{1 \cdot 1 - u1 \cdot u1}{\color{blue}{1 + u1}}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
        14. flip--N/A

          \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
        15. *-rgt-identityN/A

          \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
        16. fp-cancel-sub-sign-invN/A

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

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \sin \left(\mathsf{fma}\left(-2, u2 \cdot \pi, \frac{\pi}{2}\right)\right) \]
      5. Applied rewrites99.1%

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \sin \color{blue}{\left(\mathsf{fma}\left(u2 \cdot -2, \pi, \frac{\pi}{2}\right)\right)} \]
      8. Taylor expanded in u1 around 0

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

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

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

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

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

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

          \[\leadsto \sqrt{u1} \cdot \sin \left(\mathsf{fma}\left(u2 \cdot \mathsf{PI}\left(\right), -2, \frac{1}{2} \cdot \mathsf{PI}\left(\right)\right)\right) \]
        7. *-commutativeN/A

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

          \[\leadsto \sqrt{u1} \cdot \sin \left(\mathsf{fma}\left(\mathsf{PI}\left(\right) \cdot u2, -2, \frac{1}{2} \cdot \mathsf{PI}\left(\right)\right)\right) \]
        9. lift-PI.f32N/A

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

          \[\leadsto \sqrt{u1} \cdot \sin \left(\mathsf{fma}\left(\pi \cdot u2, -2, \frac{1}{2} \cdot \mathsf{PI}\left(\right)\right)\right) \]
        11. lift-PI.f3276.6

          \[\leadsto \sqrt{u1} \cdot \sin \left(\mathsf{fma}\left(\pi \cdot u2, -2, 0.5 \cdot \pi\right)\right) \]
      10. Applied rewrites76.6%

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

      if 0.99000001 < (cos.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u2))

      1. Initial program 57.6%

        \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
        2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        15. *-rgt-identityN/A

          \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        16. fp-cancel-sub-sign-invN/A

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        19. lower-neg.f3299.1

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      5. Applied rewrites99.1%

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \left(-2 \cdot \left({u2}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + \color{blue}{1}\right) \]
        2. associate-*r*N/A

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(-2 \cdot {u2}^{2}, \color{blue}{{\mathsf{PI}\left(\right)}^{2}}, 1\right) \]
        4. *-commutativeN/A

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left({u2}^{2} \cdot -2, {\color{blue}{\mathsf{PI}\left(\right)}}^{2}, 1\right) \]
        6. unpow2N/A

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        8. unpow2N/A

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \mathsf{PI}\left(\right), 1\right) \]
        11. lift-PI.f3288.5

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \color{blue}{\mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \pi, 1\right)} \]
    3. Recombined 2 regimes into one program.
    4. Add Preprocessing

    Alternative 9: 94.5% accurate, 0.6× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\cos \left(\left(2 \cdot \pi\right) \cdot u2\right) \leq 0.9900000095367432:\\ \;\;\;\;\sqrt{u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \pi, 1\right)\\ \end{array} \end{array} \]
    (FPCore (cosTheta_i u1 u2)
     :precision binary32
     (if (<= (cos (* (* 2.0 PI) u2)) 0.9900000095367432)
       (* (sqrt u1) (cos (* (+ PI PI) u2)))
       (*
        (sqrt (- (log1p (* (- u1) 1.0))))
        (fma (* (* u2 u2) -2.0) (* PI PI) 1.0))))
    float code(float cosTheta_i, float u1, float u2) {
    	float tmp;
    	if (cosf(((2.0f * ((float) M_PI)) * u2)) <= 0.9900000095367432f) {
    		tmp = sqrtf(u1) * cosf(((((float) M_PI) + ((float) M_PI)) * u2));
    	} else {
    		tmp = sqrtf(-log1pf((-u1 * 1.0f))) * fmaf(((u2 * u2) * -2.0f), (((float) M_PI) * ((float) M_PI)), 1.0f);
    	}
    	return tmp;
    }
    
    function code(cosTheta_i, u1, u2)
    	tmp = Float32(0.0)
    	if (cos(Float32(Float32(Float32(2.0) * Float32(pi)) * u2)) <= Float32(0.9900000095367432))
    		tmp = Float32(sqrt(u1) * cos(Float32(Float32(Float32(pi) + Float32(pi)) * u2)));
    	else
    		tmp = Float32(sqrt(Float32(-log1p(Float32(Float32(-u1) * Float32(1.0))))) * fma(Float32(Float32(u2 * u2) * Float32(-2.0)), Float32(Float32(pi) * Float32(pi)), Float32(1.0)));
    	end
    	return tmp
    end
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;\cos \left(\left(2 \cdot \pi\right) \cdot u2\right) \leq 0.9900000095367432:\\
    \;\;\;\;\sqrt{u1} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;\sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \pi, 1\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (cos.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u2)) < 0.99000001

      1. Initial program 57.6%

        \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
        2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        15. *-rgt-identityN/A

          \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        16. fp-cancel-sub-sign-invN/A

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        19. lower-neg.f3299.1

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      5. Applied rewrites99.1%

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

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

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

        if 0.99000001 < (cos.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u2))

        1. Initial program 57.6%

          \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
          2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

            \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
          15. *-rgt-identityN/A

            \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
          16. fp-cancel-sub-sign-invN/A

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

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

            \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
          19. lower-neg.f3299.1

            \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        5. Applied rewrites99.1%

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

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

            \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \left(-2 \cdot \left({u2}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + \color{blue}{1}\right) \]
          2. associate-*r*N/A

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

            \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(-2 \cdot {u2}^{2}, \color{blue}{{\mathsf{PI}\left(\right)}^{2}}, 1\right) \]
          4. *-commutativeN/A

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

            \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left({u2}^{2} \cdot -2, {\color{blue}{\mathsf{PI}\left(\right)}}^{2}, 1\right) \]
          6. unpow2N/A

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

            \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
          8. unpow2N/A

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

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

            \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \mathsf{PI}\left(\right), 1\right) \]
          11. lift-PI.f3288.5

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \color{blue}{\mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \pi, 1\right)} \]
      8. Recombined 2 regimes into one program.
      9. Add Preprocessing

      Alternative 10: 88.5% accurate, 1.6× speedup?

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

        \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
        2. count-2-revN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

          \[\leadsto \sqrt{-\log \color{blue}{\left(1 - u1\right)}} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        15. *-rgt-identityN/A

          \[\leadsto \sqrt{-\log \left(1 - \color{blue}{u1 \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        16. fp-cancel-sub-sign-invN/A

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(\mathsf{neg}\left(u1\right)\right) \cdot 1}\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
        19. lower-neg.f3299.1

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\color{blue}{\left(-u1\right)} \cdot 1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right) \]
      5. Applied rewrites99.1%

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \left(-2 \cdot \left({u2}^{2} \cdot {\mathsf{PI}\left(\right)}^{2}\right) + \color{blue}{1}\right) \]
        2. associate-*r*N/A

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(-2 \cdot {u2}^{2}, \color{blue}{{\mathsf{PI}\left(\right)}^{2}}, 1\right) \]
        4. *-commutativeN/A

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left({u2}^{2} \cdot -2, {\color{blue}{\mathsf{PI}\left(\right)}}^{2}, 1\right) \]
        6. unpow2N/A

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, {\mathsf{PI}\left(\right)}^{2}, 1\right) \]
        8. unpow2N/A

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

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

          \[\leadsto \sqrt{-\mathsf{log1p}\left(\left(-u1\right) \cdot 1\right)} \cdot \mathsf{fma}\left(\left(u2 \cdot u2\right) \cdot -2, \pi \cdot \mathsf{PI}\left(\right), 1\right) \]
        11. lift-PI.f3288.5

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

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

      Alternative 11: 49.6% accurate, 1.7× speedup?

      \[\begin{array}{l} \\ \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(0.6666666666666666 \cdot \left(u2 \cdot u2\right) - 2, u2 \cdot u2, 1\right) \end{array} \]
      (FPCore (cosTheta_i u1 u2)
       :precision binary32
       (*
        (sqrt (- (log (- 1.0 u1))))
        (fma (- (* 0.6666666666666666 (* u2 u2)) 2.0) (* u2 u2) 1.0)))
      float code(float cosTheta_i, float u1, float u2) {
      	return sqrtf(-logf((1.0f - u1))) * fmaf(((0.6666666666666666f * (u2 * u2)) - 2.0f), (u2 * u2), 1.0f);
      }
      
      function code(cosTheta_i, u1, u2)
      	return Float32(sqrt(Float32(-log(Float32(Float32(1.0) - u1)))) * fma(Float32(Float32(Float32(0.6666666666666666) * Float32(u2 * u2)) - Float32(2.0)), Float32(u2 * u2), Float32(1.0)))
      end
      
      \begin{array}{l}
      
      \\
      \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(0.6666666666666666 \cdot \left(u2 \cdot u2\right) - 2, u2 \cdot u2, 1\right)
      \end{array}
      
      Derivation
      1. Initial program 57.6%

        \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
        2. count-2-revN/A

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(\left(\pi + \pi\right) \cdot u2\right)} \]
        2. *-commutativeN/A

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right)} \cdot \pi - \pi \cdot \pi}{\pi - \pi}\right) \]
        6. lift-PI.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)} - \pi \cdot \pi}{\pi - \pi}\right) \]
        7. lift-PI.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right) - \color{blue}{\mathsf{PI}\left(\right)} \cdot \pi}{\pi - \pi}\right) \]
        8. lift-PI.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right) - \mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}}{\pi - \pi}\right) \]
        9. +-inversesN/A

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

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

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

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \color{blue}{\left(1 + 1\right)}\right) \]
        16. metadata-evalN/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \color{blue}{2}\right) \]
        17. lower-*.f3249.4

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(u2 \cdot 2\right)} \]
        2. *-commutativeN/A

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(u2 + u2\right)} \]
        4. lower-+.f3249.4

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(u2 + u2\right)} \]
      7. Applied rewrites49.4%

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

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \color{blue}{\left(1 + {u2}^{2} \cdot \left(\frac{2}{3} \cdot {u2}^{2} - 2\right)\right)} \]
      9. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \left({u2}^{2} \cdot \left(\frac{2}{3} \cdot {u2}^{2} - 2\right) + \color{blue}{1}\right) \]
        2. *-commutativeN/A

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(\frac{2}{3} \cdot {u2}^{2} - 2, {u2}^{2}, 1\right) \]
        6. unpow2N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(\frac{2}{3} \cdot \left(u2 \cdot u2\right) - 2, {u2}^{2}, 1\right) \]
        7. lower-*.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(\frac{2}{3} \cdot \left(u2 \cdot u2\right) - 2, {u2}^{2}, 1\right) \]
        8. unpow2N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(\frac{2}{3} \cdot \left(u2 \cdot u2\right) - 2, u2 \cdot \color{blue}{u2}, 1\right) \]
        9. lower-*.f3249.4

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(0.6666666666666666 \cdot \left(u2 \cdot u2\right) - 2, u2 \cdot \color{blue}{u2}, 1\right) \]
      10. Applied rewrites49.4%

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \color{blue}{\mathsf{fma}\left(0.6666666666666666 \cdot \left(u2 \cdot u2\right) - 2, u2 \cdot u2, 1\right)} \]
      11. Add Preprocessing

      Alternative 12: 49.4% accurate, 2.3× speedup?

      \[\begin{array}{l} \\ \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(u2 \cdot u2, -2, 1\right) \end{array} \]
      (FPCore (cosTheta_i u1 u2)
       :precision binary32
       (* (sqrt (- (log (- 1.0 u1)))) (fma (* u2 u2) -2.0 1.0)))
      float code(float cosTheta_i, float u1, float u2) {
      	return sqrtf(-logf((1.0f - u1))) * fmaf((u2 * u2), -2.0f, 1.0f);
      }
      
      function code(cosTheta_i, u1, u2)
      	return Float32(sqrt(Float32(-log(Float32(Float32(1.0) - u1)))) * fma(Float32(u2 * u2), Float32(-2.0), Float32(1.0)))
      end
      
      \begin{array}{l}
      
      \\
      \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(u2 \cdot u2, -2, 1\right)
      \end{array}
      
      Derivation
      1. Initial program 57.6%

        \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
        2. count-2-revN/A

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(\left(\pi + \pi\right) \cdot u2\right)} \]
        2. *-commutativeN/A

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right)} \cdot \pi - \pi \cdot \pi}{\pi - \pi}\right) \]
        6. lift-PI.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)} - \pi \cdot \pi}{\pi - \pi}\right) \]
        7. lift-PI.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right) - \color{blue}{\mathsf{PI}\left(\right)} \cdot \pi}{\pi - \pi}\right) \]
        8. lift-PI.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right) - \mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}}{\pi - \pi}\right) \]
        9. +-inversesN/A

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

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

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

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \color{blue}{\left(1 + 1\right)}\right) \]
        16. metadata-evalN/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \color{blue}{2}\right) \]
        17. lower-*.f3249.4

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(u2 \cdot 2\right)} \]
        2. *-commutativeN/A

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(u2 + u2\right)} \]
        4. lower-+.f3249.4

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(u2 + u2\right)} \]
      7. Applied rewrites49.4%

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

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \color{blue}{\left(1 + -2 \cdot {u2}^{2}\right)} \]
      9. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \left(-2 \cdot {u2}^{2} + \color{blue}{1}\right) \]
        2. *-commutativeN/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \left({u2}^{2} \cdot -2 + 1\right) \]
        3. lower-fma.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left({u2}^{2}, \color{blue}{-2}, 1\right) \]
        4. unpow2N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(u2 \cdot u2, -2, 1\right) \]
        5. lower-*.f3249.4

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \mathsf{fma}\left(u2 \cdot u2, -2, 1\right) \]
      10. Applied rewrites49.4%

        \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \color{blue}{\mathsf{fma}\left(u2 \cdot u2, -2, 1\right)} \]
      11. Add Preprocessing

      Alternative 13: 49.4% accurate, 4.4× speedup?

      \[\begin{array}{l} \\ \sqrt{-\log \left(1 - u1\right)} \end{array} \]
      (FPCore (cosTheta_i u1 u2) :precision binary32 (sqrt (- (log (- 1.0 u1)))))
      float code(float cosTheta_i, float u1, float u2) {
      	return sqrtf(-logf((1.0f - u1)));
      }
      
      module fmin_fmax_functions
          implicit none
          private
          public fmax
          public fmin
      
          interface fmax
              module procedure fmax88
              module procedure fmax44
              module procedure fmax84
              module procedure fmax48
          end interface
          interface fmin
              module procedure fmin88
              module procedure fmin44
              module procedure fmin84
              module procedure fmin48
          end interface
      contains
          real(8) function fmax88(x, y) result (res)
              real(8), intent (in) :: x
              real(8), intent (in) :: y
              res = merge(y, merge(x, max(x, y), y /= y), x /= x)
          end function
          real(4) function fmax44(x, y) result (res)
              real(4), intent (in) :: x
              real(4), intent (in) :: y
              res = merge(y, merge(x, max(x, y), y /= y), x /= x)
          end function
          real(8) function fmax84(x, y) result(res)
              real(8), intent (in) :: x
              real(4), intent (in) :: y
              res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
          end function
          real(8) function fmax48(x, y) result(res)
              real(4), intent (in) :: x
              real(8), intent (in) :: y
              res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
          end function
          real(8) function fmin88(x, y) result (res)
              real(8), intent (in) :: x
              real(8), intent (in) :: y
              res = merge(y, merge(x, min(x, y), y /= y), x /= x)
          end function
          real(4) function fmin44(x, y) result (res)
              real(4), intent (in) :: x
              real(4), intent (in) :: y
              res = merge(y, merge(x, min(x, y), y /= y), x /= x)
          end function
          real(8) function fmin84(x, y) result(res)
              real(8), intent (in) :: x
              real(4), intent (in) :: y
              res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
          end function
          real(8) function fmin48(x, y) result(res)
              real(4), intent (in) :: x
              real(8), intent (in) :: y
              res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
          end function
      end module
      
      real(4) function code(costheta_i, u1, u2)
      use fmin_fmax_functions
          real(4), intent (in) :: costheta_i
          real(4), intent (in) :: u1
          real(4), intent (in) :: u2
          code = sqrt(-log((1.0e0 - u1)))
      end function
      
      function code(cosTheta_i, u1, u2)
      	return sqrt(Float32(-log(Float32(Float32(1.0) - u1))))
      end
      
      function tmp = code(cosTheta_i, u1, u2)
      	tmp = sqrt(-log((single(1.0) - u1)));
      end
      
      \begin{array}{l}
      
      \\
      \sqrt{-\log \left(1 - u1\right)}
      \end{array}
      
      Derivation
      1. Initial program 57.6%

        \[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\color{blue}{\left(2 \cdot \pi\right)} \cdot u2\right) \]
        2. count-2-revN/A

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(\left(\pi + \pi\right) \cdot u2\right)} \]
        2. *-commutativeN/A

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\color{blue}{\mathsf{PI}\left(\right)} \cdot \pi - \pi \cdot \pi}{\pi - \pi}\right) \]
        6. lift-PI.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)} - \pi \cdot \pi}{\pi - \pi}\right) \]
        7. lift-PI.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right) - \color{blue}{\mathsf{PI}\left(\right)} \cdot \pi}{\pi - \pi}\right) \]
        8. lift-PI.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \frac{\mathsf{PI}\left(\right) \cdot \mathsf{PI}\left(\right) - \mathsf{PI}\left(\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}}{\pi - \pi}\right) \]
        9. +-inversesN/A

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

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

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

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

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \color{blue}{\left(1 + 1\right)}\right) \]
        16. metadata-evalN/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(u2 \cdot \color{blue}{2}\right) \]
        17. lower-*.f3249.4

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

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(u2 \cdot 2\right)} \]
        2. *-commutativeN/A

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

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(u2 + u2\right)} \]
        4. lower-+.f3249.4

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \cdot \cos \color{blue}{\left(u2 + u2\right)} \]
      7. Applied rewrites49.4%

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

        \[\leadsto \color{blue}{\sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)}} \]
      9. Step-by-step derivation
        1. lift-log.f32N/A

          \[\leadsto \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)} \]
        2. lift--.f32N/A

          \[\leadsto \sqrt{\mathsf{neg}\left(\log \left(1 - u1\right)\right)} \]
        3. lift-neg.f32N/A

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \]
        4. lift-sqrt.f3249.6

          \[\leadsto \sqrt{-\log \left(1 - u1\right)} \]
      10. Applied rewrites49.6%

        \[\leadsto \color{blue}{\sqrt{-\log \left(1 - u1\right)}} \]
      11. Add Preprocessing

      Reproduce

      ?
      herbie shell --seed 2025140 
      (FPCore (cosTheta_i u1 u2)
        :name "Beckmann Sample, near normal, slope_x"
        :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)))) (cos (* (* 2.0 PI) u2))))