HairBSDF, sample_f, cosTheta

Percentage Accurate: 99.5% → 99.5%
Time: 5.0s
Alternatives: 18
Speedup: 0.8×

Specification

?
\[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
\[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
(FPCore (u v)
  :precision binary32
  :pre (and (and (<= 1e-5 u) (<= u 1.0))
     (and (<= 0.0 v) (<= v 109.746574)))
  (+ 1.0 (* v (log (+ u (* (- 1.0 u) (exp (/ -2.0 v))))))))
float code(float u, float v) {
	return 1.0f + (v * logf((u + ((1.0f - u) * expf((-2.0f / v))))));
}
real(4) function code(u, v)
use fmin_fmax_functions
    real(4), intent (in) :: u
    real(4), intent (in) :: v
    code = 1.0e0 + (v * log((u + ((1.0e0 - u) * exp(((-2.0e0) / v))))))
end function
function code(u, v)
	return Float32(Float32(1.0) + Float32(v * log(Float32(u + Float32(Float32(Float32(1.0) - u) * exp(Float32(Float32(-2.0) / v)))))))
end
function tmp = code(u, v)
	tmp = single(1.0) + (v * log((u + ((single(1.0) - u) * exp((single(-2.0) / v))))));
end
1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right)

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

\[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
\[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
(FPCore (u v)
  :precision binary32
  :pre (and (and (<= 1e-5 u) (<= u 1.0))
     (and (<= 0.0 v) (<= v 109.746574)))
  (+ 1.0 (* v (log (+ u (* (- 1.0 u) (exp (/ -2.0 v))))))))
float code(float u, float v) {
	return 1.0f + (v * logf((u + ((1.0f - u) * expf((-2.0f / v))))));
}
real(4) function code(u, v)
use fmin_fmax_functions
    real(4), intent (in) :: u
    real(4), intent (in) :: v
    code = 1.0e0 + (v * log((u + ((1.0e0 - u) * exp(((-2.0e0) / v))))))
end function
function code(u, v)
	return Float32(Float32(1.0) + Float32(v * log(Float32(u + Float32(Float32(Float32(1.0) - u) * exp(Float32(Float32(-2.0) / v)))))))
end
function tmp = code(u, v)
	tmp = single(1.0) + (v * log((u + ((single(1.0) - u) * exp((single(-2.0) / v))))));
end
1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right)

Alternative 1: 99.5% accurate, 0.8× speedup?

\[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
\[\mathsf{fma}\left(\frac{-1}{-\frac{-1}{\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right)}}, -v, 1\right) \]
(FPCore (u v)
  :precision binary32
  :pre (and (and (<= 1e-5 u) (<= u 1.0))
     (and (<= 0.0 v) (<= v 109.746574)))
  (fma
 (/ -1.0 (- (/ -1.0 (log (fma (exp (/ -2.0 v)) (- 1.0 u) u)))))
 (- v)
 1.0))
float code(float u, float v) {
	return fmaf((-1.0f / -(-1.0f / logf(fmaf(expf((-2.0f / v)), (1.0f - u), u)))), -v, 1.0f);
}
function code(u, v)
	return fma(Float32(Float32(-1.0) / Float32(-Float32(Float32(-1.0) / log(fma(exp(Float32(Float32(-2.0) / v)), Float32(Float32(1.0) - u), u))))), Float32(-v), Float32(1.0))
end
\mathsf{fma}\left(\frac{-1}{-\frac{-1}{\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right)}}, -v, 1\right)
Derivation
  1. Initial program 99.5%

    \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
  2. Step-by-step derivation
    1. Applied rewrites99.4%

      \[\leadsto 1 + \log \left({\left(\frac{1}{\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)}\right)}^{\left(-v\right)}\right) \]
    2. Step-by-step derivation
      1. Applied rewrites99.4%

        \[\leadsto \left(-v\right) \cdot \log \left(\frac{1}{\left|\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right|}\right) - -1 \]
      2. Step-by-step derivation
        1. Applied rewrites99.5%

          \[\leadsto \mathsf{fma}\left(-\log \left(\mathsf{fma}\left(1 - u, e^{\frac{-2}{v}}, u\right)\right), -v, 1\right) \]
        2. Step-by-step derivation
          1. Applied rewrites99.5%

            \[\leadsto \mathsf{fma}\left(\frac{-1}{-\frac{-1}{\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right)}}, -v, 1\right) \]
          2. Add Preprocessing

          Alternative 2: 99.5% accurate, 1.0× speedup?

          \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
          \[\mathsf{fma}\left(-\log \left(\mathsf{fma}\left(1 - u, e^{\frac{-2}{v}}, u\right)\right), -v, 1\right) \]
          (FPCore (u v)
            :precision binary32
            :pre (and (and (<= 1e-5 u) (<= u 1.0))
               (and (<= 0.0 v) (<= v 109.746574)))
            (fma (- (log (fma (- 1.0 u) (exp (/ -2.0 v)) u))) (- v) 1.0))
          float code(float u, float v) {
          	return fmaf(-logf(fmaf((1.0f - u), expf((-2.0f / v)), u)), -v, 1.0f);
          }
          
          function code(u, v)
          	return fma(Float32(-log(fma(Float32(Float32(1.0) - u), exp(Float32(Float32(-2.0) / v)), u))), Float32(-v), Float32(1.0))
          end
          
          \mathsf{fma}\left(-\log \left(\mathsf{fma}\left(1 - u, e^{\frac{-2}{v}}, u\right)\right), -v, 1\right)
          
          Derivation
          1. Initial program 99.5%

            \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
          2. Step-by-step derivation
            1. Applied rewrites99.4%

              \[\leadsto 1 + \log \left({\left(\frac{1}{\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)}\right)}^{\left(-v\right)}\right) \]
            2. Step-by-step derivation
              1. Applied rewrites99.4%

                \[\leadsto \left(-v\right) \cdot \log \left(\frac{1}{\left|\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right|}\right) - -1 \]
              2. Step-by-step derivation
                1. Applied rewrites99.5%

                  \[\leadsto \mathsf{fma}\left(-\log \left(\mathsf{fma}\left(1 - u, e^{\frac{-2}{v}}, u\right)\right), -v, 1\right) \]
                2. Add Preprocessing

                Alternative 3: 99.5% accurate, 1.0× speedup?

                \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                \[\mathsf{fma}\left(\log \left(e^{\frac{-2}{v}} \cdot \left(1 - u\right) + u\right), v, 1\right) \]
                (FPCore (u v)
                  :precision binary32
                  :pre (and (and (<= 1e-5 u) (<= u 1.0))
                     (and (<= 0.0 v) (<= v 109.746574)))
                  (fma (log (+ (* (exp (/ -2.0 v)) (- 1.0 u)) u)) v 1.0))
                float code(float u, float v) {
                	return fmaf(logf(((expf((-2.0f / v)) * (1.0f - u)) + u)), v, 1.0f);
                }
                
                function code(u, v)
                	return fma(log(Float32(Float32(exp(Float32(Float32(-2.0) / v)) * Float32(Float32(1.0) - u)) + u)), v, Float32(1.0))
                end
                
                \mathsf{fma}\left(\log \left(e^{\frac{-2}{v}} \cdot \left(1 - u\right) + u\right), v, 1\right)
                
                Derivation
                1. Initial program 99.5%

                  \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                2. Taylor expanded in u around 0

                  \[\leadsto 1 + v \cdot \log \left(u + e^{\frac{-2}{v}}\right) \]
                3. Step-by-step derivation
                  1. Applied rewrites95.9%

                    \[\leadsto 1 + v \cdot \log \left(u + e^{\frac{-2}{v}}\right) \]
                  2. Step-by-step derivation
                    1. Applied rewrites95.9%

                      \[\leadsto \mathsf{fma}\left(\log \left(e^{\frac{-2}{v}} + u\right), v, 1\right) \]
                    2. Taylor expanded in v around 0

                      \[\leadsto \mathsf{fma}\left(\log \left(e^{\frac{-2}{v}} \cdot \left(1 - u\right) + u\right), v, 1\right) \]
                    3. Step-by-step derivation
                      1. Applied rewrites99.5%

                        \[\leadsto \mathsf{fma}\left(\log \left(e^{\frac{-2}{v}} \cdot \left(1 - u\right) + u\right), v, 1\right) \]
                      2. Add Preprocessing

                      Alternative 4: 95.9% accurate, 1.2× speedup?

                      \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                      \[\mathsf{fma}\left(\log \left(e^{\frac{-2}{v}} + u\right), v, 1\right) \]
                      (FPCore (u v)
                        :precision binary32
                        :pre (and (and (<= 1e-5 u) (<= u 1.0))
                           (and (<= 0.0 v) (<= v 109.746574)))
                        (fma (log (+ (exp (/ -2.0 v)) u)) v 1.0))
                      float code(float u, float v) {
                      	return fmaf(logf((expf((-2.0f / v)) + u)), v, 1.0f);
                      }
                      
                      function code(u, v)
                      	return fma(log(Float32(exp(Float32(Float32(-2.0) / v)) + u)), v, Float32(1.0))
                      end
                      
                      \mathsf{fma}\left(\log \left(e^{\frac{-2}{v}} + u\right), v, 1\right)
                      
                      Derivation
                      1. Initial program 99.5%

                        \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                      2. Taylor expanded in u around 0

                        \[\leadsto 1 + v \cdot \log \left(u + e^{\frac{-2}{v}}\right) \]
                      3. Step-by-step derivation
                        1. Applied rewrites95.9%

                          \[\leadsto 1 + v \cdot \log \left(u + e^{\frac{-2}{v}}\right) \]
                        2. Step-by-step derivation
                          1. Applied rewrites95.9%

                            \[\leadsto \mathsf{fma}\left(\log \left(e^{\frac{-2}{v}} + u\right), v, 1\right) \]
                          2. Add Preprocessing

                          Alternative 5: 94.1% accurate, 1.3× speedup?

                          \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                          \[\log \left(\mathsf{expm1}\left(\frac{-2}{v}\right) \cdot \left(-u\right)\right) \cdot v - -1 \]
                          (FPCore (u v)
                            :precision binary32
                            :pre (and (and (<= 1e-5 u) (<= u 1.0))
                               (and (<= 0.0 v) (<= v 109.746574)))
                            (- (* (log (* (expm1 (/ -2.0 v)) (- u))) v) -1.0))
                          float code(float u, float v) {
                          	return (logf((expm1f((-2.0f / v)) * -u)) * v) - -1.0f;
                          }
                          
                          function code(u, v)
                          	return Float32(Float32(log(Float32(expm1(Float32(Float32(-2.0) / v)) * Float32(-u))) * v) - Float32(-1.0))
                          end
                          
                          \log \left(\mathsf{expm1}\left(\frac{-2}{v}\right) \cdot \left(-u\right)\right) \cdot v - -1
                          
                          Derivation
                          1. Initial program 99.5%

                            \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                          2. Taylor expanded in u around -inf

                            \[\leadsto 1 + v \cdot \log \left(-1 \cdot \left(u \cdot \left(e^{\frac{-2}{v}} - 1\right)\right)\right) \]
                          3. Step-by-step derivation
                            1. Applied rewrites94.1%

                              \[\leadsto 1 + v \cdot \log \left(-1 \cdot \left(u \cdot \mathsf{expm1}\left(\frac{-2}{v}\right)\right)\right) \]
                            2. Step-by-step derivation
                              1. Applied rewrites94.1%

                                \[\leadsto \log \left(\mathsf{expm1}\left(\frac{-2}{v}\right) \cdot \left(-u\right)\right) \cdot v - -1 \]
                              2. Add Preprocessing

                              Alternative 6: 94.1% accurate, 1.3× speedup?

                              \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                              \[\mathsf{fma}\left(\log \left(\mathsf{expm1}\left(\frac{-2}{v}\right) \cdot \left(-u\right)\right), v, 1\right) \]
                              (FPCore (u v)
                                :precision binary32
                                :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                   (and (<= 0.0 v) (<= v 109.746574)))
                                (fma (log (* (expm1 (/ -2.0 v)) (- u))) v 1.0))
                              float code(float u, float v) {
                              	return fmaf(logf((expm1f((-2.0f / v)) * -u)), v, 1.0f);
                              }
                              
                              function code(u, v)
                              	return fma(log(Float32(expm1(Float32(Float32(-2.0) / v)) * Float32(-u))), v, Float32(1.0))
                              end
                              
                              \mathsf{fma}\left(\log \left(\mathsf{expm1}\left(\frac{-2}{v}\right) \cdot \left(-u\right)\right), v, 1\right)
                              
                              Derivation
                              1. Initial program 99.5%

                                \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                              2. Taylor expanded in u around -inf

                                \[\leadsto 1 + v \cdot \log \left(-1 \cdot \left(u \cdot \left(e^{\frac{-2}{v}} - 1\right)\right)\right) \]
                              3. Step-by-step derivation
                                1. Applied rewrites94.1%

                                  \[\leadsto 1 + v \cdot \log \left(-1 \cdot \left(u \cdot \mathsf{expm1}\left(\frac{-2}{v}\right)\right)\right) \]
                                2. Step-by-step derivation
                                  1. Applied rewrites94.1%

                                    \[\leadsto \mathsf{fma}\left(\log \left(\mathsf{expm1}\left(\frac{-2}{v}\right) \cdot \left(-u\right)\right), v, 1\right) \]
                                  2. Add Preprocessing

                                  Alternative 7: 91.2% accurate, 0.6× speedup?

                                  \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                  \[\begin{array}{l} \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{expm1}\left(\frac{2}{v}\right) \cdot v, u, -1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5\\ \end{array} \]
                                  (FPCore (u v)
                                    :precision binary32
                                    :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                       (and (<= 0.0 v) (<= v 109.746574)))
                                    (if (<= (* v (log (+ u (* (- 1.0 u) (exp (/ -2.0 v)))))) -1.0)
                                    (fma (* (expm1 (/ 2.0 v)) v) u -1.0)
                                    (+ (/ 1.0 (* 2.0 (/ 0.5 0.5))) 0.5)))
                                  float code(float u, float v) {
                                  	float tmp;
                                  	if ((v * logf((u + ((1.0f - u) * expf((-2.0f / v)))))) <= -1.0f) {
                                  		tmp = fmaf((expm1f((2.0f / v)) * v), u, -1.0f);
                                  	} else {
                                  		tmp = (1.0f / (2.0f * (0.5f / 0.5f))) + 0.5f;
                                  	}
                                  	return tmp;
                                  }
                                  
                                  function code(u, v)
                                  	tmp = Float32(0.0)
                                  	if (Float32(v * log(Float32(u + Float32(Float32(Float32(1.0) - u) * exp(Float32(Float32(-2.0) / v)))))) <= Float32(-1.0))
                                  		tmp = fma(Float32(expm1(Float32(Float32(2.0) / v)) * v), u, Float32(-1.0));
                                  	else
                                  		tmp = Float32(Float32(Float32(1.0) / Float32(Float32(2.0) * Float32(Float32(0.5) / Float32(0.5)))) + Float32(0.5));
                                  	end
                                  	return tmp
                                  end
                                  
                                  \begin{array}{l}
                                  \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\
                                  \;\;\;\;\mathsf{fma}\left(\mathsf{expm1}\left(\frac{2}{v}\right) \cdot v, u, -1\right)\\
                                  
                                  \mathbf{else}:\\
                                  \;\;\;\;\frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5\\
                                  
                                  
                                  \end{array}
                                  
                                  Derivation
                                  1. Split input into 2 regimes
                                  2. if (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v)))))) < -1

                                    1. Initial program 99.5%

                                      \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                    2. Taylor expanded in u around 0

                                      \[\leadsto \frac{u \cdot \left(v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)\right)}{e^{\frac{-2}{v}}} - 1 \]
                                    3. Step-by-step derivation
                                      1. Applied rewrites10.8%

                                        \[\leadsto \frac{u \cdot \left(v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)\right)}{e^{\frac{-2}{v}}} - 1 \]
                                      2. Step-by-step derivation
                                        1. Applied rewrites10.8%

                                          \[\leadsto \mathsf{fma}\left(v \cdot \left(-1 + e^{\frac{2}{v}}\right), u, -1\right) \]
                                        2. Applied rewrites10.8%

                                          \[\leadsto \mathsf{fma}\left(\mathsf{expm1}\left(\frac{2}{v}\right) \cdot v, u, -1\right) \]

                                        if -1 < (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v))))))

                                        1. Initial program 99.5%

                                          \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                        2. Step-by-step derivation
                                          1. Applied rewrites99.3%

                                            \[\leadsto \mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right) + 0.5 \]
                                          2. Step-by-step derivation
                                            1. pow1N/A

                                              \[\leadsto \frac{1}{{\left({\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{1}\right)}^{-1}} + \frac{1}{2} \]
                                            2. metadata-evalN/A

                                              \[\leadsto \frac{1}{{\left({\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}\right)}^{-1}} + \frac{1}{2} \]
                                            3. pow-negN/A

                                              \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                            4. remove-sound-/N/A

                                              \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                            5. lower-/.f32N/A

                                              \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                            6. remove-sound-powN/A

                                              \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                            7. lower-pow.f3299.3%

                                              \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right)\right)}^{-1}}\right)}^{-1}} + 0.5 \]
                                          3. Applied rewrites99.3%

                                            \[\leadsto \frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right)\right)}^{-1}} + 0.5 \]
                                          4. Step-by-step derivation
                                            1. Applied rewrites99.3%

                                              \[\leadsto \frac{1}{2 \cdot \frac{0.5}{\mathsf{fma}\left(\log \left(\mathsf{fma}\left(1 - u, e^{\frac{-2}{v}}, u\right)\right), v, 0.5\right)}} + 0.5 \]
                                            2. Taylor expanded in v around 0

                                              \[\leadsto \frac{1}{2 \cdot \frac{0.5}{\frac{1}{2}}} + 0.5 \]
                                            3. Step-by-step derivation
                                              1. Applied rewrites86.7%

                                                \[\leadsto \frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5 \]
                                            4. Recombined 2 regimes into one program.
                                            5. Add Preprocessing

                                            Alternative 8: 91.0% accurate, 0.6× speedup?

                                            \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                            \[\begin{array}{l} \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\ \;\;\;\;\mathsf{fma}\left(\left(-\frac{\frac{-1.3333333333333333}{v} - 2}{v}\right) + 2, u, -1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5\\ \end{array} \]
                                            (FPCore (u v)
                                              :precision binary32
                                              :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                 (and (<= 0.0 v) (<= v 109.746574)))
                                              (if (<= (* v (log (+ u (* (- 1.0 u) (exp (/ -2.0 v)))))) -1.0)
                                              (fma (+ (- (/ (- (/ -1.3333333333333333 v) 2.0) v)) 2.0) u -1.0)
                                              (+ (/ 1.0 (* 2.0 (/ 0.5 0.5))) 0.5)))
                                            float code(float u, float v) {
                                            	float tmp;
                                            	if ((v * logf((u + ((1.0f - u) * expf((-2.0f / v)))))) <= -1.0f) {
                                            		tmp = fmaf((-(((-1.3333333333333333f / v) - 2.0f) / v) + 2.0f), u, -1.0f);
                                            	} else {
                                            		tmp = (1.0f / (2.0f * (0.5f / 0.5f))) + 0.5f;
                                            	}
                                            	return tmp;
                                            }
                                            
                                            function code(u, v)
                                            	tmp = Float32(0.0)
                                            	if (Float32(v * log(Float32(u + Float32(Float32(Float32(1.0) - u) * exp(Float32(Float32(-2.0) / v)))))) <= Float32(-1.0))
                                            		tmp = fma(Float32(Float32(-Float32(Float32(Float32(Float32(-1.3333333333333333) / v) - Float32(2.0)) / v)) + Float32(2.0)), u, Float32(-1.0));
                                            	else
                                            		tmp = Float32(Float32(Float32(1.0) / Float32(Float32(2.0) * Float32(Float32(0.5) / Float32(0.5)))) + Float32(0.5));
                                            	end
                                            	return tmp
                                            end
                                            
                                            \begin{array}{l}
                                            \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\
                                            \;\;\;\;\mathsf{fma}\left(\left(-\frac{\frac{-1.3333333333333333}{v} - 2}{v}\right) + 2, u, -1\right)\\
                                            
                                            \mathbf{else}:\\
                                            \;\;\;\;\frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5\\
                                            
                                            
                                            \end{array}
                                            
                                            Derivation
                                            1. Split input into 2 regimes
                                            2. if (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v)))))) < -1

                                              1. Initial program 99.5%

                                                \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                              2. Taylor expanded in u around 0

                                                \[\leadsto u \cdot \left(u \cdot \left(\frac{-1}{2} \cdot \frac{v \cdot {\left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}^{2}}{e^{\frac{-4}{v}}} + \frac{1}{3} \cdot \frac{u \cdot \left(v \cdot {\left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}^{3}\right)}{e^{\frac{-6}{v}}}\right) + \frac{v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}{e^{\frac{-2}{v}}}\right) - 1 \]
                                              3. Applied rewrites6.0%

                                                \[\leadsto u \cdot \mathsf{fma}\left(u, \mathsf{fma}\left(-0.5, \frac{v \cdot {\left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}^{2}}{e^{\frac{-4}{v}}}, 0.3333333333333333 \cdot \frac{u \cdot \left(v \cdot {\left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}^{3}\right)}{e^{\frac{-6}{v}}}\right), \frac{v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}{e^{\frac{-2}{v}}}\right) - 1 \]
                                              4. Taylor expanded in v around -inf

                                                \[\leadsto u \cdot \left(2 + -1 \cdot \frac{\left(-1 \cdot \frac{\frac{4}{3} + u \cdot \left(\frac{8}{3} \cdot u - 4\right)}{v} + 2 \cdot u\right) - 2}{v}\right) - 1 \]
                                              5. Step-by-step derivation
                                                1. Applied rewrites12.8%

                                                  \[\leadsto u \cdot \left(2 + -1 \cdot \frac{\mathsf{fma}\left(-1, \frac{1.3333333333333333 + u \cdot \left(2.6666666666666665 \cdot u - 4\right)}{v}, 2 \cdot u\right) - 2}{v}\right) - 1 \]
                                                2. Taylor expanded in u around 0

                                                  \[\leadsto u \cdot \left(2 + -1 \cdot \frac{\frac{\frac{-4}{3}}{v} - 2}{v}\right) - 1 \]
                                                3. Step-by-step derivation
                                                  1. Applied rewrites12.6%

                                                    \[\leadsto u \cdot \left(2 + -1 \cdot \frac{\frac{-1.3333333333333333}{v} - 2}{v}\right) - 1 \]
                                                  2. Applied rewrites12.6%

                                                    \[\leadsto \mathsf{fma}\left(\left(-\frac{\frac{-1.3333333333333333}{v} - 2}{v}\right) + 2, u, -1\right) \]

                                                  if -1 < (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v))))))

                                                  1. Initial program 99.5%

                                                    \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                  2. Step-by-step derivation
                                                    1. Applied rewrites99.3%

                                                      \[\leadsto \mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right) + 0.5 \]
                                                    2. Step-by-step derivation
                                                      1. pow1N/A

                                                        \[\leadsto \frac{1}{{\left({\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{1}\right)}^{-1}} + \frac{1}{2} \]
                                                      2. metadata-evalN/A

                                                        \[\leadsto \frac{1}{{\left({\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}\right)}^{-1}} + \frac{1}{2} \]
                                                      3. pow-negN/A

                                                        \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                      4. remove-sound-/N/A

                                                        \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                      5. lower-/.f32N/A

                                                        \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                      6. remove-sound-powN/A

                                                        \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                      7. lower-pow.f3299.3%

                                                        \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right)\right)}^{-1}}\right)}^{-1}} + 0.5 \]
                                                    3. Applied rewrites99.3%

                                                      \[\leadsto \frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right)\right)}^{-1}} + 0.5 \]
                                                    4. Step-by-step derivation
                                                      1. Applied rewrites99.3%

                                                        \[\leadsto \frac{1}{2 \cdot \frac{0.5}{\mathsf{fma}\left(\log \left(\mathsf{fma}\left(1 - u, e^{\frac{-2}{v}}, u\right)\right), v, 0.5\right)}} + 0.5 \]
                                                      2. Taylor expanded in v around 0

                                                        \[\leadsto \frac{1}{2 \cdot \frac{0.5}{\frac{1}{2}}} + 0.5 \]
                                                      3. Step-by-step derivation
                                                        1. Applied rewrites86.7%

                                                          \[\leadsto \frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5 \]
                                                      4. Recombined 2 regimes into one program.
                                                      5. Add Preprocessing

                                                      Alternative 9: 90.8% accurate, 0.7× speedup?

                                                      \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                                      \[\begin{array}{l} \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\ \;\;\;\;\mathsf{fma}\left(\frac{2 - \left(u + u\right)}{v} - -2, u, -1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5\\ \end{array} \]
                                                      (FPCore (u v)
                                                        :precision binary32
                                                        :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                           (and (<= 0.0 v) (<= v 109.746574)))
                                                        (if (<= (* v (log (+ u (* (- 1.0 u) (exp (/ -2.0 v)))))) -1.0)
                                                        (fma (- (/ (- 2.0 (+ u u)) v) -2.0) u -1.0)
                                                        (+ (/ 1.0 (* 2.0 (/ 0.5 0.5))) 0.5)))
                                                      float code(float u, float v) {
                                                      	float tmp;
                                                      	if ((v * logf((u + ((1.0f - u) * expf((-2.0f / v)))))) <= -1.0f) {
                                                      		tmp = fmaf((((2.0f - (u + u)) / v) - -2.0f), u, -1.0f);
                                                      	} else {
                                                      		tmp = (1.0f / (2.0f * (0.5f / 0.5f))) + 0.5f;
                                                      	}
                                                      	return tmp;
                                                      }
                                                      
                                                      function code(u, v)
                                                      	tmp = Float32(0.0)
                                                      	if (Float32(v * log(Float32(u + Float32(Float32(Float32(1.0) - u) * exp(Float32(Float32(-2.0) / v)))))) <= Float32(-1.0))
                                                      		tmp = fma(Float32(Float32(Float32(Float32(2.0) - Float32(u + u)) / v) - Float32(-2.0)), u, Float32(-1.0));
                                                      	else
                                                      		tmp = Float32(Float32(Float32(1.0) / Float32(Float32(2.0) * Float32(Float32(0.5) / Float32(0.5)))) + Float32(0.5));
                                                      	end
                                                      	return tmp
                                                      end
                                                      
                                                      \begin{array}{l}
                                                      \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\
                                                      \;\;\;\;\mathsf{fma}\left(\frac{2 - \left(u + u\right)}{v} - -2, u, -1\right)\\
                                                      
                                                      \mathbf{else}:\\
                                                      \;\;\;\;\frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5\\
                                                      
                                                      
                                                      \end{array}
                                                      
                                                      Derivation
                                                      1. Split input into 2 regimes
                                                      2. if (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v)))))) < -1

                                                        1. Initial program 99.5%

                                                          \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                        2. Taylor expanded in u around 0

                                                          \[\leadsto u \cdot \left(\frac{-1}{2} \cdot \frac{u \cdot \left(v \cdot {\left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}^{2}\right)}{e^{\frac{-4}{v}}} + \frac{v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}{e^{\frac{-2}{v}}}\right) - 1 \]
                                                        3. Step-by-step derivation
                                                          1. Applied rewrites5.7%

                                                            \[\leadsto u \cdot \mathsf{fma}\left(-0.5, \frac{u \cdot \left(v \cdot {\left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}^{2}\right)}{e^{\frac{-4}{v}}}, \frac{v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}{e^{\frac{-2}{v}}}\right) - 1 \]
                                                          2. Taylor expanded in v around -inf

                                                            \[\leadsto u \cdot \left(2 + -1 \cdot \frac{2 \cdot u - 2}{v}\right) - 1 \]
                                                          3. Step-by-step derivation
                                                            1. Applied rewrites14.6%

                                                              \[\leadsto u \cdot \left(2 + -1 \cdot \frac{2 \cdot u - 2}{v}\right) - 1 \]
                                                            2. Applied rewrites14.6%

                                                              \[\leadsto \mathsf{fma}\left(\left(-\frac{\mathsf{fma}\left(2, u, -2\right)}{v}\right) - -2, u, -1\right) \]
                                                            3. Applied rewrites14.6%

                                                              \[\leadsto \mathsf{fma}\left(\frac{2 - \left(u + u\right)}{v} - -2, u, -1\right) \]

                                                            if -1 < (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v))))))

                                                            1. Initial program 99.5%

                                                              \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                            2. Step-by-step derivation
                                                              1. Applied rewrites99.3%

                                                                \[\leadsto \mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right) + 0.5 \]
                                                              2. Step-by-step derivation
                                                                1. pow1N/A

                                                                  \[\leadsto \frac{1}{{\left({\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{1}\right)}^{-1}} + \frac{1}{2} \]
                                                                2. metadata-evalN/A

                                                                  \[\leadsto \frac{1}{{\left({\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}\right)}^{-1}} + \frac{1}{2} \]
                                                                3. pow-negN/A

                                                                  \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                4. remove-sound-/N/A

                                                                  \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                5. lower-/.f32N/A

                                                                  \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                6. remove-sound-powN/A

                                                                  \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                7. lower-pow.f3299.3%

                                                                  \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right)\right)}^{-1}}\right)}^{-1}} + 0.5 \]
                                                              3. Applied rewrites99.3%

                                                                \[\leadsto \frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right)\right)}^{-1}} + 0.5 \]
                                                              4. Step-by-step derivation
                                                                1. Applied rewrites99.3%

                                                                  \[\leadsto \frac{1}{2 \cdot \frac{0.5}{\mathsf{fma}\left(\log \left(\mathsf{fma}\left(1 - u, e^{\frac{-2}{v}}, u\right)\right), v, 0.5\right)}} + 0.5 \]
                                                                2. Taylor expanded in v around 0

                                                                  \[\leadsto \frac{1}{2 \cdot \frac{0.5}{\frac{1}{2}}} + 0.5 \]
                                                                3. Step-by-step derivation
                                                                  1. Applied rewrites86.7%

                                                                    \[\leadsto \frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5 \]
                                                                4. Recombined 2 regimes into one program.
                                                                5. Add Preprocessing

                                                                Alternative 10: 90.8% accurate, 0.7× speedup?

                                                                \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                                                \[\begin{array}{l} \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{v} - -2, u, -2\right) - -1\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5\\ \end{array} \]
                                                                (FPCore (u v)
                                                                  :precision binary32
                                                                  :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                                     (and (<= 0.0 v) (<= v 109.746574)))
                                                                  (if (<= (* v (log (+ u (* (- 1.0 u) (exp (/ -2.0 v)))))) -1.0)
                                                                  (- (fma (- (/ 2.0 v) -2.0) u -2.0) -1.0)
                                                                  (+ (/ 1.0 (* 2.0 (/ 0.5 0.5))) 0.5)))
                                                                float code(float u, float v) {
                                                                	float tmp;
                                                                	if ((v * logf((u + ((1.0f - u) * expf((-2.0f / v)))))) <= -1.0f) {
                                                                		tmp = fmaf(((2.0f / v) - -2.0f), u, -2.0f) - -1.0f;
                                                                	} else {
                                                                		tmp = (1.0f / (2.0f * (0.5f / 0.5f))) + 0.5f;
                                                                	}
                                                                	return tmp;
                                                                }
                                                                
                                                                function code(u, v)
                                                                	tmp = Float32(0.0)
                                                                	if (Float32(v * log(Float32(u + Float32(Float32(Float32(1.0) - u) * exp(Float32(Float32(-2.0) / v)))))) <= Float32(-1.0))
                                                                		tmp = Float32(fma(Float32(Float32(Float32(2.0) / v) - Float32(-2.0)), u, Float32(-2.0)) - Float32(-1.0));
                                                                	else
                                                                		tmp = Float32(Float32(Float32(1.0) / Float32(Float32(2.0) * Float32(Float32(0.5) / Float32(0.5)))) + Float32(0.5));
                                                                	end
                                                                	return tmp
                                                                end
                                                                
                                                                \begin{array}{l}
                                                                \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\
                                                                \;\;\;\;\mathsf{fma}\left(\frac{2}{v} - -2, u, -2\right) - -1\\
                                                                
                                                                \mathbf{else}:\\
                                                                \;\;\;\;\frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5\\
                                                                
                                                                
                                                                \end{array}
                                                                
                                                                Derivation
                                                                1. Split input into 2 regimes
                                                                2. if (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v)))))) < -1

                                                                  1. Initial program 99.5%

                                                                    \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                  2. Taylor expanded in v around inf

                                                                    \[\leadsto 1 + \left(-2 \cdot \left(1 - u\right) + \frac{1}{2} \cdot \frac{-4 \cdot {\left(1 - u\right)}^{2} + 4 \cdot \left(1 - u\right)}{v}\right) \]
                                                                  3. Step-by-step derivation
                                                                    1. Applied rewrites14.6%

                                                                      \[\leadsto 1 + \mathsf{fma}\left(-2, 1 - u, 0.5 \cdot \frac{\mathsf{fma}\left(-4, {\left(1 - u\right)}^{2}, 4 \cdot \left(1 - u\right)\right)}{v}\right) \]
                                                                    2. Taylor expanded in u around 0

                                                                      \[\leadsto 1 + \left(u \cdot \left(2 + 2 \cdot \frac{1}{v}\right) - 2\right) \]
                                                                    3. Step-by-step derivation
                                                                      1. Applied rewrites14.4%

                                                                        \[\leadsto 1 + \left(u \cdot \left(2 + 2 \cdot \frac{1}{v}\right) - 2\right) \]
                                                                      2. Applied rewrites14.4%

                                                                        \[\leadsto \mathsf{fma}\left(\frac{2}{v} - -2, u, -2\right) - -1 \]

                                                                      if -1 < (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v))))))

                                                                      1. Initial program 99.5%

                                                                        \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                      2. Step-by-step derivation
                                                                        1. Applied rewrites99.3%

                                                                          \[\leadsto \mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right) + 0.5 \]
                                                                        2. Step-by-step derivation
                                                                          1. pow1N/A

                                                                            \[\leadsto \frac{1}{{\left({\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{1}\right)}^{-1}} + \frac{1}{2} \]
                                                                          2. metadata-evalN/A

                                                                            \[\leadsto \frac{1}{{\left({\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}\right)}^{-1}} + \frac{1}{2} \]
                                                                          3. pow-negN/A

                                                                            \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                          4. remove-sound-/N/A

                                                                            \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                          5. lower-/.f32N/A

                                                                            \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                          6. remove-sound-powN/A

                                                                            \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                          7. lower-pow.f3299.3%

                                                                            \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right)\right)}^{-1}}\right)}^{-1}} + 0.5 \]
                                                                        3. Applied rewrites99.3%

                                                                          \[\leadsto \frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right)\right)}^{-1}} + 0.5 \]
                                                                        4. Step-by-step derivation
                                                                          1. Applied rewrites99.3%

                                                                            \[\leadsto \frac{1}{2 \cdot \frac{0.5}{\mathsf{fma}\left(\log \left(\mathsf{fma}\left(1 - u, e^{\frac{-2}{v}}, u\right)\right), v, 0.5\right)}} + 0.5 \]
                                                                          2. Taylor expanded in v around 0

                                                                            \[\leadsto \frac{1}{2 \cdot \frac{0.5}{\frac{1}{2}}} + 0.5 \]
                                                                          3. Step-by-step derivation
                                                                            1. Applied rewrites86.7%

                                                                              \[\leadsto \frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5 \]
                                                                          4. Recombined 2 regimes into one program.
                                                                          5. Add Preprocessing

                                                                          Alternative 11: 90.8% accurate, 0.7× speedup?

                                                                          \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                                                          \[\begin{array}{l} \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{v} + 2, u, -1\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5\\ \end{array} \]
                                                                          (FPCore (u v)
                                                                            :precision binary32
                                                                            :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                                               (and (<= 0.0 v) (<= v 109.746574)))
                                                                            (if (<= (* v (log (+ u (* (- 1.0 u) (exp (/ -2.0 v)))))) -1.0)
                                                                            (fma (+ (/ 2.0 v) 2.0) u -1.0)
                                                                            (+ (/ 1.0 (* 2.0 (/ 0.5 0.5))) 0.5)))
                                                                          float code(float u, float v) {
                                                                          	float tmp;
                                                                          	if ((v * logf((u + ((1.0f - u) * expf((-2.0f / v)))))) <= -1.0f) {
                                                                          		tmp = fmaf(((2.0f / v) + 2.0f), u, -1.0f);
                                                                          	} else {
                                                                          		tmp = (1.0f / (2.0f * (0.5f / 0.5f))) + 0.5f;
                                                                          	}
                                                                          	return tmp;
                                                                          }
                                                                          
                                                                          function code(u, v)
                                                                          	tmp = Float32(0.0)
                                                                          	if (Float32(v * log(Float32(u + Float32(Float32(Float32(1.0) - u) * exp(Float32(Float32(-2.0) / v)))))) <= Float32(-1.0))
                                                                          		tmp = fma(Float32(Float32(Float32(2.0) / v) + Float32(2.0)), u, Float32(-1.0));
                                                                          	else
                                                                          		tmp = Float32(Float32(Float32(1.0) / Float32(Float32(2.0) * Float32(Float32(0.5) / Float32(0.5)))) + Float32(0.5));
                                                                          	end
                                                                          	return tmp
                                                                          end
                                                                          
                                                                          \begin{array}{l}
                                                                          \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\
                                                                          \;\;\;\;\mathsf{fma}\left(\frac{2}{v} + 2, u, -1\right)\\
                                                                          
                                                                          \mathbf{else}:\\
                                                                          \;\;\;\;\frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5\\
                                                                          
                                                                          
                                                                          \end{array}
                                                                          
                                                                          Derivation
                                                                          1. Split input into 2 regimes
                                                                          2. if (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v)))))) < -1

                                                                            1. Initial program 99.5%

                                                                              \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                            2. Taylor expanded in u around 0

                                                                              \[\leadsto u \cdot \left(\frac{-1}{2} \cdot \frac{u \cdot \left(v \cdot {\left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}^{2}\right)}{e^{\frac{-4}{v}}} + \frac{v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}{e^{\frac{-2}{v}}}\right) - 1 \]
                                                                            3. Step-by-step derivation
                                                                              1. Applied rewrites5.7%

                                                                                \[\leadsto u \cdot \mathsf{fma}\left(-0.5, \frac{u \cdot \left(v \cdot {\left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}^{2}\right)}{e^{\frac{-4}{v}}}, \frac{v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}{e^{\frac{-2}{v}}}\right) - 1 \]
                                                                              2. Taylor expanded in v around -inf

                                                                                \[\leadsto u \cdot \left(2 + -1 \cdot \frac{2 \cdot u - 2}{v}\right) - 1 \]
                                                                              3. Step-by-step derivation
                                                                                1. Applied rewrites14.6%

                                                                                  \[\leadsto u \cdot \left(2 + -1 \cdot \frac{2 \cdot u - 2}{v}\right) - 1 \]
                                                                                2. Taylor expanded in u around 0

                                                                                  \[\leadsto u \cdot \left(2 + \frac{2}{v}\right) - 1 \]
                                                                                3. Step-by-step derivation
                                                                                  1. Applied rewrites14.4%

                                                                                    \[\leadsto u \cdot \left(2 + \frac{2}{v}\right) - 1 \]
                                                                                  2. Applied rewrites14.4%

                                                                                    \[\leadsto \mathsf{fma}\left(\frac{2}{v} + 2, u, -1\right) \]

                                                                                  if -1 < (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v))))))

                                                                                  1. Initial program 99.5%

                                                                                    \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                                  2. Step-by-step derivation
                                                                                    1. Applied rewrites99.3%

                                                                                      \[\leadsto \mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right) + 0.5 \]
                                                                                    2. Step-by-step derivation
                                                                                      1. pow1N/A

                                                                                        \[\leadsto \frac{1}{{\left({\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{1}\right)}^{-1}} + \frac{1}{2} \]
                                                                                      2. metadata-evalN/A

                                                                                        \[\leadsto \frac{1}{{\left({\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{\left(\mathsf{neg}\left(-1\right)\right)}\right)}^{-1}} + \frac{1}{2} \]
                                                                                      3. pow-negN/A

                                                                                        \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                                      4. remove-sound-/N/A

                                                                                        \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                                      5. lower-/.f32N/A

                                                                                        \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                                      6. remove-sound-powN/A

                                                                                        \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, \frac{1}{2}\right)\right)}^{-1}}\right)}^{-1}} + \frac{1}{2} \]
                                                                                      7. lower-pow.f3299.3%

                                                                                        \[\leadsto \frac{1}{{\left(\frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right)\right)}^{-1}}\right)}^{-1}} + 0.5 \]
                                                                                    3. Applied rewrites99.3%

                                                                                      \[\leadsto \frac{1}{{\left(\mathsf{fma}\left(\log \left(\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right), v, 0.5\right)\right)}^{-1}} + 0.5 \]
                                                                                    4. Step-by-step derivation
                                                                                      1. Applied rewrites99.3%

                                                                                        \[\leadsto \frac{1}{2 \cdot \frac{0.5}{\mathsf{fma}\left(\log \left(\mathsf{fma}\left(1 - u, e^{\frac{-2}{v}}, u\right)\right), v, 0.5\right)}} + 0.5 \]
                                                                                      2. Taylor expanded in v around 0

                                                                                        \[\leadsto \frac{1}{2 \cdot \frac{0.5}{\frac{1}{2}}} + 0.5 \]
                                                                                      3. Step-by-step derivation
                                                                                        1. Applied rewrites86.7%

                                                                                          \[\leadsto \frac{1}{2 \cdot \frac{0.5}{0.5}} + 0.5 \]
                                                                                      4. Recombined 2 regimes into one program.
                                                                                      5. Add Preprocessing

                                                                                      Alternative 12: 87.9% accurate, 1.5× speedup?

                                                                                      \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                                                                      \[\mathsf{fma}\left(-v, \log \left(\mathsf{fma}\left(\frac{1 - u}{v}, 2, 1\right)\right), 1\right) \]
                                                                                      (FPCore (u v)
                                                                                        :precision binary32
                                                                                        :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                                                           (and (<= 0.0 v) (<= v 109.746574)))
                                                                                        (fma (- v) (log (fma (/ (- 1.0 u) v) 2.0 1.0)) 1.0))
                                                                                      float code(float u, float v) {
                                                                                      	return fmaf(-v, logf(fmaf(((1.0f - u) / v), 2.0f, 1.0f)), 1.0f);
                                                                                      }
                                                                                      
                                                                                      function code(u, v)
                                                                                      	return fma(Float32(-v), log(fma(Float32(Float32(Float32(1.0) - u) / v), Float32(2.0), Float32(1.0))), Float32(1.0))
                                                                                      end
                                                                                      
                                                                                      \mathsf{fma}\left(-v, \log \left(\mathsf{fma}\left(\frac{1 - u}{v}, 2, 1\right)\right), 1\right)
                                                                                      
                                                                                      Derivation
                                                                                      1. Initial program 99.5%

                                                                                        \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                                      2. Step-by-step derivation
                                                                                        1. Applied rewrites99.4%

                                                                                          \[\leadsto 1 + \log \left({\left(\frac{1}{\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)}\right)}^{\left(-v\right)}\right) \]
                                                                                        2. Step-by-step derivation
                                                                                          1. Applied rewrites99.4%

                                                                                            \[\leadsto \mathsf{fma}\left(-v, \log \left(\frac{1}{\left|\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right|}\right), 1\right) \]
                                                                                          2. Taylor expanded in v around inf

                                                                                            \[\leadsto \mathsf{fma}\left(-v, \log \left(1 + 2 \cdot \frac{1 - u}{v}\right), 1\right) \]
                                                                                          3. Step-by-step derivation
                                                                                            1. Applied rewrites87.9%

                                                                                              \[\leadsto \mathsf{fma}\left(-v, \log \left(1 + 2 \cdot \frac{1 - u}{v}\right), 1\right) \]
                                                                                            2. Step-by-step derivation
                                                                                              1. Applied rewrites87.9%

                                                                                                \[\leadsto \mathsf{fma}\left(-v, \log \left(\mathsf{fma}\left(\frac{1 - u}{v}, 2, 1\right)\right), 1\right) \]
                                                                                              2. Add Preprocessing

                                                                                              Alternative 13: 87.7% accurate, 1.8× speedup?

                                                                                              \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                                                                              \[\mathsf{fma}\left(-v, \log \left(1 + \frac{2}{v}\right), 1\right) \]
                                                                                              (FPCore (u v)
                                                                                                :precision binary32
                                                                                                :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                                                                   (and (<= 0.0 v) (<= v 109.746574)))
                                                                                                (fma (- v) (log (+ 1.0 (/ 2.0 v))) 1.0))
                                                                                              float code(float u, float v) {
                                                                                              	return fmaf(-v, logf((1.0f + (2.0f / v))), 1.0f);
                                                                                              }
                                                                                              
                                                                                              function code(u, v)
                                                                                              	return fma(Float32(-v), log(Float32(Float32(1.0) + Float32(Float32(2.0) / v))), Float32(1.0))
                                                                                              end
                                                                                              
                                                                                              \mathsf{fma}\left(-v, \log \left(1 + \frac{2}{v}\right), 1\right)
                                                                                              
                                                                                              Derivation
                                                                                              1. Initial program 99.5%

                                                                                                \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                                              2. Step-by-step derivation
                                                                                                1. Applied rewrites99.4%

                                                                                                  \[\leadsto 1 + \log \left({\left(\frac{1}{\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)}\right)}^{\left(-v\right)}\right) \]
                                                                                                2. Step-by-step derivation
                                                                                                  1. Applied rewrites99.4%

                                                                                                    \[\leadsto \mathsf{fma}\left(-v, \log \left(\frac{1}{\left|\mathsf{fma}\left(e^{\frac{-2}{v}}, 1 - u, u\right)\right|}\right), 1\right) \]
                                                                                                  2. Taylor expanded in v around inf

                                                                                                    \[\leadsto \mathsf{fma}\left(-v, \log \left(1 + 2 \cdot \frac{1 - u}{v}\right), 1\right) \]
                                                                                                  3. Step-by-step derivation
                                                                                                    1. Applied rewrites87.9%

                                                                                                      \[\leadsto \mathsf{fma}\left(-v, \log \left(1 + 2 \cdot \frac{1 - u}{v}\right), 1\right) \]
                                                                                                    2. Taylor expanded in u around 0

                                                                                                      \[\leadsto \mathsf{fma}\left(-v, \log \left(1 + \frac{2}{v}\right), 1\right) \]
                                                                                                    3. Step-by-step derivation
                                                                                                      1. Applied rewrites87.7%

                                                                                                        \[\leadsto \mathsf{fma}\left(-v, \log \left(1 + \frac{2}{v}\right), 1\right) \]
                                                                                                      2. Add Preprocessing

                                                                                                      Alternative 14: 50.4% accurate, 0.7× speedup?

                                                                                                      \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                                                                                      \[\begin{array}{l} \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\ \;\;\;\;\mathsf{fma}\left(\frac{2}{v} + 2, u, -1\right)\\ \mathbf{else}:\\ \;\;\;\;\left(u + u\right) - -1\\ \end{array} \]
                                                                                                      (FPCore (u v)
                                                                                                        :precision binary32
                                                                                                        :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                                                                           (and (<= 0.0 v) (<= v 109.746574)))
                                                                                                        (if (<= (* v (log (+ u (* (- 1.0 u) (exp (/ -2.0 v)))))) -1.0)
                                                                                                        (fma (+ (/ 2.0 v) 2.0) u -1.0)
                                                                                                        (- (+ u u) -1.0)))
                                                                                                      float code(float u, float v) {
                                                                                                      	float tmp;
                                                                                                      	if ((v * logf((u + ((1.0f - u) * expf((-2.0f / v)))))) <= -1.0f) {
                                                                                                      		tmp = fmaf(((2.0f / v) + 2.0f), u, -1.0f);
                                                                                                      	} else {
                                                                                                      		tmp = (u + u) - -1.0f;
                                                                                                      	}
                                                                                                      	return tmp;
                                                                                                      }
                                                                                                      
                                                                                                      function code(u, v)
                                                                                                      	tmp = Float32(0.0)
                                                                                                      	if (Float32(v * log(Float32(u + Float32(Float32(Float32(1.0) - u) * exp(Float32(Float32(-2.0) / v)))))) <= Float32(-1.0))
                                                                                                      		tmp = fma(Float32(Float32(Float32(2.0) / v) + Float32(2.0)), u, Float32(-1.0));
                                                                                                      	else
                                                                                                      		tmp = Float32(Float32(u + u) - Float32(-1.0));
                                                                                                      	end
                                                                                                      	return tmp
                                                                                                      end
                                                                                                      
                                                                                                      \begin{array}{l}
                                                                                                      \mathbf{if}\;v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \leq -1:\\
                                                                                                      \;\;\;\;\mathsf{fma}\left(\frac{2}{v} + 2, u, -1\right)\\
                                                                                                      
                                                                                                      \mathbf{else}:\\
                                                                                                      \;\;\;\;\left(u + u\right) - -1\\
                                                                                                      
                                                                                                      
                                                                                                      \end{array}
                                                                                                      
                                                                                                      Derivation
                                                                                                      1. Split input into 2 regimes
                                                                                                      2. if (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v)))))) < -1

                                                                                                        1. Initial program 99.5%

                                                                                                          \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                                                        2. Taylor expanded in u around 0

                                                                                                          \[\leadsto u \cdot \left(\frac{-1}{2} \cdot \frac{u \cdot \left(v \cdot {\left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}^{2}\right)}{e^{\frac{-4}{v}}} + \frac{v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}{e^{\frac{-2}{v}}}\right) - 1 \]
                                                                                                        3. Step-by-step derivation
                                                                                                          1. Applied rewrites5.7%

                                                                                                            \[\leadsto u \cdot \mathsf{fma}\left(-0.5, \frac{u \cdot \left(v \cdot {\left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}^{2}\right)}{e^{\frac{-4}{v}}}, \frac{v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)}{e^{\frac{-2}{v}}}\right) - 1 \]
                                                                                                          2. Taylor expanded in v around -inf

                                                                                                            \[\leadsto u \cdot \left(2 + -1 \cdot \frac{2 \cdot u - 2}{v}\right) - 1 \]
                                                                                                          3. Step-by-step derivation
                                                                                                            1. Applied rewrites14.6%

                                                                                                              \[\leadsto u \cdot \left(2 + -1 \cdot \frac{2 \cdot u - 2}{v}\right) - 1 \]
                                                                                                            2. Taylor expanded in u around 0

                                                                                                              \[\leadsto u \cdot \left(2 + \frac{2}{v}\right) - 1 \]
                                                                                                            3. Step-by-step derivation
                                                                                                              1. Applied rewrites14.4%

                                                                                                                \[\leadsto u \cdot \left(2 + \frac{2}{v}\right) - 1 \]
                                                                                                              2. Applied rewrites14.4%

                                                                                                                \[\leadsto \mathsf{fma}\left(\frac{2}{v} + 2, u, -1\right) \]

                                                                                                              if -1 < (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 #s(literal 1 binary32) u) (exp.f32 (/.f32 #s(literal -2 binary32) v))))))

                                                                                                              1. Initial program 99.5%

                                                                                                                \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                                                              2. Taylor expanded in v around inf

                                                                                                                \[\leadsto 1 + -2 \cdot \left(1 - u\right) \]
                                                                                                              3. Step-by-step derivation
                                                                                                                1. Applied rewrites8.2%

                                                                                                                  \[\leadsto 1 + -2 \cdot \left(1 - u\right) \]
                                                                                                                2. Taylor expanded in u around inf

                                                                                                                  \[\leadsto 1 + 2 \cdot u \]
                                                                                                                3. Step-by-step derivation
                                                                                                                  1. Applied rewrites46.4%

                                                                                                                    \[\leadsto 1 + 2 \cdot u \]
                                                                                                                  2. Step-by-step derivation
                                                                                                                    1. Applied rewrites46.4%

                                                                                                                      \[\leadsto \left(u + u\right) - -1 \]
                                                                                                                  3. Recombined 2 regimes into one program.
                                                                                                                  4. Add Preprocessing

                                                                                                                  Alternative 15: 46.4% accurate, 5.7× speedup?

                                                                                                                  \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                                                                                                  \[\left(u + u\right) - -1 \]
                                                                                                                  (FPCore (u v)
                                                                                                                    :precision binary32
                                                                                                                    :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                                                                                       (and (<= 0.0 v) (<= v 109.746574)))
                                                                                                                    (- (+ u u) -1.0))
                                                                                                                  float code(float u, float v) {
                                                                                                                  	return (u + u) - -1.0f;
                                                                                                                  }
                                                                                                                  
                                                                                                                  real(4) function code(u, v)
                                                                                                                  use fmin_fmax_functions
                                                                                                                      real(4), intent (in) :: u
                                                                                                                      real(4), intent (in) :: v
                                                                                                                      code = (u + u) - (-1.0e0)
                                                                                                                  end function
                                                                                                                  
                                                                                                                  function code(u, v)
                                                                                                                  	return Float32(Float32(u + u) - Float32(-1.0))
                                                                                                                  end
                                                                                                                  
                                                                                                                  function tmp = code(u, v)
                                                                                                                  	tmp = (u + u) - single(-1.0);
                                                                                                                  end
                                                                                                                  
                                                                                                                  \left(u + u\right) - -1
                                                                                                                  
                                                                                                                  Derivation
                                                                                                                  1. Initial program 99.5%

                                                                                                                    \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                                                                  2. Taylor expanded in v around inf

                                                                                                                    \[\leadsto 1 + -2 \cdot \left(1 - u\right) \]
                                                                                                                  3. Step-by-step derivation
                                                                                                                    1. Applied rewrites8.2%

                                                                                                                      \[\leadsto 1 + -2 \cdot \left(1 - u\right) \]
                                                                                                                    2. Taylor expanded in u around inf

                                                                                                                      \[\leadsto 1 + 2 \cdot u \]
                                                                                                                    3. Step-by-step derivation
                                                                                                                      1. Applied rewrites46.4%

                                                                                                                        \[\leadsto 1 + 2 \cdot u \]
                                                                                                                      2. Step-by-step derivation
                                                                                                                        1. Applied rewrites46.4%

                                                                                                                          \[\leadsto \left(u + u\right) - -1 \]
                                                                                                                        2. Add Preprocessing

                                                                                                                        Alternative 16: 19.9% accurate, 5.7× speedup?

                                                                                                                        \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                                                                                                        \[0 + \left(u + u\right) \]
                                                                                                                        (FPCore (u v)
                                                                                                                          :precision binary32
                                                                                                                          :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                                                                                             (and (<= 0.0 v) (<= v 109.746574)))
                                                                                                                          (+ 0.0 (+ u u)))
                                                                                                                        float code(float u, float v) {
                                                                                                                        	return 0.0f + (u + u);
                                                                                                                        }
                                                                                                                        
                                                                                                                        real(4) function code(u, v)
                                                                                                                        use fmin_fmax_functions
                                                                                                                            real(4), intent (in) :: u
                                                                                                                            real(4), intent (in) :: v
                                                                                                                            code = 0.0e0 + (u + u)
                                                                                                                        end function
                                                                                                                        
                                                                                                                        function code(u, v)
                                                                                                                        	return Float32(Float32(0.0) + Float32(u + u))
                                                                                                                        end
                                                                                                                        
                                                                                                                        function tmp = code(u, v)
                                                                                                                        	tmp = single(0.0) + (u + u);
                                                                                                                        end
                                                                                                                        
                                                                                                                        0 + \left(u + u\right)
                                                                                                                        
                                                                                                                        Derivation
                                                                                                                        1. Initial program 99.5%

                                                                                                                          \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                                                                        2. Taylor expanded in v around inf

                                                                                                                          \[\leadsto 1 + -2 \cdot \left(1 - u\right) \]
                                                                                                                        3. Step-by-step derivation
                                                                                                                          1. Applied rewrites8.2%

                                                                                                                            \[\leadsto 1 + -2 \cdot \left(1 - u\right) \]
                                                                                                                          2. Taylor expanded in u around inf

                                                                                                                            \[\leadsto 1 + 2 \cdot u \]
                                                                                                                          3. Step-by-step derivation
                                                                                                                            1. Applied rewrites46.4%

                                                                                                                              \[\leadsto 1 + 2 \cdot u \]
                                                                                                                            2. Taylor expanded in undef-var around zero

                                                                                                                              \[\leadsto 0 + 2 \cdot u \]
                                                                                                                            3. Step-by-step derivation
                                                                                                                              1. Applied rewrites19.9%

                                                                                                                                \[\leadsto 0 + 2 \cdot u \]
                                                                                                                              2. Step-by-step derivation
                                                                                                                                1. Applied rewrites19.9%

                                                                                                                                  \[\leadsto 0 + \left(u + u\right) \]
                                                                                                                                2. Add Preprocessing

                                                                                                                                Alternative 17: 8.2% accurate, 5.9× speedup?

                                                                                                                                \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                                                                                                                \[\mathsf{fma}\left(2, u, -1\right) \]
                                                                                                                                (FPCore (u v)
                                                                                                                                  :precision binary32
                                                                                                                                  :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                                                                                                     (and (<= 0.0 v) (<= v 109.746574)))
                                                                                                                                  (fma 2.0 u -1.0))
                                                                                                                                float code(float u, float v) {
                                                                                                                                	return fmaf(2.0f, u, -1.0f);
                                                                                                                                }
                                                                                                                                
                                                                                                                                function code(u, v)
                                                                                                                                	return fma(Float32(2.0), u, Float32(-1.0))
                                                                                                                                end
                                                                                                                                
                                                                                                                                \mathsf{fma}\left(2, u, -1\right)
                                                                                                                                
                                                                                                                                Derivation
                                                                                                                                1. Initial program 99.5%

                                                                                                                                  \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                                                                                2. Taylor expanded in u around 0

                                                                                                                                  \[\leadsto \frac{u \cdot \left(v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)\right)}{e^{\frac{-2}{v}}} - 1 \]
                                                                                                                                3. Step-by-step derivation
                                                                                                                                  1. Applied rewrites10.8%

                                                                                                                                    \[\leadsto \frac{u \cdot \left(v \cdot \left(1 + -1 \cdot e^{\frac{-2}{v}}\right)\right)}{e^{\frac{-2}{v}}} - 1 \]
                                                                                                                                  2. Taylor expanded in v around inf

                                                                                                                                    \[\leadsto 2 \cdot u - 1 \]
                                                                                                                                  3. Step-by-step derivation
                                                                                                                                    1. Applied rewrites8.2%

                                                                                                                                      \[\leadsto 2 \cdot u - 1 \]
                                                                                                                                    2. Applied rewrites8.2%

                                                                                                                                      \[\leadsto \mathsf{fma}\left(2, u, -1\right) \]
                                                                                                                                    3. Add Preprocessing

                                                                                                                                    Alternative 18: 6.1% accurate, 35.6× speedup?

                                                                                                                                    \[\left(10^{-5} \leq u \land u \leq 1\right) \land \left(0 \leq v \land v \leq 109.746574\right)\]
                                                                                                                                    \[-1 \]
                                                                                                                                    (FPCore (u v)
                                                                                                                                      :precision binary32
                                                                                                                                      :pre (and (and (<= 1e-5 u) (<= u 1.0))
                                                                                                                                         (and (<= 0.0 v) (<= v 109.746574)))
                                                                                                                                      -1.0)
                                                                                                                                    float code(float u, float v) {
                                                                                                                                    	return -1.0f;
                                                                                                                                    }
                                                                                                                                    
                                                                                                                                    real(4) function code(u, v)
                                                                                                                                    use fmin_fmax_functions
                                                                                                                                        real(4), intent (in) :: u
                                                                                                                                        real(4), intent (in) :: v
                                                                                                                                        code = -1.0e0
                                                                                                                                    end function
                                                                                                                                    
                                                                                                                                    function code(u, v)
                                                                                                                                    	return Float32(-1.0)
                                                                                                                                    end
                                                                                                                                    
                                                                                                                                    function tmp = code(u, v)
                                                                                                                                    	tmp = single(-1.0);
                                                                                                                                    end
                                                                                                                                    
                                                                                                                                    -1
                                                                                                                                    
                                                                                                                                    Derivation
                                                                                                                                    1. Initial program 99.5%

                                                                                                                                      \[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right) \]
                                                                                                                                    2. Taylor expanded in u around 0

                                                                                                                                      \[\leadsto -1 \]
                                                                                                                                    3. Step-by-step derivation
                                                                                                                                      1. Applied rewrites6.1%

                                                                                                                                        \[\leadsto -1 \]
                                                                                                                                      2. Add Preprocessing

                                                                                                                                      Reproduce

                                                                                                                                      ?
                                                                                                                                      herbie shell --seed 2026070 
                                                                                                                                      (FPCore (u v)
                                                                                                                                        :name "HairBSDF, sample_f, cosTheta"
                                                                                                                                        :precision binary32
                                                                                                                                        :pre (and (and (<= 1e-5 u) (<= u 1.0)) (and (<= 0.0 v) (<= v 109.746574)))
                                                                                                                                        (+ 1.0 (* v (log (+ u (* (- 1.0 u) (exp (/ -2.0 v))))))))