tanhf (example 3.4)

Average Error: 30.7 → 0.5

Time: 17.9s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -0.02298820551471121229059058066468423930928 \lor \neg \left(x \le 0.01805643764531137188122933423528593266383\right):\\ \;\;\;\;\left(1 - \cos x\right) \cdot {\left(\sin x\right)}^{-1}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2} \cdot x + \left({x}^{3} \cdot \frac{1}{24} + {x}^{5} \cdot \frac{1}{240}\right)\\ \end{array}\]

C

double f(double x) {
        double r31588 = 1.0;
        double r31589 = x;
        double r31590 = cos(r31589);
        double r31591 = r31588 - r31590;
        double r31592 = sin(r31589);
        double r31593 = r31591 / r31592;
        return r31593;
}

↓

double f(double x) {
        double r31594 = x;
        double r31595 = -0.022988205514711212;
        bool r31596 = r31594 <= r31595;
        double r31597 = 0.018056437645311372;
        bool r31598 = r31594 <= r31597;
        double r31599 = !r31598;
        bool r31600 = r31596 || r31599;
        double r31601 = 1.0;
        double r31602 = cos(r31594);
        double r31603 = r31601 - r31602;
        double r31604 = sin(r31594);
        double r31605 = -1.0;
        double r31606 = pow(r31604, r31605);
        double r31607 = r31603 * r31606;
        double r31608 = 0.5;
        double r31609 = r31608 * r31594;
        double r31610 = 3.0;
        double r31611 = pow(r31594, r31610);
        double r31612 = 0.041666666666666664;
        double r31613 = r31611 * r31612;
        double r31614 = 5.0;
        double r31615 = pow(r31594, r31614);
        double r31616 = 0.004166666666666667;
        double r31617 = r31615 * r31616;
        double r31618 = r31613 + r31617;
        double r31619 = r31609 + r31618;
        double r31620 = r31600 ? r31607 : r31619;
        return r31620;
}

Error

Bits error versus x

Target

Original	30.7
Target	0.0
Herbie	0.5

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

Derivation

1. Split input into 2 regimes

2. if x < -0.022988205514711212 or 0.018056437645311372 < x

   1. Initial program 0.9

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

   3. Applied *-un-lft-identity 0.9

      \[\leadsto \frac{1 - \cos x}{\color{blue}{1 \cdot \sin x}}\]

   4. Applied *-un-lft-identity 0.9

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

   5. Applied times-frac 0.9

      \[\leadsto \color{blue}{\frac{1}{1} \cdot \frac{1 - \cos x}{\sin x}}\]

   6. Simplified 0.9

      \[\leadsto \color{blue}{1} \cdot \frac{1 - \cos x}{\sin x}\]
   7. Using strategy rm

   8. Applied add-log-exp 1.0

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

   10. Applied div-inv 1.1

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

   11. Applied exp-prod 1.3

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

   12. Applied log-pow 1.2

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

   13. Simplified 1.0

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

   15. Applied inv-pow 1.0

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

   if -0.022988205514711212 < x < 0.018056437645311372

   1. Initial program 59.8

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

   3. Applied *-un-lft-identity 59.8

      \[\leadsto \frac{1 - \cos x}{\color{blue}{1 \cdot \sin x}}\]

   4. Applied *-un-lft-identity 59.8

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

   5. Applied times-frac 59.8

      \[\leadsto \color{blue}{\frac{1}{1} \cdot \frac{1 - \cos x}{\sin x}}\]

   6. Simplified 59.8

      \[\leadsto \color{blue}{1} \cdot \frac{1 - \cos x}{\sin x}\]
   7. Using strategy rm

   8. Applied add-log-exp 59.8

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

   10. Applied div-inv 59.9

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

   11. Applied exp-prod 59.9

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

   12. Applied log-pow 59.9

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

   13. Simplified 59.9

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

   14. Taylor expanded around 0 0.0

       \[\leadsto 1 \cdot \color{blue}{\left(\frac{1}{2} \cdot x + \left(\frac{1}{24} \cdot {x}^{3} + \frac{1}{240} \cdot {x}^{5}\right)\right)}\]

   15. Simplified 0.0

       \[\leadsto 1 \cdot \color{blue}{\left(\left({x}^{3} \cdot \frac{1}{24} + {x}^{5} \cdot \frac{1}{240}\right) + \frac{1}{2} \cdot x\right)}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -0.02298820551471121229059058066468423930928 \lor \neg \left(x \le 0.01805643764531137188122933423528593266383\right):\\ \;\;\;\;\left(1 - \cos x\right) \cdot {\left(\sin x\right)}^{-1}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2} \cdot x + \left({x}^{3} \cdot \frac{1}{24} + {x}^{5} \cdot \frac{1}{240}\right)\\ \end{array}\]

Reproduce

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

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

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