Average Error: 36.3 → 15.1
Time: 57.2s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -5.060005299698439 \cdot 10^{-87}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\tan \varepsilon \cdot \sin \varepsilon\right) \cdot \left(\tan x \cdot \tan x\right)}{\cos \varepsilon}}, \tan x \cdot \tan \varepsilon + 1, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \le 8.448789684450496 \cdot 10^{-72}:\\ \;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\tan \varepsilon \cdot \sin \varepsilon\right) \cdot \left(\tan x \cdot \tan x\right)}{\cos \varepsilon}}, \tan x \cdot \tan \varepsilon + 1, -\tan x\right)\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -5.060005299698439 \cdot 10^{-87}:\\
\;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\tan \varepsilon \cdot \sin \varepsilon\right) \cdot \left(\tan x \cdot \tan x\right)}{\cos \varepsilon}}, \tan x \cdot \tan \varepsilon + 1, -\tan x\right)\\

\mathbf{elif}\;\varepsilon \le 8.448789684450496 \cdot 10^{-72}:\\
\;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\tan \varepsilon \cdot \sin \varepsilon\right) \cdot \left(\tan x \cdot \tan x\right)}{\cos \varepsilon}}, \tan x \cdot \tan \varepsilon + 1, -\tan x\right)\\

\end{array}
double f(double x, double eps) {
        double r6183040 = x;
        double r6183041 = eps;
        double r6183042 = r6183040 + r6183041;
        double r6183043 = tan(r6183042);
        double r6183044 = tan(r6183040);
        double r6183045 = r6183043 - r6183044;
        return r6183045;
}
↓
double f(double x, double eps) {
        double r6183046 = eps;
        double r6183047 = -5.060005299698439e-87;
        bool r6183048 = r6183046 <= r6183047;
        double r6183049 = tan(r6183046);
        double r6183050 = x;
        double r6183051 = tan(r6183050);
        double r6183052 = r6183049 + r6183051;
        double r6183053 = 1.0;
        double r6183054 = sin(r6183046);
        double r6183055 = r6183049 * r6183054;
        double r6183056 = r6183051 * r6183051;
        double r6183057 = r6183055 * r6183056;
        double r6183058 = cos(r6183046);
        double r6183059 = r6183057 / r6183058;
        double r6183060 = r6183053 - r6183059;
        double r6183061 = r6183052 / r6183060;
        double r6183062 = r6183051 * r6183049;
        double r6183063 = r6183062 + r6183053;
        double r6183064 = -r6183051;
        double r6183065 = fma(r6183061, r6183063, r6183064);
        double r6183066 = 8.448789684450496e-72;
        bool r6183067 = r6183046 <= r6183066;
        double r6183068 = r6183050 * r6183046;
        double r6183069 = r6183050 + r6183046;
        double r6183070 = fma(r6183068, r6183069, r6183046);
        double r6183071 = r6183067 ? r6183070 : r6183065;
        double r6183072 = r6183048 ? r6183065 : r6183071;
        return r6183072;
}

Error

Bits error versus x

Bits error versus eps

Target

Original36.3
Target15.3
Herbie15.1
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 2 regimes

  2. if eps < -5.060005299698439e-87 or 8.448789684450496e-72 < eps

    1. Initial program 30.0

      \[\tan \left(x + \varepsilon\right) - \tan x\]
    2. Using strategy rm

    3. Applied tan-sum6.2

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
    4. Using strategy rm

    5. Applied flip--6.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/6.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-neg6.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)}\]
    8. Using strategy rm

    9. Applied swap-sqr6.2

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \color{blue}{\left(\tan x \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan \varepsilon\right)}}, 1 + \tan x \cdot \tan \varepsilon, -\tan x\right)\]
    10. Using strategy rm

    11. Applied tan-quot6.2

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan x\right) \cdot \left(\color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}} \cdot \tan \varepsilon\right)}, 1 + \tan x \cdot \tan \varepsilon, -\tan x\right)\]

    12. Applied associate-*l/6.2

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan x\right) \cdot \color{blue}{\frac{\sin \varepsilon \cdot \tan \varepsilon}{\cos \varepsilon}}}, 1 + \tan x \cdot \tan \varepsilon, -\tan x\right)\]

    13. Applied associate-*r/6.2

      \[\leadsto \mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \color{blue}{\frac{\left(\tan x \cdot \tan x\right) \cdot \left(\sin \varepsilon \cdot \tan \varepsilon\right)}{\cos \varepsilon}}}, 1 + \tan x \cdot \tan \varepsilon, -\tan x\right)\]

    if -5.060005299698439e-87 < eps < 8.448789684450496e-72

    1. Initial program 47.7

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

    2. Taylor expanded around 0 31.5

      \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)}\]

    3. Simplified31.2

      \[\leadsto \color{blue}{\mathsf{fma}\left(x \cdot \varepsilon, \varepsilon + x, \varepsilon\right)}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification15.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -5.060005299698439 \cdot 10^{-87}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\tan \varepsilon \cdot \sin \varepsilon\right) \cdot \left(\tan x \cdot \tan x\right)}{\cos \varepsilon}}, \tan x \cdot \tan \varepsilon + 1, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \le 8.448789684450496 \cdot 10^{-72}:\\ \;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\tan \varepsilon \cdot \sin \varepsilon\right) \cdot \left(\tan x \cdot \tan x\right)}{\cos \varepsilon}}, \tan x \cdot \tan \varepsilon + 1, -\tan x\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019165 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))