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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.4968426811240258 \cdot 10^{-90}:\\ \;\;\;\;\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 5.7485271720269307 \cdot 10^{-167}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{1}{\frac{\cos \varepsilon}{\log \left(e^{\tan x \cdot \sin \varepsilon}\right)}}} - \tan x\\ \end{array}\]

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

↓

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

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

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

\end{array}

double f(double x, double eps) {
        double r123937 = x;
        double r123938 = eps;
        double r123939 = r123937 + r123938;
        double r123940 = tan(r123939);
        double r123941 = tan(r123937);
        double r123942 = r123940 - r123941;
        return r123942;
}

↓

double f(double x, double eps) {
        double r123943 = eps;
        double r123944 = -1.4968426811240258e-90;
        bool r123945 = r123943 <= r123944;
        double r123946 = 1.0;
        double r123947 = x;
        double r123948 = tan(r123947);
        double r123949 = tan(r123943);
        double r123950 = r123948 * r123949;
        double r123951 = r123946 - r123950;
        double r123952 = r123948 + r123949;
        double r123953 = r123951 / r123952;
        double r123954 = r123946 / r123953;
        double r123955 = r123954 - r123948;
        double r123956 = 5.748527172026931e-167;
        bool r123957 = r123943 <= r123956;
        double r123958 = 2.0;
        double r123959 = pow(r123943, r123958);
        double r123960 = pow(r123947, r123958);
        double r123961 = fma(r123943, r123960, r123943);
        double r123962 = fma(r123959, r123947, r123961);
        double r123963 = cos(r123943);
        double r123964 = sin(r123943);
        double r123965 = r123948 * r123964;
        double r123966 = exp(r123965);
        double r123967 = log(r123966);
        double r123968 = r123963 / r123967;
        double r123969 = r123946 / r123968;
        double r123970 = r123946 - r123969;
        double r123971 = r123952 / r123970;
        double r123972 = r123971 - r123948;
        double r123973 = r123957 ? r123962 : r123972;
        double r123974 = r123945 ? r123955 : r123973;
        return r123974;
}

Original	36.6
Target	15.4
Herbie	15.8

Derivation

Split input into 3 regimes
if eps < -1.4968426811240258e-90
1. Initial program 30.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum6.8
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied clear-num6.9
  \[\leadsto \color{blue}{\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}}} - \tan x\]
if -1.4968426811240258e-90 < eps < 5.748527172026931e-167
1. Initial program 48.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 30.0
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]
3. Simplified30.0
  \[\leadsto \color{blue}{\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)}\]
if 5.748527172026931e-167 < eps
1. Initial program 32.4
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum13.0
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot13.1
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
6. Applied associate-*r/13.1
  \[\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 clear-num13.1
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{1}{\frac{\cos \varepsilon}{\tan x \cdot \sin \varepsilon}}}} - \tan x\]
9. Using strategy rm
10. Applied add-log-exp13.1
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \frac{1}{\frac{\cos \varepsilon}{\color{blue}{\log \left(e^{\tan x \cdot \sin \varepsilon}\right)}}}} - \tan x\]
Recombined 3 regimes into one program.
Final simplification15.8
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.4968426811240258 \cdot 10^{-90}:\\ \;\;\;\;\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 5.7485271720269307 \cdot 10^{-167}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{1}{\frac{\cos \varepsilon}{\log \left(e^{\tan x \cdot \sin \varepsilon}\right)}}} - \tan x\\ \end{array}\]

Error

Target

Derivation

`if eps < -1.4968426811240258e-90`

`if -1.4968426811240258e-90 < eps < 5.748527172026931e-167`

`if 5.748527172026931e-167 < eps`

Reproduce