The quadratic formula (r1)

Average Error: 33.8 → 10.1

Time: 9.2s

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 -3.12428337420519208 \cdot 10^{57}:\\ \;\;\;\;1 \cdot \left(\frac{c}{b} - \frac{b}{a}\right)\\ \mathbf{elif}\;b \le 3.84613441880260993 \cdot 10^{-81}:\\ \;\;\;\;\frac{\frac{\sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)} - b}{2}}{a}\\ \mathbf{else}:\\ \;\;\;\;-1 \cdot \frac{c}{b}\\ \end{array}\]

C

double f(double a, double b, double c) {
        double r98510 = b;
        double r98511 = -r98510;
        double r98512 = r98510 * r98510;
        double r98513 = 4.0;
        double r98514 = a;
        double r98515 = r98513 * r98514;
        double r98516 = c;
        double r98517 = r98515 * r98516;
        double r98518 = r98512 - r98517;
        double r98519 = sqrt(r98518);
        double r98520 = r98511 + r98519;
        double r98521 = 2.0;
        double r98522 = r98521 * r98514;
        double r98523 = r98520 / r98522;
        return r98523;
}

↓

double f(double a, double b, double c) {
        double r98524 = b;
        double r98525 = -3.124283374205192e+57;
        bool r98526 = r98524 <= r98525;
        double r98527 = 1.0;
        double r98528 = c;
        double r98529 = r98528 / r98524;
        double r98530 = a;
        double r98531 = r98524 / r98530;
        double r98532 = r98529 - r98531;
        double r98533 = r98527 * r98532;
        double r98534 = 3.84613441880261e-81;
        bool r98535 = r98524 <= r98534;
        double r98536 = r98524 * r98524;
        double r98537 = 4.0;
        double r98538 = r98530 * r98528;
        double r98539 = r98537 * r98538;
        double r98540 = r98536 - r98539;
        double r98541 = sqrt(r98540);
        double r98542 = r98541 - r98524;
        double r98543 = 2.0;
        double r98544 = r98542 / r98543;
        double r98545 = r98544 / r98530;
        double r98546 = -1.0;
        double r98547 = r98546 * r98529;
        double r98548 = r98535 ? r98545 : r98547;
        double r98549 = r98526 ? r98533 : r98548;
        return r98549;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	33.8
Target	20.4
Herbie	10.1

\[\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 3 regimes

2. if b < -3.124283374205192e+57

   1. Initial program 39.5

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

   2. Simplified 39.5

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

   4. Applied pow1 39.5

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

   5. Applied pow1 39.5

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

   6. Applied pow1 39.5

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

   7. Applied pow-prod-down 39.5

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

   8. Applied pow-prod-down 39.5

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

   9. Simplified 39.5

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

   10. Taylor expanded around -inf 5.4

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

   11. Simplified 5.4

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

   if -3.124283374205192e+57 < b < 3.84613441880261e-81

   1. Initial program 12.7

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

   2. Simplified 12.7

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

   4. Applied pow1 12.7

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

   5. Applied pow1 12.7

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

   6. Applied pow1 12.7

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

   7. Applied pow-prod-down 12.7

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

   8. Applied pow-prod-down 12.7

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

   9. Simplified 12.7

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

   11. Applied *-un-lft-identity 12.7

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

   12. Applied div-inv 12.7

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

   13. Applied times-frac 12.8

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

   14. Simplified 12.8

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

   16. Applied associate-*r/ 12.7

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

   17. Simplified 12.7

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

   if 3.84613441880261e-81 < b

   1. Initial program 53.0

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

   2. Simplified 53.0

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

   4. Applied pow1 53.0

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

   5. Applied pow1 53.0

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

   6. Applied pow1 53.0

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

   7. Applied pow-prod-down 53.0

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

   8. Applied pow-prod-down 53.0

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

   9. Simplified 53.0

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

   10. Taylor expanded around inf 9.5

       \[\leadsto \color{blue}{-1 \cdot \frac{c}{b}}\]
3. Recombined 3 regimes into one program.

4. Final simplification 10.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -3.12428337420519208 \cdot 10^{57}:\\ \;\;\;\;1 \cdot \left(\frac{c}{b} - \frac{b}{a}\right)\\ \mathbf{elif}\;b \le 3.84613441880260993 \cdot 10^{-81}:\\ \;\;\;\;\frac{\frac{\sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)} - b}{2}}{a}\\ \mathbf{else}:\\ \;\;\;\;-1 \cdot \frac{c}{b}\\ \end{array}\]

Reproduce

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