Area of a triangle

Average Error: 0.2 → 0.1

Time: 57.4s

Precision: 64

\[\left(0\right) \lt a \land \left(0\right) \lt b \land \left(0\right) \lt c\]

Math

\[\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(\frac{\left(\frac{\left(c + b\right) + a}{2} \cdot \frac{\left(\frac{a + \left(c + b\right)}{2} - a\right) \cdot \left(a + \frac{a + \left(c + b\right)}{2}\right)}{\frac{\left(c + b\right) + a}{2} + a}\right) \cdot \left(\frac{\left(c + b\right) + a}{2} + a\right)}{\frac{a + \left(c + b\right)}{2} + a} \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]

C

double f(double a, double b, double c) {
        double r4372026 = a;
        double r4372027 = b;
        double r4372028 = r4372026 + r4372027;
        double r4372029 = c;
        double r4372030 = r4372028 + r4372029;
        double r4372031 = 2.0;
        double r4372032 = /* ERROR: no posit support in C */;
        double r4372033 = r4372030 / r4372032;
        double r4372034 = r4372033 - r4372026;
        double r4372035 = r4372033 * r4372034;
        double r4372036 = r4372033 - r4372027;
        double r4372037 = r4372035 * r4372036;
        double r4372038 = r4372033 - r4372029;
        double r4372039 = r4372037 * r4372038;
        double r4372040 = sqrt(r4372039);
        return r4372040;
}

↓

double f(double a, double b, double c) {
        double r4372041 = c;
        double r4372042 = b;
        double r4372043 = r4372041 + r4372042;
        double r4372044 = a;
        double r4372045 = r4372043 + r4372044;
        double r4372046 = 2.0;
        double r4372047 = r4372045 / r4372046;
        double r4372048 = r4372044 + r4372043;
        double r4372049 = r4372048 / r4372046;
        double r4372050 = r4372049 - r4372044;
        double r4372051 = r4372044 + r4372049;
        double r4372052 = r4372050 * r4372051;
        double r4372053 = r4372047 + r4372044;
        double r4372054 = r4372052 / r4372053;
        double r4372055 = r4372047 * r4372054;
        double r4372056 = r4372055 * r4372053;
        double r4372057 = r4372049 + r4372044;
        double r4372058 = r4372056 / r4372057;
        double r4372059 = r4372044 + r4372042;
        double r4372060 = r4372059 + r4372041;
        double r4372061 = r4372060 / r4372046;
        double r4372062 = r4372061 - r4372042;
        double r4372063 = r4372058 * r4372062;
        double r4372064 = r4372061 - r4372041;
        double r4372065 = r4372063 * r4372064;
        double r4372066 = sqrt(r4372065);
        return r4372066;
}

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 \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(a \cdot a\right)\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{a}\right)}\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)}\]

4. Applied associate-*r/ 0.2

   \[\leadsto \sqrt{\left(\left(\color{blue}{\left(\frac{\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) \cdot \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(a \cdot a\right)\right)\right)}{\left(\frac{\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)}\]
5. Using strategy rm

6. Applied associate-/l* 0.2

   \[\leadsto \sqrt{\left(\left(\color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{a}\right)}{\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(a \cdot a\right)\right)}\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)}\]

7. Simplified 0.1

   \[\leadsto \sqrt{\left(\left(\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{\color{blue}{\left(\frac{\left(1.0\right)}{\left(\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right) - a\right)}\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)}\]
8. Using strategy rm

9. Applied p16-flip-- 0.1

   \[\leadsto \sqrt{\left(\left(\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{\left(\frac{\left(1.0\right)}{\color{blue}{\left(\frac{\left(\left(\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right)\right) - \left(a \cdot a\right)\right)}{\left(\frac{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right)}{a}\right)}\right)}}\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)}\]

10. Applied associate-/r/ 0.1

    \[\leadsto \sqrt{\left(\left(\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{\color{blue}{\left(\left(\frac{\left(1.0\right)}{\left(\left(\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right)\right) - \left(a \cdot a\right)\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right)}{a}\right)\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)}\]

11. Applied associate-/r* 0.1

    \[\leadsto \sqrt{\left(\left(\color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{\left(\frac{\left(1.0\right)}{\left(\left(\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right)\right) - \left(a \cdot a\right)\right)}\right)}\right)}{\left(\frac{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\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)}\]

12. Simplified 0.1

    \[\leadsto \sqrt{\left(\left(\left(\frac{\color{blue}{\left(\left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) - a\right)\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right)}{a}\right)\right)}}{\left(\frac{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\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)}\]
13. Using strategy rm

14. Applied p16-flip-- 0.2

    \[\leadsto \sqrt{\left(\left(\left(\frac{\left(\left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) \cdot \color{blue}{\left(\frac{\left(\left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right)\right) - \left(a \cdot a\right)\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right)}{a}\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right)}{a}\right)\right)}{\left(\frac{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\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)}\]

15. Simplified 0.1

    \[\leadsto \sqrt{\left(\left(\left(\frac{\left(\left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) \cdot \left(\frac{\color{blue}{\left(\left(\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right) - a\right) \cdot \left(\frac{a}{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}{\left(2\right)}\right)}\right)\right)}}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right)}{a}\right)}\right)\right) \cdot \left(\frac{\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right)}{a}\right)\right)}{\left(\frac{\left(\frac{\left(\frac{a}{\left(\frac{c}{b}\right)}\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)}\]

16. Final simplification 0.1

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

Reproduce

herbie shell --seed 2019133 
(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))))