Average Error: 36.8 → 15.2
Time: 10.6s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -5.97198873028037458 \cdot 10^{-27} \lor \neg \left(\varepsilon \le 4.74228187640458693 \cdot 10^{-23}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{\log \left({e}^{\left(1 - \tan x \cdot \tan \varepsilon\right)} \cdot {e}^{\left(\mathsf{fma}\left(-\tan \varepsilon, \tan x, \tan \varepsilon \cdot \tan x\right)\right)}\right)} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -5.97198873028037458 \cdot 10^{-27} \lor \neg \left(\varepsilon \le 4.74228187640458693 \cdot 10^{-23}\right):\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{\log \left({e}^{\left(1 - \tan x \cdot \tan \varepsilon\right)} \cdot {e}^{\left(\mathsf{fma}\left(-\tan \varepsilon, \tan x, \tan \varepsilon \cdot \tan x\right)\right)}\right)} - \tan x\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\

\end{array}
double f(double x, double eps) {
        double r167261 = x;
        double r167262 = eps;
        double r167263 = r167261 + r167262;
        double r167264 = tan(r167263);
        double r167265 = tan(r167261);
        double r167266 = r167264 - r167265;
        return r167266;
}

double f(double x, double eps) {
        double r167267 = eps;
        double r167268 = -5.9719887302803746e-27;
        bool r167269 = r167267 <= r167268;
        double r167270 = 4.742281876404587e-23;
        bool r167271 = r167267 <= r167270;
        double r167272 = !r167271;
        bool r167273 = r167269 || r167272;
        double r167274 = x;
        double r167275 = tan(r167274);
        double r167276 = tan(r167267);
        double r167277 = r167275 + r167276;
        double r167278 = exp(1.0);
        double r167279 = 1.0;
        double r167280 = r167275 * r167276;
        double r167281 = r167279 - r167280;
        double r167282 = pow(r167278, r167281);
        double r167283 = -r167276;
        double r167284 = r167276 * r167275;
        double r167285 = fma(r167283, r167275, r167284);
        double r167286 = pow(r167278, r167285);
        double r167287 = r167282 * r167286;
        double r167288 = log(r167287);
        double r167289 = r167277 / r167288;
        double r167290 = r167289 - r167275;
        double r167291 = 2.0;
        double r167292 = pow(r167267, r167291);
        double r167293 = pow(r167274, r167291);
        double r167294 = fma(r167267, r167293, r167267);
        double r167295 = fma(r167292, r167274, r167294);
        double r167296 = r167273 ? r167290 : r167295;
        return r167296;
}

Error

Bits error versus x

Bits error versus eps

Target

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

Derivation

  1. Split input into 2 regimes
  2. if eps < -5.9719887302803746e-27 or 4.742281876404587e-23 < eps

    1. Initial program 29.8

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

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
    4. Using strategy rm
    5. Applied add-log-exp1.8

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\log \left(e^{\tan x \cdot \tan \varepsilon}\right)}} - \tan x\]
    6. Applied add-log-exp1.8

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\log \left(e^{1}\right)} - \log \left(e^{\tan x \cdot \tan \varepsilon}\right)} - \tan x\]
    7. Applied diff-log1.9

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\log \left(\frac{e^{1}}{e^{\tan x \cdot \tan \varepsilon}}\right)}} - \tan x\]
    8. Simplified1.8

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \color{blue}{\left(e^{1 - \tan x \cdot \tan \varepsilon}\right)}} - \tan x\]
    9. Using strategy rm
    10. Applied *-un-lft-identity1.8

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \left(e^{\color{blue}{1 \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)}}\right)} - \tan x\]
    11. Applied exp-prod1.9

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \color{blue}{\left({\left(e^{1}\right)}^{\left(1 - \tan x \cdot \tan \varepsilon\right)}\right)}} - \tan x\]
    12. Simplified1.9

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \left({\color{blue}{e}}^{\left(1 - \tan x \cdot \tan \varepsilon\right)}\right)} - \tan x\]
    13. Using strategy rm
    14. Applied add-cube-cbrt1.9

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \left({e}^{\left(\color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{1}\right) \cdot \sqrt[3]{1}} - \tan x \cdot \tan \varepsilon\right)}\right)} - \tan x\]
    15. Applied prod-diff1.9

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \left({e}^{\color{blue}{\left(\mathsf{fma}\left(\sqrt[3]{1} \cdot \sqrt[3]{1}, \sqrt[3]{1}, -\tan \varepsilon \cdot \tan x\right) + \mathsf{fma}\left(-\tan \varepsilon, \tan x, \tan \varepsilon \cdot \tan x\right)\right)}}\right)} - \tan x\]
    16. Applied unpow-prod-up1.9

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\log \color{blue}{\left({e}^{\left(\mathsf{fma}\left(\sqrt[3]{1} \cdot \sqrt[3]{1}, \sqrt[3]{1}, -\tan \varepsilon \cdot \tan x\right)\right)} \cdot {e}^{\left(\mathsf{fma}\left(-\tan \varepsilon, \tan x, \tan \varepsilon \cdot \tan x\right)\right)}\right)}} - \tan x\]
    17. Simplified1.9

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

    if -5.9719887302803746e-27 < eps < 4.742281876404587e-23

    1. Initial program 45.1

      \[\tan \left(x + \varepsilon\right) - \tan x\]
    2. Taylor expanded around 0 30.9

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

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

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -5.97198873028037458 \cdot 10^{-27} \lor \neg \left(\varepsilon \le 4.74228187640458693 \cdot 10^{-23}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{\log \left({e}^{\left(1 - \tan x \cdot \tan \varepsilon\right)} \cdot {e}^{\left(\mathsf{fma}\left(-\tan \varepsilon, \tan x, \tan \varepsilon \cdot \tan x\right)\right)}\right)} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \end{array}\]

Reproduce

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

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

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