The quadratic formula (r1)

Average Error: 33.8 → 10.3

Time: 14.6s

Precision: 64

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

C

double f(double a, double b, double c) {
        double r84651 = b;
        double r84652 = -r84651;
        double r84653 = r84651 * r84651;
        double r84654 = 4.0;
        double r84655 = a;
        double r84656 = r84654 * r84655;
        double r84657 = c;
        double r84658 = r84656 * r84657;
        double r84659 = r84653 - r84658;
        double r84660 = sqrt(r84659);
        double r84661 = r84652 + r84660;
        double r84662 = 2.0;
        double r84663 = r84662 * r84655;
        double r84664 = r84661 / r84663;
        return r84664;
}

↓

double f(double a, double b, double c) {
        double r84665 = b;
        double r84666 = -4.919628179067154e+153;
        bool r84667 = r84665 <= r84666;
        double r84668 = c;
        double r84669 = r84668 / r84665;
        double r84670 = a;
        double r84671 = r84665 / r84670;
        double r84672 = r84669 - r84671;
        double r84673 = 1.0;
        double r84674 = r84672 * r84673;
        double r84675 = 2.071930020515771e-74;
        bool r84676 = r84665 <= r84675;
        double r84677 = r84665 * r84665;
        double r84678 = 4.0;
        double r84679 = r84678 * r84670;
        double r84680 = r84679 * r84668;
        double r84681 = r84677 - r84680;
        double r84682 = sqrt(r84681);
        double r84683 = r84682 - r84665;
        double r84684 = 2.0;
        double r84685 = r84684 * r84670;
        double r84686 = r84683 / r84685;
        double r84687 = -1.0;
        double r84688 = r84687 * r84669;
        double r84689 = r84676 ? r84686 : r84688;
        double r84690 = r84667 ? r84674 : r84689;
        return r84690;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	33.8
Target	20.4
Herbie	10.3

\[\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 < -4.919628179067154e+153

   1. Initial program 63.8

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

   2. Simplified 63.8

      \[\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 63.8

      \[\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 63.8

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

   7. Applied add-cube-cbrt 63.8

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

   8. Applied times-frac 63.8

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

   9. Simplified 63.8

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

   10. Simplified 63.8

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

   12. Applied *-un-lft-identity 63.8

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

   13. Applied associate-*l* 63.8

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

   14. Simplified 63.8

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

   15. Taylor expanded around -inf 2.1

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

   16. Simplified 2.1

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

   if -4.919628179067154e+153 < b < 2.071930020515771e-74

   1. Initial program 12.8

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

   2. Simplified 12.8

      \[\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 13.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 13.0

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

   7. Applied add-cube-cbrt 13.0

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

   8. Applied times-frac 13.0

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

   9. Simplified 13.0

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

   10. Simplified 12.9

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

   12. Applied *-un-lft-identity 12.9

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

   13. Applied associate-*l* 12.9

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

   14. Simplified 12.8

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

   if 2.071930020515771e-74 < b

   1. Initial program 53.2

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

   2. Simplified 53.2

      \[\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 53.2

      \[\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 53.2

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

   7. Applied add-cube-cbrt 53.2

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

   8. Applied times-frac 53.2

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

   9. Simplified 53.2

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

   10. Simplified 53.2

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

   12. Applied *-un-lft-identity 53.2

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

   13. Applied associate-*l* 53.2

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

   14. Simplified 53.2

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

   15. Taylor expanded around inf 9.2

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

4. Final simplification 10.3

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

Reproduce

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