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

Average Error: 13.3 → 0.2

Time: 1.1m

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)\]

↓

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

C

double f(double x, double y, double z, double a) {
        double r31326926 = x;
        double r31326927 = y;
        double r31326928 = z;
        double r31326929 = r31326927 + r31326928;
        double r31326930 = tan(r31326929);
        double r31326931 = a;
        double r31326932 = tan(r31326931);
        double r31326933 = r31326930 - r31326932;
        double r31326934 = r31326926 + r31326933;
        return r31326934;
}

↓

double f(double x, double y, double z, double a) {
        double r31326935 = z;
        double r31326936 = cos(r31326935);
        double r31326937 = y;
        double r31326938 = tan(r31326937);
        double r31326939 = sin(r31326937);
        double r31326940 = r31326938 * r31326939;
        double r31326941 = r31326936 * r31326940;
        double r31326942 = sin(r31326935);
        double r31326943 = tan(r31326935);
        double r31326944 = r31326942 * r31326943;
        double r31326945 = cos(r31326937);
        double r31326946 = r31326944 * r31326945;
        double r31326947 = r31326941 - r31326946;
        double r31326948 = r31326936 * r31326945;
        double r31326949 = r31326938 - r31326943;
        double r31326950 = r31326948 * r31326949;
        double r31326951 = r31326947 / r31326950;
        double r31326952 = 1.0;
        double r31326953 = r31326938 * r31326942;
        double r31326954 = r31326953 / r31326936;
        double r31326955 = r31326952 - r31326954;
        double r31326956 = r31326951 / r31326955;
        double r31326957 = a;
        double r31326958 = tan(r31326957);
        double r31326959 = r31326956 - r31326958;
        double r31326960 = x;
        double r31326961 = r31326959 + r31326960;
        return r31326961;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus a

Derivation

1. Initial program 13.3

   \[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 tan-quot 0.2

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

6. Applied associate-*r/ 0.2

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

8. Applied flip-+ 0.2

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

10. Applied tan-quot 0.2

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

11. Applied associate-*l/ 0.2

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

12. Applied tan-quot 0.2

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

13. Applied associate-*r/ 0.2

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

14. Applied frac-sub 0.2

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

15. Applied associate-/l/ 0.2

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

16. Final simplification 0.2

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

Reproduce

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