tanhf (example 3.4)

Average Error: 30.2 → 0.7

Time: 14.1s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\frac{1 - \cos x}{\sin x}\]

↓

\[\begin{array}{l} \mathbf{if}\;\frac{1 - \cos x}{\sin x} \le -0.0097901793206562754:\\ \;\;\;\;\frac{{1}^{3} - \sqrt[3]{{\left({\left(\cos x\right)}^{3}\right)}^{3}}}{\sin x \cdot \mathsf{fma}\left(1, 1, \cos x \cdot \left(1 + \cos x\right)\right)}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le -0.0:\\ \;\;\;\;\mathsf{fma}\left(0.04166666666666663, {x}^{3}, \mathsf{fma}\left(0.004166666666666624, {x}^{5}, 0.5 \cdot x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{1}^{3} - \mathsf{expm1}\left(\mathsf{log1p}\left({\left(\cos x\right)}^{3}\right)\right)}{\sin x \cdot \mathsf{fma}\left(1, 1, \cos x \cdot \left(1 + \cos x\right)\right)}\\ \end{array}\]

C

double f(double x) {
        double r52294 = 1.0;
        double r52295 = x;
        double r52296 = cos(r52295);
        double r52297 = r52294 - r52296;
        double r52298 = sin(r52295);
        double r52299 = r52297 / r52298;
        return r52299;
}

↓

double f(double x) {
        double r52300 = 1.0;
        double r52301 = x;
        double r52302 = cos(r52301);
        double r52303 = r52300 - r52302;
        double r52304 = sin(r52301);
        double r52305 = r52303 / r52304;
        double r52306 = -0.009790179320656275;
        bool r52307 = r52305 <= r52306;
        double r52308 = 3.0;
        double r52309 = pow(r52300, r52308);
        double r52310 = pow(r52302, r52308);
        double r52311 = pow(r52310, r52308);
        double r52312 = cbrt(r52311);
        double r52313 = r52309 - r52312;
        double r52314 = r52300 + r52302;
        double r52315 = r52302 * r52314;
        double r52316 = fma(r52300, r52300, r52315);
        double r52317 = r52304 * r52316;
        double r52318 = r52313 / r52317;
        double r52319 = -0.0;
        bool r52320 = r52305 <= r52319;
        double r52321 = 0.04166666666666663;
        double r52322 = pow(r52301, r52308);
        double r52323 = 0.004166666666666624;
        double r52324 = 5.0;
        double r52325 = pow(r52301, r52324);
        double r52326 = 0.5;
        double r52327 = r52326 * r52301;
        double r52328 = fma(r52323, r52325, r52327);
        double r52329 = fma(r52321, r52322, r52328);
        double r52330 = log1p(r52310);
        double r52331 = expm1(r52330);
        double r52332 = r52309 - r52331;
        double r52333 = r52332 / r52317;
        double r52334 = r52320 ? r52329 : r52333;
        double r52335 = r52307 ? r52318 : r52334;
        return r52335;
}

Error

Bits error versus x

Target

Original	30.2
Target	0.0
Herbie	0.7

\[\tan \left(\frac{x}{2}\right)\]

Derivation

1. Split input into 3 regimes

2. if (/ (- 1.0 (cos x)) (sin x)) < -0.009790179320656275

   1. Initial program 0.8

      \[\frac{1 - \cos x}{\sin x}\]
   2. Using strategy rm

   3. Applied add-log-exp 0.9

      \[\leadsto \color{blue}{\log \left(e^{\frac{1 - \cos x}{\sin x}}\right)}\]
   4. Using strategy rm

   5. Applied div-inv 1.0

      \[\leadsto \log \left(e^{\color{blue}{\left(1 - \cos x\right) \cdot \frac{1}{\sin x}}}\right)\]

   6. Applied exp-prod 1.2

      \[\leadsto \log \color{blue}{\left({\left(e^{1 - \cos x}\right)}^{\left(\frac{1}{\sin x}\right)}\right)}\]

   7. Applied log-pow 1.1

      \[\leadsto \color{blue}{\frac{1}{\sin x} \cdot \log \left(e^{1 - \cos x}\right)}\]

   8. Simplified 0.9

      \[\leadsto \frac{1}{\sin x} \cdot \color{blue}{\left(1 - \cos x\right)}\]
   9. Using strategy rm

   10. Applied flip3-- 1.0

       \[\leadsto \frac{1}{\sin x} \cdot \color{blue}{\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)}}\]

   11. Applied frac-times 1.0

       \[\leadsto \color{blue}{\frac{1 \cdot \left({1}^{3} - {\left(\cos x\right)}^{3}\right)}{\sin x \cdot \left(1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)\right)}}\]

   12. Simplified 1.0

       \[\leadsto \frac{\color{blue}{{1}^{3} - {\left(\cos x\right)}^{3}}}{\sin x \cdot \left(1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)\right)}\]

   13. Simplified 1.0

       \[\leadsto \frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\sin x \cdot \mathsf{fma}\left(1, 1, \cos x \cdot \left(1 + \cos x\right)\right)}}\]
   14. Using strategy rm

   15. Applied add-cbrt-cube 1.1

       \[\leadsto \frac{{1}^{3} - \color{blue}{\sqrt[3]{\left({\left(\cos x\right)}^{3} \cdot {\left(\cos x\right)}^{3}\right) \cdot {\left(\cos x\right)}^{3}}}}{\sin x \cdot \mathsf{fma}\left(1, 1, \cos x \cdot \left(1 + \cos x\right)\right)}\]

   16. Simplified 1.0

       \[\leadsto \frac{{1}^{3} - \sqrt[3]{\color{blue}{{\left({\left(\cos x\right)}^{3}\right)}^{3}}}}{\sin x \cdot \mathsf{fma}\left(1, 1, \cos x \cdot \left(1 + \cos x\right)\right)}\]

   if -0.009790179320656275 < (/ (- 1.0 (cos x)) (sin x)) < -0.0

   1. Initial program 60.2

      \[\frac{1 - \cos x}{\sin x}\]
   2. Using strategy rm

   3. Applied add-log-exp 60.2

      \[\leadsto \color{blue}{\log \left(e^{\frac{1 - \cos x}{\sin x}}\right)}\]
   4. Using strategy rm

   5. Applied div-inv 60.2

      \[\leadsto \log \left(e^{\color{blue}{\left(1 - \cos x\right) \cdot \frac{1}{\sin x}}}\right)\]

   6. Applied exp-prod 60.2

      \[\leadsto \log \color{blue}{\left({\left(e^{1 - \cos x}\right)}^{\left(\frac{1}{\sin x}\right)}\right)}\]

   7. Applied log-pow 60.2

      \[\leadsto \color{blue}{\frac{1}{\sin x} \cdot \log \left(e^{1 - \cos x}\right)}\]

   8. Simplified 60.2

      \[\leadsto \frac{1}{\sin x} \cdot \color{blue}{\left(1 - \cos x\right)}\]
   9. Using strategy rm

   10. Applied flip3-- 60.2

       \[\leadsto \frac{1}{\sin x} \cdot \color{blue}{\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)}}\]

   11. Applied frac-times 60.2

       \[\leadsto \color{blue}{\frac{1 \cdot \left({1}^{3} - {\left(\cos x\right)}^{3}\right)}{\sin x \cdot \left(1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)\right)}}\]

   12. Simplified 60.2

       \[\leadsto \frac{\color{blue}{{1}^{3} - {\left(\cos x\right)}^{3}}}{\sin x \cdot \left(1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)\right)}\]

   13. Simplified 60.2

       \[\leadsto \frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\sin x \cdot \mathsf{fma}\left(1, 1, \cos x \cdot \left(1 + \cos x\right)\right)}}\]

   14. Taylor expanded around 0 0.1

       \[\leadsto \color{blue}{0.04166666666666663 \cdot {x}^{3} + \left(0.004166666666666624 \cdot {x}^{5} + 0.5 \cdot x\right)}\]

   15. Simplified 0.1

       \[\leadsto \color{blue}{\mathsf{fma}\left(0.04166666666666663, {x}^{3}, \mathsf{fma}\left(0.004166666666666624, {x}^{5}, 0.5 \cdot x\right)\right)}\]

   if -0.0 < (/ (- 1.0 (cos x)) (sin x))

   1. Initial program 1.6

      \[\frac{1 - \cos x}{\sin x}\]
   2. Using strategy rm

   3. Applied add-log-exp 1.6

      \[\leadsto \color{blue}{\log \left(e^{\frac{1 - \cos x}{\sin x}}\right)}\]
   4. Using strategy rm

   5. Applied div-inv 1.7

      \[\leadsto \log \left(e^{\color{blue}{\left(1 - \cos x\right) \cdot \frac{1}{\sin x}}}\right)\]

   6. Applied exp-prod 1.9

      \[\leadsto \log \color{blue}{\left({\left(e^{1 - \cos x}\right)}^{\left(\frac{1}{\sin x}\right)}\right)}\]

   7. Applied log-pow 1.9

      \[\leadsto \color{blue}{\frac{1}{\sin x} \cdot \log \left(e^{1 - \cos x}\right)}\]

   8. Simplified 1.6

      \[\leadsto \frac{1}{\sin x} \cdot \color{blue}{\left(1 - \cos x\right)}\]
   9. Using strategy rm

   10. Applied flip3-- 1.7

       \[\leadsto \frac{1}{\sin x} \cdot \color{blue}{\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)}}\]

   11. Applied frac-times 1.7

       \[\leadsto \color{blue}{\frac{1 \cdot \left({1}^{3} - {\left(\cos x\right)}^{3}\right)}{\sin x \cdot \left(1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)\right)}}\]

   12. Simplified 1.7

       \[\leadsto \frac{\color{blue}{{1}^{3} - {\left(\cos x\right)}^{3}}}{\sin x \cdot \left(1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)\right)}\]

   13. Simplified 1.7

       \[\leadsto \frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\sin x \cdot \mathsf{fma}\left(1, 1, \cos x \cdot \left(1 + \cos x\right)\right)}}\]
   14. Using strategy rm

   15. Applied expm1-log1p-u 1.7

       \[\leadsto \frac{{1}^{3} - \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left({\left(\cos x\right)}^{3}\right)\right)}}{\sin x \cdot \mathsf{fma}\left(1, 1, \cos x \cdot \left(1 + \cos x\right)\right)}\]
3. Recombined 3 regimes into one program.

4. Final simplification 0.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{1 - \cos x}{\sin x} \le -0.0097901793206562754:\\ \;\;\;\;\frac{{1}^{3} - \sqrt[3]{{\left({\left(\cos x\right)}^{3}\right)}^{3}}}{\sin x \cdot \mathsf{fma}\left(1, 1, \cos x \cdot \left(1 + \cos x\right)\right)}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le -0.0:\\ \;\;\;\;\mathsf{fma}\left(0.04166666666666663, {x}^{3}, \mathsf{fma}\left(0.004166666666666624, {x}^{5}, 0.5 \cdot x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{1}^{3} - \mathsf{expm1}\left(\mathsf{log1p}\left({\left(\cos x\right)}^{3}\right)\right)}{\sin x \cdot \mathsf{fma}\left(1, 1, \cos x \cdot \left(1 + \cos x\right)\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2020042 +o rules:numerics
(FPCore (x)
  :name "tanhf (example 3.4)"
  :precision binary64
  :herbie-expected 2

  :herbie-target
  (tan (/ x 2))

  (/ (- 1 (cos x)) (sin x)))