tanhf (example 3.4)

Average Error: 30.2 → 0.7

Time: 19.9s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r48296 = 1.0;
        double r48297 = x;
        double r48298 = cos(r48297);
        double r48299 = r48296 - r48298;
        double r48300 = sin(r48297);
        double r48301 = r48299 / r48300;
        return r48301;
}

↓

double f(double x) {
        double r48302 = 1.0;
        double r48303 = x;
        double r48304 = cos(r48303);
        double r48305 = r48302 - r48304;
        double r48306 = sin(r48303);
        double r48307 = r48305 / r48306;
        double r48308 = -0.014198217077059884;
        bool r48309 = r48307 <= r48308;
        double r48310 = 3.0;
        double r48311 = pow(r48302, r48310);
        double r48312 = r48304 * r48304;
        double r48313 = r48304 * r48312;
        double r48314 = r48311 - r48313;
        double r48315 = r48302 + r48304;
        double r48316 = r48304 * r48315;
        double r48317 = r48302 * r48302;
        double r48318 = r48316 + r48317;
        double r48319 = r48314 / r48318;
        double r48320 = log(r48319);
        double r48321 = exp(r48320);
        double r48322 = r48321 / r48306;
        double r48323 = 2.589932435073377e-05;
        bool r48324 = r48307 <= r48323;
        double r48325 = 0.041666666666666664;
        double r48326 = r48303 * r48325;
        double r48327 = r48303 * r48326;
        double r48328 = 0.5;
        double r48329 = r48327 + r48328;
        double r48330 = r48329 * r48303;
        double r48331 = 5.0;
        double r48332 = pow(r48303, r48331);
        double r48333 = 0.004166666666666667;
        double r48334 = r48332 * r48333;
        double r48335 = r48330 + r48334;
        double r48336 = pow(r48304, r48310);
        double r48337 = exp(r48336);
        double r48338 = log(r48337);
        double r48339 = r48311 - r48338;
        double r48340 = r48339 / r48318;
        double r48341 = log(r48340);
        double r48342 = exp(r48341);
        double r48343 = r48342 / r48306;
        double r48344 = r48324 ? r48335 : r48343;
        double r48345 = r48309 ? r48322 : r48344;
        return r48345;
}

Error

Bits error versus x

Target

Original	30.2
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.014198217077059884

   1. Initial program 0.8

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

   3. Applied flip3-- 0.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 0.9

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

   6. Applied add-exp-log 0.9

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

   7. Applied add-exp-log 0.9

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

   8. Applied div-exp 1.0

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

   9. Simplified 0.9

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

   11. Applied add-cbrt-cube 1.2

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

   12. Applied rem-cube-cbrt 0.9

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

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

   1. Initial program 59.8

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

   2. Taylor expanded around 0 0.3

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

   3. Simplified 0.3

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

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

   1. Initial program 1.1

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

   3. Applied flip3-- 1.2

      \[\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.2

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

   6. Applied add-exp-log 1.2

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

   7. Applied add-exp-log 1.2

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

   8. Applied div-exp 1.2

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

   9. Simplified 1.2

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

   11. Applied add-log-exp 1.3

       \[\leadsto \frac{e^{\log \left(\frac{{1}^{3} - \color{blue}{\log \left(e^{{\left(\cos x\right)}^{3}}\right)}}{1 \cdot 1 + \left(\cos x + 1\right) \cdot \cos x}\right)}}{\sin x}\]
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.01419821707705988360348481336359327542596:\\ \;\;\;\;\frac{e^{\log \left(\frac{{1}^{3} - \cos x \cdot \left(\cos x \cdot \cos x\right)}{\cos x \cdot \left(1 + \cos x\right) + 1 \cdot 1}\right)}}{\sin x}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le 2.589932435073376851492402139776061176235 \cdot 10^{-5}:\\ \;\;\;\;\left(x \cdot \left(x \cdot \frac{1}{24}\right) + \frac{1}{2}\right) \cdot x + {x}^{5} \cdot \frac{1}{240}\\ \mathbf{else}:\\ \;\;\;\;\frac{e^{\log \left(\frac{{1}^{3} - \log \left(e^{{\left(\cos x\right)}^{3}}\right)}{\cos x \cdot \left(1 + \cos x\right) + 1 \cdot 1}\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)))