The quadratic formula (r2)

Average Error: 34.0 → 7.2

Time: 28.5s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;b \le -3.575938583654324 \cdot 10^{+94}:\\ \;\;\;\;\frac{2 \cdot c}{2 \cdot \left(\frac{a}{b} \cdot c - b\right)}\\ \mathbf{elif}\;b \le 4.0232110844075136 \cdot 10^{-262}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ \mathbf{elif}\;b \le 2.6656023684116586 \cdot 10^{+55}:\\ \;\;\;\;\frac{1}{2} \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array}\]

C

double f(double a, double b, double c) {
        double r4610425 = b;
        double r4610426 = -r4610425;
        double r4610427 = r4610425 * r4610425;
        double r4610428 = 4.0;
        double r4610429 = a;
        double r4610430 = c;
        double r4610431 = r4610429 * r4610430;
        double r4610432 = r4610428 * r4610431;
        double r4610433 = r4610427 - r4610432;
        double r4610434 = sqrt(r4610433);
        double r4610435 = r4610426 - r4610434;
        double r4610436 = 2.0;
        double r4610437 = r4610436 * r4610429;
        double r4610438 = r4610435 / r4610437;
        return r4610438;
}

↓

double f(double a, double b, double c) {
        double r4610439 = b;
        double r4610440 = -3.575938583654324e+94;
        bool r4610441 = r4610439 <= r4610440;
        double r4610442 = 2.0;
        double r4610443 = c;
        double r4610444 = r4610442 * r4610443;
        double r4610445 = a;
        double r4610446 = r4610445 / r4610439;
        double r4610447 = r4610446 * r4610443;
        double r4610448 = r4610447 - r4610439;
        double r4610449 = r4610442 * r4610448;
        double r4610450 = r4610444 / r4610449;
        double r4610451 = 4.0232110844075136e-262;
        bool r4610452 = r4610439 <= r4610451;
        double r4610453 = -r4610439;
        double r4610454 = r4610439 * r4610439;
        double r4610455 = 4.0;
        double r4610456 = r4610445 * r4610443;
        double r4610457 = r4610455 * r4610456;
        double r4610458 = r4610454 - r4610457;
        double r4610459 = sqrt(r4610458);
        double r4610460 = r4610453 + r4610459;
        double r4610461 = r4610444 / r4610460;
        double r4610462 = 2.6656023684116586e+55;
        bool r4610463 = r4610439 <= r4610462;
        double r4610464 = 0.5;
        double r4610465 = r4610453 - r4610459;
        double r4610466 = r4610465 / r4610445;
        double r4610467 = r4610464 * r4610466;
        double r4610468 = r4610453 / r4610445;
        double r4610469 = r4610463 ? r4610467 : r4610468;
        double r4610470 = r4610452 ? r4610461 : r4610469;
        double r4610471 = r4610441 ? r4610450 : r4610470;
        return r4610471;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	34.0
Target	21.3
Herbie	7.2

\[\begin{array}{l} \mathbf{if}\;b \lt 0:\\ \;\;\;\;\frac{c}{a \cdot \frac{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}\\ \end{array}\]

Derivation

1. Split input into 4 regimes

2. if b < -3.575938583654324e+94

   1. Initial program 58.9

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

   3. Applied *-un-lft-identity 58.9

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

   4. Applied *-un-lft-identity 58.9

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

   5. Applied distribute-rgt-neg-in 58.9

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

   6. Applied distribute-lft-out-- 58.9

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

   7. Applied associate-/l* 58.9

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

   9. Applied flip-- 59.0

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

   10. Applied associate-/r/ 59.0

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

   11. Applied associate-/r* 59.0

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

   12. Simplified 30.3

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

   13. Taylor expanded around inf 29.6

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

   14. Taylor expanded around -inf 6.4

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

   15. Simplified 2.5

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

   if -3.575938583654324e+94 < b < 4.0232110844075136e-262

   1. Initial program 30.8

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

   3. Applied *-un-lft-identity 30.8

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

   4. Applied *-un-lft-identity 30.8

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

   5. Applied distribute-rgt-neg-in 30.8

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

   6. Applied distribute-lft-out-- 30.8

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

   7. Applied associate-/l* 30.8

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

   9. Applied flip-- 31.0

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

   10. Applied associate-/r/ 31.0

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

   11. Applied associate-/r* 31.0

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

   12. Simplified 16.1

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

   13. Taylor expanded around inf 9.8

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

   if 4.0232110844075136e-262 < b < 2.6656023684116586e+55

   1. Initial program 9.0

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

   3. Applied *-un-lft-identity 9.0

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

   4. Applied *-un-lft-identity 9.0

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

   5. Applied distribute-rgt-neg-in 9.0

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

   6. Applied distribute-lft-out-- 9.0

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

   7. Applied associate-/l* 9.2

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

   9. Applied *-un-lft-identity 9.2

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

   10. Applied times-frac 9.2

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

   11. Applied add-sqr-sqrt 9.2

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

   12. Applied times-frac 9.2

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

   13. Simplified 9.2

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

   14. Simplified 9.0

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

   if 2.6656023684116586e+55 < b

   1. Initial program 37.1

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

   3. Applied *-un-lft-identity 37.1

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

   4. Applied *-un-lft-identity 37.1

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

   5. Applied distribute-rgt-neg-in 37.1

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

   6. Applied distribute-lft-out-- 37.1

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

   7. Applied associate-/l* 37.2

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

   9. Applied flip-- 60.2

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

   10. Applied associate-/r/ 60.2

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

   11. Applied associate-/r* 60.2

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

   12. Simplified 60.3

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

   13. Taylor expanded around inf 60.3

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

   14. Taylor expanded around 0 6.5

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

   15. Simplified 6.5

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

4. Final simplification 7.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -3.575938583654324 \cdot 10^{+94}:\\ \;\;\;\;\frac{2 \cdot c}{2 \cdot \left(\frac{a}{b} \cdot c - b\right)}\\ \mathbf{elif}\;b \le 4.0232110844075136 \cdot 10^{-262}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ \mathbf{elif}\;b \le 2.6656023684116586 \cdot 10^{+55}:\\ \;\;\;\;\frac{1}{2} \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array}\]

Reproduce

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

  :herbie-target
  (if (< b 0) (/ c (* a (/ (+ (- b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)))) (/ (- (- b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)))

  (/ (- (- b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)))