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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -8.29565067036897 \cdot 10^{-18}:\\ \;\;\;\;\frac{\tan \varepsilon + \tan x}{\log \left(e^{1 - \tan x \cdot \tan \varepsilon}\right)} - \tan x\\ \mathbf{elif}\;\varepsilon \le 3.143523747535153 \cdot 10^{-69}:\\ \;\;\;\;x \cdot \left(\varepsilon \cdot \left(x + \varepsilon\right)\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan \varepsilon + \tan x\right) \cdot \cos x - \sin x \cdot \left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right)}{\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 -8.29565067036897 \cdot 10^{-18}:\\
\;\;\;\;\frac{\tan \varepsilon + \tan x}{\log \left(e^{1 - \tan x \cdot \tan \varepsilon}\right)} - \tan x\\

\mathbf{elif}\;\varepsilon \le 3.143523747535153 \cdot 10^{-69}:\\
\;\;\;\;x \cdot \left(\varepsilon \cdot \left(x + \varepsilon\right)\right) + \varepsilon\\

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

\end{array}

double f(double x, double eps) {
        double r3333317 = x;
        double r3333318 = eps;
        double r3333319 = r3333317 + r3333318;
        double r3333320 = tan(r3333319);
        double r3333321 = tan(r3333317);
        double r3333322 = r3333320 - r3333321;
        return r3333322;
}

↓

double f(double x, double eps) {
        double r3333323 = eps;
        double r3333324 = -8.29565067036897e-18;
        bool r3333325 = r3333323 <= r3333324;
        double r3333326 = tan(r3333323);
        double r3333327 = x;
        double r3333328 = tan(r3333327);
        double r3333329 = r3333326 + r3333328;
        double r3333330 = 1.0;
        double r3333331 = r3333328 * r3333326;
        double r3333332 = r3333330 - r3333331;
        double r3333333 = exp(r3333332);
        double r3333334 = log(r3333333);
        double r3333335 = r3333329 / r3333334;
        double r3333336 = r3333335 - r3333328;
        double r3333337 = 3.143523747535153e-69;
        bool r3333338 = r3333323 <= r3333337;
        double r3333339 = r3333327 + r3333323;
        double r3333340 = r3333323 * r3333339;
        double r3333341 = r3333327 * r3333340;
        double r3333342 = r3333341 + r3333323;
        double r3333343 = cos(r3333327);
        double r3333344 = r3333329 * r3333343;
        double r3333345 = sin(r3333327);
        double r3333346 = sin(r3333323);
        double r3333347 = r3333328 * r3333346;
        double r3333348 = cos(r3333323);
        double r3333349 = r3333347 / r3333348;
        double r3333350 = r3333330 - r3333349;
        double r3333351 = r3333345 * r3333350;
        double r3333352 = r3333344 - r3333351;
        double r3333353 = r3333350 * r3333343;
        double r3333354 = r3333352 / r3333353;
        double r3333355 = r3333338 ? r3333342 : r3333354;
        double r3333356 = r3333325 ? r3333336 : r3333355;
        return r3333356;
}

Original	37.4
Target	15.3
Herbie	15.4

Derivation

Split input into 3 regimes
if eps < -8.29565067036897e-18
1. Initial program 30.3
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum0.9
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied add-log-exp1.0
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\log \left(e^{\tan x \cdot \tan \varepsilon}\right)}} - \tan x\]
6. Applied add-log-exp1.0
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\log \left(e^{1}\right)} - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)} - \tan x\]
7. Applied diff-log1.0
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\log \left(\frac{e^{1}}{e^{\tan x \cdot \tan \varepsilon}}\right)}} - \tan x\]
8. Simplified1.0
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \color{blue}{\left(e^{1 - \tan \varepsilon \cdot \tan x}\right)}} - \tan x\]
if -8.29565067036897e-18 < eps < 3.143523747535153e-69
1. Initial program 46.7
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 31.2
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
3. Simplified31.1
  \[\leadsto \color{blue}{\varepsilon + \left(\varepsilon \cdot \left(x + \varepsilon\right)\right) \cdot x}\]
if 3.143523747535153e-69 < eps
1. Initial program 30.5
  \[\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 - \tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
6. Applied associate-*r/5.9
  \[\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-quot5.9
  \[\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-sub5.9
  \[\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.4
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -8.29565067036897 \cdot 10^{-18}:\\ \;\;\;\;\frac{\tan \varepsilon + \tan x}{\log \left(e^{1 - \tan x \cdot \tan \varepsilon}\right)} - \tan x\\ \mathbf{elif}\;\varepsilon \le 3.143523747535153 \cdot 10^{-69}:\\ \;\;\;\;x \cdot \left(\varepsilon \cdot \left(x + \varepsilon\right)\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan \varepsilon + \tan x\right) \cdot \cos x - \sin x \cdot \left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right)}{\left(1 - \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}\right) \cdot \cos x}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -8.29565067036897e-18`

`if -8.29565067036897e-18 < eps < 3.143523747535153e-69`

`if 3.143523747535153e-69 < eps`

Reproduce

In
Out