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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.80364681435499689 \cdot 10^{-54} \lor \neg \left(\varepsilon \le 5.66748466896461997 \cdot 10^{-20}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}}, 1 + \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}, -\tan x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -1.80364681435499689 \cdot 10^{-54} \lor \neg \left(\varepsilon \le 5.66748466896461997 \cdot 10^{-20}\right):\\
\;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}}, 1 + \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}, -\tan x\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\

\end{array}

double f(double x, double eps) {
        double r166380 = x;
        double r166381 = eps;
        double r166382 = r166380 + r166381;
        double r166383 = tan(r166382);
        double r166384 = tan(r166380);
        double r166385 = r166383 - r166384;
        return r166385;
}

↓

double f(double x, double eps) {
        double r166386 = eps;
        double r166387 = -1.803646814354997e-54;
        bool r166388 = r166386 <= r166387;
        double r166389 = 5.66748466896462e-20;
        bool r166390 = r166386 <= r166389;
        double r166391 = !r166390;
        bool r166392 = r166388 || r166391;
        double r166393 = x;
        double r166394 = tan(r166393);
        double r166395 = tan(r166386);
        double r166396 = r166394 + r166395;
        double r166397 = 1.0;
        double r166398 = sin(r166393);
        double r166399 = sin(r166386);
        double r166400 = r166398 * r166399;
        double r166401 = cos(r166386);
        double r166402 = cos(r166393);
        double r166403 = r166401 * r166402;
        double r166404 = r166400 / r166403;
        double r166405 = r166404 * r166404;
        double r166406 = r166397 - r166405;
        double r166407 = r166396 / r166406;
        double r166408 = r166397 + r166404;
        double r166409 = -r166394;
        double r166410 = fma(r166407, r166408, r166409);
        double r166411 = 2.0;
        double r166412 = pow(r166386, r166411);
        double r166413 = pow(r166393, r166411);
        double r166414 = fma(r166386, r166413, r166386);
        double r166415 = fma(r166412, r166393, r166414);
        double r166416 = r166392 ? r166410 : r166415;
        return r166416;
}

Original	36.8
Target	15.2
Herbie	15.1

Derivation

Split input into 2 regimes
if eps < -1.803646814354997e-54 or 5.66748466896462e-20 < eps
1. Initial program 29.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum2.7
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Taylor expanded around inf 2.8
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}}} - \tan x\]
5. Using strategy rm
6. Applied flip--2.8
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{1 \cdot 1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}}{1 + \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}}}} - \tan x\]
7. Applied associate-/r/2.8
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}} \cdot \left(1 + \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} - \tan x\]
8. Applied fma-neg2.8
  \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}}, 1 + \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}, -\tan x\right)}\]
if -1.803646814354997e-54 < eps < 5.66748466896462e-20
1. Initial program 45.7
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 30.9
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
3. Simplified30.9
  \[\leadsto \color{blue}{\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)}\]
Recombined 2 regimes into one program.
Final simplification15.1
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.80364681435499689 \cdot 10^{-54} \lor \neg \left(\varepsilon \le 5.66748466896461997 \cdot 10^{-20}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}}, 1 + \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}, -\tan x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \end{array}\]

Error

Target

Derivation

`if eps < -1.803646814354997e-54 or 5.66748466896462e-20 < eps`

`if -1.803646814354997e-54 < eps < 5.66748466896462e-20`

Reproduce