Average Error: 0.1 → 0.3
Time: 47.2s
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{\frac{\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} \cdot \frac{\left(a + b\right) + c}{2} - b \cdot b\right)}{\frac{\left(a + b\right) + c}{2} + b} \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{\frac{\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} \cdot \frac{\left(a + b\right) + c}{2} - b \cdot b\right)}{\frac{\left(a + b\right) + c}{2} + b} \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 r3209813 = a;
        double r3209814 = b;
        double r3209815 = r3209813 + r3209814;
        double r3209816 = c;
        double r3209817 = r3209815 + r3209816;
        double r3209818 = 2.0;
        double r3209819 = /* ERROR: no posit support in C */;
        double r3209820 = r3209817 / r3209819;
        double r3209821 = r3209820 - r3209813;
        double r3209822 = r3209820 * r3209821;
        double r3209823 = r3209820 - r3209814;
        double r3209824 = r3209822 * r3209823;
        double r3209825 = r3209820 - r3209816;
        double r3209826 = r3209824 * r3209825;
        double r3209827 = sqrt(r3209826);
        return r3209827;
}
↓
double f(double a, double b, double c) {
        double r3209828 = a;
        double r3209829 = b;
        double r3209830 = r3209828 + r3209829;
        double r3209831 = c;
        double r3209832 = r3209830 + r3209831;
        double r3209833 = 2.0;
        double r3209834 = r3209832 / r3209833;
        double r3209835 = r3209834 - r3209828;
        double r3209836 = r3209834 * r3209835;
        double r3209837 = r3209834 * r3209834;
        double r3209838 = r3209829 * r3209829;
        double r3209839 = r3209837 - r3209838;
        double r3209840 = r3209836 * r3209839;
        double r3209841 = r3209834 + r3209829;
        double r3209842 = r3209840 / r3209841;
        double r3209843 = r3209831 * r3209831;
        double r3209844 = r3209837 - r3209843;
        double r3209845 = r3209834 + r3209831;
        double r3209846 = r3209844 / r3209845;
        double r3209847 = r3209842 * r3209846;
        double r3209848 = sqrt(r3209847);
        return r3209848;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Derivation

  1. Initial program 0.1

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

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

  7. Final simplification0.3

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