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

↓

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

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -2.62152936434175349 \cdot 10^{-15}:\\
\;\;\;\;\frac{1}{\frac{1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}{\tan x + \tan \varepsilon}} - \tan x\\

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

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

\end{array}

double f(double x, double eps) {
        double r116021 = x;
        double r116022 = eps;
        double r116023 = r116021 + r116022;
        double r116024 = tan(r116023);
        double r116025 = tan(r116021);
        double r116026 = r116024 - r116025;
        return r116026;
}

↓

double f(double x, double eps) {
        double r116027 = eps;
        double r116028 = -2.6215293643417535e-15;
        bool r116029 = r116027 <= r116028;
        double r116030 = 1.0;
        double r116031 = x;
        double r116032 = tan(r116031);
        double r116033 = sin(r116027);
        double r116034 = r116032 * r116033;
        double r116035 = cos(r116027);
        double r116036 = r116034 / r116035;
        double r116037 = r116030 - r116036;
        double r116038 = tan(r116027);
        double r116039 = r116032 + r116038;
        double r116040 = r116037 / r116039;
        double r116041 = r116030 / r116040;
        double r116042 = r116041 - r116032;
        double r116043 = 6.814433610919413e-84;
        bool r116044 = r116027 <= r116043;
        double r116045 = 2.0;
        double r116046 = pow(r116027, r116045);
        double r116047 = pow(r116031, r116045);
        double r116048 = fma(r116027, r116047, r116027);
        double r116049 = fma(r116046, r116031, r116048);
        double r116050 = cos(r116031);
        double r116051 = r116039 * r116050;
        double r116052 = sin(r116031);
        double r116053 = r116037 * r116052;
        double r116054 = r116051 - r116053;
        double r116055 = r116037 * r116050;
        double r116056 = r116054 / r116055;
        double r116057 = r116044 ? r116049 : r116056;
        double r116058 = r116029 ? r116042 : r116057;
        return r116058;
}

Original	36.6
Target	15.0
Herbie	15.1

Derivation

Split input into 3 regimes
if eps < -2.6215293643417535e-15
1. Initial program 29.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum0.7
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot0.7
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
6. Applied associate-*r/0.7
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
7. Using strategy rm
8. Applied clear-num0.8
  \[\leadsto \color{blue}{\frac{1}{\frac{1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}{\tan x + \tan \varepsilon}}} - \tan x\]
if -2.6215293643417535e-15 < eps < 6.814433610919413e-84
1. Initial program 45.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum45.9
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Taylor expanded around 0 30.4
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
5. Simplified30.4
  \[\leadsto \color{blue}{\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)}\]
if 6.814433610919413e-84 < eps
1. Initial program 30.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum6.7
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot6.7
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
6. Applied associate-*r/6.7
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
7. Using strategy rm
8. Applied tan-quot6.7
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}} - \color{blue}{\frac{\sin x}{\cos x}}\]
9. Applied frac-sub6.7
  \[\leadsto \color{blue}{\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right) \cdot \sin x}{\left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right) \cdot \cos x}}\]
Recombined 3 regimes into one program.
Final simplification15.1
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.62152936434175349 \cdot 10^{-15}:\\ \;\;\;\;\frac{1}{\frac{1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}{\tan x + \tan \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 6.8144336109194134 \cdot 10^{-84}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right) \cdot \sin x}{\left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right) \cdot \cos x}\\ \end{array}\]

Error

Target

Derivation

`if eps < -2.6215293643417535e-15`

`if -2.6215293643417535e-15 < eps < 6.814433610919413e-84`

`if 6.814433610919413e-84 < eps`

Reproduce