Average Error: 33.6 → 9.5
Time: 3.6m
Precision: 64
\[\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 -9.026475235538753 \cdot 10^{-68}:\\ \;\;\;\;-\frac{c}{b}\\ \mathbf{elif}\;b \le 2.850331809009435 \cdot 10^{+96}:\\ \;\;\;\;\frac{\frac{-1}{2} \cdot \left(\sqrt{(a \cdot \left(c \cdot -4\right) + \left(b \cdot b\right))_*} + b\right)}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array}\]
\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 -9.026475235538753 \cdot 10^{-68}:\\
\;\;\;\;-\frac{c}{b}\\

\mathbf{elif}\;b \le 2.850331809009435 \cdot 10^{+96}:\\
\;\;\;\;\frac{\frac{-1}{2} \cdot \left(\sqrt{(a \cdot \left(c \cdot -4\right) + \left(b \cdot b\right))_*} + b\right)}{a}\\

\mathbf{else}:\\
\;\;\;\;\frac{-b}{a}\\

\end{array}
double f(double a, double b, double c) {
        double r22531295 = b;
        double r22531296 = -r22531295;
        double r22531297 = r22531295 * r22531295;
        double r22531298 = 4.0;
        double r22531299 = a;
        double r22531300 = c;
        double r22531301 = r22531299 * r22531300;
        double r22531302 = r22531298 * r22531301;
        double r22531303 = r22531297 - r22531302;
        double r22531304 = sqrt(r22531303);
        double r22531305 = r22531296 - r22531304;
        double r22531306 = 2.0;
        double r22531307 = r22531306 * r22531299;
        double r22531308 = r22531305 / r22531307;
        return r22531308;
}
↓
double f(double a, double b, double c) {
        double r22531309 = b;
        double r22531310 = -9.026475235538753e-68;
        bool r22531311 = r22531309 <= r22531310;
        double r22531312 = c;
        double r22531313 = r22531312 / r22531309;
        double r22531314 = -r22531313;
        double r22531315 = 2.850331809009435e+96;
        bool r22531316 = r22531309 <= r22531315;
        double r22531317 = -0.5;
        double r22531318 = a;
        double r22531319 = -4.0;
        double r22531320 = r22531312 * r22531319;
        double r22531321 = r22531309 * r22531309;
        double r22531322 = fma(r22531318, r22531320, r22531321);
        double r22531323 = sqrt(r22531322);
        double r22531324 = r22531323 + r22531309;
        double r22531325 = r22531317 * r22531324;
        double r22531326 = r22531325 / r22531318;
        double r22531327 = -r22531309;
        double r22531328 = r22531327 / r22531318;
        double r22531329 = r22531316 ? r22531326 : r22531328;
        double r22531330 = r22531311 ? r22531314 : r22531329;
        return r22531330;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original33.6
Target20.7
Herbie9.5
\[\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 3 regimes

  2. if b < -9.026475235538753e-68

    1. Initial program 53.5

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

    2. Simplified53.5

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

    4. Applied *-un-lft-identity53.5

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

    5. Applied div-inv53.5

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

    6. Applied times-frac53.5

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

    7. Simplified53.5

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

    8. Simplified53.5

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

    9. Taylor expanded around -inf 8.3

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

    10. Simplified8.3

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

    if -9.026475235538753e-68 < b < 2.850331809009435e+96

    1. Initial program 12.6

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

    2. Simplified12.6

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

    4. Applied *-un-lft-identity12.6

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

    5. Applied div-inv12.6

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

    6. Applied times-frac12.7

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

    7. Simplified12.7

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

    8. Simplified12.7

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

    10. Applied associate-*r/12.6

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

    if 2.850331809009435e+96 < b

    1. Initial program 43.5

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

    2. Simplified43.5

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

    4. Applied *-un-lft-identity43.5

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

    5. Applied associate-/l*43.6

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

    6. Taylor expanded around 0 4.1

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

    7. Simplified4.1

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

  4. Final simplification9.5

    \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -9.026475235538753 \cdot 10^{-68}:\\ \;\;\;\;-\frac{c}{b}\\ \mathbf{elif}\;b \le 2.850331809009435 \cdot 10^{+96}:\\ \;\;\;\;\frac{\frac{-1}{2} \cdot \left(\sqrt{(a \cdot \left(c \cdot -4\right) + \left(b \cdot b\right))_*} + b\right)}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array}\]

Reproduce

herbie shell --seed 2019104 +o rules:numerics
(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)))