tanhf (example 3.4)

Average Error: 30.8 → 0.5

Time: 7.8s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\frac{1 - \cos x}{\sin x} \le -7.381705518837608200402589098132466460811 \cdot 10^{-4}:\\ \;\;\;\;\frac{\log \left(e^{\left(\cos x \cdot \left(\cos x + 1\right) + 1 \cdot 1\right) \cdot \left(1 - \cos x\right)}\right)}{\left(\cos x \cdot \left(\cos x + 1\right) + 1 \cdot 1\right) \cdot \sin x}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le 6.126676536166742739145801843747562998033 \cdot 10^{-5}:\\ \;\;\;\;\frac{1}{24} \cdot {x}^{3} + \left(\frac{1}{240} \cdot {x}^{5} + \frac{1}{2} \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\log \left(e^{{1}^{3} - {\left(\cos x\right)}^{3}}\right)}{\left(\cos x \cdot \frac{{\left(\cos x\right)}^{2} - 1 \cdot 1}{\cos x - 1} + 1 \cdot 1\right) \cdot \sin x}\\ \end{array}\]

C

double f(double x) {
        double r72095 = 1.0;
        double r72096 = x;
        double r72097 = cos(r72096);
        double r72098 = r72095 - r72097;
        double r72099 = sin(r72096);
        double r72100 = r72098 / r72099;
        return r72100;
}

↓

double f(double x) {
        double r72101 = 1.0;
        double r72102 = x;
        double r72103 = cos(r72102);
        double r72104 = r72101 - r72103;
        double r72105 = sin(r72102);
        double r72106 = r72104 / r72105;
        double r72107 = -0.0007381705518837608;
        bool r72108 = r72106 <= r72107;
        double r72109 = r72103 + r72101;
        double r72110 = r72103 * r72109;
        double r72111 = r72101 * r72101;
        double r72112 = r72110 + r72111;
        double r72113 = r72112 * r72104;
        double r72114 = exp(r72113);
        double r72115 = log(r72114);
        double r72116 = r72112 * r72105;
        double r72117 = r72115 / r72116;
        double r72118 = 6.126676536166743e-05;
        bool r72119 = r72106 <= r72118;
        double r72120 = 0.041666666666666664;
        double r72121 = 3.0;
        double r72122 = pow(r72102, r72121);
        double r72123 = r72120 * r72122;
        double r72124 = 0.004166666666666667;
        double r72125 = 5.0;
        double r72126 = pow(r72102, r72125);
        double r72127 = r72124 * r72126;
        double r72128 = 0.5;
        double r72129 = r72128 * r72102;
        double r72130 = r72127 + r72129;
        double r72131 = r72123 + r72130;
        double r72132 = pow(r72101, r72121);
        double r72133 = pow(r72103, r72121);
        double r72134 = r72132 - r72133;
        double r72135 = exp(r72134);
        double r72136 = log(r72135);
        double r72137 = 2.0;
        double r72138 = pow(r72103, r72137);
        double r72139 = r72138 - r72111;
        double r72140 = r72103 - r72101;
        double r72141 = r72139 / r72140;
        double r72142 = r72103 * r72141;
        double r72143 = r72142 + r72111;
        double r72144 = r72143 * r72105;
        double r72145 = r72136 / r72144;
        double r72146 = r72119 ? r72131 : r72145;
        double r72147 = r72108 ? r72117 : r72146;
        return r72147;
}

Error

Bits error versus x

Target

Original	30.8
Target	0.0
Herbie	0.5

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

Derivation

1. Split input into 3 regimes

2. if (/ (- 1.0 (cos x)) (sin x)) < -0.0007381705518837608

   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(\cos x + 1\right) + 1 \cdot 1\right) \cdot \sin x}}\]
   6. Using strategy rm

   7. Applied add-log-exp 1.0

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

   8. Applied add-log-exp 1.0

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

   9. Applied diff-log 1.1

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

   10. Simplified 1.0

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

   12. Applied difference-cubes 1.0

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

   13. Simplified 1.0

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

   if -0.0007381705518837608 < (/ (- 1.0 (cos x)) (sin x)) < 6.126676536166743e-05

   1. Initial program 60.1

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

   2. Taylor expanded around 0 0.0

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

   if 6.126676536166743e-05 < (/ (- 1.0 (cos x)) (sin x))

   1. Initial program 1.0

      \[\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(\cos x + 1\right) + 1 \cdot 1\right) \cdot \sin x}}\]
   6. Using strategy rm

   7. Applied add-log-exp 1.1

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

   8. Applied add-log-exp 1.1

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

   9. Applied diff-log 1.2

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

   10. Simplified 1.1

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

   12. Applied flip-+ 1.1

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

   13. Simplified 1.1

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

4. Final simplification 0.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{1 - \cos x}{\sin x} \le -7.381705518837608200402589098132466460811 \cdot 10^{-4}:\\ \;\;\;\;\frac{\log \left(e^{\left(\cos x \cdot \left(\cos x + 1\right) + 1 \cdot 1\right) \cdot \left(1 - \cos x\right)}\right)}{\left(\cos x \cdot \left(\cos x + 1\right) + 1 \cdot 1\right) \cdot \sin x}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le 6.126676536166742739145801843747562998033 \cdot 10^{-5}:\\ \;\;\;\;\frac{1}{24} \cdot {x}^{3} + \left(\frac{1}{240} \cdot {x}^{5} + \frac{1}{2} \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\log \left(e^{{1}^{3} - {\left(\cos x\right)}^{3}}\right)}{\left(\cos x \cdot \frac{{\left(\cos x\right)}^{2} - 1 \cdot 1}{\cos x - 1} + 1 \cdot 1\right) \cdot \sin x}\\ \end{array}\]

Reproduce

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

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

  (/ (- 1 (cos x)) (sin x)))