The quadratic formula (r1)

Average Error: 34.3 → 8.6

Time: 5.0s

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 -1.7884666465826799 \cdot 10^{121}:\\ \;\;\;\;\frac{2 \cdot \frac{a \cdot c}{b} - 2 \cdot b}{2 \cdot a}\\ \mathbf{elif}\;b \le -6.27850456875614525 \cdot 10^{-182}:\\ \;\;\;\;\frac{\left(-b\right) + \sqrt{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}} \cdot \sqrt{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{elif}\;b \le 1.32579379880372662 \cdot 10^{154}:\\ \;\;\;\;\frac{1}{1} \cdot \frac{\left(\frac{1}{2} \cdot 4\right) \cdot c}{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{1}}{\frac{2}{\frac{4}{1} \cdot c} \cdot \left(\left(-b\right) - \left(b - 2 \cdot \frac{a \cdot c}{b}\right)\right)}\\ \end{array}\]

C

double f(double a, double b, double c) {
        double r73550 = b;
        double r73551 = -r73550;
        double r73552 = r73550 * r73550;
        double r73553 = 4.0;
        double r73554 = a;
        double r73555 = r73553 * r73554;
        double r73556 = c;
        double r73557 = r73555 * r73556;
        double r73558 = r73552 - r73557;
        double r73559 = sqrt(r73558);
        double r73560 = r73551 + r73559;
        double r73561 = 2.0;
        double r73562 = r73561 * r73554;
        double r73563 = r73560 / r73562;
        return r73563;
}

↓

double f(double a, double b, double c) {
        double r73564 = b;
        double r73565 = -1.78846664658268e+121;
        bool r73566 = r73564 <= r73565;
        double r73567 = 2.0;
        double r73568 = a;
        double r73569 = c;
        double r73570 = r73568 * r73569;
        double r73571 = r73570 / r73564;
        double r73572 = r73567 * r73571;
        double r73573 = 2.0;
        double r73574 = r73573 * r73564;
        double r73575 = r73572 - r73574;
        double r73576 = r73567 * r73568;
        double r73577 = r73575 / r73576;
        double r73578 = -6.278504568756145e-182;
        bool r73579 = r73564 <= r73578;
        double r73580 = -r73564;
        double r73581 = r73564 * r73564;
        double r73582 = 4.0;
        double r73583 = r73582 * r73568;
        double r73584 = r73583 * r73569;
        double r73585 = r73581 - r73584;
        double r73586 = sqrt(r73585);
        double r73587 = sqrt(r73586);
        double r73588 = r73587 * r73587;
        double r73589 = r73580 + r73588;
        double r73590 = r73589 / r73576;
        double r73591 = 1.3257937988037266e+154;
        bool r73592 = r73564 <= r73591;
        double r73593 = 1.0;
        double r73594 = r73593 / r73593;
        double r73595 = r73593 / r73567;
        double r73596 = r73595 * r73582;
        double r73597 = r73596 * r73569;
        double r73598 = r73580 - r73586;
        double r73599 = r73597 / r73598;
        double r73600 = r73594 * r73599;
        double r73601 = r73582 / r73593;
        double r73602 = r73601 * r73569;
        double r73603 = r73567 / r73602;
        double r73604 = r73564 - r73572;
        double r73605 = r73580 - r73604;
        double r73606 = r73603 * r73605;
        double r73607 = r73594 / r73606;
        double r73608 = r73592 ? r73600 : r73607;
        double r73609 = r73579 ? r73590 : r73608;
        double r73610 = r73566 ? r73577 : r73609;
        return r73610;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	34.3
Target	20.8
Herbie	8.6

\[\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 < -1.78846664658268e+121

   1. Initial program 52.3

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

   2. Taylor expanded around -inf 10.1

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

   if -1.78846664658268e+121 < b < -6.278504568756145e-182

   1. Initial program 7.0

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

   3. Applied add-sqr-sqrt 7.0

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

   4. Applied sqrt-prod 7.2

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

   if -6.278504568756145e-182 < b < 1.3257937988037266e+154

   1. Initial program 31.2

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

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

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

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

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

      \[\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* 15.6

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

       \[\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-/l* 14.5

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

   13. Simplified 9.6

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

   15. Applied div-inv 9.6

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

   16. Simplified 9.1

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

   if 1.3257937988037266e+154 < b

   1. Initial program 64.0

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

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

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

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

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

      \[\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* 37.6

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

       \[\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-/l* 37.6

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

   13. Simplified 37.5

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

   14. Taylor expanded around inf 8.1

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

4. Final simplification 8.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -1.7884666465826799 \cdot 10^{121}:\\ \;\;\;\;\frac{2 \cdot \frac{a \cdot c}{b} - 2 \cdot b}{2 \cdot a}\\ \mathbf{elif}\;b \le -6.27850456875614525 \cdot 10^{-182}:\\ \;\;\;\;\frac{\left(-b\right) + \sqrt{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}} \cdot \sqrt{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}{2 \cdot a}\\ \mathbf{elif}\;b \le 1.32579379880372662 \cdot 10^{154}:\\ \;\;\;\;\frac{1}{1} \cdot \frac{\left(\frac{1}{2} \cdot 4\right) \cdot c}{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1}{1}}{\frac{2}{\frac{4}{1} \cdot c} \cdot \left(\left(-b\right) - \left(b - 2 \cdot \frac{a \cdot c}{b}\right)\right)}\\ \end{array}\]

Reproduce

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