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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -3.49173971340657552 \cdot 10^{-152} \lor \neg \left(\varepsilon \le 3.3040955223418242 \cdot 10^{-60}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \left(1 + \log \left(e^{\tan x \cdot \tan \varepsilon}\right)\right) - \tan x\\ \mathbf{else}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -3.49173971340657552 \cdot 10^{-152} \lor \neg \left(\varepsilon \le 3.3040955223418242 \cdot 10^{-60}\right):\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \left(1 + \log \left(e^{\tan x \cdot \tan \varepsilon}\right)\right) - \tan x\\

\mathbf{else}:\\
\;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\

\end{array}

double f(double x, double eps) {
        double r165447 = x;
        double r165448 = eps;
        double r165449 = r165447 + r165448;
        double r165450 = tan(r165449);
        double r165451 = tan(r165447);
        double r165452 = r165450 - r165451;
        return r165452;
}

↓

double f(double x, double eps) {
        double r165453 = eps;
        double r165454 = -3.4917397134065755e-152;
        bool r165455 = r165453 <= r165454;
        double r165456 = 3.304095522341824e-60;
        bool r165457 = r165453 <= r165456;
        double r165458 = !r165457;
        bool r165459 = r165455 || r165458;
        double r165460 = x;
        double r165461 = tan(r165460);
        double r165462 = tan(r165453);
        double r165463 = r165461 + r165462;
        double r165464 = 1.0;
        double r165465 = r165461 * r165462;
        double r165466 = r165465 * r165465;
        double r165467 = r165464 - r165466;
        double r165468 = r165463 / r165467;
        double r165469 = exp(r165465);
        double r165470 = log(r165469);
        double r165471 = r165464 + r165470;
        double r165472 = r165468 * r165471;
        double r165473 = r165472 - r165461;
        double r165474 = 2.0;
        double r165475 = pow(r165453, r165474);
        double r165476 = r165460 * r165475;
        double r165477 = pow(r165460, r165474);
        double r165478 = r165477 * r165453;
        double r165479 = r165453 + r165478;
        double r165480 = r165476 + r165479;
        double r165481 = r165459 ? r165473 : r165480;
        return r165481;
}

Original	36.8
Target	15.4
Herbie	15.9

Derivation

Split input into 2 regimes
if eps < -3.4917397134065755e-152 or 3.304095522341824e-60 < eps
1. Initial program 31.3
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum8.3
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--8.4
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}{1 + \tan x \cdot \tan \varepsilon}}} - \tan x\]
6. Applied associate-/r/8.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right)} - \tan x\]
7. Simplified8.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\]
8. Using strategy rm
9. Applied add-log-exp8.5
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \left(1 + \color{blue}{\log \left(e^{\tan x \cdot \tan \varepsilon}\right)}\right) - \tan x\]
if -3.4917397134065755e-152 < eps < 3.304095522341824e-60
1. Initial program 48.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum48.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--48.4
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}{1 + \tan x \cdot \tan \varepsilon}}} - \tan x\]
6. Applied associate-/r/48.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right)} - \tan x\]
7. Simplified48.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\]
8. Taylor expanded around 0 31.3
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
Recombined 2 regimes into one program.
Final simplification15.9
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -3.49173971340657552 \cdot 10^{-152} \lor \neg \left(\varepsilon \le 3.3040955223418242 \cdot 10^{-60}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \left(1 + \log \left(e^{\tan x \cdot \tan \varepsilon}\right)\right) - \tan x\\ \mathbf{else}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -3.4917397134065755e-152 or 3.304095522341824e-60 < eps`

`if -3.4917397134065755e-152 < eps < 3.304095522341824e-60`

Reproduce

In
Out