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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -6.30345879620911344 \cdot 10^{-39}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}, 1 + \tan x \cdot \tan \varepsilon, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \le 1.0217107006174054 \cdot 10^{-22}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\tan x \cdot \tan x - \tan \varepsilon \cdot \tan \varepsilon}{\tan x - \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \le -6.30345879620911344 \cdot 10^{-39}:\\
\;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}, 1 + \tan x \cdot \tan \varepsilon, -\tan x\right)\\

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

\mathbf{else}:\\
\;\;\;\;\frac{\frac{\tan x \cdot \tan x - \tan \varepsilon \cdot \tan \varepsilon}{\tan x - \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\

\end{array}

double f(double x, double eps) {
        double r110851 = x;
        double r110852 = eps;
        double r110853 = r110851 + r110852;
        double r110854 = tan(r110853);
        double r110855 = tan(r110851);
        double r110856 = r110854 - r110855;
        return r110856;
}

↓

double f(double x, double eps) {
        double r110857 = eps;
        double r110858 = -6.303458796209113e-39;
        bool r110859 = r110857 <= r110858;
        double r110860 = x;
        double r110861 = tan(r110860);
        double r110862 = tan(r110857);
        double r110863 = r110861 + r110862;
        double r110864 = 1.0;
        double r110865 = r110861 * r110862;
        double r110866 = r110865 * r110865;
        double r110867 = r110864 - r110866;
        double r110868 = r110863 / r110867;
        double r110869 = r110864 + r110865;
        double r110870 = -r110861;
        double r110871 = fma(r110868, r110869, r110870);
        double r110872 = 1.0217107006174054e-22;
        bool r110873 = r110857 <= r110872;
        double r110874 = 2.0;
        double r110875 = pow(r110857, r110874);
        double r110876 = pow(r110860, r110874);
        double r110877 = fma(r110857, r110876, r110857);
        double r110878 = fma(r110875, r110860, r110877);
        double r110879 = r110861 * r110861;
        double r110880 = r110862 * r110862;
        double r110881 = r110879 - r110880;
        double r110882 = r110861 - r110862;
        double r110883 = r110881 / r110882;
        double r110884 = r110864 - r110865;
        double r110885 = r110883 / r110884;
        double r110886 = r110885 - r110861;
        double r110887 = r110873 ? r110878 : r110886;
        double r110888 = r110859 ? r110871 : r110887;
        return r110888;
}

Original	36.9
Target	15.5
Herbie	15.1

Derivation

Split input into 3 regimes
if eps < -6.303458796209113e-39
1. Initial program 30.5
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum3.2
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--3.2
  \[\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/3.2
  \[\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. Applied fma-neg3.2
  \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{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\right)}\]
if -6.303458796209113e-39 < eps < 1.0217107006174054e-22
1. Initial program 45.5
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 31.3
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
3. Simplified31.3
  \[\leadsto \color{blue}{\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)}\]
if 1.0217107006174054e-22 < eps
1. Initial program 29.7
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum1.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip-+1.5
  \[\leadsto \frac{\color{blue}{\frac{\tan x \cdot \tan x - \tan \varepsilon \cdot \tan \varepsilon}{\tan x - \tan \varepsilon}}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\]
Recombined 3 regimes into one program.
Final simplification15.1
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -6.30345879620911344 \cdot 10^{-39}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}, 1 + \tan x \cdot \tan \varepsilon, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \le 1.0217107006174054 \cdot 10^{-22}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\tan x \cdot \tan x - \tan \varepsilon \cdot \tan \varepsilon}{\tan x - \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]

Error

Target

Derivation

`if eps < -6.303458796209113e-39`

`if -6.303458796209113e-39 < eps < 1.0217107006174054e-22`

`if 1.0217107006174054e-22 < eps`

Reproduce