Average Error: 36.9 → 15.2
Time: 33.0s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.026001680385522531129045443270932914202 \cdot 10^{-44}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, \left(\tan x \cdot \tan \varepsilon + \frac{\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\right) + 1, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \le 2.292531808674073827691883868428785214333 \cdot 10^{-46}:\\ \;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, \left(\tan x \cdot \tan \varepsilon + \frac{\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\right) + 1, -\tan x\right)\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -1.026001680385522531129045443270932914202 \cdot 10^{-44}:\\
\;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, \left(\tan x \cdot \tan \varepsilon + \frac{\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\right) + 1, -\tan x\right)\\

\mathbf{elif}\;\varepsilon \le 2.292531808674073827691883868428785214333 \cdot 10^{-46}:\\
\;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, \left(\tan x \cdot \tan \varepsilon + \frac{\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\right) + 1, -\tan x\right)\\

\end{array}
double f(double x, double eps) {
        double r4607352 = x;
        double r4607353 = eps;
        double r4607354 = r4607352 + r4607353;
        double r4607355 = tan(r4607354);
        double r4607356 = tan(r4607352);
        double r4607357 = r4607355 - r4607356;
        return r4607357;
}

double f(double x, double eps) {
        double r4607358 = eps;
        double r4607359 = -1.0260016803855225e-44;
        bool r4607360 = r4607358 <= r4607359;
        double r4607361 = tan(r4607358);
        double r4607362 = x;
        double r4607363 = tan(r4607362);
        double r4607364 = r4607361 + r4607363;
        double r4607365 = 1.0;
        double r4607366 = sin(r4607358);
        double r4607367 = sin(r4607362);
        double r4607368 = r4607366 * r4607367;
        double r4607369 = r4607368 * r4607368;
        double r4607370 = r4607369 * r4607368;
        double r4607371 = cos(r4607362);
        double r4607372 = cos(r4607358);
        double r4607373 = r4607371 * r4607372;
        double r4607374 = r4607373 * r4607373;
        double r4607375 = r4607374 * r4607373;
        double r4607376 = r4607370 / r4607375;
        double r4607377 = r4607365 - r4607376;
        double r4607378 = r4607364 / r4607377;
        double r4607379 = r4607363 * r4607361;
        double r4607380 = r4607369 / r4607374;
        double r4607381 = r4607379 + r4607380;
        double r4607382 = r4607381 + r4607365;
        double r4607383 = -r4607363;
        double r4607384 = fma(r4607378, r4607382, r4607383);
        double r4607385 = 2.292531808674074e-46;
        bool r4607386 = r4607358 <= r4607385;
        double r4607387 = r4607362 * r4607358;
        double r4607388 = r4607362 + r4607358;
        double r4607389 = fma(r4607387, r4607388, r4607358);
        double r4607390 = r4607386 ? r4607389 : r4607384;
        double r4607391 = r4607360 ? r4607384 : r4607390;
        return r4607391;
}

Error

Bits error versus x

Bits error versus eps

Target

Original36.9
Target15.3
Herbie15.2
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 2 regimes
  2. if eps < -1.0260016803855225e-44 or 2.292531808674074e-46 < eps

    1. Initial program 30.1

      \[\tan \left(x + \varepsilon\right) - \tan x\]
    2. Using strategy rm
    3. Applied tan-sum3.5

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
    4. Using strategy rm
    5. Applied flip3--3.5

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)}}} - \tan x\]
    6. Applied associate-/r/3.5

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right)} - \tan x\]
    7. Applied fma-neg3.5

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \tan \varepsilon\right)}^{3}}, 1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)}\]
    8. Using strategy rm
    9. Applied tan-quot3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}\right)}^{3}}, 1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    10. Applied tan-quot3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\color{blue}{\frac{\sin x}{\cos x}} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)}^{3}}, 1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    11. Applied frac-times3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\color{blue}{\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right)}}^{3}}, 1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    12. Applied cube-div3.6

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \color{blue}{\frac{{\left(\sin x \cdot \sin \varepsilon\right)}^{3}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}}}, 1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    13. Simplified3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \frac{\color{blue}{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}}{{\left(\cos x \cdot \cos \varepsilon\right)}^{3}}}, 1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    14. Simplified3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\color{blue}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}}, 1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    15. Using strategy rm
    16. Applied tan-quot3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, 1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    17. Applied tan-quot3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, 1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\color{blue}{\frac{\sin x}{\cos x}} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    18. Applied frac-times3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, 1 \cdot 1 + \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \color{blue}{\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    19. Applied tan-quot3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, 1 \cdot 1 + \left(\left(\tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}\right) \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    20. Applied tan-quot3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, 1 \cdot 1 + \left(\left(\color{blue}{\frac{\sin x}{\cos x}} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    21. Applied frac-times3.5

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{{1}^{3} - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, 1 \cdot 1 + \left(\color{blue}{\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1 \cdot \left(\tan x \cdot \tan \varepsilon\right)\right), -\tan x\right)\]
    22. Applied frac-times3.5

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

    if -1.0260016803855225e-44 < eps < 2.292531808674074e-46

    1. Initial program 46.2

      \[\tan \left(x + \varepsilon\right) - \tan x\]
    2. Taylor expanded around 0 31.3

      \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
    3. Simplified31.1

      \[\leadsto \color{blue}{\mathsf{fma}\left(x \cdot \varepsilon, \varepsilon + x, \varepsilon\right)}\]
  3. Recombined 2 regimes into one program.
  4. Final simplification15.2

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.026001680385522531129045443270932914202 \cdot 10^{-44}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, \left(\tan x \cdot \tan \varepsilon + \frac{\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\right) + 1, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \le 2.292531808674073827691883868428785214333 \cdot 10^{-46}:\\ \;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}}, \left(\tan x \cdot \tan \varepsilon + \frac{\left(\sin \varepsilon \cdot \sin x\right) \cdot \left(\sin \varepsilon \cdot \sin x\right)}{\left(\cos x \cdot \cos \varepsilon\right) \cdot \left(\cos x \cdot \cos \varepsilon\right)}\right) + 1, -\tan x\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019169 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))