The quadratic formula (r1)

Average Error: 34.6 → 7.5

Time: 56.3s

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 -7.943482039519133630405882994043698433958 \cdot 10^{75}:\\ \;\;\;\;\left(\frac{c}{b} - \frac{b}{a}\right) \cdot 1\\ \mathbf{elif}\;b \le -4.718078597954240507360630293401646945929 \cdot 10^{-288}:\\ \;\;\;\;\frac{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} + \left(-b\right)}{a \cdot 2}\\ \mathbf{elif}\;b \le 1.132821374632338820562375169502615703862 \cdot 10^{81}:\\ \;\;\;\;\frac{\frac{4}{\sqrt[3]{\frac{\sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(c \cdot a\right)}}}{c}} \cdot \sqrt[3]{\frac{\sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(c \cdot a\right)}}}{c}}}}{2} \cdot \frac{\frac{\frac{\frac{a}{\sqrt[3]{\frac{\sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(c \cdot a\right)}}}{c}}}}{\sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(c \cdot a\right)}}}}{\sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot -1}{b}\\ \end{array}\]

C

double f(double a, double b, double c) {
        double r187517 = b;
        double r187518 = -r187517;
        double r187519 = r187517 * r187517;
        double r187520 = 4.0;
        double r187521 = a;
        double r187522 = r187520 * r187521;
        double r187523 = c;
        double r187524 = r187522 * r187523;
        double r187525 = r187519 - r187524;
        double r187526 = sqrt(r187525);
        double r187527 = r187518 + r187526;
        double r187528 = 2.0;
        double r187529 = r187528 * r187521;
        double r187530 = r187527 / r187529;
        return r187530;
}

↓

double f(double a, double b, double c) {
        double r187531 = b;
        double r187532 = -7.943482039519134e+75;
        bool r187533 = r187531 <= r187532;
        double r187534 = c;
        double r187535 = r187534 / r187531;
        double r187536 = a;
        double r187537 = r187531 / r187536;
        double r187538 = r187535 - r187537;
        double r187539 = 1.0;
        double r187540 = r187538 * r187539;
        double r187541 = -4.7180785979542405e-288;
        bool r187542 = r187531 <= r187541;
        double r187543 = r187531 * r187531;
        double r187544 = 4.0;
        double r187545 = r187544 * r187536;
        double r187546 = r187545 * r187534;
        double r187547 = r187543 - r187546;
        double r187548 = sqrt(r187547);
        double r187549 = -r187531;
        double r187550 = r187548 + r187549;
        double r187551 = 2.0;
        double r187552 = r187536 * r187551;
        double r187553 = r187550 / r187552;
        double r187554 = 1.1328213746323388e+81;
        bool r187555 = r187531 <= r187554;
        double r187556 = r187534 * r187536;
        double r187557 = r187544 * r187556;
        double r187558 = r187543 - r187557;
        double r187559 = sqrt(r187558);
        double r187560 = r187549 - r187559;
        double r187561 = cbrt(r187560);
        double r187562 = r187561 / r187534;
        double r187563 = cbrt(r187562);
        double r187564 = r187563 * r187563;
        double r187565 = r187544 / r187564;
        double r187566 = r187565 / r187551;
        double r187567 = r187536 / r187563;
        double r187568 = r187567 / r187561;
        double r187569 = r187549 - r187548;
        double r187570 = cbrt(r187569);
        double r187571 = r187568 / r187570;
        double r187572 = r187571 / r187536;
        double r187573 = r187566 * r187572;
        double r187574 = -1.0;
        double r187575 = r187534 * r187574;
        double r187576 = r187575 / r187531;
        double r187577 = r187555 ? r187573 : r187576;
        double r187578 = r187542 ? r187553 : r187577;
        double r187579 = r187533 ? r187540 : r187578;
        return r187579;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	34.6
Target	21.0
Herbie	7.5

\[\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 < -7.943482039519134e+75

   1. Initial program 42.7

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

   2. Taylor expanded around -inf 4.2

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

   3. Simplified 4.2

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

   if -7.943482039519134e+75 < b < -4.7180785979542405e-288

   1. Initial program 9.3

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

   if -4.7180785979542405e-288 < b < 1.1328213746323388e+81

   1. Initial program 30.8

      \[\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-+ 30.8

      \[\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.0

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

   6. Applied add-cube-cbrt 16.7

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

   7. Applied associate-/r* 16.7

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

   8. Simplified 16.0

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

   10. Applied *-un-lft-identity 16.0

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

   11. Applied *-un-lft-identity 16.0

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

   12. Applied add-cube-cbrt 16.2

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

   13. Applied times-frac 16.2

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

   14. Applied times-frac 15.6

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

   15. Applied times-frac 15.2

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

   16. Applied times-frac 12.0

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

   if 1.1328213746323388e+81 < b

   1. Initial program 59.0

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

   2. Taylor expanded around inf 2.5

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

   3. Simplified 2.5

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

4. Final simplification 7.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -7.943482039519133630405882994043698433958 \cdot 10^{75}:\\ \;\;\;\;\left(\frac{c}{b} - \frac{b}{a}\right) \cdot 1\\ \mathbf{elif}\;b \le -4.718078597954240507360630293401646945929 \cdot 10^{-288}:\\ \;\;\;\;\frac{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} + \left(-b\right)}{a \cdot 2}\\ \mathbf{elif}\;b \le 1.132821374632338820562375169502615703862 \cdot 10^{81}:\\ \;\;\;\;\frac{\frac{4}{\sqrt[3]{\frac{\sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(c \cdot a\right)}}}{c}} \cdot \sqrt[3]{\frac{\sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(c \cdot a\right)}}}{c}}}}{2} \cdot \frac{\frac{\frac{\frac{a}{\sqrt[3]{\frac{\sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(c \cdot a\right)}}}{c}}}}{\sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(c \cdot a\right)}}}}{\sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot -1}{b}\\ \end{array}\]

Reproduce

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

  :herbie-target
  (if (< b 0.0) (/ (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)) (/ c (* a (/ (- (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)))))

  (/ (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)))