The quadratic formula (r1)

Average Error: 33.5 → 10.0

Time: 11.0s

Precision: 64

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

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;b \le -1.478406535480561669630649836752919254545 \cdot 10^{60}:\\ \;\;\;\;1 \cdot \left(\frac{c}{b} - \frac{b}{a}\right)\\ \mathbf{elif}\;b \le 2.175674080408202904737521150531781836244 \cdot 10^{-169}:\\ \;\;\;\;\frac{1}{2} \cdot \frac{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} - b}{a}\\ \mathbf{elif}\;b \le 3.705250296078930544323375298653357812472 \cdot 10^{-110} \lor \neg \left(b \le 29494967590524297216\right):\\ \;\;\;\;\frac{1}{2} \cdot \left(-2 \cdot \frac{c}{b}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{-\left(4 \cdot a\right) \cdot c}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} + b}}{a} \cdot \frac{1}{2}\\ \end{array}\]

C

double f(double a, double b, double c) {
        double r163408 = b;
        double r163409 = -r163408;
        double r163410 = r163408 * r163408;
        double r163411 = 4.0;
        double r163412 = a;
        double r163413 = r163411 * r163412;
        double r163414 = c;
        double r163415 = r163413 * r163414;
        double r163416 = r163410 - r163415;
        double r163417 = sqrt(r163416);
        double r163418 = r163409 + r163417;
        double r163419 = 2.0;
        double r163420 = r163419 * r163412;
        double r163421 = r163418 / r163420;
        return r163421;
}

↓

double f(double a, double b, double c) {
        double r163422 = b;
        double r163423 = -1.4784065354805617e+60;
        bool r163424 = r163422 <= r163423;
        double r163425 = 1.0;
        double r163426 = c;
        double r163427 = r163426 / r163422;
        double r163428 = a;
        double r163429 = r163422 / r163428;
        double r163430 = r163427 - r163429;
        double r163431 = r163425 * r163430;
        double r163432 = 2.175674080408203e-169;
        bool r163433 = r163422 <= r163432;
        double r163434 = 1.0;
        double r163435 = 2.0;
        double r163436 = r163434 / r163435;
        double r163437 = r163422 * r163422;
        double r163438 = 4.0;
        double r163439 = r163438 * r163428;
        double r163440 = r163439 * r163426;
        double r163441 = r163437 - r163440;
        double r163442 = sqrt(r163441);
        double r163443 = r163442 - r163422;
        double r163444 = r163443 / r163428;
        double r163445 = r163436 * r163444;
        double r163446 = 3.7052502960789305e-110;
        bool r163447 = r163422 <= r163446;
        double r163448 = 2.9494967590524297e+19;
        bool r163449 = r163422 <= r163448;
        double r163450 = !r163449;
        bool r163451 = r163447 || r163450;
        double r163452 = -2.0;
        double r163453 = r163452 * r163427;
        double r163454 = r163436 * r163453;
        double r163455 = -r163440;
        double r163456 = r163442 + r163422;
        double r163457 = r163455 / r163456;
        double r163458 = r163457 / r163428;
        double r163459 = r163458 * r163436;
        double r163460 = r163451 ? r163454 : r163459;
        double r163461 = r163433 ? r163445 : r163460;
        double r163462 = r163424 ? r163431 : r163461;
        return r163462;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	33.5
Target	20.5
Herbie	10.0

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

Derivation

1. Split input into 4 regimes

2. if b < -1.4784065354805617e+60

   1. Initial program 39.0

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

   2. Simplified 39.0

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

   3. Taylor expanded around -inf 5.4

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

   4. Simplified 5.4

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

   if -1.4784065354805617e+60 < b < 2.175674080408203e-169

   1. Initial program 10.7

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

   2. Simplified 10.7

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

   4. Applied clear-num 10.9

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

   6. Applied *-un-lft-identity 10.9

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

   7. Applied times-frac 10.9

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

   8. Applied add-cube-cbrt 10.9

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

   9. Applied times-frac 10.9

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

   10. Simplified 10.9

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

   11. Simplified 10.7

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

   if 2.175674080408203e-169 < b < 3.7052502960789305e-110 or 2.9494967590524297e+19 < b

   1. Initial program 52.0

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

   2. Simplified 52.0

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

   4. Applied clear-num 52.0

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

   6. Applied *-un-lft-identity 52.0

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

   7. Applied times-frac 52.0

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

   8. Applied add-cube-cbrt 52.0

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

   9. Applied times-frac 52.0

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

   10. Simplified 52.0

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

   11. Simplified 52.0

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

   12. Taylor expanded around inf 9.9

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

   if 3.7052502960789305e-110 < b < 2.9494967590524297e+19

   1. Initial program 37.3

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

   2. Simplified 37.3

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

   4. Applied clear-num 37.3

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

   6. Applied *-un-lft-identity 37.3

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

   7. Applied times-frac 37.3

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

   8. Applied add-cube-cbrt 37.3

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

   9. Applied times-frac 37.3

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

   10. Simplified 37.3

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

   11. Simplified 37.3

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

   13. Applied flip-- 37.3

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

   14. Simplified 16.2

       \[\leadsto \frac{1}{2} \cdot \frac{\frac{\color{blue}{0 - \left(4 \cdot a\right) \cdot c}}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} + b}}{a}\]
3. Recombined 4 regimes into one program.

4. Final simplification 10.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -1.478406535480561669630649836752919254545 \cdot 10^{60}:\\ \;\;\;\;1 \cdot \left(\frac{c}{b} - \frac{b}{a}\right)\\ \mathbf{elif}\;b \le 2.175674080408202904737521150531781836244 \cdot 10^{-169}:\\ \;\;\;\;\frac{1}{2} \cdot \frac{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} - b}{a}\\ \mathbf{elif}\;b \le 3.705250296078930544323375298653357812472 \cdot 10^{-110} \lor \neg \left(b \le 29494967590524297216\right):\\ \;\;\;\;\frac{1}{2} \cdot \left(-2 \cdot \frac{c}{b}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{-\left(4 \cdot a\right) \cdot c}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} + b}}{a} \cdot \frac{1}{2}\\ \end{array}\]

Reproduce

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

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

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