Jmat.Real.dawson

Average Error: 4.2 → 3.3

Time: 2.2m

Precision: 64

Math

\[\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x\]

↓

\[\frac{\left(\left(x \cdot x\right) \cdot \left(\left(0.0072644182 \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) + \left(x \cdot x\right) \cdot 0.0424060604\right) + 0.1049934947\right) + \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(0.0001789971 \cdot \left(x \cdot x\right) + 0.0005064034\right)\right) + 1}{\left(\left(1 + \left(x \cdot x\right) \cdot 0.7715471019\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\left(x \cdot x\right) \cdot 0.0694555761 + 0.2909738639\right) + \left(0.0008327945 \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(x \cdot x\right)\right)\right) + \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(0.0140005442 + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(2 \cdot 0.0001789971\right)\right)} \cdot x\]

C

double f(double x) {
        double r4409887 = 1.0;
        double r4409888 = /* ERROR: no posit support in C */;
        double r4409889 = 0.1049934947;
        double r4409890 = /* ERROR: no posit support in C */;
        double r4409891 = x;
        double r4409892 = r4409891 * r4409891;
        double r4409893 = r4409890 * r4409892;
        double r4409894 = r4409888 + r4409893;
        double r4409895 = 0.0424060604;
        double r4409896 = /* ERROR: no posit support in C */;
        double r4409897 = r4409892 * r4409892;
        double r4409898 = r4409896 * r4409897;
        double r4409899 = r4409894 + r4409898;
        double r4409900 = 0.0072644182;
        double r4409901 = /* ERROR: no posit support in C */;
        double r4409902 = r4409897 * r4409892;
        double r4409903 = r4409901 * r4409902;
        double r4409904 = r4409899 + r4409903;
        double r4409905 = 0.0005064034;
        double r4409906 = /* ERROR: no posit support in C */;
        double r4409907 = r4409902 * r4409892;
        double r4409908 = r4409906 * r4409907;
        double r4409909 = r4409904 + r4409908;
        double r4409910 = 0.0001789971;
        double r4409911 = /* ERROR: no posit support in C */;
        double r4409912 = r4409907 * r4409892;
        double r4409913 = r4409911 * r4409912;
        double r4409914 = r4409909 + r4409913;
        double r4409915 = 0.7715471019;
        double r4409916 = /* ERROR: no posit support in C */;
        double r4409917 = r4409916 * r4409892;
        double r4409918 = r4409888 + r4409917;
        double r4409919 = 0.2909738639;
        double r4409920 = /* ERROR: no posit support in C */;
        double r4409921 = r4409920 * r4409897;
        double r4409922 = r4409918 + r4409921;
        double r4409923 = 0.0694555761;
        double r4409924 = /* ERROR: no posit support in C */;
        double r4409925 = r4409924 * r4409902;
        double r4409926 = r4409922 + r4409925;
        double r4409927 = 0.0140005442;
        double r4409928 = /* ERROR: no posit support in C */;
        double r4409929 = r4409928 * r4409907;
        double r4409930 = r4409926 + r4409929;
        double r4409931 = 0.0008327945;
        double r4409932 = /* ERROR: no posit support in C */;
        double r4409933 = r4409932 * r4409912;
        double r4409934 = r4409930 + r4409933;
        double r4409935 = 2.0;
        double r4409936 = /* ERROR: no posit support in C */;
        double r4409937 = r4409936 * r4409911;
        double r4409938 = r4409912 * r4409892;
        double r4409939 = r4409937 * r4409938;
        double r4409940 = r4409934 + r4409939;
        double r4409941 = r4409914 / r4409940;
        double r4409942 = r4409941 * r4409891;
        return r4409942;
}

↓

double f(double x) {
        double r4409943 = x;
        double r4409944 = r4409943 * r4409943;
        double r4409945 = 0.0072644182;
        double r4409946 = r4409944 * r4409944;
        double r4409947 = r4409945 * r4409946;
        double r4409948 = 0.0424060604;
        double r4409949 = r4409944 * r4409948;
        double r4409950 = r4409947 + r4409949;
        double r4409951 = 0.1049934947;
        double r4409952 = r4409950 + r4409951;
        double r4409953 = r4409944 * r4409952;
        double r4409954 = r4409946 * r4409946;
        double r4409955 = 0.0001789971;
        double r4409956 = r4409955 * r4409944;
        double r4409957 = 0.0005064034;
        double r4409958 = r4409956 + r4409957;
        double r4409959 = r4409954 * r4409958;
        double r4409960 = r4409953 + r4409959;
        double r4409961 = 1.0;
        double r4409962 = r4409960 + r4409961;
        double r4409963 = 0.7715471019;
        double r4409964 = r4409944 * r4409963;
        double r4409965 = r4409961 + r4409964;
        double r4409966 = 0.0694555761;
        double r4409967 = r4409944 * r4409966;
        double r4409968 = 0.2909738639;
        double r4409969 = r4409967 + r4409968;
        double r4409970 = 0.0008327945;
        double r4409971 = r4409970 * r4409946;
        double r4409972 = r4409971 * r4409944;
        double r4409973 = r4409969 + r4409972;
        double r4409974 = r4409946 * r4409973;
        double r4409975 = r4409965 + r4409974;
        double r4409976 = 0.0140005442;
        double r4409977 = 2.0;
        double r4409978 = r4409977 * r4409955;
        double r4409979 = r4409946 * r4409978;
        double r4409980 = r4409976 + r4409979;
        double r4409981 = r4409954 * r4409980;
        double r4409982 = r4409975 + r4409981;
        double r4409983 = r4409962 / r4409982;
        double r4409984 = r4409983 * r4409943;
        return r4409984;
}

Error

Bits error versus x

Derivation

1. Initial program 4.2

   \[\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.1049934947\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.0424060604\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0072644182\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0005064034\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0001789971\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(0.7715471019\right) \cdot \left(x \cdot x\right)\right)}\right)}{\left(\left(0.2909738639\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0694555761\right) \cdot \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0140005442\right) \cdot \left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(0.0008327945\right) \cdot \left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}{\left(\left(\left(2\right) \cdot \left(0.0001789971\right)\right) \cdot \left(\left(\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)\right)\right)}\right)}\right) \cdot x\]

2. Simplified 3.3

   \[\leadsto \color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}{\left(1\right)}\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0424060604\right)}{\left(\left(0.0072644182\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}{\left(0.1049934947\right)}\right)\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\right)\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\left(0.0008327945\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}\right)}{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0140005442\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(2\right) \cdot \left(0.0001789971\right)\right)\right)}\right)\right)}\right)}\right) \cdot x}\]
3. Using strategy rm

4. Applied p16-*-un-lft-identity 3.3

   \[\leadsto \left(\frac{\left(\frac{\left(\frac{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}{\left(1\right)}\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0424060604\right)}{\left(\left(0.0072644182\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}{\left(0.1049934947\right)}\right)\right)}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\right)\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\left(0.0008327945\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}\right)}{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0140005442\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(2\right) \cdot \left(0.0001789971\right)\right)\right)}\right)\right)}\right)\right)}}\right) \cdot x\]

5. Applied associate-/r* 3.3

   \[\leadsto \color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0005064034\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0001789971\right)\right)}\right)\right)}{\left(1\right)}\right)}{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(0.0424060604\right)}{\left(\left(0.0072644182\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}{\left(0.1049934947\right)}\right)\right)}\right)}{\left(1.0\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\right)\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\left(0.0008327945\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}\right)}{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0140005442\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(2\right) \cdot \left(0.0001789971\right)\right)\right)}\right)\right)}\right)}\right)} \cdot x\]

6. Simplified 3.3

   \[\leadsto \left(\frac{\color{blue}{\left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(\frac{\left(\frac{\left(\left(0.0072644182\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right)}{\left(\left(x \cdot x\right) \cdot \left(0.0424060604\right)\right)}\right)}{\left(0.1049934947\right)}\right)\right)}{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(\left(0.0001789971\right) \cdot \left(x \cdot x\right)\right)}{\left(0.0005064034\right)}\right)\right)}\right)}{\left(1\right)}\right)}}{\left(\frac{\left(\frac{\left(\frac{\left(1\right)}{\left(\left(x \cdot x\right) \cdot \left(0.7715471019\right)\right)}\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\frac{\left(\frac{\left(\left(x \cdot x\right) \cdot \left(0.0694555761\right)\right)}{\left(0.2909738639\right)}\right)}{\left(\left(\left(0.0008327945\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(x \cdot x\right)\right)}\right)\right)}\right)}{\left(\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(\frac{\left(0.0140005442\right)}{\left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(2\right) \cdot \left(0.0001789971\right)\right)\right)}\right)\right)}\right)}\right) \cdot x\]

7. Final simplification 3.3

   \[\leadsto \frac{\left(\left(x \cdot x\right) \cdot \left(\left(0.0072644182 \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) + \left(x \cdot x\right) \cdot 0.0424060604\right) + 0.1049934947\right) + \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(0.0001789971 \cdot \left(x \cdot x\right) + 0.0005064034\right)\right) + 1}{\left(\left(1 + \left(x \cdot x\right) \cdot 0.7715471019\right) + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(\left(x \cdot x\right) \cdot 0.0694555761 + 0.2909738639\right) + \left(0.0008327945 \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(x \cdot x\right)\right)\right) + \left(\left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)\right) \cdot \left(0.0140005442 + \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \cdot \left(2 \cdot 0.0001789971\right)\right)} \cdot x\]

Reproduce

herbie shell --seed 2019165 
(FPCore (x)
  :name "Jmat.Real.dawson"
  (*.p16 (/.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.1049934947) (*.p16 x x))) (*.p16 (real->posit16 0.0424060604) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0072644182) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0005064034) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0001789971) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (+.p16 (real->posit16 1) (*.p16 (real->posit16 0.7715471019) (*.p16 x x))) (*.p16 (real->posit16 0.2909738639) (*.p16 (*.p16 x x) (*.p16 x x)))) (*.p16 (real->posit16 0.0694555761) (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0140005442) (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (real->posit16 0.0008327945) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)))) (*.p16 (*.p16 (real->posit16 2) (real->posit16 0.0001789971)) (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 (*.p16 x x) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x)) (*.p16 x x))))) x))