Average Error: 1.6 → 1.6
Time: 31.3s
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 - c \cdot \left(4 \cdot a\right)}}{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 - c \cdot \left(4 \cdot a\right)}}{2 \cdot a}
double f(double a, double b, double c) {
        double r424201 = b;
        double r424202 = -r424201;
        double r424203 = r424201 * r424201;
        double r424204 = 4.0;
        double r424205 = /* ERROR: no posit support in C */;
        double r424206 = a;
        double r424207 = c;
        double r424208 = r424206 * r424207;
        double r424209 = r424205 * r424208;
        double r424210 = r424203 - r424209;
        double r424211 = sqrt(r424210);
        double r424212 = r424202 - r424211;
        double r424213 = 2.0;
        double r424214 = /* ERROR: no posit support in C */;
        double r424215 = r424214 * r424206;
        double r424216 = r424212 / r424215;
        return r424216;
}
↓
double f(double a, double b, double c) {
        double r424217 = b;
        double r424218 = -r424217;
        double r424219 = r424217 * r424217;
        double r424220 = c;
        double r424221 = 4.0;
        double r424222 = a;
        double r424223 = r424221 * r424222;
        double r424224 = r424220 * r424223;
        double r424225 = r424219 - r424224;
        double r424226 = sqrt(r424225);
        double r424227 = r424218 - r424226;
        double r424228 = 2.0;
        double r424229 = r424228 * r424222;
        double r424230 = r424227 / r424229;
        return r424230;
}

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

  6. Final simplification1.6

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

Reproduce

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