The quadratic formula (r1)

Average Error: 34.6 → 7.5

Time: 54.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{\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} \cdot \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}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot -1}{b}\\ \end{array}\]

C

double f(double a, double b, double c) {
        double r217170 = b;
        double r217171 = -r217170;
        double r217172 = r217170 * r217170;
        double r217173 = 4.0;
        double r217174 = a;
        double r217175 = r217173 * r217174;
        double r217176 = c;
        double r217177 = r217175 * r217176;
        double r217178 = r217172 - r217177;
        double r217179 = sqrt(r217178);
        double r217180 = r217171 + r217179;
        double r217181 = 2.0;
        double r217182 = r217181 * r217174;
        double r217183 = r217180 / r217182;
        return r217183;
}

↓

double f(double a, double b, double c) {
        double r217184 = b;
        double r217185 = -7.943482039519134e+75;
        bool r217186 = r217184 <= r217185;
        double r217187 = c;
        double r217188 = r217187 / r217184;
        double r217189 = a;
        double r217190 = r217184 / r217189;
        double r217191 = r217188 - r217190;
        double r217192 = 1.0;
        double r217193 = r217191 * r217192;
        double r217194 = -4.7180785979542405e-288;
        bool r217195 = r217184 <= r217194;
        double r217196 = r217184 * r217184;
        double r217197 = 4.0;
        double r217198 = r217197 * r217189;
        double r217199 = r217198 * r217187;
        double r217200 = r217196 - r217199;
        double r217201 = sqrt(r217200);
        double r217202 = -r217184;
        double r217203 = r217201 + r217202;
        double r217204 = 2.0;
        double r217205 = r217189 * r217204;
        double r217206 = r217203 / r217205;
        double r217207 = 1.1328213746323388e+81;
        bool r217208 = r217184 <= r217207;
        double r217209 = r217187 * r217189;
        double r217210 = r217197 * r217209;
        double r217211 = r217196 - r217210;
        double r217212 = sqrt(r217211);
        double r217213 = r217202 - r217212;
        double r217214 = cbrt(r217213);
        double r217215 = r217214 / r217187;
        double r217216 = cbrt(r217215);
        double r217217 = r217189 / r217216;
        double r217218 = r217217 / r217214;
        double r217219 = r217202 - r217201;
        double r217220 = cbrt(r217219);
        double r217221 = r217218 / r217220;
        double r217222 = r217221 / r217189;
        double r217223 = r217216 * r217216;
        double r217224 = r217197 / r217223;
        double r217225 = r217224 / r217204;
        double r217226 = r217222 * r217225;
        double r217227 = -1.0;
        double r217228 = r217187 * r217227;
        double r217229 = r217228 / r217184;
        double r217230 = r217208 ? r217226 : r217229;
        double r217231 = r217195 ? r217206 : r217230;
        double r217232 = r217186 ? r217193 : r217231;
        return r217232;
}

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)}}}}{\sqrt[3]{\color{blue}{1 \cdot \left(\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\right)}}}}{2 \cdot a}\]

   11. Applied cbrt-prod 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}{\sqrt[3]{1} \cdot \sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}}}{2 \cdot a}\]

   12. 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)}}}}}{\sqrt[3]{1} \cdot \sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}}{2 \cdot a}\]

   13. 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)}}}}{\sqrt[3]{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 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)}}}}{\sqrt[3]{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.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)}}}}}{\sqrt[3]{1} \cdot \sqrt[3]{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}}}{2 \cdot a}\]

   16. 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}}{\sqrt[3]{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}\]

   17. 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}}{\sqrt[3]{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{\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} \cdot \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}\\ \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)))