tanhf (example 3.4)

Average Error: 30.0 → 0.5

Time: 30.1s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -0.01968992941986992192826555481133254943416:\\ \;\;\;\;\frac{\frac{\left(1 \cdot \left(1 \cdot 1\right) - \cos x \cdot \frac{1}{2}\right) - \cos x \cdot \left(\frac{1}{2} \cdot \cos \left(2 \cdot x\right)\right)}{1 \cdot 1 + \frac{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\left(\cos x \cdot \cos x\right) \cdot \cos x + 1 \cdot \left(1 \cdot 1\right)\right)}{\left(1 \cdot \cos x\right) \cdot \left(1 \cdot \cos x - \cos x \cdot \cos x\right) + \left(\cos x \cdot \cos x\right) \cdot \left(\left(\sqrt[3]{\cos x \cdot \cos x} \cdot \sqrt[3]{\cos x \cdot \cos x}\right) \cdot \sqrt[3]{\cos x \cdot \cos x}\right)}}}{\sin x}\\ \mathbf{elif}\;x \le 0.01864714034028851566415774243523628683761:\\ \;\;\;\;0.5 \cdot x + \left(0.004166666666666624108117389368999283760786 \cdot {x}^{5} + \left(\left(x \cdot x\right) \cdot x\right) \cdot 0.04166666666666662965923251249478198587894\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(1 \cdot \left(1 \cdot 1\right) - \cos x \cdot \frac{1}{2}\right) - \cos x \cdot \left(\frac{1}{2} \cdot \cos \left(2 \cdot x\right)\right)}{\sin x \cdot \left(1 \cdot 1 + \cos x \cdot \left(\cos x + 1\right)\right)}\\ \end{array}\]

C

double f(double x) {
        double r5835846 = 1.0;
        double r5835847 = x;
        double r5835848 = cos(r5835847);
        double r5835849 = r5835846 - r5835848;
        double r5835850 = sin(r5835847);
        double r5835851 = r5835849 / r5835850;
        return r5835851;
}

↓

double f(double x) {
        double r5835852 = x;
        double r5835853 = -0.019689929419869922;
        bool r5835854 = r5835852 <= r5835853;
        double r5835855 = 1.0;
        double r5835856 = r5835855 * r5835855;
        double r5835857 = r5835855 * r5835856;
        double r5835858 = cos(r5835852);
        double r5835859 = 0.5;
        double r5835860 = r5835858 * r5835859;
        double r5835861 = r5835857 - r5835860;
        double r5835862 = 2.0;
        double r5835863 = r5835862 * r5835852;
        double r5835864 = cos(r5835863);
        double r5835865 = r5835859 * r5835864;
        double r5835866 = r5835858 * r5835865;
        double r5835867 = r5835861 - r5835866;
        double r5835868 = r5835858 * r5835858;
        double r5835869 = r5835868 * r5835858;
        double r5835870 = r5835869 + r5835857;
        double r5835871 = r5835869 * r5835870;
        double r5835872 = r5835855 * r5835858;
        double r5835873 = r5835872 - r5835868;
        double r5835874 = r5835872 * r5835873;
        double r5835875 = cbrt(r5835868);
        double r5835876 = r5835875 * r5835875;
        double r5835877 = r5835876 * r5835875;
        double r5835878 = r5835868 * r5835877;
        double r5835879 = r5835874 + r5835878;
        double r5835880 = r5835871 / r5835879;
        double r5835881 = r5835856 + r5835880;
        double r5835882 = r5835867 / r5835881;
        double r5835883 = sin(r5835852);
        double r5835884 = r5835882 / r5835883;
        double r5835885 = 0.018647140340288516;
        bool r5835886 = r5835852 <= r5835885;
        double r5835887 = 0.5;
        double r5835888 = r5835887 * r5835852;
        double r5835889 = 0.004166666666666624;
        double r5835890 = 5.0;
        double r5835891 = pow(r5835852, r5835890);
        double r5835892 = r5835889 * r5835891;
        double r5835893 = r5835852 * r5835852;
        double r5835894 = r5835893 * r5835852;
        double r5835895 = 0.04166666666666663;
        double r5835896 = r5835894 * r5835895;
        double r5835897 = r5835892 + r5835896;
        double r5835898 = r5835888 + r5835897;
        double r5835899 = r5835858 + r5835855;
        double r5835900 = r5835858 * r5835899;
        double r5835901 = r5835856 + r5835900;
        double r5835902 = r5835883 * r5835901;
        double r5835903 = r5835867 / r5835902;
        double r5835904 = r5835886 ? r5835898 : r5835903;
        double r5835905 = r5835854 ? r5835884 : r5835904;
        return r5835905;
}

Error

Bits error versus x

Target

Original	30.0
Target	0.0
Herbie	0.5

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

Derivation

1. Split input into 3 regimes

2. if x < -0.019689929419869922

   1. Initial program 0.9

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

   3. Applied flip3-- 1.1

      \[\leadsto \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}\]

   4. Simplified 1.0

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

   6. Applied sqr-cos 1.0

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

   7. Applied distribute-lft-in 1.0

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

   8. Applied associate--r+ 1.0

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

   10. Applied flip3-+ 1.0

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

   11. Simplified 1.0

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

   12. Simplified 1.0

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

   14. Applied add-cube-cbrt 1.1

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

   if -0.019689929419869922 < x < 0.018647140340288516

   1. Initial program 59.9

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

   3. Applied flip3-- 59.9

      \[\leadsto \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}\]

   4. Simplified 59.9

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

   6. Applied sqr-cos 59.9

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

   7. Applied distribute-lft-in 59.9

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

   8. Applied associate--r+ 59.8

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

   9. Taylor expanded around 0 0.0

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

   10. Simplified 0.0

       \[\leadsto \color{blue}{0.5 \cdot x + \left(0.004166666666666624108117389368999283760786 \cdot {x}^{5} + \left(\left(x \cdot x\right) \cdot x\right) \cdot 0.04166666666666662965923251249478198587894\right)}\]

   if 0.018647140340288516 < x

   1. Initial program 0.9

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

   3. Applied flip3-- 1.0

      \[\leadsto \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}\]

   4. Simplified 1.1

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

   6. Applied sqr-cos 0.9

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

   7. Applied distribute-lft-in 0.9

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

   8. Applied associate--r+ 0.9

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

   10. Applied div-inv 1.0

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

   11. Applied associate-/l* 1.0

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

   12. Simplified 1.0

       \[\leadsto \frac{\left(1 \cdot \left(1 \cdot 1\right) - \cos x \cdot \frac{1}{2}\right) - \cos x \cdot \left(\frac{1}{2} \cdot \cos \left(2 \cdot x\right)\right)}{\color{blue}{\sin x \cdot \left(1 \cdot 1 + \cos x \cdot \left(\cos x + 1\right)\right)}}\]
3. Recombined 3 regimes into one program.

4. Final simplification 0.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -0.01968992941986992192826555481133254943416:\\ \;\;\;\;\frac{\frac{\left(1 \cdot \left(1 \cdot 1\right) - \cos x \cdot \frac{1}{2}\right) - \cos x \cdot \left(\frac{1}{2} \cdot \cos \left(2 \cdot x\right)\right)}{1 \cdot 1 + \frac{\left(\left(\cos x \cdot \cos x\right) \cdot \cos x\right) \cdot \left(\left(\cos x \cdot \cos x\right) \cdot \cos x + 1 \cdot \left(1 \cdot 1\right)\right)}{\left(1 \cdot \cos x\right) \cdot \left(1 \cdot \cos x - \cos x \cdot \cos x\right) + \left(\cos x \cdot \cos x\right) \cdot \left(\left(\sqrt[3]{\cos x \cdot \cos x} \cdot \sqrt[3]{\cos x \cdot \cos x}\right) \cdot \sqrt[3]{\cos x \cdot \cos x}\right)}}}{\sin x}\\ \mathbf{elif}\;x \le 0.01864714034028851566415774243523628683761:\\ \;\;\;\;0.5 \cdot x + \left(0.004166666666666624108117389368999283760786 \cdot {x}^{5} + \left(\left(x \cdot x\right) \cdot x\right) \cdot 0.04166666666666662965923251249478198587894\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(1 \cdot \left(1 \cdot 1\right) - \cos x \cdot \frac{1}{2}\right) - \cos x \cdot \left(\frac{1}{2} \cdot \cos \left(2 \cdot x\right)\right)}{\sin x \cdot \left(1 \cdot 1 + \cos x \cdot \left(\cos x + 1\right)\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2019173 
(FPCore (x)
  :name "tanhf (example 3.4)"
  :herbie-expected 2

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

  (/ (- 1.0 (cos x)) (sin x)))