The quadratic formula (r2)

Average Error: 34.5 → 6.9

Time: 8.4s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;b \le -2.7757959561449348 \cdot 10^{129}:\\ \;\;\;\;-1 \cdot \frac{c}{b}\\ \mathbf{elif}\;b \le 9.70088188146619881 \cdot 10^{-222}:\\ \;\;\;\;\frac{1}{\frac{\frac{0.5}{c}}{\frac{1}{\sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)} - b}}}\\ \mathbf{elif}\;b \le 3.2649111998892948 \cdot 10^{111}:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-2 \cdot b}{2 \cdot a}\\ \end{array}\]

C

double f(double a, double b, double c) {
        double r79394 = b;
        double r79395 = -r79394;
        double r79396 = r79394 * r79394;
        double r79397 = 4.0;
        double r79398 = a;
        double r79399 = c;
        double r79400 = r79398 * r79399;
        double r79401 = r79397 * r79400;
        double r79402 = r79396 - r79401;
        double r79403 = sqrt(r79402);
        double r79404 = r79395 - r79403;
        double r79405 = 2.0;
        double r79406 = r79405 * r79398;
        double r79407 = r79404 / r79406;
        return r79407;
}

↓

double f(double a, double b, double c) {
        double r79408 = b;
        double r79409 = -2.775795956144935e+129;
        bool r79410 = r79408 <= r79409;
        double r79411 = -1.0;
        double r79412 = c;
        double r79413 = r79412 / r79408;
        double r79414 = r79411 * r79413;
        double r79415 = 9.700881881466199e-222;
        bool r79416 = r79408 <= r79415;
        double r79417 = 1.0;
        double r79418 = 0.5;
        double r79419 = r79418 / r79412;
        double r79420 = r79408 * r79408;
        double r79421 = 4.0;
        double r79422 = a;
        double r79423 = r79422 * r79412;
        double r79424 = r79421 * r79423;
        double r79425 = r79420 - r79424;
        double r79426 = sqrt(r79425);
        double r79427 = r79426 - r79408;
        double r79428 = r79417 / r79427;
        double r79429 = r79419 / r79428;
        double r79430 = r79417 / r79429;
        double r79431 = 3.264911199889295e+111;
        bool r79432 = r79408 <= r79431;
        double r79433 = -r79408;
        double r79434 = r79433 - r79426;
        double r79435 = 2.0;
        double r79436 = r79435 * r79422;
        double r79437 = r79434 / r79436;
        double r79438 = -2.0;
        double r79439 = r79438 * r79408;
        double r79440 = r79439 / r79436;
        double r79441 = r79432 ? r79437 : r79440;
        double r79442 = r79416 ? r79430 : r79441;
        double r79443 = r79410 ? r79414 : r79442;
        return r79443;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	34.5
Target	20.6
Herbie	6.9

\[\begin{array}{l} \mathbf{if}\;b \lt 0.0:\\ \;\;\;\;\frac{c}{a \cdot \frac{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \end{array}\]

Derivation

1. Split input into 4 regimes

2. if b < -2.775795956144935e+129

   1. Initial program 61.4

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

   2. Taylor expanded around -inf 2.2

      \[\leadsto \color{blue}{-1 \cdot \frac{c}{b}}\]

   if -2.775795956144935e+129 < b < 9.700881881466199e-222

   1. Initial program 31.8

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

   3. Applied flip-- 31.9

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

   4. Simplified 15.9

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

   5. Simplified 15.9

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

   7. Applied *-un-lft-identity 15.9

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

   8. Applied *-un-lft-identity 15.9

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

   9. Applied times-frac 15.9

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

   10. Applied associate-/l* 16.1

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

   11. Simplified 16.1

       \[\leadsto \frac{\frac{1}{1}}{\color{blue}{\frac{2 \cdot a}{\frac{4 \cdot \left(a \cdot c\right) - 0}{\sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)} - b}}}}\]
   12. Using strategy rm

   13. Applied div-inv 16.2

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

   14. Applied associate-/r* 15.3

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

   15. Simplified 15.3

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

   16. Taylor expanded around 0 9.6

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

   if 9.700881881466199e-222 < b < 3.264911199889295e+111

   1. Initial program 8.1

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

   if 3.264911199889295e+111 < b

   1. Initial program 49.7

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

   3. Applied flip-- 63.3

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

   4. Simplified 62.3

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

   5. Simplified 62.3

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

   6. Taylor expanded around 0 3.7

      \[\leadsto \frac{\color{blue}{-2 \cdot b}}{2 \cdot a}\]
3. Recombined 4 regimes into one program.

4. Final simplification 6.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -2.7757959561449348 \cdot 10^{129}:\\ \;\;\;\;-1 \cdot \frac{c}{b}\\ \mathbf{elif}\;b \le 9.70088188146619881 \cdot 10^{-222}:\\ \;\;\;\;\frac{1}{\frac{\frac{0.5}{c}}{\frac{1}{\sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)} - b}}}\\ \mathbf{elif}\;b \le 3.2649111998892948 \cdot 10^{111}:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-2 \cdot b}{2 \cdot a}\\ \end{array}\]

Reproduce

herbie shell --seed 2020047 
(FPCore (a b c)
  :name "The quadratic formula (r2)"
  :precision binary64

  :herbie-target
  (if (< b 0.0) (/ c (* a (/ (+ (- b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)))) (/ (- (- b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)))

  (/ (- (- b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)))