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

Average Error: 12.8 → 0.3

Time: 12.6s

Precision: 64

\[\left(x = 0.0 \lor 0.588414199999999998 \le x \le 505.590899999999976\right) \land \left(-1.79665800000000009 \cdot 10^{308} \le y \le -9.425585000000013 \cdot 10^{-310} \lor 1.284938 \cdot 10^{-309} \le y \le 1.7512240000000001 \cdot 10^{308}\right) \land \left(-1.7767070000000002 \cdot 10^{308} \le z \le -8.59979600000002 \cdot 10^{-310} \lor 3.29314499999998 \cdot 10^{-311} \le z \le 1.72515400000000009 \cdot 10^{308}\right) \land \left(-1.79665800000000009 \cdot 10^{308} \le a \le -9.425585000000013 \cdot 10^{-310} \lor 1.284938 \cdot 10^{-309} \le a \le 1.7512240000000001 \cdot 10^{308}\right)\]

Math

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

↓

\[x + \left(\left(\frac{\sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \cos y} + \frac{\sin z}{\left(1 - \left(\sqrt[3]{\frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}} \cdot \sqrt[3]{\frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}}\right) \cdot \sqrt[3]{\frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}}\right) \cdot \cos z}\right) - \frac{\sin a}{\cos a}\right)\]

C

double f(double x, double y, double z, double a) {
        double r175205 = x;
        double r175206 = y;
        double r175207 = z;
        double r175208 = r175206 + r175207;
        double r175209 = tan(r175208);
        double r175210 = a;
        double r175211 = tan(r175210);
        double r175212 = r175209 - r175211;
        double r175213 = r175205 + r175212;
        return r175213;
}

↓

double f(double x, double y, double z, double a) {
        double r175214 = x;
        double r175215 = y;
        double r175216 = sin(r175215);
        double r175217 = 1.0;
        double r175218 = z;
        double r175219 = sin(r175218);
        double r175220 = r175216 * r175219;
        double r175221 = cos(r175218);
        double r175222 = cos(r175215);
        double r175223 = r175221 * r175222;
        double r175224 = r175220 / r175223;
        double r175225 = r175217 - r175224;
        double r175226 = r175225 * r175222;
        double r175227 = r175216 / r175226;
        double r175228 = cbrt(r175224);
        double r175229 = r175228 * r175228;
        double r175230 = r175229 * r175228;
        double r175231 = r175217 - r175230;
        double r175232 = r175231 * r175221;
        double r175233 = r175219 / r175232;
        double r175234 = r175227 + r175233;
        double r175235 = a;
        double r175236 = sin(r175235);
        double r175237 = cos(r175235);
        double r175238 = r175236 / r175237;
        double r175239 = r175234 - r175238;
        double r175240 = r175214 + r175239;
        return r175240;
}

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. Taylor expanded around inf 0.2

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

6. Applied add-cube-cbrt 0.3

   \[\leadsto x + \left(\left(\frac{\sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \cos y} + \frac{\sin z}{\left(1 - \color{blue}{\left(\sqrt[3]{\frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}} \cdot \sqrt[3]{\frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}}\right) \cdot \sqrt[3]{\frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}}}\right) \cdot \cos z}\right) - \frac{\sin a}{\cos a}\right)\]

7. Final simplification 0.3

   \[\leadsto x + \left(\left(\frac{\sin y}{\left(1 - \frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}\right) \cdot \cos y} + \frac{\sin z}{\left(1 - \left(\sqrt[3]{\frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}} \cdot \sqrt[3]{\frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}}\right) \cdot \sqrt[3]{\frac{\sin y \cdot \sin z}{\cos z \cdot \cos y}}\right) \cdot \cos z}\right) - \frac{\sin a}{\cos a}\right)\]

Reproduce

herbie shell --seed 2020036 
(FPCore (x y z a)
  :name "(+ x (- (tan (+ y z)) (tan a)))"
  :precision binary64
  :pre (and (or (== x 0.0) (<= 0.5884142 x 505.5909)) (or (<= -1.796658e+308 y -9.425585e-310) (<= 1.284938e-309 y 1.7512240000000001e+308)) (or (<= -1.7767070000000002e+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.7512240000000001e+308)))
  (+ x (- (tan (+ y z)) (tan a))))