Average Error: 33.4 → 16.7
Time: 18.5s
Precision: 64
\[\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 8.670930634061063 \cdot 10^{-143}:\\ \;\;\;\;\frac{\left(\sqrt{\mathsf{fma}\left(c, \left(a \cdot -4\right), \left(b \cdot b\right)\right)} - b\right) \cdot \frac{1}{2}}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{-\frac{b}{c}}\\ \end{array}\]
\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 8.670930634061063 \cdot 10^{-143}:\\
\;\;\;\;\frac{\left(\sqrt{\mathsf{fma}\left(c, \left(a \cdot -4\right), \left(b \cdot b\right)\right)} - b\right) \cdot \frac{1}{2}}{a}\\

\mathbf{else}:\\
\;\;\;\;\frac{1}{-\frac{b}{c}}\\

\end{array}
double f(double a, double b, double c) {
        double r3898028 = b;
        double r3898029 = -r3898028;
        double r3898030 = r3898028 * r3898028;
        double r3898031 = 4.0;
        double r3898032 = a;
        double r3898033 = r3898031 * r3898032;
        double r3898034 = c;
        double r3898035 = r3898033 * r3898034;
        double r3898036 = r3898030 - r3898035;
        double r3898037 = sqrt(r3898036);
        double r3898038 = r3898029 + r3898037;
        double r3898039 = 2.0;
        double r3898040 = r3898039 * r3898032;
        double r3898041 = r3898038 / r3898040;
        return r3898041;
}
↓
double f(double a, double b, double c) {
        double r3898042 = b;
        double r3898043 = 8.670930634061063e-143;
        bool r3898044 = r3898042 <= r3898043;
        double r3898045 = c;
        double r3898046 = a;
        double r3898047 = -4.0;
        double r3898048 = r3898046 * r3898047;
        double r3898049 = r3898042 * r3898042;
        double r3898050 = fma(r3898045, r3898048, r3898049);
        double r3898051 = sqrt(r3898050);
        double r3898052 = r3898051 - r3898042;
        double r3898053 = 0.5;
        double r3898054 = r3898052 * r3898053;
        double r3898055 = r3898054 / r3898046;
        double r3898056 = 1.0;
        double r3898057 = r3898042 / r3898045;
        double r3898058 = -r3898057;
        double r3898059 = r3898056 / r3898058;
        double r3898060 = r3898044 ? r3898055 : r3898059;
        return r3898060;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original33.4
Target19.8
Herbie16.7
\[\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 2 regimes

  2. if b < 8.670930634061063e-143

    1. Initial program 20.2

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

    2. Simplified20.2

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

    4. Applied *-un-lft-identity20.2

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

    5. Applied div-inv20.2

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

    6. Applied times-frac20.3

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

    7. Simplified20.3

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

    8. Simplified20.3

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

    10. Applied associate-*r/20.2

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

    if 8.670930634061063e-143 < b

    1. Initial program 49.8

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

    2. Simplified49.8

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

    4. Applied clear-num49.9

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

    5. Taylor expanded around 0 12.3

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

    6. Simplified12.3

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

  4. Final simplification16.7

    \[\leadsto \begin{array}{l} \mathbf{if}\;b \le 8.670930634061063 \cdot 10^{-143}:\\ \;\;\;\;\frac{\left(\sqrt{\mathsf{fma}\left(c, \left(a \cdot -4\right), \left(b \cdot b\right)\right)} - b\right) \cdot \frac{1}{2}}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{-\frac{b}{c}}\\ \end{array}\]

Reproduce

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