The quadratic formula (r1)

Average Error: 34.0 → 7.3

Time: 47.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 r25599519 = b;
        double r25599520 = -r25599519;
        double r25599521 = r25599519 * r25599519;
        double r25599522 = 4.0;
        double r25599523 = a;
        double r25599524 = r25599522 * r25599523;
        double r25599525 = c;
        double r25599526 = r25599524 * r25599525;
        double r25599527 = r25599521 - r25599526;
        double r25599528 = sqrt(r25599527);
        double r25599529 = r25599520 + r25599528;
        double r25599530 = 2.0;
        double r25599531 = r25599530 * r25599523;
        double r25599532 = r25599529 / r25599531;
        return r25599532;
}

↓

double f(double a, double b, double c) {
        double r25599533 = b;
        double r25599534 = -3.157094219357017e+135;
        bool r25599535 = r25599533 <= r25599534;
        double r25599536 = c;
        double r25599537 = r25599536 / r25599533;
        double r25599538 = a;
        double r25599539 = r25599533 / r25599538;
        double r25599540 = r25599537 - r25599539;
        double r25599541 = 9.088113400659685e-185;
        bool r25599542 = r25599533 <= r25599541;
        double r25599543 = r25599533 * r25599533;
        double r25599544 = r25599536 * r25599538;
        double r25599545 = 4.0;
        double r25599546 = r25599544 * r25599545;
        double r25599547 = r25599543 - r25599546;
        double r25599548 = sqrt(r25599547);
        double r25599549 = r25599548 - r25599533;
        double r25599550 = 2.0;
        double r25599551 = r25599538 * r25599550;
        double r25599552 = r25599549 / r25599551;
        double r25599553 = 1.8091015183831773e+43;
        bool r25599554 = r25599533 <= r25599553;
        double r25599555 = 1.0;
        double r25599556 = r25599548 + r25599533;
        double r25599557 = r25599555 / r25599556;
        double r25599558 = 0.5;
        double r25599559 = sqrt(r25599558);
        double r25599560 = -0.25;
        double r25599561 = r25599536 / r25599560;
        double r25599562 = r25599561 * r25599559;
        double r25599563 = r25599559 * r25599562;
        double r25599564 = r25599557 * r25599563;
        double r25599565 = -r25599537;
        double r25599566 = r25599554 ? r25599564 : r25599565;
        double r25599567 = r25599542 ? r25599552 : r25599566;
        double r25599568 = r25599535 ? r25599540 : r25599567;
        return r25599568;
}

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{\color{blue}{1 \cdot \left(\sqrt{b \cdot b - \left(c \cdot a\right) \cdot 4} - b\right)}}{2 \cdot a}\]

   5. 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}}}\]
   6. Using strategy rm

   7. 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}}}}\]

   8. 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)}}\]

   9. 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)}\]

   10. 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}}\]

   11. 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}\]
   12. Using strategy rm

   13. 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}\]

   14. 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}\]

   15. 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}\]

   16. 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}\]

   17. 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}\]

   18. 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}\]

   19. 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)))