The quadratic formula (r1)

Average Error: 34.0 → 7.3

Time: 57.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 -3.157094219357017 \cdot 10^{+135}:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \le 9.088113400659685 \cdot 10^{-185}:\\ \;\;\;\;\frac{\sqrt{b \cdot b - \left(c \cdot a\right) \cdot 4} - b}{a \cdot 2}\\ \mathbf{elif}\;b \le 1.8091015183831773 \cdot 10^{+43}:\\ \;\;\;\;\frac{1}{\sqrt{b \cdot b - \left(c \cdot a\right) \cdot 4} + b} \cdot \left(\sqrt{\frac{1}{2}} \cdot \left(\frac{c}{\frac{-1}{4}} \cdot \sqrt{\frac{1}{2}}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array}\]

C

double f(double a, double b, double c) {
        double r13409416 = b;
        double r13409417 = -r13409416;
        double r13409418 = r13409416 * r13409416;
        double r13409419 = 4.0;
        double r13409420 = a;
        double r13409421 = r13409419 * r13409420;
        double r13409422 = c;
        double r13409423 = r13409421 * r13409422;
        double r13409424 = r13409418 - r13409423;
        double r13409425 = sqrt(r13409424);
        double r13409426 = r13409417 + r13409425;
        double r13409427 = 2.0;
        double r13409428 = r13409427 * r13409420;
        double r13409429 = r13409426 / r13409428;
        return r13409429;
}

↓

double f(double a, double b, double c) {
        double r13409430 = b;
        double r13409431 = -3.157094219357017e+135;
        bool r13409432 = r13409430 <= r13409431;
        double r13409433 = c;
        double r13409434 = r13409433 / r13409430;
        double r13409435 = a;
        double r13409436 = r13409430 / r13409435;
        double r13409437 = r13409434 - r13409436;
        double r13409438 = 9.088113400659685e-185;
        bool r13409439 = r13409430 <= r13409438;
        double r13409440 = r13409430 * r13409430;
        double r13409441 = r13409433 * r13409435;
        double r13409442 = 4.0;
        double r13409443 = r13409441 * r13409442;
        double r13409444 = r13409440 - r13409443;
        double r13409445 = sqrt(r13409444);
        double r13409446 = r13409445 - r13409430;
        double r13409447 = 2.0;
        double r13409448 = r13409435 * r13409447;
        double r13409449 = r13409446 / r13409448;
        double r13409450 = 1.8091015183831773e+43;
        bool r13409451 = r13409430 <= r13409450;
        double r13409452 = 1.0;
        double r13409453 = r13409445 + r13409430;
        double r13409454 = r13409452 / r13409453;
        double r13409455 = 0.5;
        double r13409456 = sqrt(r13409455);
        double r13409457 = -0.25;
        double r13409458 = r13409433 / r13409457;
        double r13409459 = r13409458 * r13409456;
        double r13409460 = r13409456 * r13409459;
        double r13409461 = r13409454 * r13409460;
        double r13409462 = -r13409434;
        double r13409463 = r13409451 ? r13409461 : r13409462;
        double r13409464 = r13409439 ? r13409449 : r13409463;
        double r13409465 = r13409432 ? r13409437 : r13409464;
        return r13409465;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	34.0
Target	20.9
Herbie	7.3

\[\begin{array}{l} \mathbf{if}\;b \lt 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 < -3.157094219357017e+135

   1. Initial program 54.4

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

   2. Simplified 54.4

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

   3. Taylor expanded around -inf 2.8

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

   if -3.157094219357017e+135 < b < 9.088113400659685e-185

   1. Initial program 10.8

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

   2. Simplified 10.8

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

   if 9.088113400659685e-185 < b < 1.8091015183831773e+43

   1. Initial program 34.4

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

   2. Simplified 34.3

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

   4. Applied *-un-lft-identity 34.3

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

   5. Applied *-un-lft-identity 34.3

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

   6. Applied distribute-lft-out-- 34.3

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

   7. Applied associate-/l* 34.4

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

   9. Applied flip-- 34.5

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

   10. Applied associate-/r/ 34.5

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

   11. Applied *-un-lft-identity 34.5

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

   12. Applied times-frac 34.6

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

   13. Simplified 17.1

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

   15. Applied add-sqr-sqrt 17.6

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

   16. Applied *-un-lft-identity 17.6

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

   17. Applied times-frac 17.5

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

   18. Applied *-un-lft-identity 17.5

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

   19. Applied times-frac 17.4

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

   20. Simplified 17.4

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

   21. Simplified 7.7

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

   if 1.8091015183831773e+43 < b

   1. Initial program 56.4

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

   2. Simplified 56.4

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

   3. Taylor expanded around inf 4.2

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

   4. Simplified 4.2

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

4. Final simplification 7.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -3.157094219357017 \cdot 10^{+135}:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \le 9.088113400659685 \cdot 10^{-185}:\\ \;\;\;\;\frac{\sqrt{b \cdot b - \left(c \cdot a\right) \cdot 4} - b}{a \cdot 2}\\ \mathbf{elif}\;b \le 1.8091015183831773 \cdot 10^{+43}:\\ \;\;\;\;\frac{1}{\sqrt{b \cdot b - \left(c \cdot a\right) \cdot 4} + b} \cdot \left(\sqrt{\frac{1}{2}} \cdot \left(\frac{c}{\frac{-1}{4}} \cdot \sqrt{\frac{1}{2}}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array}\]

Reproduce

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

  :herbie-target
  (if (< b 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)))