(+ x (- (tan (+ y z)) (tan a)))

Average Error: 12.8 → 0.3

Time: 34.6s

Precision: 64

\[\left(x = 0 \lor 0.5884142 \le x \le 505.5909\right) \land \left(-1.796658 \cdot 10^{+308} \le y \le -9.425585 \cdot 10^{-310} \lor 1.284938 \cdot 10^{-309} \le y \le 1.751224 \cdot 10^{+308}\right) \land \left(-1.776707 \cdot 10^{+308} \le z \le -8.599796 \cdot 10^{-310} \lor 3.293145 \cdot 10^{-311} \le z \le 1.725154 \cdot 10^{+308}\right) \land \left(-1.796658 \cdot 10^{+308} \le a \le -9.425585 \cdot 10^{-310} \lor 1.284938 \cdot 10^{-309} \le a \le 1.751224 \cdot 10^{+308}\right)\]

Math

\[x + \left(\tan \left(y + z\right) - \tan a\right)\]

↓

\[\log \left(e^{x} \cdot \frac{e^{\frac{\tan y + \tan z}{1 - \frac{\sin y \cdot \tan z}{\cos y}}}}{e^{\tan a}}\right)\]

C

double f(double x, double y, double z, double a) {
        double r5547425 = x;
        double r5547426 = y;
        double r5547427 = z;
        double r5547428 = r5547426 + r5547427;
        double r5547429 = tan(r5547428);
        double r5547430 = a;
        double r5547431 = tan(r5547430);
        double r5547432 = r5547429 - r5547431;
        double r5547433 = r5547425 + r5547432;
        return r5547433;
}

↓

double f(double x, double y, double z, double a) {
        double r5547434 = x;
        double r5547435 = exp(r5547434);
        double r5547436 = y;
        double r5547437 = tan(r5547436);
        double r5547438 = z;
        double r5547439 = tan(r5547438);
        double r5547440 = r5547437 + r5547439;
        double r5547441 = 1.0;
        double r5547442 = sin(r5547436);
        double r5547443 = r5547442 * r5547439;
        double r5547444 = cos(r5547436);
        double r5547445 = r5547443 / r5547444;
        double r5547446 = r5547441 - r5547445;
        double r5547447 = r5547440 / r5547446;
        double r5547448 = exp(r5547447);
        double r5547449 = a;
        double r5547450 = tan(r5547449);
        double r5547451 = exp(r5547450);
        double r5547452 = r5547448 / r5547451;
        double r5547453 = r5547435 * r5547452;
        double r5547454 = log(r5547453);
        return r5547454;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus a

Derivation

1. Initial program 12.8

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

3. Applied tan-sum 0.2

   \[\leadsto x + \left(\color{blue}{\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z}} - \tan a\right)\]
4. Using strategy rm

5. Applied add-log-exp 0.3

   \[\leadsto \color{blue}{\log \left(e^{x + \left(\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} - \tan a\right)}\right)}\]
6. Using strategy rm

7. Applied tan-quot 0.3

   \[\leadsto \log \left(e^{x + \left(\frac{\tan y + \tan z}{1 - \color{blue}{\frac{\sin y}{\cos y}} \cdot \tan z} - \tan a\right)}\right)\]

8. Applied associate-*l/ 0.3

   \[\leadsto \log \left(e^{x + \left(\frac{\tan y + \tan z}{1 - \color{blue}{\frac{\sin y \cdot \tan z}{\cos y}}} - \tan a\right)}\right)\]
9. Using strategy rm

10. Applied add-log-exp 0.3

    \[\leadsto \log \left(e^{x + \left(\frac{\tan y + \tan z}{1 - \frac{\sin y \cdot \tan z}{\cos y}} - \color{blue}{\log \left(e^{\tan a}\right)}\right)}\right)\]

11. Applied add-log-exp 0.3

    \[\leadsto \log \left(e^{x + \left(\color{blue}{\log \left(e^{\frac{\tan y + \tan z}{1 - \frac{\sin y \cdot \tan z}{\cos y}}}\right)} - \log \left(e^{\tan a}\right)\right)}\right)\]

12. Applied diff-log 0.3

    \[\leadsto \log \left(e^{x + \color{blue}{\log \left(\frac{e^{\frac{\tan y + \tan z}{1 - \frac{\sin y \cdot \tan z}{\cos y}}}}{e^{\tan a}}\right)}}\right)\]

13. Applied add-log-exp 0.3

    \[\leadsto \log \left(e^{\color{blue}{\log \left(e^{x}\right)} + \log \left(\frac{e^{\frac{\tan y + \tan z}{1 - \frac{\sin y \cdot \tan z}{\cos y}}}}{e^{\tan a}}\right)}\right)\]

14. Applied sum-log 0.3

    \[\leadsto \log \left(e^{\color{blue}{\log \left(e^{x} \cdot \frac{e^{\frac{\tan y + \tan z}{1 - \frac{\sin y \cdot \tan z}{\cos y}}}}{e^{\tan a}}\right)}}\right)\]

15. Applied rem-exp-log 0.3

    \[\leadsto \log \color{blue}{\left(e^{x} \cdot \frac{e^{\frac{\tan y + \tan z}{1 - \frac{\sin y \cdot \tan z}{\cos y}}}}{e^{\tan a}}\right)}\]

16. Final simplification 0.3

    \[\leadsto \log \left(e^{x} \cdot \frac{e^{\frac{\tan y + \tan z}{1 - \frac{\sin y \cdot \tan z}{\cos y}}}}{e^{\tan a}}\right)\]

Reproduce

herbie shell --seed 2019168 
(FPCore (x y z a)
  :name "(+ x (- (tan (+ y z)) (tan a)))"
  :pre (and (or (== x 0) (<= 0.5884142 x 505.5909)) (or (<= -1.796658e+308 y -9.425585e-310) (<= 1.284938e-309 y 1.751224e+308)) (or (<= -1.776707e+308 z -8.599796e-310) (<= 3.293145e-311 z 1.725154e+308)) (or (<= -1.796658e+308 a -9.425585e-310) (<= 1.284938e-309 a 1.751224e+308)))
  (+ x (- (tan (+ y z)) (tan a))))