tanhf (example 3.4)

Average Error: 30.2 → 0.6

Time: 24.6s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r4859568 = 1.0;
        double r4859569 = x;
        double r4859570 = cos(r4859569);
        double r4859571 = r4859568 - r4859570;
        double r4859572 = sin(r4859569);
        double r4859573 = r4859571 / r4859572;
        return r4859573;
}

↓

double f(double x) {
        double r4859574 = x;
        double r4859575 = -0.02266404857182586;
        bool r4859576 = r4859574 <= r4859575;
        double r4859577 = 1.0;
        double r4859578 = r4859577 * r4859577;
        double r4859579 = r4859577 * r4859578;
        double r4859580 = cos(r4859574);
        double r4859581 = r4859580 * r4859580;
        double r4859582 = r4859580 * r4859581;
        double r4859583 = r4859579 - r4859582;
        double r4859584 = r4859577 + r4859580;
        double r4859585 = r4859580 * r4859584;
        double r4859586 = r4859585 + r4859578;
        double r4859587 = sin(r4859574);
        double r4859588 = r4859586 * r4859587;
        double r4859589 = r4859583 / r4859588;
        double r4859590 = exp(r4859589);
        double r4859591 = log(r4859590);
        double r4859592 = 0.021092325268080338;
        bool r4859593 = r4859574 <= r4859592;
        double r4859594 = 0.5;
        double r4859595 = r4859594 * r4859574;
        double r4859596 = r4859574 * r4859574;
        double r4859597 = r4859596 * r4859574;
        double r4859598 = 0.04166666666666663;
        double r4859599 = r4859597 * r4859598;
        double r4859600 = 0.004166666666666624;
        double r4859601 = 5.0;
        double r4859602 = pow(r4859574, r4859601);
        double r4859603 = r4859600 * r4859602;
        double r4859604 = r4859599 + r4859603;
        double r4859605 = r4859595 + r4859604;
        double r4859606 = 0.5;
        double r4859607 = r4859580 * r4859606;
        double r4859608 = r4859579 - r4859607;
        double r4859609 = 2.0;
        double r4859610 = r4859609 * r4859574;
        double r4859611 = cos(r4859610);
        double r4859612 = r4859606 * r4859611;
        double r4859613 = exp(r4859612);
        double r4859614 = log(r4859613);
        double r4859615 = r4859614 * r4859580;
        double r4859616 = r4859608 - r4859615;
        double r4859617 = r4859577 * r4859580;
        double r4859618 = r4859581 + r4859617;
        double r4859619 = r4859578 + r4859618;
        double r4859620 = r4859616 / r4859619;
        double r4859621 = r4859620 / r4859587;
        double r4859622 = r4859593 ? r4859605 : r4859621;
        double r4859623 = r4859576 ? r4859591 : r4859622;
        return r4859623;
}

Error

Bits error versus x

Target

Original	30.2
Target	0.0
Herbie	0.6

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

Derivation

1. Split input into 3 regimes

2. if x < -0.02266404857182586

   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. Applied associate-/l/ 1.0

      \[\leadsto \color{blue}{\frac{{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)}}\]

   5. Simplified 1.0

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

   7. Applied add-log-exp 1.3

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

   8. Simplified 1.2

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

   if -0.02266404857182586 < x < 0.021092325268080338

   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. Applied associate-/l/ 59.9

      \[\leadsto \color{blue}{\frac{{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)}}\]

   5. Simplified 59.9

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

   6. 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)}\]

   7. Simplified 0.0

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

   if 0.021092325268080338 < 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.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 add-log-exp 1.1

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

   8. Applied sqr-cos 1.0

      \[\leadsto \frac{\frac{1 \cdot \left(1 \cdot 1\right) - \cos x \cdot \log \left(e^{\color{blue}{\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}\]

   9. Applied exp-sum 1.0

      \[\leadsto \frac{\frac{1 \cdot \left(1 \cdot 1\right) - \cos x \cdot \log \color{blue}{\left(e^{\frac{1}{2}} \cdot e^{\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}\]

   10. Applied log-prod 0.9

       \[\leadsto \frac{\frac{1 \cdot \left(1 \cdot 1\right) - \cos x \cdot \color{blue}{\left(\log \left(e^{\frac{1}{2}}\right) + \log \left(e^{\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}\]

   11. Applied distribute-rgt-in 0.9

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

   12. Applied associate--r+ 1.0

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

   13. Simplified 1.0

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

4. Final simplification 0.6

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

Reproduce

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

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

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