Beckmann Sample, near normal, slope_x

Percentage Accurate: 57.3% → 99.2%
Time: 3.7s
Alternatives: 12
Speedup: 1.0×

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 12 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.3% 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(\left(0.25 - u2\right) \cdot \left(\pi + \pi\right)\right) \end{array} \]
(FPCore (cosTheta_i u1 u2)
 :precision binary32
 (* (sqrt (- (log1p (- u1)))) (sin (* (- 0.25 u2) (+ PI PI)))))
float code(float cosTheta_i, float u1, float u2) {
	return sqrtf(-log1pf(-u1)) * sinf(((0.25f - u2) * (((float) M_PI) + ((float) M_PI))));
}
function code(cosTheta_i, u1, u2)
	return Float32(sqrt(Float32(-log1p(Float32(-u1)))) * sin(Float32(Float32(Float32(0.25) - u2) * Float32(Float32(pi) + Float32(pi)))))
end
\begin{array}{l}

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

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

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

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

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

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

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

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

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

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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. distribute-rgt-neg-inN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1}{4} + \color{blue}{\left(\mathsf{neg}\left(u2\right)\right)}\right) \cdot \left(\pi + \pi\right)\right) \]
    7. sub-flip-reverseN/A

      \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(\frac{1}{4} - u2\right)} \cdot \left(\pi + \pi\right)\right) \]
    8. lower--.f3299.2

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Alternative 3: 97.7% accurate, 0.8× speedup?

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

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

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


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

    1. Initial program 57.3%

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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. distribute-rgt-neg-inN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1}{4} + \color{blue}{\left(\mathsf{neg}\left(u2\right)\right)}\right) \cdot \left(\pi + \pi\right)\right) \]
      7. sub-flip-reverseN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(\frac{1}{4} - u2\right)} \cdot \left(\pi + \pi\right)\right) \]
      8. lower--.f3299.2

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

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

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

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

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

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

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

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

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

    1. Initial program 57.3%

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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. distribute-rgt-neg-inN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{u1 \cdot \left(u1 \cdot \frac{1}{2}\right) + u1} \cdot \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + \frac{1}{4}\right)\right) \]
      8. associate-*r*N/A

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

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

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

        \[\leadsto \sqrt{\mathsf{fma}\left(u1 \cdot u1, \color{blue}{\frac{1}{2}}, u1\right)} \cdot \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + \frac{1}{4}\right)\right) \]
      12. lower-unsound-*.f3288.5

        \[\leadsto \sqrt{\mathsf{fma}\left(u1 \cdot u1, 0.5, u1\right)} \cdot \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + 0.25\right)\right) \]
    10. Applied rewrites88.5%

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

Alternative 4: 97.6% accurate, 0.8× speedup?

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

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

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


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

    1. Initial program 57.3%

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

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

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

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

    1. Initial program 57.3%

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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. distribute-rgt-neg-inN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{u1 \cdot \left(u1 \cdot \frac{1}{2}\right) + u1} \cdot \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + \frac{1}{4}\right)\right) \]
      8. associate-*r*N/A

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

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

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

        \[\leadsto \sqrt{\mathsf{fma}\left(u1 \cdot u1, \color{blue}{\frac{1}{2}}, u1\right)} \cdot \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + \frac{1}{4}\right)\right) \]
      12. lower-unsound-*.f3288.5

        \[\leadsto \sqrt{\mathsf{fma}\left(u1 \cdot u1, 0.5, u1\right)} \cdot \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + 0.25\right)\right) \]
    10. Applied rewrites88.5%

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

Alternative 5: 97.5% accurate, 0.9× speedup?

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

\\
\begin{array}{l}
\mathbf{if}\;u1 \leq 0.003700000001117587:\\
\;\;\;\;\sqrt{u1 \cdot \left(1 + 0.5 \cdot u1\right)} \cdot \sin \left(\left(0.25 - u2\right) \cdot \left(\pi + \pi\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\sqrt{-\log \left(1 - u1\right)} \cdot \cos \left(\left(\pi + \pi\right) \cdot u2\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if u1 < 0.0037

    1. Initial program 57.3%

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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. distribute-rgt-neg-inN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1}{4} + \color{blue}{\left(\mathsf{neg}\left(u2\right)\right)}\right) \cdot \left(\pi + \pi\right)\right) \]
      7. sub-flip-reverseN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(\frac{1}{4} - u2\right)} \cdot \left(\pi + \pi\right)\right) \]
      8. lower--.f3299.2

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

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

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

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

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

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

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

    if 0.0037 < u1

    1. Initial program 57.3%

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

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

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

Alternative 6: 97.4% 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.003700000001117587:\\ \;\;\;\;\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.003700000001117587)
     (* (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.003700000001117587f) {
		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.003700000001117587))
		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.003700000001117587:\\
\;\;\;\;\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.0037

    1. Initial program 57.3%

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

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

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

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

    1. Initial program 57.3%

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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. distribute-rgt-neg-inN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + 0.25\right)\right) \]
      8. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \mathsf{Rewrite=>}\left(lift-sin.f32, \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + \frac{1}{4}\right)\right)\right) \]
      9. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \sin \mathsf{Rewrite=>}\left(lift-*.f32, \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + \frac{1}{4}\right)\right)\right) \]
      10. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \sin \left(\left(\pi + \pi\right) \cdot \mathsf{Rewrite=>}\left(lift-+.f32, \left(\left(-u2\right) + \frac{1}{4}\right)\right)\right) \]
      11. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \sin \mathsf{Rewrite=>}\left(distribute-rgt-in, \left(\left(-u2\right) \cdot \left(\pi + \pi\right) + \frac{1}{4} \cdot \left(\pi + \pi\right)\right)\right) \]
    10. Applied rewrites88.3%

      \[\leadsto \color{blue}{\sqrt{\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.7% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;u2 \leq 0.00014000000373926014:\\ \;\;\;\;\sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(0.5 \cdot \pi\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.00014000000373926014)
   (* (sqrt (- (log1p (- u1)))) (sin (* 0.5 PI)))
   (* (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.00014000000373926014f) {
		tmp = sqrtf(-log1pf(-u1)) * sinf((0.5f * ((float) M_PI)));
	} 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.00014000000373926014))
		tmp = Float32(sqrt(Float32(-log1p(Float32(-u1)))) * sin(Float32(Float32(0.5) * Float32(pi))));
	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.00014000000373926014:\\
\;\;\;\;\sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(0.5 \cdot \pi\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 < 1.40000004e-4

    1. Initial program 57.3%

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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. distribute-rgt-neg-inN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\frac{1}{2} \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \]
      2. lower-PI.f3280.2

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(0.5 \cdot \pi\right) \]
    8. Applied rewrites80.2%

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

    if 1.40000004e-4 < u2

    1. Initial program 57.3%

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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. distribute-rgt-neg-inN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + 0.25\right)\right) \]
      8. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \mathsf{Rewrite=>}\left(lift-sin.f32, \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + \frac{1}{4}\right)\right)\right) \]
      9. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \sin \mathsf{Rewrite=>}\left(lift-*.f32, \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + \frac{1}{4}\right)\right)\right) \]
      10. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \sin \left(\left(\pi + \pi\right) \cdot \mathsf{Rewrite=>}\left(lift-+.f32, \left(\left(-u2\right) + \frac{1}{4}\right)\right)\right) \]
      11. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \sin \mathsf{Rewrite=>}\left(distribute-rgt-in, \left(\left(-u2\right) \cdot \left(\pi + \pi\right) + \frac{1}{4} \cdot \left(\pi + \pi\right)\right)\right) \]
    10. Applied rewrites88.3%

      \[\leadsto \color{blue}{\sqrt{\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 8: 94.0% accurate, 0.5× speedup?

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

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

\mathbf{else}:\\
\;\;\;\;t\_0\\


\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.109999999

    1. Initial program 57.3%

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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. distribute-rgt-neg-inN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{\mathsf{fma}\left(0.5, u1, 1\right) \cdot u1} \cdot \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + 0.25\right)\right) \]
      8. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \mathsf{Rewrite=>}\left(lift-sin.f32, \sin \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + \frac{1}{4}\right)\right)\right) \]
      9. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \sin \mathsf{Rewrite=>}\left(lift-*.f32, \left(\left(\pi + \pi\right) \cdot \left(\left(-u2\right) + \frac{1}{4}\right)\right)\right) \]
      10. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \sin \left(\left(\pi + \pi\right) \cdot \mathsf{Rewrite=>}\left(lift-+.f32, \left(\left(-u2\right) + \frac{1}{4}\right)\right)\right) \]
      11. lower-fma.f32N/A

        \[\leadsto \sqrt{\mathsf{fma}\left(\frac{1}{2}, u1, 1\right) \cdot u1} \cdot \sin \mathsf{Rewrite=>}\left(distribute-rgt-in, \left(\left(-u2\right) \cdot \left(\pi + \pi\right) + \frac{1}{4} \cdot \left(\pi + \pi\right)\right)\right) \]
    10. Applied rewrites88.3%

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

    if 0.109999999 < (*.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.3%

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

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

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

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

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

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

      \[\leadsto \color{blue}{\sqrt{-\log \left(1 - u1\right)}} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 9: 86.7% accurate, 0.5× speedup?

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

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

\mathbf{else}:\\
\;\;\;\;t\_0\\


\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.0132

    1. Initial program 57.3%

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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{-\mathsf{log1p}\left(-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. distribute-rgt-neg-inN/A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\left(\frac{1}{4} + \color{blue}{\left(\mathsf{neg}\left(u2\right)\right)}\right) \cdot \left(\pi + \pi\right)\right) \]
      7. sub-flip-reverseN/A

        \[\leadsto \sqrt{-\mathsf{log1p}\left(-u1\right)} \cdot \sin \left(\color{blue}{\left(\frac{1}{4} - u2\right)} \cdot \left(\pi + \pi\right)\right) \]
      8. lower--.f3299.2

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

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

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

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

      if 0.0132 < (*.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.3%

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

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

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

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

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

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

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

    Alternative 10: 86.6% accurate, 0.5× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} t_0 := \sqrt{-\log \left(1 - u1\right)}\\ t_1 := \cos \left(\left(2 \cdot \pi\right) \cdot u2\right)\\ \mathbf{if}\;t\_0 \cdot t\_1 \leq 0.013199999928474426:\\ \;\;\;\;\sqrt{u1} \cdot t\_1\\ \mathbf{else}:\\ \;\;\;\;t\_0\\ \end{array} \end{array} \]
    (FPCore (cosTheta_i u1 u2)
     :precision binary32
     (let* ((t_0 (sqrt (- (log (- 1.0 u1))))) (t_1 (cos (* (* 2.0 PI) u2))))
       (if (<= (* t_0 t_1) 0.013199999928474426) (* (sqrt u1) t_1) t_0)))
    float code(float cosTheta_i, float u1, float u2) {
    	float t_0 = sqrtf(-logf((1.0f - u1)));
    	float t_1 = cosf(((2.0f * ((float) M_PI)) * u2));
    	float tmp;
    	if ((t_0 * t_1) <= 0.013199999928474426f) {
    		tmp = sqrtf(u1) * t_1;
    	} else {
    		tmp = t_0;
    	}
    	return tmp;
    }
    
    function code(cosTheta_i, u1, u2)
    	t_0 = sqrt(Float32(-log(Float32(Float32(1.0) - u1))))
    	t_1 = cos(Float32(Float32(Float32(2.0) * Float32(pi)) * u2))
    	tmp = Float32(0.0)
    	if (Float32(t_0 * t_1) <= Float32(0.013199999928474426))
    		tmp = Float32(sqrt(u1) * t_1);
    	else
    		tmp = t_0;
    	end
    	return tmp
    end
    
    function tmp_2 = code(cosTheta_i, u1, u2)
    	t_0 = sqrt(-log((single(1.0) - u1)));
    	t_1 = cos(((single(2.0) * single(pi)) * u2));
    	tmp = single(0.0);
    	if ((t_0 * t_1) <= single(0.013199999928474426))
    		tmp = sqrt(u1) * t_1;
    	else
    		tmp = t_0;
    	end
    	tmp_2 = tmp;
    end
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    t_0 := \sqrt{-\log \left(1 - u1\right)}\\
    t_1 := \cos \left(\left(2 \cdot \pi\right) \cdot u2\right)\\
    \mathbf{if}\;t\_0 \cdot t\_1 \leq 0.013199999928474426:\\
    \;\;\;\;\sqrt{u1} \cdot t\_1\\
    
    \mathbf{else}:\\
    \;\;\;\;t\_0\\
    
    
    \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.0132

      1. Initial program 57.3%

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

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

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

        if 0.0132 < (*.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.3%

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

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

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

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

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

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

          \[\leadsto \color{blue}{\sqrt{-\log \left(1 - u1\right)}} \]
      4. Recombined 2 regimes into one program.
      5. Add Preprocessing

      Alternative 11: 49.3% 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.3%

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

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

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

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

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

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

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

      Alternative 12: 6.6% accurate, 5.5× speedup?

      \[\begin{array}{l} \\ \sqrt{-\log 1} \end{array} \]
      (FPCore (cosTheta_i u1 u2) :precision binary32 (sqrt (- (log 1.0))))
      float code(float cosTheta_i, float u1, float u2) {
      	return sqrtf(-logf(1.0f));
      }
      
      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))
      end function
      
      function code(cosTheta_i, u1, u2)
      	return sqrt(Float32(-log(Float32(1.0))))
      end
      
      function tmp = code(cosTheta_i, u1, u2)
      	tmp = sqrt(-log(single(1.0)));
      end
      
      \begin{array}{l}
      
      \\
      \sqrt{-\log 1}
      \end{array}
      
      Derivation
      1. Initial program 57.3%

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

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

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

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

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

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

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

        \[\leadsto \sqrt{-\log 1} \]
      6. Step-by-step derivation
        1. Applied rewrites6.6%

          \[\leadsto \sqrt{-\log 1} \]
        2. Add Preprocessing

        Reproduce

        ?
        herbie shell --seed 2025162 
        (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))))