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

Average Error: 13.3 → 0.2

Time: 26.2s

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

↓

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

C

double f(double x, double y, double z, double a) {
        double r148761 = x;
        double r148762 = y;
        double r148763 = z;
        double r148764 = r148762 + r148763;
        double r148765 = tan(r148764);
        double r148766 = a;
        double r148767 = tan(r148766);
        double r148768 = r148765 - r148767;
        double r148769 = r148761 + r148768;
        return r148769;
}

↓

double f(double x, double y, double z, double a) {
        double r148770 = y;
        double r148771 = sin(r148770);
        double r148772 = z;
        double r148773 = cos(r148772);
        double r148774 = r148771 * r148773;
        double r148775 = cos(r148770);
        double r148776 = sin(r148772);
        double r148777 = r148775 * r148776;
        double r148778 = r148774 + r148777;
        double r148779 = a;
        double r148780 = cos(r148779);
        double r148781 = r148778 * r148780;
        double r148782 = 1.0;
        double r148783 = tan(r148770);
        double r148784 = tan(r148772);
        double r148785 = r148783 * r148784;
        double r148786 = r148782 + r148785;
        double r148787 = r148781 * r148786;
        double r148788 = r148775 * r148773;
        double r148789 = r148785 * r148785;
        double r148790 = r148782 - r148789;
        double r148791 = sin(r148779);
        double r148792 = r148790 * r148791;
        double r148793 = r148788 * r148792;
        double r148794 = r148787 - r148793;
        double r148795 = r148782 - r148785;
        double r148796 = r148794 / r148795;
        double r148797 = r148796 / r148780;
        double r148798 = r148797 / r148788;
        double r148799 = r148783 * r148776;
        double r148800 = r148799 / r148773;
        double r148801 = r148782 + r148800;
        double r148802 = r148798 / r148801;
        double r148803 = x;
        double r148804 = r148802 + r148803;
        return r148804;
}

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-quot 13.3

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

4. Applied tan-sum 0.2

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

5. Applied frac-sub 0.2

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

7. Applied clear-num 0.2

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

9. Applied flip-- 0.2

   \[\leadsto x + \frac{1}{\frac{\left(1 - \tan y \cdot \tan z\right) \cdot \cos a}{\left(\tan y + \tan z\right) \cdot \cos a - \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}} \cdot \sin a}}\]

10. Applied associate-*l/ 0.2

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

11. Applied tan-quot 0.2

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

12. Applied tan-quot 0.2

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

13. Applied frac-add 0.2

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

14. Applied associate-*l/ 0.2

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

15. Applied frac-sub 0.2

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

16. Applied associate-/r/ 0.3

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

17. Applied associate-/r* 0.2

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

18. Simplified 0.2

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

20. Applied tan-quot 0.2

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

21. Applied associate-*r/ 0.2

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

22. Final simplification 0.2

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

Reproduce

herbie shell --seed 2019298 
(FPCore (x y z a)
  :name "(+ x (- (tan (+ y z)) (tan a)))"
  :precision binary64
  :pre (and (or (== x 0.0) (<= 0.588414199999999998 x 505.590899999999976)) (or (<= -1.79665800000000009e308 y -9.425585000000013e-310) (<= 1.284938e-309 y 1.75122399999999993e308)) (or (<= -1.776707e308 z -8.59979600000002e-310) (<= 3.29314499999998e-311 z 1.72515400000000009e308)) (or (<= -1.79665800000000009e308 a -9.425585000000013e-310) (<= 1.284938e-309 a 1.75122399999999993e308)))
  (+ x (- (tan (+ y z)) (tan a))))