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

Average Error: 13.1 → 0.2

Time: 38.2s

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

↓

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

C

double f(double x, double y, double z, double a) {
        double r5161748 = x;
        double r5161749 = y;
        double r5161750 = z;
        double r5161751 = r5161749 + r5161750;
        double r5161752 = tan(r5161751);
        double r5161753 = a;
        double r5161754 = tan(r5161753);
        double r5161755 = r5161752 - r5161754;
        double r5161756 = r5161748 + r5161755;
        return r5161756;
}

↓

double f(double x, double y, double z, double a) {
        double r5161757 = x;
        double r5161758 = z;
        double r5161759 = tan(r5161758);
        double r5161760 = y;
        double r5161761 = tan(r5161760);
        double r5161762 = r5161759 + r5161761;
        double r5161763 = 1.0;
        double r5161764 = sin(r5161760);
        double r5161765 = cos(r5161760);
        double r5161766 = r5161765 / r5161759;
        double r5161767 = r5161764 / r5161766;
        double r5161768 = r5161767 * r5161767;
        double r5161769 = r5161767 * r5161768;
        double r5161770 = r5161763 - r5161769;
        double r5161771 = r5161762 / r5161770;
        double r5161772 = fma(r5161767, r5161767, r5161767);
        double r5161773 = cbrt(r5161766);
        double r5161774 = r5161773 * r5161773;
        double r5161775 = r5161763 / r5161774;
        double r5161776 = r5161764 / r5161773;
        double r5161777 = r5161775 * r5161776;
        double r5161778 = r5161768 * r5161777;
        double r5161779 = r5161763 - r5161778;
        double r5161780 = r5161762 / r5161779;
        double r5161781 = fma(r5161771, r5161772, r5161780);
        double r5161782 = a;
        double r5161783 = tan(r5161782);
        double r5161784 = r5161781 - r5161783;
        double r5161785 = -1.0;
        double r5161786 = fma(r5161783, r5161785, r5161783);
        double r5161787 = r5161784 + r5161786;
        double r5161788 = r5161757 + r5161787;
        return r5161788;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus a

Derivation

1. Initial program 13.1

   \[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 - \color{blue}{\frac{\sin y}{\cos y}} \cdot \tan z} - \tan a\right)\]

6. Applied associate-*l/ 0.2

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

8. Applied add-cube-cbrt 0.3

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

9. Applied flip3-- 0.3

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

10. Applied associate-/r/ 0.3

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

11. Applied prod-diff 0.3

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

12. Simplified 0.2

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

13. Simplified 0.2

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

15. Applied add-cube-cbrt 0.2

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

16. Applied *-un-lft-identity 0.2

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

17. Applied times-frac 0.2

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

18. Final simplification 0.2

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

Reproduce

herbie shell --seed 2019164 +o rules:numerics
(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))))