Average Error: 0.2 → 0.2
Time: 55.8s
Precision: 64
\[\left(0\right) \lt a \land \left(0\right) \lt b \land \left(0\right) \lt c\]
\[\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
↓
\[\sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \frac{\frac{\left(a + b\right) + c}{2} \cdot \frac{\left(a + b\right) + c}{2} - c \cdot c}{\frac{\left(a + b\right) + c}{2} + c}}\]
\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}
↓
\sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \frac{\frac{\left(a + b\right) + c}{2} \cdot \frac{\left(a + b\right) + c}{2} - c \cdot c}{\frac{\left(a + b\right) + c}{2} + c}}
double f(double a, double b, double c) {
        double r3775924 = a;
        double r3775925 = b;
        double r3775926 = r3775924 + r3775925;
        double r3775927 = c;
        double r3775928 = r3775926 + r3775927;
        double r3775929 = 2.0;
        double r3775930 = /* ERROR: no posit support in C */;
        double r3775931 = r3775928 / r3775930;
        double r3775932 = r3775931 - r3775924;
        double r3775933 = r3775931 * r3775932;
        double r3775934 = r3775931 - r3775925;
        double r3775935 = r3775933 * r3775934;
        double r3775936 = r3775931 - r3775927;
        double r3775937 = r3775935 * r3775936;
        double r3775938 = sqrt(r3775937);
        return r3775938;
}
↓
double f(double a, double b, double c) {
        double r3775939 = a;
        double r3775940 = b;
        double r3775941 = r3775939 + r3775940;
        double r3775942 = c;
        double r3775943 = r3775941 + r3775942;
        double r3775944 = 2.0;
        double r3775945 = r3775943 / r3775944;
        double r3775946 = r3775945 - r3775939;
        double r3775947 = r3775945 * r3775946;
        double r3775948 = r3775945 - r3775940;
        double r3775949 = r3775947 * r3775948;
        double r3775950 = r3775945 * r3775945;
        double r3775951 = r3775942 * r3775942;
        double r3775952 = r3775950 - r3775951;
        double r3775953 = r3775945 + r3775942;
        double r3775954 = r3775952 / r3775953;
        double r3775955 = r3775949 * r3775954;
        double r3775956 = sqrt(r3775955);
        return r3775956;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Derivation

  1. Initial program 0.2

    \[\sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}\]
  2. Using strategy rm

  3. Applied p16-flip--0.2

    \[\leadsto \sqrt{\left(\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - b\right)\right) \cdot \color{blue}{\left(\frac{\left(\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)\right) - \left(c \cdot c\right)\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{c}\right)}\right)}\right)}\]

  4. Final simplification0.2

    \[\leadsto \sqrt{\left(\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} - a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \frac{\frac{\left(a + b\right) + c}{2} \cdot \frac{\left(a + b\right) + c}{2} - c \cdot c}{\frac{\left(a + b\right) + c}{2} + c}}\]

Reproduce

herbie shell --seed 2019134 +o rules:numerics
(FPCore (a b c)
  :name "Area of a triangle"
  :pre (and (<.p16 (real->posit16 0) a) (<.p16 (real->posit16 0) b) (<.p16 (real->posit16 0) c))
  (sqrt.p16 (*.p16 (*.p16 (*.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) a)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) b)) (-.p16 (/.p16 (+.p16 (+.p16 a b) c) (real->posit16 2)) c))))