Average Error: 1.6 → 1.6
Time: 31.5s
Precision: 64
\[\frac{\left(\left(-b\right) - \left(\sqrt{\left(\left(b \cdot b\right) - \left(\left(4\right) \cdot \left(a \cdot c\right)\right)\right)}\right)\right)}{\left(\left(2\right) \cdot a\right)}\]
↓
\[\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot c\right) \cdot a}}{2 \cdot a}\]
\frac{\left(\left(-b\right) - \left(\sqrt{\left(\left(b \cdot b\right) - \left(\left(4\right) \cdot \left(a \cdot c\right)\right)\right)}\right)\right)}{\left(\left(2\right) \cdot a\right)}
↓
\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot c\right) \cdot a}}{2 \cdot a}
double f(double a, double b, double c) {
        double r1132185 = b;
        double r1132186 = -r1132185;
        double r1132187 = r1132185 * r1132185;
        double r1132188 = 4.0;
        double r1132189 = /* ERROR: no posit support in C */;
        double r1132190 = a;
        double r1132191 = c;
        double r1132192 = r1132190 * r1132191;
        double r1132193 = r1132189 * r1132192;
        double r1132194 = r1132187 - r1132193;
        double r1132195 = sqrt(r1132194);
        double r1132196 = r1132186 - r1132195;
        double r1132197 = 2.0;
        double r1132198 = /* ERROR: no posit support in C */;
        double r1132199 = r1132198 * r1132190;
        double r1132200 = r1132196 / r1132199;
        return r1132200;
}
↓
double f(double a, double b, double c) {
        double r1132201 = b;
        double r1132202 = -r1132201;
        double r1132203 = r1132201 * r1132201;
        double r1132204 = 4.0;
        double r1132205 = c;
        double r1132206 = r1132204 * r1132205;
        double r1132207 = a;
        double r1132208 = r1132206 * r1132207;
        double r1132209 = r1132203 - r1132208;
        double r1132210 = sqrt(r1132209);
        double r1132211 = r1132202 - r1132210;
        double r1132212 = 2.0;
        double r1132213 = r1132212 * r1132207;
        double r1132214 = r1132211 / r1132213;
        return r1132214;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Derivation

  1. Initial program 1.6

    \[\frac{\left(\left(-b\right) - \left(\sqrt{\left(\left(b \cdot b\right) - \left(\left(4\right) \cdot \left(a \cdot c\right)\right)\right)}\right)\right)}{\left(\left(2\right) \cdot a\right)}\]
  2. Using strategy rm

  3. Applied -p16-rgt-identity-expand1.6

    \[\leadsto \frac{\left(\color{blue}{\left(\left(-b\right) - \left(0.0\right)\right)} - \left(\sqrt{\left(\left(b \cdot b\right) - \left(\left(4\right) \cdot \left(a \cdot c\right)\right)\right)}\right)\right)}{\left(\left(2\right) \cdot a\right)}\]

  4. Applied associate--l-1.6

    \[\leadsto \frac{\color{blue}{\left(\left(-b\right) - \left(\frac{\left(0.0\right)}{\left(\sqrt{\left(\left(b \cdot b\right) - \left(\left(4\right) \cdot \left(a \cdot c\right)\right)\right)}\right)}\right)\right)}}{\left(\left(2\right) \cdot a\right)}\]

  5. Simplified1.6

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

  6. Final simplification1.6

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

Reproduce

herbie shell --seed 2019165 
(FPCore (a b c)
  :name "quadm (p42, negative)"
  (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))