tanhf (example 3.4)

Average Error: 30.2 → 0.7

Time: 14.7s

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 r40505 = 1.0;
        double r40506 = x;
        double r40507 = cos(r40506);
        double r40508 = r40505 - r40507;
        double r40509 = sin(r40506);
        double r40510 = r40508 / r40509;
        return r40510;
}

↓

double f(double x) {
        double r40511 = 1.0;
        double r40512 = x;
        double r40513 = cos(r40512);
        double r40514 = r40511 - r40513;
        double r40515 = sin(r40512);
        double r40516 = r40514 / r40515;
        double r40517 = -0.009790179320656275;
        bool r40518 = r40516 <= r40517;
        double r40519 = 3.0;
        double r40520 = pow(r40511, r40519);
        double r40521 = pow(r40513, r40519);
        double r40522 = pow(r40521, r40519);
        double r40523 = cbrt(r40522);
        double r40524 = r40520 - r40523;
        double r40525 = r40511 + r40513;
        double r40526 = r40513 * r40525;
        double r40527 = fma(r40511, r40511, r40526);
        double r40528 = r40515 * r40527;
        double r40529 = r40524 / r40528;
        double r40530 = -0.0;
        bool r40531 = r40516 <= r40530;
        double r40532 = 0.04166666666666663;
        double r40533 = pow(r40512, r40519);
        double r40534 = 0.004166666666666624;
        double r40535 = 5.0;
        double r40536 = pow(r40512, r40535);
        double r40537 = 0.5;
        double r40538 = r40537 * r40512;
        double r40539 = fma(r40534, r40536, r40538);
        double r40540 = fma(r40532, r40533, r40539);
        double r40541 = log1p(r40521);
        double r40542 = expm1(r40541);
        double r40543 = r40520 - r40542;
        double r40544 = r40543 / r40528;
        double r40545 = r40531 ? r40540 : r40544;
        double r40546 = r40518 ? r40529 : r40545;
        return r40546;
}

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)))