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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.26738906910148332 \cdot 10^{-121}:\\ \;\;\;\;\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 3.0489110693032172 \cdot 10^{-33}:\\ \;\;\;\;\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{{\left(\tan x\right)}^{3} + {\left(\tan \varepsilon\right)}^{3}}{\tan \varepsilon \cdot \left(\tan \varepsilon - \tan x\right) + \tan x \cdot \tan x}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -1.26738906910148332 \cdot 10^{-121}:\\
\;\;\;\;\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x\\

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

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

\end{array}

double f(double x, double eps) {
        double r112762 = x;
        double r112763 = eps;
        double r112764 = r112762 + r112763;
        double r112765 = tan(r112764);
        double r112766 = tan(r112762);
        double r112767 = r112765 - r112766;
        return r112767;
}

↓

double f(double x, double eps) {
        double r112768 = eps;
        double r112769 = -1.2673890691014833e-121;
        bool r112770 = r112768 <= r112769;
        double r112771 = 1.0;
        double r112772 = x;
        double r112773 = tan(r112772);
        double r112774 = tan(r112768);
        double r112775 = r112773 * r112774;
        double r112776 = r112771 - r112775;
        double r112777 = r112773 + r112774;
        double r112778 = r112776 / r112777;
        double r112779 = r112771 / r112778;
        double r112780 = r112779 - r112773;
        double r112781 = 3.0489110693032172e-33;
        bool r112782 = r112768 <= r112781;
        double r112783 = r112772 * r112768;
        double r112784 = r112768 + r112772;
        double r112785 = r112783 * r112784;
        double r112786 = r112785 + r112768;
        double r112787 = 3.0;
        double r112788 = pow(r112773, r112787);
        double r112789 = pow(r112774, r112787);
        double r112790 = r112788 + r112789;
        double r112791 = r112774 - r112773;
        double r112792 = r112774 * r112791;
        double r112793 = r112773 * r112773;
        double r112794 = r112792 + r112793;
        double r112795 = r112790 / r112794;
        double r112796 = r112795 / r112776;
        double r112797 = r112796 - r112773;
        double r112798 = r112782 ? r112786 : r112797;
        double r112799 = r112770 ? r112780 : r112798;
        return r112799;
}

Original	36.9
Target	15.2
Herbie	15.6

Derivation

Split input into 3 regimes
if eps < -1.2673890691014833e-121
1. Initial program 32.0
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum9.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied clear-num9.5
  \[\leadsto \color{blue}{\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}}} - \tan x\]
if -1.2673890691014833e-121 < eps < 3.0489110693032172e-33
1. Initial program 46.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum46.9
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot46.9
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x}{\cos x}} \cdot \tan \varepsilon} - \tan x\]
6. Applied associate-*l/46.9
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x \cdot \tan \varepsilon}{\cos x}}} - \tan x\]
7. Taylor expanded around 0 31.0
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
8. Simplified30.8
  \[\leadsto \color{blue}{\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon}\]
if 3.0489110693032172e-33 < eps
1. Initial program 29.5
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum2.1
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip3-+2.3
  \[\leadsto \frac{\color{blue}{\frac{{\left(\tan x\right)}^{3} + {\left(\tan \varepsilon\right)}^{3}}{\tan x \cdot \tan x + \left(\tan \varepsilon \cdot \tan \varepsilon - \tan x \cdot \tan \varepsilon\right)}}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\]
6. Simplified2.3
  \[\leadsto \frac{\frac{{\left(\tan x\right)}^{3} + {\left(\tan \varepsilon\right)}^{3}}{\color{blue}{\tan \varepsilon \cdot \left(\tan \varepsilon - \tan x\right) + \tan x \cdot \tan x}}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\]
Recombined 3 regimes into one program.
Final simplification15.6
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.26738906910148332 \cdot 10^{-121}:\\ \;\;\;\;\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 3.0489110693032172 \cdot 10^{-33}:\\ \;\;\;\;\left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{{\left(\tan x\right)}^{3} + {\left(\tan \varepsilon\right)}^{3}}{\tan \varepsilon \cdot \left(\tan \varepsilon - \tan x\right) + \tan x \cdot \tan x}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -1.2673890691014833e-121`

`if -1.2673890691014833e-121 < eps < 3.0489110693032172e-33`

`if 3.0489110693032172e-33 < eps`

Reproduce

In
Out