Average Error: 13.3 → 0.3
Time: 1.2m
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)\]
\[x + \left(\tan \left(y + z\right) - \tan a\right)\]
↓
\[\mathsf{fma}\left(-\tan a, 1, \tan a\right) + \left(\mathsf{fma}\left(\frac{\tan z + \tan y}{1 - \left(\tan z \cdot \tan y\right) \cdot \left(\tan z \cdot \tan y\right)}, \tan z \cdot \tan y, \frac{\tan z + \tan y}{1 - \left(\tan z \cdot \tan y\right) \cdot \left(\tan z \cdot \tan y\right)}\right) - \left(\tan a - x\right)\right)\]
x + \left(\tan \left(y + z\right) - \tan a\right)
↓
\mathsf{fma}\left(-\tan a, 1, \tan a\right) + \left(\mathsf{fma}\left(\frac{\tan z + \tan y}{1 - \left(\tan z \cdot \tan y\right) \cdot \left(\tan z \cdot \tan y\right)}, \tan z \cdot \tan y, \frac{\tan z + \tan y}{1 - \left(\tan z \cdot \tan y\right) \cdot \left(\tan z \cdot \tan y\right)}\right) - \left(\tan a - x\right)\right)
double f(double x, double y, double z, double a) {
        double r4814951 = x;
        double r4814952 = y;
        double r4814953 = z;
        double r4814954 = r4814952 + r4814953;
        double r4814955 = tan(r4814954);
        double r4814956 = a;
        double r4814957 = tan(r4814956);
        double r4814958 = r4814955 - r4814957;
        double r4814959 = r4814951 + r4814958;
        return r4814959;
}
↓
double f(double x, double y, double z, double a) {
        double r4814960 = a;
        double r4814961 = tan(r4814960);
        double r4814962 = -r4814961;
        double r4814963 = 1.0;
        double r4814964 = fma(r4814962, r4814963, r4814961);
        double r4814965 = z;
        double r4814966 = tan(r4814965);
        double r4814967 = y;
        double r4814968 = tan(r4814967);
        double r4814969 = r4814966 + r4814968;
        double r4814970 = r4814966 * r4814968;
        double r4814971 = r4814970 * r4814970;
        double r4814972 = r4814963 - r4814971;
        double r4814973 = r4814969 / r4814972;
        double r4814974 = fma(r4814973, r4814970, r4814973);
        double r4814975 = x;
        double r4814976 = r4814961 - r4814975;
        double r4814977 = r4814974 - r4814976;
        double r4814978 = r4814964 + r4814977;
        return r4814978;
}

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-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 *-un-lft-identity0.2

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

  6. Applied flip--0.2

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

  7. Applied associate-/r/0.2

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

  8. Applied prod-diff0.2

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

  9. Applied associate-+r+0.2

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

  10. Simplified0.3

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

  11. Final simplification0.3

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

Reproduce

herbie shell --seed 2019200 +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))))