Beckmann Distribution sample, tan2theta, alphax != alphay, u1 <= 0.5

Percentage Accurate: 61.3% → 90.3%
Time: 12.2s
Alternatives: 8
Speedup: 3.5×

Specification

?
\[\left(\left(\left(\left(0.0001 \leq alphax \land alphax \leq 1\right) \land \left(0.0001 \leq alphay \land alphay \leq 1\right)\right) \land \left(2.328306437 \cdot 10^{-10} \leq u0 \land u0 \leq 1\right)\right) \land \left(0 \leq cos2phi \land cos2phi \leq 1\right)\right) \land 0 \leq sin2phi\]
\[\begin{array}{l} \\ \frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \end{array} \]
(FPCore (alphax alphay u0 cos2phi sin2phi)
 :precision binary32
 (/
  (- (log (- 1.0 u0)))
  (+ (/ cos2phi (* alphax alphax)) (/ sin2phi (* alphay alphay)))))
float code(float alphax, float alphay, float u0, float cos2phi, float sin2phi) {
	return -logf((1.0f - u0)) / ((cos2phi / (alphax * alphax)) + (sin2phi / (alphay * alphay)));
}
real(4) function code(alphax, alphay, u0, cos2phi, sin2phi)
    real(4), intent (in) :: alphax
    real(4), intent (in) :: alphay
    real(4), intent (in) :: u0
    real(4), intent (in) :: cos2phi
    real(4), intent (in) :: sin2phi
    code = -log((1.0e0 - u0)) / ((cos2phi / (alphax * alphax)) + (sin2phi / (alphay * alphay)))
end function
function code(alphax, alphay, u0, cos2phi, sin2phi)
	return Float32(Float32(-log(Float32(Float32(1.0) - u0))) / Float32(Float32(cos2phi / Float32(alphax * alphax)) + Float32(sin2phi / Float32(alphay * alphay))))
end
function tmp = code(alphax, alphay, u0, cos2phi, sin2phi)
	tmp = -log((single(1.0) - u0)) / ((cos2phi / (alphax * alphax)) + (sin2phi / (alphay * alphay)));
end
\begin{array}{l}

\\
\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
\end{array}

Sampling outcomes in binary32 precision:

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 8 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: 61.3% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \end{array} \]
(FPCore (alphax alphay u0 cos2phi sin2phi)
 :precision binary32
 (/
  (- (log (- 1.0 u0)))
  (+ (/ cos2phi (* alphax alphax)) (/ sin2phi (* alphay alphay)))))
float code(float alphax, float alphay, float u0, float cos2phi, float sin2phi) {
	return -logf((1.0f - u0)) / ((cos2phi / (alphax * alphax)) + (sin2phi / (alphay * alphay)));
}
real(4) function code(alphax, alphay, u0, cos2phi, sin2phi)
    real(4), intent (in) :: alphax
    real(4), intent (in) :: alphay
    real(4), intent (in) :: u0
    real(4), intent (in) :: cos2phi
    real(4), intent (in) :: sin2phi
    code = -log((1.0e0 - u0)) / ((cos2phi / (alphax * alphax)) + (sin2phi / (alphay * alphay)))
end function
function code(alphax, alphay, u0, cos2phi, sin2phi)
	return Float32(Float32(-log(Float32(Float32(1.0) - u0))) / Float32(Float32(cos2phi / Float32(alphax * alphax)) + Float32(sin2phi / Float32(alphay * alphay))))
end
function tmp = code(alphax, alphay, u0, cos2phi, sin2phi)
	tmp = -log((single(1.0) - u0)) / ((cos2phi / (alphax * alphax)) + (sin2phi / (alphay * alphay)));
end
\begin{array}{l}

\\
\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
\end{array}

Alternative 1: 90.3% accurate, 0.9× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;1 - u0 \leq 0.9998840093612671:\\ \;\;\;\;\frac{\log \left(1 - u0\right)}{cos2phi \cdot \frac{-1}{alphax \cdot alphax} - \frac{sin2phi}{alphay \cdot alphay}}\\ \mathbf{else}:\\ \;\;\;\;\frac{u0}{\frac{cos2phi}{alphax \cdot alphax} - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}}\\ \end{array} \end{array} \]
(FPCore (alphax alphay u0 cos2phi sin2phi)
 :precision binary32
 (if (<= (- 1.0 u0) 0.9998840093612671)
   (/
    (log (- 1.0 u0))
    (- (* cos2phi (/ -1.0 (* alphax alphax))) (/ sin2phi (* alphay alphay))))
   (/
    u0
    (- (/ cos2phi (* alphax alphax)) (/ -1.0 (* (/ alphay sin2phi) alphay))))))
float code(float alphax, float alphay, float u0, float cos2phi, float sin2phi) {
	float tmp;
	if ((1.0f - u0) <= 0.9998840093612671f) {
		tmp = logf((1.0f - u0)) / ((cos2phi * (-1.0f / (alphax * alphax))) - (sin2phi / (alphay * alphay)));
	} else {
		tmp = u0 / ((cos2phi / (alphax * alphax)) - (-1.0f / ((alphay / sin2phi) * alphay)));
	}
	return tmp;
}
real(4) function code(alphax, alphay, u0, cos2phi, sin2phi)
    real(4), intent (in) :: alphax
    real(4), intent (in) :: alphay
    real(4), intent (in) :: u0
    real(4), intent (in) :: cos2phi
    real(4), intent (in) :: sin2phi
    real(4) :: tmp
    if ((1.0e0 - u0) <= 0.9998840093612671e0) then
        tmp = log((1.0e0 - u0)) / ((cos2phi * ((-1.0e0) / (alphax * alphax))) - (sin2phi / (alphay * alphay)))
    else
        tmp = u0 / ((cos2phi / (alphax * alphax)) - ((-1.0e0) / ((alphay / sin2phi) * alphay)))
    end if
    code = tmp
end function
function code(alphax, alphay, u0, cos2phi, sin2phi)
	tmp = Float32(0.0)
	if (Float32(Float32(1.0) - u0) <= Float32(0.9998840093612671))
		tmp = Float32(log(Float32(Float32(1.0) - u0)) / Float32(Float32(cos2phi * Float32(Float32(-1.0) / Float32(alphax * alphax))) - Float32(sin2phi / Float32(alphay * alphay))));
	else
		tmp = Float32(u0 / Float32(Float32(cos2phi / Float32(alphax * alphax)) - Float32(Float32(-1.0) / Float32(Float32(alphay / sin2phi) * alphay))));
	end
	return tmp
end
function tmp_2 = code(alphax, alphay, u0, cos2phi, sin2phi)
	tmp = single(0.0);
	if ((single(1.0) - u0) <= single(0.9998840093612671))
		tmp = log((single(1.0) - u0)) / ((cos2phi * (single(-1.0) / (alphax * alphax))) - (sin2phi / (alphay * alphay)));
	else
		tmp = u0 / ((cos2phi / (alphax * alphax)) - (single(-1.0) / ((alphay / sin2phi) * alphay)));
	end
	tmp_2 = tmp;
end
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;1 - u0 \leq 0.9998840093612671:\\
\;\;\;\;\frac{\log \left(1 - u0\right)}{cos2phi \cdot \frac{-1}{alphax \cdot alphax} - \frac{sin2phi}{alphay \cdot alphay}}\\

\mathbf{else}:\\
\;\;\;\;\frac{u0}{\frac{cos2phi}{alphax \cdot alphax} - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}}\\


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

    1. Initial program 87.1%

      \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-/.f32N/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{cos2phi}{alphax \cdot alphax}} + \frac{sin2phi}{alphay \cdot alphay}} \]
      2. clear-numN/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{\frac{alphax \cdot alphax}{cos2phi}}} + \frac{sin2phi}{alphay \cdot alphay}} \]
      3. lower-/.f32N/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{\frac{alphax \cdot alphax}{cos2phi}}} + \frac{sin2phi}{alphay \cdot alphay}} \]
      4. lower-/.f3287.0

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{1}{\color{blue}{\frac{alphax \cdot alphax}{cos2phi}}} + \frac{sin2phi}{alphay \cdot alphay}} \]
    4. Applied rewrites87.0%

      \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{\frac{alphax \cdot alphax}{cos2phi}}} + \frac{sin2phi}{alphay \cdot alphay}} \]
    5. Step-by-step derivation
      1. lift-/.f32N/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{\frac{alphax \cdot alphax}{cos2phi}}} + \frac{sin2phi}{alphay \cdot alphay}} \]
      2. lift-/.f32N/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{1}{\color{blue}{\frac{alphax \cdot alphax}{cos2phi}}} + \frac{sin2phi}{alphay \cdot alphay}} \]
      3. frac-2negN/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{1}{\color{blue}{\frac{\mathsf{neg}\left(alphax \cdot alphax\right)}{\mathsf{neg}\left(cos2phi\right)}}} + \frac{sin2phi}{alphay \cdot alphay}} \]
      4. associate-/r/N/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{\mathsf{neg}\left(alphax \cdot alphax\right)} \cdot \left(\mathsf{neg}\left(cos2phi\right)\right)} + \frac{sin2phi}{alphay \cdot alphay}} \]
      5. lower-*.f32N/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{\mathsf{neg}\left(alphax \cdot alphax\right)} \cdot \left(\mathsf{neg}\left(cos2phi\right)\right)} + \frac{sin2phi}{alphay \cdot alphay}} \]
      6. lower-/.f32N/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{\mathsf{neg}\left(alphax \cdot alphax\right)}} \cdot \left(\mathsf{neg}\left(cos2phi\right)\right) + \frac{sin2phi}{alphay \cdot alphay}} \]
      7. lift-*.f32N/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{1}{\mathsf{neg}\left(\color{blue}{alphax \cdot alphax}\right)} \cdot \left(\mathsf{neg}\left(cos2phi\right)\right) + \frac{sin2phi}{alphay \cdot alphay}} \]
      8. distribute-lft-neg-inN/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{1}{\color{blue}{\left(\mathsf{neg}\left(alphax\right)\right) \cdot alphax}} \cdot \left(\mathsf{neg}\left(cos2phi\right)\right) + \frac{sin2phi}{alphay \cdot alphay}} \]
      9. lower-*.f32N/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{1}{\color{blue}{\left(\mathsf{neg}\left(alphax\right)\right) \cdot alphax}} \cdot \left(\mathsf{neg}\left(cos2phi\right)\right) + \frac{sin2phi}{alphay \cdot alphay}} \]
      10. lower-neg.f32N/A

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{1}{\color{blue}{\left(-alphax\right)} \cdot alphax} \cdot \left(\mathsf{neg}\left(cos2phi\right)\right) + \frac{sin2phi}{alphay \cdot alphay}} \]
      11. lower-neg.f3287.1

        \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{1}{\left(-alphax\right) \cdot alphax} \cdot \color{blue}{\left(-cos2phi\right)} + \frac{sin2phi}{alphay \cdot alphay}} \]
    6. Applied rewrites87.1%

      \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{\left(-alphax\right) \cdot alphax} \cdot \left(-cos2phi\right)} + \frac{sin2phi}{alphay \cdot alphay}} \]

    if 0.999884009 < (-.f32 #s(literal 1 binary32) u0)

    1. Initial program 42.9%

      \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
    2. Add Preprocessing
    3. Taylor expanded in u0 around 0

      \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
    4. Step-by-step derivation
      1. lower-/.f32N/A

        \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
      2. +-commutativeN/A

        \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
      3. lower-+.f32N/A

        \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
      4. lower-/.f32N/A

        \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}} + \frac{cos2phi}{{alphax}^{2}}} \]
      5. unpow2N/A

        \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
      6. lower-*.f32N/A

        \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
      7. lower-/.f32N/A

        \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \color{blue}{\frac{cos2phi}{{alphax}^{2}}}} \]
      8. unpow2N/A

        \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
      9. lower-*.f3291.8

        \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
    5. Applied rewrites91.8%

      \[\leadsto \color{blue}{\frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{alphax \cdot alphax}}} \]
    6. Step-by-step derivation
      1. Applied rewrites91.7%

        \[\leadsto \frac{u0}{{alphay}^{-2} \cdot {\left(\frac{1}{sin2phi}\right)}^{-1} + \frac{\color{blue}{cos2phi}}{alphax \cdot alphax}} \]
      2. Step-by-step derivation
        1. Applied rewrites91.9%

          \[\leadsto \frac{u0}{\frac{-1}{\left(-alphay\right) \cdot \frac{alphay}{sin2phi}} + \frac{\color{blue}{cos2phi}}{alphax \cdot alphax}} \]
      3. Recombined 2 regimes into one program.
      4. Final simplification90.0%

        \[\leadsto \begin{array}{l} \mathbf{if}\;1 - u0 \leq 0.9998840093612671:\\ \;\;\;\;\frac{\log \left(1 - u0\right)}{cos2phi \cdot \frac{-1}{alphax \cdot alphax} - \frac{sin2phi}{alphay \cdot alphay}}\\ \mathbf{else}:\\ \;\;\;\;\frac{u0}{\frac{cos2phi}{alphax \cdot alphax} - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}}\\ \end{array} \]
      5. Add Preprocessing

      Alternative 2: 90.3% accurate, 0.9× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{cos2phi}{alphax \cdot alphax}\\ \mathbf{if}\;1 - u0 \leq 0.9998840093612671:\\ \;\;\;\;\frac{-\log \left(1 - u0\right)}{t\_0 + \frac{sin2phi}{alphay \cdot alphay}}\\ \mathbf{else}:\\ \;\;\;\;\frac{u0}{t\_0 - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}}\\ \end{array} \end{array} \]
      (FPCore (alphax alphay u0 cos2phi sin2phi)
       :precision binary32
       (let* ((t_0 (/ cos2phi (* alphax alphax))))
         (if (<= (- 1.0 u0) 0.9998840093612671)
           (/ (- (log (- 1.0 u0))) (+ t_0 (/ sin2phi (* alphay alphay))))
           (/ u0 (- t_0 (/ -1.0 (* (/ alphay sin2phi) alphay)))))))
      float code(float alphax, float alphay, float u0, float cos2phi, float sin2phi) {
      	float t_0 = cos2phi / (alphax * alphax);
      	float tmp;
      	if ((1.0f - u0) <= 0.9998840093612671f) {
      		tmp = -logf((1.0f - u0)) / (t_0 + (sin2phi / (alphay * alphay)));
      	} else {
      		tmp = u0 / (t_0 - (-1.0f / ((alphay / sin2phi) * alphay)));
      	}
      	return tmp;
      }
      
      real(4) function code(alphax, alphay, u0, cos2phi, sin2phi)
          real(4), intent (in) :: alphax
          real(4), intent (in) :: alphay
          real(4), intent (in) :: u0
          real(4), intent (in) :: cos2phi
          real(4), intent (in) :: sin2phi
          real(4) :: t_0
          real(4) :: tmp
          t_0 = cos2phi / (alphax * alphax)
          if ((1.0e0 - u0) <= 0.9998840093612671e0) then
              tmp = -log((1.0e0 - u0)) / (t_0 + (sin2phi / (alphay * alphay)))
          else
              tmp = u0 / (t_0 - ((-1.0e0) / ((alphay / sin2phi) * alphay)))
          end if
          code = tmp
      end function
      
      function code(alphax, alphay, u0, cos2phi, sin2phi)
      	t_0 = Float32(cos2phi / Float32(alphax * alphax))
      	tmp = Float32(0.0)
      	if (Float32(Float32(1.0) - u0) <= Float32(0.9998840093612671))
      		tmp = Float32(Float32(-log(Float32(Float32(1.0) - u0))) / Float32(t_0 + Float32(sin2phi / Float32(alphay * alphay))));
      	else
      		tmp = Float32(u0 / Float32(t_0 - Float32(Float32(-1.0) / Float32(Float32(alphay / sin2phi) * alphay))));
      	end
      	return tmp
      end
      
      function tmp_2 = code(alphax, alphay, u0, cos2phi, sin2phi)
      	t_0 = cos2phi / (alphax * alphax);
      	tmp = single(0.0);
      	if ((single(1.0) - u0) <= single(0.9998840093612671))
      		tmp = -log((single(1.0) - u0)) / (t_0 + (sin2phi / (alphay * alphay)));
      	else
      		tmp = u0 / (t_0 - (single(-1.0) / ((alphay / sin2phi) * alphay)));
      	end
      	tmp_2 = tmp;
      end
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_0 := \frac{cos2phi}{alphax \cdot alphax}\\
      \mathbf{if}\;1 - u0 \leq 0.9998840093612671:\\
      \;\;\;\;\frac{-\log \left(1 - u0\right)}{t\_0 + \frac{sin2phi}{alphay \cdot alphay}}\\
      
      \mathbf{else}:\\
      \;\;\;\;\frac{u0}{t\_0 - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}}\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (-.f32 #s(literal 1 binary32) u0) < 0.999884009

        1. Initial program 87.1%

          \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
        2. Add Preprocessing

        if 0.999884009 < (-.f32 #s(literal 1 binary32) u0)

        1. Initial program 42.9%

          \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
        2. Add Preprocessing
        3. Taylor expanded in u0 around 0

          \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
        4. Step-by-step derivation
          1. lower-/.f32N/A

            \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
          2. +-commutativeN/A

            \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
          3. lower-+.f32N/A

            \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
          4. lower-/.f32N/A

            \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}} + \frac{cos2phi}{{alphax}^{2}}} \]
          5. unpow2N/A

            \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
          6. lower-*.f32N/A

            \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
          7. lower-/.f32N/A

            \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \color{blue}{\frac{cos2phi}{{alphax}^{2}}}} \]
          8. unpow2N/A

            \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
          9. lower-*.f3291.8

            \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
        5. Applied rewrites91.8%

          \[\leadsto \color{blue}{\frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{alphax \cdot alphax}}} \]
        6. Step-by-step derivation
          1. Applied rewrites91.7%

            \[\leadsto \frac{u0}{{alphay}^{-2} \cdot {\left(\frac{1}{sin2phi}\right)}^{-1} + \frac{\color{blue}{cos2phi}}{alphax \cdot alphax}} \]
          2. Step-by-step derivation
            1. Applied rewrites91.9%

              \[\leadsto \frac{u0}{\frac{-1}{\left(-alphay\right) \cdot \frac{alphay}{sin2phi}} + \frac{\color{blue}{cos2phi}}{alphax \cdot alphax}} \]
          3. Recombined 2 regimes into one program.
          4. Final simplification90.0%

            \[\leadsto \begin{array}{l} \mathbf{if}\;1 - u0 \leq 0.9998840093612671:\\ \;\;\;\;\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}\\ \mathbf{else}:\\ \;\;\;\;\frac{u0}{\frac{cos2phi}{alphax \cdot alphax} - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}}\\ \end{array} \]
          5. Add Preprocessing

          Alternative 3: 82.4% accurate, 1.1× speedup?

          \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;1 - u0 \leq 0.9995200037956238:\\ \;\;\;\;\frac{-\log \left(1 - u0\right)}{\frac{sin2phi}{alphay \cdot alphay}}\\ \mathbf{else}:\\ \;\;\;\;\frac{u0}{\frac{cos2phi}{alphax \cdot alphax} - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}}\\ \end{array} \end{array} \]
          (FPCore (alphax alphay u0 cos2phi sin2phi)
           :precision binary32
           (if (<= (- 1.0 u0) 0.9995200037956238)
             (/ (- (log (- 1.0 u0))) (/ sin2phi (* alphay alphay)))
             (/
              u0
              (- (/ cos2phi (* alphax alphax)) (/ -1.0 (* (/ alphay sin2phi) alphay))))))
          float code(float alphax, float alphay, float u0, float cos2phi, float sin2phi) {
          	float tmp;
          	if ((1.0f - u0) <= 0.9995200037956238f) {
          		tmp = -logf((1.0f - u0)) / (sin2phi / (alphay * alphay));
          	} else {
          		tmp = u0 / ((cos2phi / (alphax * alphax)) - (-1.0f / ((alphay / sin2phi) * alphay)));
          	}
          	return tmp;
          }
          
          real(4) function code(alphax, alphay, u0, cos2phi, sin2phi)
              real(4), intent (in) :: alphax
              real(4), intent (in) :: alphay
              real(4), intent (in) :: u0
              real(4), intent (in) :: cos2phi
              real(4), intent (in) :: sin2phi
              real(4) :: tmp
              if ((1.0e0 - u0) <= 0.9995200037956238e0) then
                  tmp = -log((1.0e0 - u0)) / (sin2phi / (alphay * alphay))
              else
                  tmp = u0 / ((cos2phi / (alphax * alphax)) - ((-1.0e0) / ((alphay / sin2phi) * alphay)))
              end if
              code = tmp
          end function
          
          function code(alphax, alphay, u0, cos2phi, sin2phi)
          	tmp = Float32(0.0)
          	if (Float32(Float32(1.0) - u0) <= Float32(0.9995200037956238))
          		tmp = Float32(Float32(-log(Float32(Float32(1.0) - u0))) / Float32(sin2phi / Float32(alphay * alphay)));
          	else
          		tmp = Float32(u0 / Float32(Float32(cos2phi / Float32(alphax * alphax)) - Float32(Float32(-1.0) / Float32(Float32(alphay / sin2phi) * alphay))));
          	end
          	return tmp
          end
          
          function tmp_2 = code(alphax, alphay, u0, cos2phi, sin2phi)
          	tmp = single(0.0);
          	if ((single(1.0) - u0) <= single(0.9995200037956238))
          		tmp = -log((single(1.0) - u0)) / (sin2phi / (alphay * alphay));
          	else
          		tmp = u0 / ((cos2phi / (alphax * alphax)) - (single(-1.0) / ((alphay / sin2phi) * alphay)));
          	end
          	tmp_2 = tmp;
          end
          
          \begin{array}{l}
          
          \\
          \begin{array}{l}
          \mathbf{if}\;1 - u0 \leq 0.9995200037956238:\\
          \;\;\;\;\frac{-\log \left(1 - u0\right)}{\frac{sin2phi}{alphay \cdot alphay}}\\
          
          \mathbf{else}:\\
          \;\;\;\;\frac{u0}{\frac{cos2phi}{alphax \cdot alphax} - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}}\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if (-.f32 #s(literal 1 binary32) u0) < 0.999520004

            1. Initial program 89.3%

              \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-/.f32N/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{cos2phi}{alphax \cdot alphax}} + \frac{sin2phi}{alphay \cdot alphay}} \]
              2. clear-numN/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{\frac{alphax \cdot alphax}{cos2phi}}} + \frac{sin2phi}{alphay \cdot alphay}} \]
              3. inv-powN/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{{\left(\frac{alphax \cdot alphax}{cos2phi}\right)}^{-1}} + \frac{sin2phi}{alphay \cdot alphay}} \]
              4. div-invN/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{{\color{blue}{\left(\left(alphax \cdot alphax\right) \cdot \frac{1}{cos2phi}\right)}}^{-1} + \frac{sin2phi}{alphay \cdot alphay}} \]
              5. unpow-prod-downN/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{{\left(alphax \cdot alphax\right)}^{-1} \cdot {\left(\frac{1}{cos2phi}\right)}^{-1}} + \frac{sin2phi}{alphay \cdot alphay}} \]
              6. inv-powN/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{alphax \cdot alphax}} \cdot {\left(\frac{1}{cos2phi}\right)}^{-1} + \frac{sin2phi}{alphay \cdot alphay}} \]
              7. lower-*.f32N/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{1}{alphax \cdot alphax} \cdot {\left(\frac{1}{cos2phi}\right)}^{-1}} + \frac{sin2phi}{alphay \cdot alphay}} \]
              8. lift-*.f32N/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{1}{\color{blue}{alphax \cdot alphax}} \cdot {\left(\frac{1}{cos2phi}\right)}^{-1} + \frac{sin2phi}{alphay \cdot alphay}} \]
              9. pow2N/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{1}{\color{blue}{{alphax}^{2}}} \cdot {\left(\frac{1}{cos2phi}\right)}^{-1} + \frac{sin2phi}{alphay \cdot alphay}} \]
              10. pow-flipN/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{{alphax}^{\left(\mathsf{neg}\left(2\right)\right)}} \cdot {\left(\frac{1}{cos2phi}\right)}^{-1} + \frac{sin2phi}{alphay \cdot alphay}} \]
              11. lower-pow.f32N/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{{alphax}^{\left(\mathsf{neg}\left(2\right)\right)}} \cdot {\left(\frac{1}{cos2phi}\right)}^{-1} + \frac{sin2phi}{alphay \cdot alphay}} \]
              12. metadata-evalN/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{{alphax}^{\color{blue}{-2}} \cdot {\left(\frac{1}{cos2phi}\right)}^{-1} + \frac{sin2phi}{alphay \cdot alphay}} \]
              13. lower-pow.f32N/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{{alphax}^{-2} \cdot \color{blue}{{\left(\frac{1}{cos2phi}\right)}^{-1}} + \frac{sin2phi}{alphay \cdot alphay}} \]
              14. lower-/.f3289.2

                \[\leadsto \frac{-\log \left(1 - u0\right)}{{alphax}^{-2} \cdot {\color{blue}{\left(\frac{1}{cos2phi}\right)}}^{-1} + \frac{sin2phi}{alphay \cdot alphay}} \]
            4. Applied rewrites89.2%

              \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{{alphax}^{-2} \cdot {\left(\frac{1}{cos2phi}\right)}^{-1}} + \frac{sin2phi}{alphay \cdot alphay}} \]
            5. Taylor expanded in alphax around inf

              \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}}} \]
            6. Step-by-step derivation
              1. lower-/.f32N/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}}} \]
              2. unpow2N/A

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}}} \]
              3. lower-*.f3267.0

                \[\leadsto \frac{-\log \left(1 - u0\right)}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}}} \]
            7. Applied rewrites67.0%

              \[\leadsto \frac{-\log \left(1 - u0\right)}{\color{blue}{\frac{sin2phi}{alphay \cdot alphay}}} \]

            if 0.999520004 < (-.f32 #s(literal 1 binary32) u0)

            1. Initial program 45.6%

              \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
            2. Add Preprocessing
            3. Taylor expanded in u0 around 0

              \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
            4. Step-by-step derivation
              1. lower-/.f32N/A

                \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
              2. +-commutativeN/A

                \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
              3. lower-+.f32N/A

                \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
              4. lower-/.f32N/A

                \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}} + \frac{cos2phi}{{alphax}^{2}}} \]
              5. unpow2N/A

                \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
              6. lower-*.f32N/A

                \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
              7. lower-/.f32N/A

                \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \color{blue}{\frac{cos2phi}{{alphax}^{2}}}} \]
              8. unpow2N/A

                \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
              9. lower-*.f3289.7

                \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
            5. Applied rewrites89.7%

              \[\leadsto \color{blue}{\frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{alphax \cdot alphax}}} \]
            6. Step-by-step derivation
              1. Applied rewrites89.7%

                \[\leadsto \frac{u0}{{alphay}^{-2} \cdot {\left(\frac{1}{sin2phi}\right)}^{-1} + \frac{\color{blue}{cos2phi}}{alphax \cdot alphax}} \]
              2. Step-by-step derivation
                1. Applied rewrites89.9%

                  \[\leadsto \frac{u0}{\frac{-1}{\left(-alphay\right) \cdot \frac{alphay}{sin2phi}} + \frac{\color{blue}{cos2phi}}{alphax \cdot alphax}} \]
              3. Recombined 2 regimes into one program.
              4. Final simplification82.0%

                \[\leadsto \begin{array}{l} \mathbf{if}\;1 - u0 \leq 0.9995200037956238:\\ \;\;\;\;\frac{-\log \left(1 - u0\right)}{\frac{sin2phi}{alphay \cdot alphay}}\\ \mathbf{else}:\\ \;\;\;\;\frac{u0}{\frac{cos2phi}{alphax \cdot alphax} - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}}\\ \end{array} \]
              5. Add Preprocessing

              Alternative 4: 75.4% accurate, 2.6× speedup?

              \[\begin{array}{l} \\ \frac{u0}{\frac{cos2phi}{alphax \cdot alphax} - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}} \end{array} \]
              (FPCore (alphax alphay u0 cos2phi sin2phi)
               :precision binary32
               (/
                u0
                (- (/ cos2phi (* alphax alphax)) (/ -1.0 (* (/ alphay sin2phi) alphay)))))
              float code(float alphax, float alphay, float u0, float cos2phi, float sin2phi) {
              	return u0 / ((cos2phi / (alphax * alphax)) - (-1.0f / ((alphay / sin2phi) * alphay)));
              }
              
              real(4) function code(alphax, alphay, u0, cos2phi, sin2phi)
                  real(4), intent (in) :: alphax
                  real(4), intent (in) :: alphay
                  real(4), intent (in) :: u0
                  real(4), intent (in) :: cos2phi
                  real(4), intent (in) :: sin2phi
                  code = u0 / ((cos2phi / (alphax * alphax)) - ((-1.0e0) / ((alphay / sin2phi) * alphay)))
              end function
              
              function code(alphax, alphay, u0, cos2phi, sin2phi)
              	return Float32(u0 / Float32(Float32(cos2phi / Float32(alphax * alphax)) - Float32(Float32(-1.0) / Float32(Float32(alphay / sin2phi) * alphay))))
              end
              
              function tmp = code(alphax, alphay, u0, cos2phi, sin2phi)
              	tmp = u0 / ((cos2phi / (alphax * alphax)) - (single(-1.0) / ((alphay / sin2phi) * alphay)));
              end
              
              \begin{array}{l}
              
              \\
              \frac{u0}{\frac{cos2phi}{alphax \cdot alphax} - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}}
              \end{array}
              
              Derivation
              1. Initial program 60.7%

                \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
              2. Add Preprocessing
              3. Taylor expanded in u0 around 0

                \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
              4. Step-by-step derivation
                1. lower-/.f32N/A

                  \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                2. +-commutativeN/A

                  \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                3. lower-+.f32N/A

                  \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                4. lower-/.f32N/A

                  \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}} + \frac{cos2phi}{{alphax}^{2}}} \]
                5. unpow2N/A

                  \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                6. lower-*.f32N/A

                  \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                7. lower-/.f32N/A

                  \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \color{blue}{\frac{cos2phi}{{alphax}^{2}}}} \]
                8. unpow2N/A

                  \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                9. lower-*.f3275.1

                  \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
              5. Applied rewrites75.1%

                \[\leadsto \color{blue}{\frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{alphax \cdot alphax}}} \]
              6. Step-by-step derivation
                1. Applied rewrites75.1%

                  \[\leadsto \frac{u0}{{alphay}^{-2} \cdot {\left(\frac{1}{sin2phi}\right)}^{-1} + \frac{\color{blue}{cos2phi}}{alphax \cdot alphax}} \]
                2. Step-by-step derivation
                  1. Applied rewrites75.2%

                    \[\leadsto \frac{u0}{\frac{-1}{\left(-alphay\right) \cdot \frac{alphay}{sin2phi}} + \frac{\color{blue}{cos2phi}}{alphax \cdot alphax}} \]
                  2. Final simplification75.2%

                    \[\leadsto \frac{u0}{\frac{cos2phi}{alphax \cdot alphax} - \frac{-1}{\frac{alphay}{sin2phi} \cdot alphay}} \]
                  3. Add Preprocessing

                  Alternative 5: 75.4% accurate, 2.9× speedup?

                  \[\begin{array}{l} \\ \frac{u0}{\frac{\frac{cos2phi}{alphax}}{alphax} + \frac{sin2phi}{alphay \cdot alphay}} \end{array} \]
                  (FPCore (alphax alphay u0 cos2phi sin2phi)
                   :precision binary32
                   (/ u0 (+ (/ (/ cos2phi alphax) alphax) (/ sin2phi (* alphay alphay)))))
                  float code(float alphax, float alphay, float u0, float cos2phi, float sin2phi) {
                  	return u0 / (((cos2phi / alphax) / alphax) + (sin2phi / (alphay * alphay)));
                  }
                  
                  real(4) function code(alphax, alphay, u0, cos2phi, sin2phi)
                      real(4), intent (in) :: alphax
                      real(4), intent (in) :: alphay
                      real(4), intent (in) :: u0
                      real(4), intent (in) :: cos2phi
                      real(4), intent (in) :: sin2phi
                      code = u0 / (((cos2phi / alphax) / alphax) + (sin2phi / (alphay * alphay)))
                  end function
                  
                  function code(alphax, alphay, u0, cos2phi, sin2phi)
                  	return Float32(u0 / Float32(Float32(Float32(cos2phi / alphax) / alphax) + Float32(sin2phi / Float32(alphay * alphay))))
                  end
                  
                  function tmp = code(alphax, alphay, u0, cos2phi, sin2phi)
                  	tmp = u0 / (((cos2phi / alphax) / alphax) + (sin2phi / (alphay * alphay)));
                  end
                  
                  \begin{array}{l}
                  
                  \\
                  \frac{u0}{\frac{\frac{cos2phi}{alphax}}{alphax} + \frac{sin2phi}{alphay \cdot alphay}}
                  \end{array}
                  
                  Derivation
                  1. Initial program 60.7%

                    \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
                  2. Add Preprocessing
                  3. Taylor expanded in u0 around 0

                    \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                  4. Step-by-step derivation
                    1. lower-/.f32N/A

                      \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                    2. +-commutativeN/A

                      \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                    3. lower-+.f32N/A

                      \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                    4. lower-/.f32N/A

                      \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}} + \frac{cos2phi}{{alphax}^{2}}} \]
                    5. unpow2N/A

                      \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                    6. lower-*.f32N/A

                      \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                    7. lower-/.f32N/A

                      \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \color{blue}{\frac{cos2phi}{{alphax}^{2}}}} \]
                    8. unpow2N/A

                      \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                    9. lower-*.f3275.1

                      \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                  5. Applied rewrites75.1%

                    \[\leadsto \color{blue}{\frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{alphax \cdot alphax}}} \]
                  6. Step-by-step derivation
                    1. Applied rewrites75.1%

                      \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{\frac{cos2phi}{alphax}}{\color{blue}{alphax}}} \]
                    2. Final simplification75.1%

                      \[\leadsto \frac{u0}{\frac{\frac{cos2phi}{alphax}}{alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
                    3. Add Preprocessing

                    Alternative 6: 75.4% accurate, 3.2× speedup?

                    \[\begin{array}{l} \\ \frac{u0}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \end{array} \]
                    (FPCore (alphax alphay u0 cos2phi sin2phi)
                     :precision binary32
                     (/ u0 (+ (/ cos2phi (* alphax alphax)) (/ sin2phi (* alphay alphay)))))
                    float code(float alphax, float alphay, float u0, float cos2phi, float sin2phi) {
                    	return u0 / ((cos2phi / (alphax * alphax)) + (sin2phi / (alphay * alphay)));
                    }
                    
                    real(4) function code(alphax, alphay, u0, cos2phi, sin2phi)
                        real(4), intent (in) :: alphax
                        real(4), intent (in) :: alphay
                        real(4), intent (in) :: u0
                        real(4), intent (in) :: cos2phi
                        real(4), intent (in) :: sin2phi
                        code = u0 / ((cos2phi / (alphax * alphax)) + (sin2phi / (alphay * alphay)))
                    end function
                    
                    function code(alphax, alphay, u0, cos2phi, sin2phi)
                    	return Float32(u0 / Float32(Float32(cos2phi / Float32(alphax * alphax)) + Float32(sin2phi / Float32(alphay * alphay))))
                    end
                    
                    function tmp = code(alphax, alphay, u0, cos2phi, sin2phi)
                    	tmp = u0 / ((cos2phi / (alphax * alphax)) + (sin2phi / (alphay * alphay)));
                    end
                    
                    \begin{array}{l}
                    
                    \\
                    \frac{u0}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
                    \end{array}
                    
                    Derivation
                    1. Initial program 60.7%

                      \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
                    2. Add Preprocessing
                    3. Taylor expanded in u0 around 0

                      \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                    4. Step-by-step derivation
                      1. lower-/.f32N/A

                        \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                      2. +-commutativeN/A

                        \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                      3. lower-+.f32N/A

                        \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                      4. lower-/.f32N/A

                        \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}} + \frac{cos2phi}{{alphax}^{2}}} \]
                      5. unpow2N/A

                        \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                      6. lower-*.f32N/A

                        \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                      7. lower-/.f32N/A

                        \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \color{blue}{\frac{cos2phi}{{alphax}^{2}}}} \]
                      8. unpow2N/A

                        \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                      9. lower-*.f3275.1

                        \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                    5. Applied rewrites75.1%

                      \[\leadsto \color{blue}{\frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{alphax \cdot alphax}}} \]
                    6. Final simplification75.1%

                      \[\leadsto \frac{u0}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
                    7. Add Preprocessing

                    Alternative 7: 66.6% accurate, 3.5× speedup?

                    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{sin2phi}{alphay \cdot alphay} \leq 1.499999973677505 \cdot 10^{-14}:\\ \;\;\;\;\left(\frac{u0}{cos2phi} \cdot alphax\right) \cdot alphax\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(alphay \cdot alphay\right) \cdot u0}{sin2phi}\\ \end{array} \end{array} \]
                    (FPCore (alphax alphay u0 cos2phi sin2phi)
                     :precision binary32
                     (if (<= (/ sin2phi (* alphay alphay)) 1.499999973677505e-14)
                       (* (* (/ u0 cos2phi) alphax) alphax)
                       (/ (* (* alphay alphay) u0) sin2phi)))
                    float code(float alphax, float alphay, float u0, float cos2phi, float sin2phi) {
                    	float tmp;
                    	if ((sin2phi / (alphay * alphay)) <= 1.499999973677505e-14f) {
                    		tmp = ((u0 / cos2phi) * alphax) * alphax;
                    	} else {
                    		tmp = ((alphay * alphay) * u0) / sin2phi;
                    	}
                    	return tmp;
                    }
                    
                    real(4) function code(alphax, alphay, u0, cos2phi, sin2phi)
                        real(4), intent (in) :: alphax
                        real(4), intent (in) :: alphay
                        real(4), intent (in) :: u0
                        real(4), intent (in) :: cos2phi
                        real(4), intent (in) :: sin2phi
                        real(4) :: tmp
                        if ((sin2phi / (alphay * alphay)) <= 1.499999973677505e-14) then
                            tmp = ((u0 / cos2phi) * alphax) * alphax
                        else
                            tmp = ((alphay * alphay) * u0) / sin2phi
                        end if
                        code = tmp
                    end function
                    
                    function code(alphax, alphay, u0, cos2phi, sin2phi)
                    	tmp = Float32(0.0)
                    	if (Float32(sin2phi / Float32(alphay * alphay)) <= Float32(1.499999973677505e-14))
                    		tmp = Float32(Float32(Float32(u0 / cos2phi) * alphax) * alphax);
                    	else
                    		tmp = Float32(Float32(Float32(alphay * alphay) * u0) / sin2phi);
                    	end
                    	return tmp
                    end
                    
                    function tmp_2 = code(alphax, alphay, u0, cos2phi, sin2phi)
                    	tmp = single(0.0);
                    	if ((sin2phi / (alphay * alphay)) <= single(1.499999973677505e-14))
                    		tmp = ((u0 / cos2phi) * alphax) * alphax;
                    	else
                    		tmp = ((alphay * alphay) * u0) / sin2phi;
                    	end
                    	tmp_2 = tmp;
                    end
                    
                    \begin{array}{l}
                    
                    \\
                    \begin{array}{l}
                    \mathbf{if}\;\frac{sin2phi}{alphay \cdot alphay} \leq 1.499999973677505 \cdot 10^{-14}:\\
                    \;\;\;\;\left(\frac{u0}{cos2phi} \cdot alphax\right) \cdot alphax\\
                    
                    \mathbf{else}:\\
                    \;\;\;\;\frac{\left(alphay \cdot alphay\right) \cdot u0}{sin2phi}\\
                    
                    
                    \end{array}
                    \end{array}
                    
                    Derivation
                    1. Split input into 2 regimes
                    2. if (/.f32 sin2phi (*.f32 alphay alphay)) < 1.49999997e-14

                      1. Initial program 61.0%

                        \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
                      2. Add Preprocessing
                      3. Taylor expanded in u0 around 0

                        \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                      4. Step-by-step derivation
                        1. lower-/.f32N/A

                          \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                        2. +-commutativeN/A

                          \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                        3. lower-+.f32N/A

                          \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                        4. lower-/.f32N/A

                          \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}} + \frac{cos2phi}{{alphax}^{2}}} \]
                        5. unpow2N/A

                          \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                        6. lower-*.f32N/A

                          \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                        7. lower-/.f32N/A

                          \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \color{blue}{\frac{cos2phi}{{alphax}^{2}}}} \]
                        8. unpow2N/A

                          \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                        9. lower-*.f3270.4

                          \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                      5. Applied rewrites70.4%

                        \[\leadsto \color{blue}{\frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{alphax \cdot alphax}}} \]
                      6. Taylor expanded in alphax around 0

                        \[\leadsto \frac{{alphax}^{2} \cdot u0}{\color{blue}{cos2phi}} \]
                      7. Step-by-step derivation
                        1. Applied rewrites53.6%

                          \[\leadsto \frac{u0 \cdot \left(alphax \cdot alphax\right)}{\color{blue}{cos2phi}} \]
                        2. Step-by-step derivation
                          1. Applied rewrites53.7%

                            \[\leadsto \left(alphax \cdot alphax\right) \cdot \frac{u0}{\color{blue}{cos2phi}} \]
                          2. Step-by-step derivation
                            1. Applied rewrites53.7%

                              \[\leadsto \color{blue}{\left(\frac{u0}{cos2phi} \cdot alphax\right) \cdot alphax} \]

                            if 1.49999997e-14 < (/.f32 sin2phi (*.f32 alphay alphay))

                            1. Initial program 60.5%

                              \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
                            2. Add Preprocessing
                            3. Taylor expanded in u0 around 0

                              \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                            4. Step-by-step derivation
                              1. lower-/.f32N/A

                                \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                              2. +-commutativeN/A

                                \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                              3. lower-+.f32N/A

                                \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                              4. lower-/.f32N/A

                                \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}} + \frac{cos2phi}{{alphax}^{2}}} \]
                              5. unpow2N/A

                                \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                              6. lower-*.f32N/A

                                \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                              7. lower-/.f32N/A

                                \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \color{blue}{\frac{cos2phi}{{alphax}^{2}}}} \]
                              8. unpow2N/A

                                \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                              9. lower-*.f3276.7

                                \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                            5. Applied rewrites76.7%

                              \[\leadsto \color{blue}{\frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{alphax \cdot alphax}}} \]
                            6. Taylor expanded in alphax around inf

                              \[\leadsto \frac{{alphay}^{2} \cdot u0}{\color{blue}{sin2phi}} \]
                            7. Step-by-step derivation
                              1. Applied rewrites71.7%

                                \[\leadsto \frac{\left(alphay \cdot alphay\right) \cdot u0}{\color{blue}{sin2phi}} \]
                            8. Recombined 2 regimes into one program.
                            9. Add Preprocessing

                            Alternative 8: 23.5% accurate, 6.9× speedup?

                            \[\begin{array}{l} \\ \frac{u0}{cos2phi} \cdot \left(alphax \cdot alphax\right) \end{array} \]
                            (FPCore (alphax alphay u0 cos2phi sin2phi)
                             :precision binary32
                             (* (/ u0 cos2phi) (* alphax alphax)))
                            float code(float alphax, float alphay, float u0, float cos2phi, float sin2phi) {
                            	return (u0 / cos2phi) * (alphax * alphax);
                            }
                            
                            real(4) function code(alphax, alphay, u0, cos2phi, sin2phi)
                                real(4), intent (in) :: alphax
                                real(4), intent (in) :: alphay
                                real(4), intent (in) :: u0
                                real(4), intent (in) :: cos2phi
                                real(4), intent (in) :: sin2phi
                                code = (u0 / cos2phi) * (alphax * alphax)
                            end function
                            
                            function code(alphax, alphay, u0, cos2phi, sin2phi)
                            	return Float32(Float32(u0 / cos2phi) * Float32(alphax * alphax))
                            end
                            
                            function tmp = code(alphax, alphay, u0, cos2phi, sin2phi)
                            	tmp = (u0 / cos2phi) * (alphax * alphax);
                            end
                            
                            \begin{array}{l}
                            
                            \\
                            \frac{u0}{cos2phi} \cdot \left(alphax \cdot alphax\right)
                            \end{array}
                            
                            Derivation
                            1. Initial program 60.7%

                              \[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}} \]
                            2. Add Preprocessing
                            3. Taylor expanded in u0 around 0

                              \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                            4. Step-by-step derivation
                              1. lower-/.f32N/A

                                \[\leadsto \color{blue}{\frac{u0}{\frac{cos2phi}{{alphax}^{2}} + \frac{sin2phi}{{alphay}^{2}}}} \]
                              2. +-commutativeN/A

                                \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                              3. lower-+.f32N/A

                                \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}} + \frac{cos2phi}{{alphax}^{2}}}} \]
                              4. lower-/.f32N/A

                                \[\leadsto \frac{u0}{\color{blue}{\frac{sin2phi}{{alphay}^{2}}} + \frac{cos2phi}{{alphax}^{2}}} \]
                              5. unpow2N/A

                                \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                              6. lower-*.f32N/A

                                \[\leadsto \frac{u0}{\frac{sin2phi}{\color{blue}{alphay \cdot alphay}} + \frac{cos2phi}{{alphax}^{2}}} \]
                              7. lower-/.f32N/A

                                \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \color{blue}{\frac{cos2phi}{{alphax}^{2}}}} \]
                              8. unpow2N/A

                                \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                              9. lower-*.f3275.1

                                \[\leadsto \frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{\color{blue}{alphax \cdot alphax}}} \]
                            5. Applied rewrites75.1%

                              \[\leadsto \color{blue}{\frac{u0}{\frac{sin2phi}{alphay \cdot alphay} + \frac{cos2phi}{alphax \cdot alphax}}} \]
                            6. Taylor expanded in alphax around 0

                              \[\leadsto \frac{{alphax}^{2} \cdot u0}{\color{blue}{cos2phi}} \]
                            7. Step-by-step derivation
                              1. Applied rewrites22.9%

                                \[\leadsto \frac{u0 \cdot \left(alphax \cdot alphax\right)}{\color{blue}{cos2phi}} \]
                              2. Step-by-step derivation
                                1. Applied rewrites22.9%

                                  \[\leadsto \left(alphax \cdot alphax\right) \cdot \frac{u0}{\color{blue}{cos2phi}} \]
                                2. Final simplification22.9%

                                  \[\leadsto \frac{u0}{cos2phi} \cdot \left(alphax \cdot alphax\right) \]
                                3. Add Preprocessing

                                Reproduce

                                ?
                                herbie shell --seed 2024255 
                                (FPCore (alphax alphay u0 cos2phi sin2phi)
                                  :name "Beckmann Distribution sample, tan2theta, alphax != alphay, u1 <= 0.5"
                                  :precision binary32
                                  :pre (and (and (and (and (and (<= 0.0001 alphax) (<= alphax 1.0)) (and (<= 0.0001 alphay) (<= alphay 1.0))) (and (<= 2.328306437e-10 u0) (<= u0 1.0))) (and (<= 0.0 cos2phi) (<= cos2phi 1.0))) (<= 0.0 sin2phi))
                                  (/ (- (log (- 1.0 u0))) (+ (/ cos2phi (* alphax alphax)) (/ sin2phi (* alphay alphay)))))