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

Average Error: 13.1 → 0.3

Time: 35.3s

Precision: 64

\[\left(x = 0.0 \lor 0.5884141999999999983472775966220069676638 \le x \le 505.5908999999999764440872240811586380005\right) \land \left(-1.7966580000000000931214523812968299911 \cdot 10^{308} \le y \le -9.425585000000013069597555966781986720373 \cdot 10^{-310} \lor 1.284937999999999548796432976649400331091 \cdot 10^{-309} \le y \le 1.751223999999999928063201074847742204824 \cdot 10^{308}\right) \land \left(-1.776707000000000001259808757982040817204 \cdot 10^{308} \le z \le -8.599796000000016667475923823712126825539 \cdot 10^{-310} \lor 3.293144999999983071955117582595641261776 \cdot 10^{-311} \le z \le 1.725154000000000087891269878141591702413 \cdot 10^{308}\right) \land \left(-1.7966580000000000931214523812968299911 \cdot 10^{308} \le a \le -9.425585000000013069597555966781986720373 \cdot 10^{-310} \lor 1.284937999999999548796432976649400331091 \cdot 10^{-309} \le a \le 1.751223999999999928063201074847742204824 \cdot 10^{308}\right)\]

Math

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

↓

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

C

double f(double x, double y, double z, double a) {
        double r5234055 = x;
        double r5234056 = y;
        double r5234057 = z;
        double r5234058 = r5234056 + r5234057;
        double r5234059 = tan(r5234058);
        double r5234060 = a;
        double r5234061 = tan(r5234060);
        double r5234062 = r5234059 - r5234061;
        double r5234063 = r5234055 + r5234062;
        return r5234063;
}

↓

double f(double x, double y, double z, double a) {
        double r5234064 = x;
        double r5234065 = y;
        double r5234066 = tan(r5234065);
        double r5234067 = cbrt(r5234066);
        double r5234068 = r5234067 * r5234067;
        double r5234069 = cbrt(r5234068);
        double r5234070 = r5234069 * r5234069;
        double r5234071 = cbrt(r5234067);
        double r5234072 = r5234071 * r5234071;
        double r5234073 = r5234070 * r5234072;
        double r5234074 = z;
        double r5234075 = tan(r5234074);
        double r5234076 = fma(r5234073, r5234067, r5234075);
        double r5234077 = 1.0;
        double r5234078 = r5234075 * r5234066;
        double r5234079 = r5234077 - r5234078;
        double r5234080 = r5234076 / r5234079;
        double r5234081 = a;
        double r5234082 = tan(r5234081);
        double r5234083 = r5234080 - r5234082;
        double r5234084 = r5234064 + r5234083;
        return r5234084;
}

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 add-cube-cbrt 0.3

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

6. Applied fma-def 0.3

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

8. Applied add-cube-cbrt 0.3

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

9. Applied cbrt-prod 0.3

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

10. Applied add-cube-cbrt 0.3

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

11. Applied cbrt-prod 0.3

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

12. Applied swap-sqr 0.3

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

13. Final simplification 0.3

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

Reproduce

herbie shell --seed 2019171 +o rules:numerics
(FPCore (x y z a)
  :name "(+ x (- (tan (+ y z)) (tan a)))"
  :pre (and (or (== x 0.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))))