Average Error: 0.2 → 0.2
Time: 43.3s
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} + c}{\frac{\frac{\left(a + b\right) + c}{2} + 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} + c}{\frac{\frac{\left(a + b\right) + c}{2} + c}{\frac{\left(a + b\right) + c}{2} - c}}}
double f(double a, double b, double c) {
        double r1399746 = a;
        double r1399747 = b;
        double r1399748 = r1399746 + r1399747;
        double r1399749 = c;
        double r1399750 = r1399748 + r1399749;
        double r1399751 = 2.0;
        double r1399752 = /* ERROR: no posit support in C */;
        double r1399753 = r1399750 / r1399752;
        double r1399754 = r1399753 - r1399746;
        double r1399755 = r1399753 * r1399754;
        double r1399756 = r1399753 - r1399747;
        double r1399757 = r1399755 * r1399756;
        double r1399758 = r1399753 - r1399749;
        double r1399759 = r1399757 * r1399758;
        double r1399760 = sqrt(r1399759);
        return r1399760;
}
↓
double f(double a, double b, double c) {
        double r1399761 = a;
        double r1399762 = b;
        double r1399763 = r1399761 + r1399762;
        double r1399764 = c;
        double r1399765 = r1399763 + r1399764;
        double r1399766 = 2.0;
        double r1399767 = r1399765 / r1399766;
        double r1399768 = r1399767 - r1399761;
        double r1399769 = r1399767 * r1399768;
        double r1399770 = r1399767 - r1399762;
        double r1399771 = r1399769 * r1399770;
        double r1399772 = r1399767 + r1399764;
        double r1399773 = r1399767 - r1399764;
        double r1399774 = r1399772 / r1399773;
        double r1399775 = r1399772 / r1399774;
        double r1399776 = r1399771 * r1399775;
        double r1399777 = sqrt(r1399776);
        return r1399777;
}

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. Using strategy rm

  5. Applied difference-of-squares0.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 \left(\frac{\color{blue}{\left(\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{c}\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)\right)}}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{c}\right)}\right)\right)}\]

  6. Applied associate-/l*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(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{c}\right)}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right)}{c}\right)}{\left(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(2\right)}\right) - c\right)}\right)}\right)}\right)}\]

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

Reproduce

herbie shell --seed 2019120 +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))))