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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le \frac{-3245935200223819}{3.369993333393829974333376885877453834205 \cdot 10^{66}} \lor \neg \left(\varepsilon \le \frac{7457503469233993}{5.653910607290829854666552002377339250648 \cdot 10^{73}}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \log \left(e^{\frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}\right)} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le \frac{-3245935200223819}{3.369993333393829974333376885877453834205 \cdot 10^{66}} \lor \neg \left(\varepsilon \le \frac{7457503469233993}{5.653910607290829854666552002377339250648 \cdot 10^{73}}\right):\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \log \left(e^{\frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}\right)} - \tan x\\

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

\end{array}

double f(double x, double eps) {
        double r448317 = x;
        double r448318 = eps;
        double r448319 = r448317 + r448318;
        double r448320 = tan(r448319);
        double r448321 = tan(r448317);
        double r448322 = r448320 - r448321;
        return r448322;
}

↓

double f(double x, double eps) {
        double r448323 = eps;
        double r448324 = -3245935200223819.0;
        double r448325 = 3.36999333339383e+66;
        double r448326 = r448324 / r448325;
        bool r448327 = r448323 <= r448326;
        double r448328 = 7457503469233993.0;
        double r448329 = 5.65391060729083e+73;
        double r448330 = r448328 / r448329;
        bool r448331 = r448323 <= r448330;
        double r448332 = !r448331;
        bool r448333 = r448327 || r448332;
        double r448334 = x;
        double r448335 = tan(r448334);
        double r448336 = tan(r448323);
        double r448337 = r448335 + r448336;
        double r448338 = 1.0;
        double r448339 = sin(r448323);
        double r448340 = r448335 * r448339;
        double r448341 = cos(r448323);
        double r448342 = r448340 / r448341;
        double r448343 = exp(r448342);
        double r448344 = log(r448343);
        double r448345 = r448338 - r448344;
        double r448346 = r448337 / r448345;
        double r448347 = r448346 - r448335;
        double r448348 = r448334 * r448323;
        double r448349 = r448334 + r448323;
        double r448350 = r448348 * r448349;
        double r448351 = r448350 + r448323;
        double r448352 = r448333 ? r448347 : r448351;
        return r448352;
}

Original	36.9
Target	15.2
Herbie	15.5

Derivation

Split input into 2 regimes
if eps < -9.631874247522397e-52 or 1.3189991825511699e-58 < eps
1. Initial program 29.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum4.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot4.4
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
6. Applied associate-*r/4.4
  \[\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 add-log-exp4.5
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\log \left(e^{\frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}\right)}} - \tan x\]
if -9.631874247522397e-52 < eps < 1.3189991825511699e-58
1. Initial program 47.0
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 31.9
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
3. Simplified31.6
  \[\leadsto \color{blue}{\left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right) + \varepsilon}\]
Recombined 2 regimes into one program.
Final simplification15.5
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le \frac{-3245935200223819}{3.369993333393829974333376885877453834205 \cdot 10^{66}} \lor \neg \left(\varepsilon \le \frac{7457503469233993}{5.653910607290829854666552002377339250648 \cdot 10^{73}}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \log \left(e^{\frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}\right)} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -9.631874247522397e-52 or 1.3189991825511699e-58 < eps`

`if -9.631874247522397e-52 < eps < 1.3189991825511699e-58`

Reproduce

In
Out