Average Error: 0.2 → 0.2
Time: 53.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(\left(\frac{\left(a + b\right) + c}{2} + b\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right)}{\frac{\left(a + b\right) + c}{2} + b} \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]
\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(\left(\frac{\left(a + b\right) + c}{2} + b\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)\right)}{\frac{\left(a + b\right) + c}{2} + b} \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}
double f(double a, double b, double c) {
        double r5802544 = a;
        double r5802545 = b;
        double r5802546 = r5802544 + r5802545;
        double r5802547 = c;
        double r5802548 = r5802546 + r5802547;
        double r5802549 = 2.0;
        double r5802550 = /* ERROR: no posit support in C */;
        double r5802551 = r5802548 / r5802550;
        double r5802552 = r5802551 - r5802544;
        double r5802553 = r5802551 * r5802552;
        double r5802554 = r5802551 - r5802545;
        double r5802555 = r5802553 * r5802554;
        double r5802556 = r5802551 - r5802547;
        double r5802557 = r5802555 * r5802556;
        double r5802558 = sqrt(r5802557);
        return r5802558;
}
↓
double f(double a, double b, double c) {
        double r5802559 = a;
        double r5802560 = b;
        double r5802561 = r5802559 + r5802560;
        double r5802562 = c;
        double r5802563 = r5802561 + r5802562;
        double r5802564 = 2.0;
        double r5802565 = r5802563 / r5802564;
        double r5802566 = r5802565 - r5802559;
        double r5802567 = r5802565 * r5802566;
        double r5802568 = r5802565 + r5802560;
        double r5802569 = r5802565 - r5802560;
        double r5802570 = r5802568 * r5802569;
        double r5802571 = r5802567 * r5802570;
        double r5802572 = r5802571 / r5802568;
        double r5802573 = r5802565 - r5802562;
        double r5802574 = r5802572 * r5802573;
        double r5802575 = sqrt(r5802574);
        return r5802575;
}

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 \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 difference-of-squares0.2

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

  7. Final simplification0.2

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

Reproduce

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