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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.65536317362885325489970813097382752723 \cdot 10^{-139}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x} \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}}, 1 + \frac{\sin x \cdot \tan \varepsilon}{\cos x}, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \le 1.213878359842027964191432566285721557288 \cdot 10^{-80}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\frac{1 - \left(\sin x \cdot \tan \varepsilon\right) \cdot \frac{1}{\cos x}}{\tan x + \tan \varepsilon}} - \tan x\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -2.65536317362885325489970813097382752723 \cdot 10^{-139}:\\
\;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x} \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}}, 1 + \frac{\sin x \cdot \tan \varepsilon}{\cos x}, -\tan x\right)\\

\mathbf{elif}\;\varepsilon \le 1.213878359842027964191432566285721557288 \cdot 10^{-80}:\\
\;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\

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

\end{array}

double f(double x, double eps) {
        double r118973 = x;
        double r118974 = eps;
        double r118975 = r118973 + r118974;
        double r118976 = tan(r118975);
        double r118977 = tan(r118973);
        double r118978 = r118976 - r118977;
        return r118978;
}

↓

double f(double x, double eps) {
        double r118979 = eps;
        double r118980 = -2.6553631736288533e-139;
        bool r118981 = r118979 <= r118980;
        double r118982 = x;
        double r118983 = tan(r118982);
        double r118984 = tan(r118979);
        double r118985 = r118983 + r118984;
        double r118986 = 1.0;
        double r118987 = sin(r118982);
        double r118988 = r118987 * r118984;
        double r118989 = cos(r118982);
        double r118990 = r118988 / r118989;
        double r118991 = r118990 * r118990;
        double r118992 = r118986 - r118991;
        double r118993 = r118985 / r118992;
        double r118994 = r118986 + r118990;
        double r118995 = -r118983;
        double r118996 = fma(r118993, r118994, r118995);
        double r118997 = 1.213878359842028e-80;
        bool r118998 = r118979 <= r118997;
        double r118999 = 2.0;
        double r119000 = pow(r118979, r118999);
        double r119001 = pow(r118982, r118999);
        double r119002 = fma(r118979, r119001, r118979);
        double r119003 = fma(r119000, r118982, r119002);
        double r119004 = r118986 / r118989;
        double r119005 = r118988 * r119004;
        double r119006 = r118986 - r119005;
        double r119007 = r119006 / r118985;
        double r119008 = r118986 / r119007;
        double r119009 = r119008 - r118983;
        double r119010 = r118998 ? r119003 : r119009;
        double r119011 = r118981 ? r118996 : r119010;
        return r119011;
}

Original	36.5
Target	14.8
Herbie	15.8

Derivation

Split input into 3 regimes
if eps < -2.6553631736288533e-139
1. Initial program 31.6
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum11.0
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot11.0
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x}{\cos x}} \cdot \tan \varepsilon} - \tan x\]
6. Applied associate-*l/11.0
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}} - \tan x\]
7. Using strategy rm
8. Applied flip--11.0
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{1 \cdot 1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x} \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}}{1 + \frac{\sin x \cdot \tan \varepsilon}{\cos x}}}} - \tan x\]
9. Applied associate-/r/11.0
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x} \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}} \cdot \left(1 + \frac{\sin x \cdot \tan \varepsilon}{\cos x}\right)} - \tan x\]
10. Applied fma-neg11.0
  \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x} \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}}, 1 + \frac{\sin x \cdot \tan \varepsilon}{\cos x}, -\tan x\right)}\]
if -2.6553631736288533e-139 < eps < 1.213878359842028e-80
1. Initial program 48.6
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 30.7
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
3. Simplified30.7
  \[\leadsto \color{blue}{\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)}\]
if 1.213878359842028e-80 < eps
1. Initial program 29.8
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum5.9
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot5.9
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x}{\cos x}} \cdot \tan \varepsilon} - \tan x\]
6. Applied associate-*l/5.9
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}} - \tan x\]
7. Using strategy rm
8. Applied div-inv5.9
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\left(\sin x \cdot \tan \varepsilon\right) \cdot \frac{1}{\cos x}}} - \tan x\]
9. Using strategy rm
10. Applied clear-num6.0
  \[\leadsto \color{blue}{\frac{1}{\frac{1 - \left(\sin x \cdot \tan \varepsilon\right) \cdot \frac{1}{\cos x}}{\tan x + \tan \varepsilon}}} - \tan x\]
Recombined 3 regimes into one program.
Final simplification15.8
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.65536317362885325489970813097382752723 \cdot 10^{-139}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \tan \varepsilon}{\cos x} \cdot \frac{\sin x \cdot \tan \varepsilon}{\cos x}}, 1 + \frac{\sin x \cdot \tan \varepsilon}{\cos x}, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \le 1.213878359842027964191432566285721557288 \cdot 10^{-80}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\frac{1 - \left(\sin x \cdot \tan \varepsilon\right) \cdot \frac{1}{\cos x}}{\tan x + \tan \varepsilon}} - \tan x\\ \end{array}\]

Error

Target

Derivation

`if eps < -2.6553631736288533e-139`

`if -2.6553631736288533e-139 < eps < 1.213878359842028e-80`

`if 1.213878359842028e-80 < eps`

Reproduce