Average Error: 0.2 → 0.2
Time: 43.7s
Precision: 64
\[\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 \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]
↓
\[\sqrt{\frac{\left(\frac{\left(a + b\right) + c}{2} \cdot \left(\frac{\left(a + b\right) + c}{2} \cdot \frac{\left(a + b\right) + c}{2} - a \cdot a\right)\right) \cdot \left(\frac{\left(a + b\right) + c}{2} - b\right)}{\frac{\left(a + b\right) + c}{2} + a} \cdot \left(\frac{\left(a + b\right) + c}{2} - c\right)}\]
double f(double a, double b, double c) {
        double r3781456 = a;
        double r3781457 = b;
        double r3781458 = r3781456 + r3781457;
        double r3781459 = c;
        double r3781460 = r3781458 + r3781459;
        double r3781461 = 2.0;
        double r3781462 = r3781460 / r3781461;
        double r3781463 = r3781462 - r3781456;
        double r3781464 = r3781462 * r3781463;
        double r3781465 = r3781462 - r3781457;
        double r3781466 = r3781464 * r3781465;
        double r3781467 = r3781462 - r3781459;
        double r3781468 = r3781466 * r3781467;
        double r3781469 = sqrt(r3781468);
        return r3781469;
}
↓
double f(double a, double b, double c) {
        double r3781470 = a;
        double r3781471 = b;
        double r3781472 = r3781470 + r3781471;
        double r3781473 = c;
        double r3781474 = r3781472 + r3781473;
        double r3781475 = 2.0;
        double r3781476 = r3781474 / r3781475;
        double r3781477 = r3781476 * r3781476;
        double r3781478 = r3781470 * r3781470;
        double r3781479 = r3781477 - r3781478;
        double r3781480 = r3781476 * r3781479;
        double r3781481 = r3781476 - r3781471;
        double r3781482 = r3781480 * r3781481;
        double r3781483 = r3781476 + r3781470;
        double r3781484 = r3781482 / r3781483;
        double r3781485 = r3781476 - r3781473;
        double r3781486 = r3781484 * r3781485;
        double r3781487 = sqrt(r3781486);
        return r3781487;
}


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

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

  6. Final simplification0.2

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

Reproduce

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