tanhf (example 3.4)

Average Error: 30.1 → 0.7

Time: 1.2m

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\frac{1 - \cos x}{\sin x} \le -0.0107629324502667868:\\ \;\;\;\;1 \cdot \frac{1}{\sin x \cdot \left({\left(\cos x\right)}^{2} + \left(1 \cdot \cos x + 1\right)\right)} - \frac{{\left(\cos x\right)}^{3}}{\sin x \cdot \left({\left(\cos x\right)}^{2} + \left(1 \cdot \cos x + 1\right)\right)}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le 4.3298603204685633 \cdot 10^{-4}:\\ \;\;\;\;\mathsf{fma}\left(0.04166666666666663, {x}^{3}, \mathsf{fma}\left(0.004166666666666624, {x}^{5}, 0.5 \cdot x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(1, \frac{\frac{{1}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}}{\sin x}, -\frac{1}{\sin x} \cdot \frac{{\left(\cos x\right)}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}\right) + \mathsf{fma}\left(-\frac{1}{\sin x}, \frac{{\left(\cos x\right)}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}, \frac{1}{\sin x} \cdot \frac{{\left(\cos x\right)}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}\right)\\ \end{array}\]

C

double f(double x) {
        double r267863 = 1.0;
        double r267864 = x;
        double r267865 = cos(r267864);
        double r267866 = r267863 - r267865;
        double r267867 = sin(r267864);
        double r267868 = r267866 / r267867;
        return r267868;
}

↓

double f(double x) {
        double r267869 = 1.0;
        double r267870 = x;
        double r267871 = cos(r267870);
        double r267872 = r267869 - r267871;
        double r267873 = sin(r267870);
        double r267874 = r267872 / r267873;
        double r267875 = -0.010762932450266787;
        bool r267876 = r267874 <= r267875;
        double r267877 = 1.0;
        double r267878 = 2.0;
        double r267879 = pow(r267871, r267878);
        double r267880 = r267869 * r267871;
        double r267881 = r267880 + r267869;
        double r267882 = r267879 + r267881;
        double r267883 = r267873 * r267882;
        double r267884 = r267877 / r267883;
        double r267885 = r267869 * r267884;
        double r267886 = 3.0;
        double r267887 = pow(r267871, r267886);
        double r267888 = r267887 / r267883;
        double r267889 = r267885 - r267888;
        double r267890 = 0.00043298603204685633;
        bool r267891 = r267874 <= r267890;
        double r267892 = 0.04166666666666663;
        double r267893 = pow(r267870, r267886);
        double r267894 = 0.004166666666666624;
        double r267895 = 5.0;
        double r267896 = pow(r267870, r267895);
        double r267897 = 0.5;
        double r267898 = r267897 * r267870;
        double r267899 = fma(r267894, r267896, r267898);
        double r267900 = fma(r267892, r267893, r267899);
        double r267901 = pow(r267869, r267886);
        double r267902 = r267869 + r267871;
        double r267903 = r267869 * r267869;
        double r267904 = fma(r267871, r267902, r267903);
        double r267905 = r267901 / r267904;
        double r267906 = r267905 / r267873;
        double r267907 = r267877 / r267873;
        double r267908 = r267887 / r267904;
        double r267909 = r267907 * r267908;
        double r267910 = -r267909;
        double r267911 = fma(r267877, r267906, r267910);
        double r267912 = -r267907;
        double r267913 = fma(r267912, r267908, r267909);
        double r267914 = r267911 + r267913;
        double r267915 = r267891 ? r267900 : r267914;
        double r267916 = r267876 ? r267889 : r267915;
        return r267916;
}

Error

Bits error versus x

Target

Original	30.1
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.010762932450266787

   1. Initial program 0.9

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

   3. Applied add-log-exp 1.0

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

   5. Applied flip3-- 1.1

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

   6. Simplified 1.1

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

   8. Applied div-sub 1.1

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

   9. Applied div-sub 1.2

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

   10. Applied exp-diff 1.3

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

   11. Applied log-div 1.1

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

   12. Simplified 1.1

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

   13. Simplified 1.0

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

   14. Taylor expanded around -inf 1.0

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

   if -0.010762932450266787 < (/ (- 1.0 (cos x)) (sin x)) < 0.00043298603204685633

   1. Initial program 59.8

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

   3. Applied add-log-exp 59.8

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

   5. Applied flip3-- 59.8

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

   6. Simplified 59.8

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

   7. Taylor expanded around 0 0.3

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

   8. Simplified 0.3

      \[\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.00043298603204685633 < (/ (- 1.0 (cos x)) (sin x))

   1. Initial program 1.0

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

   3. Applied add-log-exp 1.0

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

   5. Applied flip3-- 1.2

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

   6. Simplified 1.2

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

   8. Applied div-sub 1.2

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

   9. Applied div-sub 1.2

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

   10. Applied exp-diff 1.2

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

   11. Applied log-div 1.2

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

   12. Simplified 1.2

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

   13. Simplified 1.1

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

   15. Applied div-inv 1.2

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

   16. Applied *-un-lft-identity 1.2

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

   17. Applied *-un-lft-identity 1.2

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

   18. Applied *-un-lft-identity 1.2

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

   19. Applied unpow-prod-down 1.2

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

   20. Applied times-frac 1.2

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

   21. Applied times-frac 1.2

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

   22. Applied prod-diff 1.2

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

   23. Simplified 1.2

       \[\leadsto \color{blue}{\mathsf{fma}\left(1, \frac{\frac{{1}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}}{\sin x}, -\frac{1}{\sin x} \cdot \frac{{\left(\cos x\right)}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}\right)} + \mathsf{fma}\left(-\frac{1}{\sin x}, \frac{{\left(\cos x\right)}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}, \frac{1}{\sin x} \cdot \frac{{\left(\cos x\right)}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\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.0107629324502667868:\\ \;\;\;\;1 \cdot \frac{1}{\sin x \cdot \left({\left(\cos x\right)}^{2} + \left(1 \cdot \cos x + 1\right)\right)} - \frac{{\left(\cos x\right)}^{3}}{\sin x \cdot \left({\left(\cos x\right)}^{2} + \left(1 \cdot \cos x + 1\right)\right)}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le 4.3298603204685633 \cdot 10^{-4}:\\ \;\;\;\;\mathsf{fma}\left(0.04166666666666663, {x}^{3}, \mathsf{fma}\left(0.004166666666666624, {x}^{5}, 0.5 \cdot x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(1, \frac{\frac{{1}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}}{\sin x}, -\frac{1}{\sin x} \cdot \frac{{\left(\cos x\right)}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}\right) + \mathsf{fma}\left(-\frac{1}{\sin x}, \frac{{\left(\cos x\right)}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}, \frac{1}{\sin x} \cdot \frac{{\left(\cos x\right)}^{3}}{\mathsf{fma}\left(\cos x, 1 + \cos x, 1 \cdot 1\right)}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020056 +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)))