The quadratic formula (r1)

Average Error: 34.4 → 6.8

Time: 6.5s

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.30101840923646093 \cdot 10^{98}:\\ \;\;\;\;1 \cdot \left(\frac{c}{b} - \frac{b}{a}\right)\\ \mathbf{elif}\;b \le -2.37577225186574925 \cdot 10^{-260}:\\ \;\;\;\;\left(\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\right) \cdot \frac{1}{2 \cdot a}\\ \mathbf{elif}\;b \le 6.66645678090455348 \cdot 10^{68}:\\ \;\;\;\;\frac{\frac{1}{2} \cdot \left(\frac{4}{1} \cdot c\right)}{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \mathbf{else}:\\ \;\;\;\;-1 \cdot \frac{c}{b}\\ \end{array}\]

C

double f(double a, double b, double c) {
        double r143894 = b;
        double r143895 = -r143894;
        double r143896 = r143894 * r143894;
        double r143897 = 4.0;
        double r143898 = a;
        double r143899 = r143897 * r143898;
        double r143900 = c;
        double r143901 = r143899 * r143900;
        double r143902 = r143896 - r143901;
        double r143903 = sqrt(r143902);
        double r143904 = r143895 + r143903;
        double r143905 = 2.0;
        double r143906 = r143905 * r143898;
        double r143907 = r143904 / r143906;
        return r143907;
}

↓

double f(double a, double b, double c) {
        double r143908 = b;
        double r143909 = -4.301018409236461e+98;
        bool r143910 = r143908 <= r143909;
        double r143911 = 1.0;
        double r143912 = c;
        double r143913 = r143912 / r143908;
        double r143914 = a;
        double r143915 = r143908 / r143914;
        double r143916 = r143913 - r143915;
        double r143917 = r143911 * r143916;
        double r143918 = -2.3757722518657493e-260;
        bool r143919 = r143908 <= r143918;
        double r143920 = -r143908;
        double r143921 = r143908 * r143908;
        double r143922 = 4.0;
        double r143923 = r143922 * r143914;
        double r143924 = r143923 * r143912;
        double r143925 = r143921 - r143924;
        double r143926 = sqrt(r143925);
        double r143927 = r143920 + r143926;
        double r143928 = 1.0;
        double r143929 = 2.0;
        double r143930 = r143929 * r143914;
        double r143931 = r143928 / r143930;
        double r143932 = r143927 * r143931;
        double r143933 = 6.6664567809045535e+68;
        bool r143934 = r143908 <= r143933;
        double r143935 = r143928 / r143929;
        double r143936 = r143922 / r143928;
        double r143937 = r143936 * r143912;
        double r143938 = r143935 * r143937;
        double r143939 = r143920 - r143926;
        double r143940 = r143938 / r143939;
        double r143941 = -1.0;
        double r143942 = r143941 * r143913;
        double r143943 = r143934 ? r143940 : r143942;
        double r143944 = r143919 ? r143932 : r143943;
        double r143945 = r143910 ? r143917 : r143944;
        return r143945;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	34.4
Target	21.5
Herbie	6.8

\[\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 < -4.301018409236461e+98

   1. Initial program 47.2

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

   2. Taylor expanded around -inf 3.9

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

   3. Simplified 3.9

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

   if -4.301018409236461e+98 < b < -2.3757722518657493e-260

   1. Initial program 8.5

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

   3. Applied div-inv 8.7

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

   if -2.3757722518657493e-260 < b < 6.6664567809045535e+68

   1. Initial program 29.1

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

   3. Applied flip-+ 29.1

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

   4. Simplified 16.2

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

   6. Applied *-un-lft-identity 16.2

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

   7. Applied *-un-lft-identity 16.2

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

   8. Applied times-frac 16.2

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

   9. Applied associate-/l* 16.4

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

   10. Simplified 16.0

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

   12. Applied associate-/r* 15.8

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

   13. Simplified 9.6

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

   15. Applied *-un-lft-identity 9.6

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

   16. Applied add-sqr-sqrt 9.6

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

   17. Applied times-frac 9.6

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

   18. Applied div-inv 9.6

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

   19. Applied add-sqr-sqrt 9.6

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

   20. Applied times-frac 9.6

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

   21. Applied times-frac 9.7

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

   22. Simplified 9.7

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

   23. Simplified 9.6

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

   if 6.6664567809045535e+68 < b

   1. Initial program 58.7

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

   2. Taylor expanded around inf 3.5

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

4. Final simplification 6.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -4.30101840923646093 \cdot 10^{98}:\\ \;\;\;\;1 \cdot \left(\frac{c}{b} - \frac{b}{a}\right)\\ \mathbf{elif}\;b \le -2.37577225186574925 \cdot 10^{-260}:\\ \;\;\;\;\left(\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\right) \cdot \frac{1}{2 \cdot a}\\ \mathbf{elif}\;b \le 6.66645678090455348 \cdot 10^{68}:\\ \;\;\;\;\frac{\frac{1}{2} \cdot \left(\frac{4}{1} \cdot c\right)}{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \mathbf{else}:\\ \;\;\;\;-1 \cdot \frac{c}{b}\\ \end{array}\]

Reproduce

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