Average Error: 12.9 → 0.3
Time: 1.4m
Precision: 64
\[x + \left(\tan \left(y + z\right) - \tan a\right)\]
↓
\[\left(\log \left(e^{\frac{\tan y + \tan z}{1 - \frac{\sin z \cdot \sin y}{\cos y \cdot \cos z}}}\right) - \tan a\right) + x\]
double f(double x, double y, double z, double a) {
        double r16065946 = x;
        double r16065947 = y;
        double r16065948 = z;
        double r16065949 = r16065947 + r16065948;
        double r16065950 = tan(r16065949);
        double r16065951 = a;
        double r16065952 = tan(r16065951);
        double r16065953 = r16065950 - r16065952;
        double r16065954 = r16065946 + r16065953;
        return r16065954;
}
↓
double f(double x, double y, double z, double a) {
        double r16065955 = y;
        double r16065956 = tan(r16065955);
        double r16065957 = z;
        double r16065958 = tan(r16065957);
        double r16065959 = r16065956 + r16065958;
        double r16065960 = 1.0;
        double r16065961 = sin(r16065957);
        double r16065962 = sin(r16065955);
        double r16065963 = r16065961 * r16065962;
        double r16065964 = cos(r16065955);
        double r16065965 = cos(r16065957);
        double r16065966 = r16065964 * r16065965;
        double r16065967 = r16065963 / r16065966;
        double r16065968 = r16065960 - r16065967;
        double r16065969 = r16065959 / r16065968;
        double r16065970 = exp(r16065969);
        double r16065971 = log(r16065970);
        double r16065972 = a;
        double r16065973 = tan(r16065972);
        double r16065974 = r16065971 - r16065973;
        double r16065975 = x;
        double r16065976 = r16065974 + r16065975;
        return r16065976;
}


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

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus a

Derivation

  1. Initial program 12.9

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

  3. Applied tan-sum0.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-exp0.2

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

  6. Taylor expanded around inf 0.3

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

  7. Final simplification0.3

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

Reproduce

herbie shell --seed 2019102 
(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))))