Average Error: 0.2 → 0.2
Time: 47.6s
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 r2642730 = a;
        double r2642731 = b;
        double r2642732 = r2642730 + r2642731;
        double r2642733 = c;
        double r2642734 = r2642732 + r2642733;
        double r2642735 = 2.0;
        double r2642736 = r2642734 / r2642735;
        double r2642737 = r2642736 - r2642730;
        double r2642738 = r2642736 * r2642737;
        double r2642739 = r2642736 - r2642731;
        double r2642740 = r2642738 * r2642739;
        double r2642741 = r2642736 - r2642733;
        double r2642742 = r2642740 * r2642741;
        double r2642743 = sqrt(r2642742);
        return r2642743;
}
↓
double f(double a, double b, double c) {
        double r2642744 = a;
        double r2642745 = b;
        double r2642746 = r2642744 + r2642745;
        double r2642747 = c;
        double r2642748 = r2642746 + r2642747;
        double r2642749 = 2.0;
        double r2642750 = r2642748 / r2642749;
        double r2642751 = r2642750 * r2642750;
        double r2642752 = r2642744 * r2642744;
        double r2642753 = r2642751 - r2642752;
        double r2642754 = r2642750 * r2642753;
        double r2642755 = r2642750 - r2642745;
        double r2642756 = r2642754 * r2642755;
        double r2642757 = r2642750 + r2642744;
        double r2642758 = r2642756 / r2642757;
        double r2642759 = r2642750 - r2642747;
        double r2642760 = r2642758 * r2642759;
        double r2642761 = sqrt(r2642760);
        return r2642761;
}


\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 2019102 +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))))