Initial program 0.2
\[1 + v \cdot \log \left(u + \left(1 - u\right) \cdot e^{\frac{-2}{v}}\right)
\]
Simplified0.2
\[\leadsto \color{blue}{\mathsf{fma}\left(v, \log \left(\mathsf{fma}\left(1 - u, e^{\frac{-2}{v}}, u\right)\right), 1\right)}
\]
Proof
(fma.f32 v (log.f32 (fma.f32 (-.f32 1 u) (exp.f32 (/.f32 -2 v)) u)) 1): 0 points increase in error, 0 points decrease in error
(fma.f32 v (log.f32 (Rewrite<= fma-def_binary32 (+.f32 (*.f32 (-.f32 1 u) (exp.f32 (/.f32 -2 v))) u))) 1): 3 points increase in error, 0 points decrease in error
(fma.f32 v (log.f32 (Rewrite<= +-commutative_binary32 (+.f32 u (*.f32 (-.f32 1 u) (exp.f32 (/.f32 -2 v)))))) 1): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary32 (+.f32 (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 1 u) (exp.f32 (/.f32 -2 v)))))) 1)): 9 points increase in error, 9 points decrease in error
(Rewrite<= +-commutative_binary32 (+.f32 1 (*.f32 v (log.f32 (+.f32 u (*.f32 (-.f32 1 u) (exp.f32 (/.f32 -2 v)))))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in u around 0 0.1
\[\leadsto \mathsf{fma}\left(v, \log \color{blue}{\left(\left(1 + -1 \cdot e^{\frac{-2}{v}}\right) \cdot u + e^{\frac{-2}{v}}\right)}, 1\right)
\]
Simplified0.1
\[\leadsto \mathsf{fma}\left(v, \log \color{blue}{\left(e^{\frac{-2}{v}} - u \cdot \mathsf{expm1}\left(\frac{-2}{v}\right)\right)}, 1\right)
\]
Proof
(-.f32 (exp.f32 (/.f32 -2 v)) (*.f32 u (expm1.f32 (/.f32 -2 v)))): 0 points increase in error, 0 points decrease in error
(-.f32 (exp.f32 (/.f32 -2 v)) (*.f32 u (Rewrite<= expm1-def_binary32 (-.f32 (exp.f32 (/.f32 -2 v)) 1)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> cancel-sign-sub-inv_binary32 (+.f32 (exp.f32 (/.f32 -2 v)) (*.f32 (neg.f32 u) (-.f32 (exp.f32 (/.f32 -2 v)) 1)))): 0 points increase in error, 0 points decrease in error
(+.f32 (exp.f32 (/.f32 -2 v)) (Rewrite<= distribute-lft-neg-in_binary32 (neg.f32 (*.f32 u (-.f32 (exp.f32 (/.f32 -2 v)) 1))))): 0 points increase in error, 0 points decrease in error
(+.f32 (exp.f32 (/.f32 -2 v)) (neg.f32 (Rewrite=> *-commutative_binary32 (*.f32 (-.f32 (exp.f32 (/.f32 -2 v)) 1) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (exp.f32 (/.f32 -2 v)) (Rewrite=> distribute-lft-neg-in_binary32 (*.f32 (neg.f32 (-.f32 (exp.f32 (/.f32 -2 v)) 1)) u))): 0 points increase in error, 0 points decrease in error
(+.f32 (exp.f32 (/.f32 -2 v)) (*.f32 (neg.f32 (Rewrite=> sub-neg_binary32 (+.f32 (exp.f32 (/.f32 -2 v)) (neg.f32 1)))) u)): 0 points increase in error, 0 points decrease in error
(+.f32 (exp.f32 (/.f32 -2 v)) (*.f32 (neg.f32 (+.f32 (exp.f32 (/.f32 -2 v)) (Rewrite=> metadata-eval -1))) u)): 0 points increase in error, 0 points decrease in error
(+.f32 (exp.f32 (/.f32 -2 v)) (*.f32 (Rewrite=> distribute-neg-in_binary32 (+.f32 (neg.f32 (exp.f32 (/.f32 -2 v))) (neg.f32 -1))) u)): 0 points increase in error, 0 points decrease in error
(+.f32 (exp.f32 (/.f32 -2 v)) (*.f32 (+.f32 (Rewrite<= mul-1-neg_binary32 (*.f32 -1 (exp.f32 (/.f32 -2 v)))) (neg.f32 -1)) u)): 0 points increase in error, 0 points decrease in error
(+.f32 (exp.f32 (/.f32 -2 v)) (*.f32 (+.f32 (*.f32 -1 (exp.f32 (/.f32 -2 v))) (Rewrite=> metadata-eval 1)) u)): 0 points increase in error, 0 points decrease in error
(+.f32 (exp.f32 (/.f32 -2 v)) (*.f32 (Rewrite<= +-commutative_binary32 (+.f32 1 (*.f32 -1 (exp.f32 (/.f32 -2 v))))) u)): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary32 (+.f32 (*.f32 (+.f32 1 (*.f32 -1 (exp.f32 (/.f32 -2 v)))) u) (exp.f32 (/.f32 -2 v)))): 0 points increase in error, 0 points decrease in error
Final simplification0.1
\[\leadsto \mathsf{fma}\left(v, \log \left(e^{\frac{-2}{v}} - u \cdot \mathsf{expm1}\left(\frac{-2}{v}\right)\right), 1\right)
\]