\[\tan \left(x + \varepsilon\right) - \tan x\]

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -4.2497976182633953 \cdot 10^{-14}:\\ \;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{1}{1 - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)}, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \le 2.1114736186435238 \cdot 10^{-119}:\\ \;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \end{array}\]

\tan \left(x + \varepsilon\right) - \tan x

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -4.2497976182633953 \cdot 10^{-14}:\\
\;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{1}{1 - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)}, -\tan x\right)\\

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

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

\end{array}

double f(double x, double eps) {
        double r156495 = x;
        double r156496 = eps;
        double r156497 = r156495 + r156496;
        double r156498 = tan(r156497);
        double r156499 = tan(r156495);
        double r156500 = r156498 - r156499;
        return r156500;
}

↓

double f(double x, double eps) {
        double r156501 = eps;
        double r156502 = -4.2497976182633953e-14;
        bool r156503 = r156501 <= r156502;
        double r156504 = x;
        double r156505 = tan(r156504);
        double r156506 = tan(r156501);
        double r156507 = r156505 + r156506;
        double r156508 = 1.0;
        double r156509 = r156505 * r156506;
        double r156510 = exp(r156509);
        double r156511 = log(r156510);
        double r156512 = r156508 - r156511;
        double r156513 = r156508 / r156512;
        double r156514 = -r156505;
        double r156515 = fma(r156507, r156513, r156514);
        double r156516 = 2.1114736186435238e-119;
        bool r156517 = r156501 <= r156516;
        double r156518 = r156504 * r156501;
        double r156519 = r156504 + r156501;
        double r156520 = fma(r156518, r156519, r156501);
        double r156521 = cos(r156504);
        double r156522 = r156507 * r156521;
        double r156523 = r156508 - r156509;
        double r156524 = sin(r156504);
        double r156525 = r156523 * r156524;
        double r156526 = r156522 - r156525;
        double r156527 = r156523 * r156521;
        double r156528 = r156526 / r156527;
        double r156529 = r156517 ? r156520 : r156528;
        double r156530 = r156503 ? r156515 : r156529;
        return r156530;
}

Original	36.9
Target	15.1
Herbie	15.8

Derivation

Split input into 3 regimes
if eps < -4.2497976182633953e-14
1. Initial program 29.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum0.8
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied div-inv0.8
  \[\leadsto \color{blue}{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
6. Applied fma-neg0.8
  \[\leadsto \color{blue}{\mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{1}{1 - \tan x \cdot \tan \varepsilon}, -\tan x\right)}\]
7. Using strategy rm
8. Applied add-log-exp0.9
  \[\leadsto \mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{1}{1 - \color{blue}{\log \left(e^{\tan x \cdot \tan \varepsilon}\right)}}, -\tan x\right)\]
if -4.2497976182633953e-14 < eps < 2.1114736186435238e-119
1. Initial program 46.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum46.3
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied div-inv46.3
  \[\leadsto \color{blue}{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
6. Applied fma-neg46.3
  \[\leadsto \color{blue}{\mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{1}{1 - \tan x \cdot \tan \varepsilon}, -\tan x\right)}\]
7. Using strategy rm
8. Applied add-log-exp46.3
  \[\leadsto \mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{1}{1 - \color{blue}{\log \left(e^{\tan x \cdot \tan \varepsilon}\right)}}, -\tan x\right)\]
9. Taylor expanded around 0 31.1
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
10. Simplified30.9
  \[\leadsto \color{blue}{\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)}\]
if 2.1114736186435238e-119 < eps
1. Initial program 31.5
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-quot31.4
  \[\leadsto \tan \left(x + \varepsilon\right) - \color{blue}{\frac{\sin x}{\cos x}}\]
4. Applied tan-sum10.0
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \frac{\sin x}{\cos x}\]
5. Applied frac-sub10.1
  \[\leadsto \color{blue}{\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}}\]
Recombined 3 regimes into one program.
Final simplification15.8
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -4.2497976182633953 \cdot 10^{-14}:\\ \;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{1}{1 - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)}, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \le 2.1114736186435238 \cdot 10^{-119}:\\ \;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \end{array}\]

Error

Target

Derivation

`if eps < -4.2497976182633953e-14`

`if -4.2497976182633953e-14 < eps < 2.1114736186435238e-119`

`if 2.1114736186435238e-119 < eps`

Reproduce