Average Error: 0.2 → 0.2
Time: 52.6s
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{1.0}{\frac{2}{a + \left(c + b\right)}} - b\right)\right) \cdot \frac{\frac{\left(c + b\right) + a}{2} \cdot \frac{\left(c + b\right) + a}{2} - c \cdot c}{\frac{\left(c + b\right) + a}{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{1.0}{\frac{2}{a + \left(c + b\right)}} - b\right)\right) \cdot \frac{\frac{\left(c + b\right) + a}{2} \cdot \frac{\left(c + b\right) + a}{2} - c \cdot c}{\frac{\left(c + b\right) + a}{2} + c}}
double f(double a, double b, double c) {
        double r1609111 = a;
        double r1609112 = b;
        double r1609113 = r1609111 + r1609112;
        double r1609114 = c;
        double r1609115 = r1609113 + r1609114;
        double r1609116 = 2.0;
        double r1609117 = /* ERROR: no posit support in C */;
        double r1609118 = r1609115 / r1609117;
        double r1609119 = r1609118 - r1609111;
        double r1609120 = r1609118 * r1609119;
        double r1609121 = r1609118 - r1609112;
        double r1609122 = r1609120 * r1609121;
        double r1609123 = r1609118 - r1609114;
        double r1609124 = r1609122 * r1609123;
        double r1609125 = sqrt(r1609124);
        return r1609125;
}
↓
double f(double a, double b, double c) {
        double r1609126 = a;
        double r1609127 = b;
        double r1609128 = r1609126 + r1609127;
        double r1609129 = c;
        double r1609130 = r1609128 + r1609129;
        double r1609131 = 2.0;
        double r1609132 = r1609130 / r1609131;
        double r1609133 = r1609132 - r1609126;
        double r1609134 = r1609132 * r1609133;
        double r1609135 = 1.0;
        double r1609136 = r1609129 + r1609127;
        double r1609137 = r1609126 + r1609136;
        double r1609138 = r1609131 / r1609137;
        double r1609139 = r1609135 / r1609138;
        double r1609140 = r1609139 - r1609127;
        double r1609141 = r1609134 * r1609140;
        double r1609142 = r1609136 + r1609126;
        double r1609143 = r1609142 / r1609131;
        double r1609144 = r1609143 * r1609143;
        double r1609145 = r1609129 * r1609129;
        double r1609146 = r1609144 - r1609145;
        double r1609147 = r1609143 + r1609129;
        double r1609148 = r1609146 / r1609147;
        double r1609149 = r1609141 * r1609148;
        double r1609150 = sqrt(r1609149);
        return r1609150;
}

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-*-un-lft-identity0.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(\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\color{blue}{\left(\left(1.0\right) \cdot \left(2\right)\right)}}\right) - c\right)\right)}\]

  4. Applied associate-/r*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 \left(\color{blue}{\left(\frac{\left(\frac{\left(\frac{\left(\frac{a}{b}\right)}{c}\right)}{\left(1.0\right)}\right)}{\left(2\right)}\right)} - c\right)\right)}\]

  5. Simplified0.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(\left(\frac{\color{blue}{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}}{\left(2\right)}\right) - c\right)\right)}\]
  6. Using strategy rm

  7. Applied p16-*-un-lft-identity0.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)}{\color{blue}{\left(\left(1.0\right) \cdot \left(2\right)\right)}}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) - c\right)\right)}\]

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

  9. Simplified0.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{\color{blue}{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) - c\right)\right)}\]
  10. Using strategy rm

  11. Applied p16-*-un-lft-identity0.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{\color{blue}{\left(\left(1.0\right) \cdot \left(\frac{a}{\left(\frac{c}{b}\right)}\right)\right)}}{\left(2\right)}\right) - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) - c\right)\right)}\]

  12. 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(\color{blue}{\left(\frac{\left(1.0\right)}{\left(\frac{\left(2\right)}{\left(\frac{a}{\left(\frac{c}{b}\right)}\right)}\right)}\right)} - b\right)\right) \cdot \left(\left(\frac{\left(\frac{\left(\frac{c}{b}\right)}{a}\right)}{\left(2\right)}\right) - c\right)\right)}\]
  13. Using strategy rm

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

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

Reproduce

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