The quadratic formula (r1)

Average Error: 33.0 → 6.6

Time: 51.4s

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 -9.139254247068609 \cdot 10^{+140}:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \le 9.931313556234952 \cdot 10^{-296}:\\ \;\;\;\;\frac{\sqrt{b \cdot b - \left(c \cdot a\right) \cdot 4} - b}{a} \cdot \frac{1}{2}\\ \mathbf{elif}\;b \le 6.523631550102089 \cdot 10^{+89}:\\ \;\;\;\;\frac{c \cdot -2}{\sqrt{b \cdot b - \left(c \cdot a\right) \cdot 4} + b}\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array}\]

C

double f(double a, double b, double c) {
        double r27712794 = b;
        double r27712795 = -r27712794;
        double r27712796 = r27712794 * r27712794;
        double r27712797 = 4.0;
        double r27712798 = a;
        double r27712799 = r27712797 * r27712798;
        double r27712800 = c;
        double r27712801 = r27712799 * r27712800;
        double r27712802 = r27712796 - r27712801;
        double r27712803 = sqrt(r27712802);
        double r27712804 = r27712795 + r27712803;
        double r27712805 = 2.0;
        double r27712806 = r27712805 * r27712798;
        double r27712807 = r27712804 / r27712806;
        return r27712807;
}

↓

double f(double a, double b, double c) {
        double r27712808 = b;
        double r27712809 = -9.139254247068609e+140;
        bool r27712810 = r27712808 <= r27712809;
        double r27712811 = c;
        double r27712812 = r27712811 / r27712808;
        double r27712813 = a;
        double r27712814 = r27712808 / r27712813;
        double r27712815 = r27712812 - r27712814;
        double r27712816 = 9.931313556234952e-296;
        bool r27712817 = r27712808 <= r27712816;
        double r27712818 = r27712808 * r27712808;
        double r27712819 = r27712811 * r27712813;
        double r27712820 = 4.0;
        double r27712821 = r27712819 * r27712820;
        double r27712822 = r27712818 - r27712821;
        double r27712823 = sqrt(r27712822);
        double r27712824 = r27712823 - r27712808;
        double r27712825 = r27712824 / r27712813;
        double r27712826 = 0.5;
        double r27712827 = r27712825 * r27712826;
        double r27712828 = 6.523631550102089e+89;
        bool r27712829 = r27712808 <= r27712828;
        double r27712830 = -2.0;
        double r27712831 = r27712811 * r27712830;
        double r27712832 = r27712823 + r27712808;
        double r27712833 = r27712831 / r27712832;
        double r27712834 = -r27712812;
        double r27712835 = r27712829 ? r27712833 : r27712834;
        double r27712836 = r27712817 ? r27712827 : r27712835;
        double r27712837 = r27712810 ? r27712815 : r27712836;
        return r27712837;
}

Error

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	33.0
Target	20.1
Herbie	6.6

\[\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 4 regimes

2. if b < -9.139254247068609e+140

   1. Initial program 55.8

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

   2. Simplified 55.8

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

   3. Taylor expanded around -inf 1.6

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

   if -9.139254247068609e+140 < b < 9.931313556234952e-296

   1. Initial program 8.7

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

   2. Simplified 8.7

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

   4. Applied *-un-lft-identity 8.7

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

   5. Applied *-un-lft-identity 8.7

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

   6. Applied distribute-lft-out-- 8.7

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

   7. Applied associate-/l* 8.9

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

   9. Applied *-un-lft-identity 8.9

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

   10. Applied times-frac 8.8

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

   11. Applied add-sqr-sqrt 8.8

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

   12. Applied times-frac 8.8

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

   13. Simplified 8.8

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

   14. Simplified 8.7

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

   if 9.931313556234952e-296 < b < 6.523631550102089e+89

   1. Initial program 32.6

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

   2. Simplified 32.6

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

   4. Applied *-un-lft-identity 32.6

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

   5. Applied *-un-lft-identity 32.6

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

   6. Applied distribute-lft-out-- 32.6

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

   7. Applied associate-/l* 32.6

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

   9. Applied flip-- 32.7

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

   10. Applied associate-/r/ 32.8

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

   11. Applied *-un-lft-identity 32.8

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

   12. Applied times-frac 32.8

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

   13. Simplified 16.4

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

   14. Taylor expanded around inf 9.3

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

   16. Applied un-div-inv 9.2

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

   if 6.523631550102089e+89 < b

   1. Initial program 58.7

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

   2. Simplified 58.7

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

   3. Taylor expanded around inf 2.6

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

   4. Simplified 2.6

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

4. Final simplification 6.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -9.139254247068609 \cdot 10^{+140}:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \le 9.931313556234952 \cdot 10^{-296}:\\ \;\;\;\;\frac{\sqrt{b \cdot b - \left(c \cdot a\right) \cdot 4} - b}{a} \cdot \frac{1}{2}\\ \mathbf{elif}\;b \le 6.523631550102089 \cdot 10^{+89}:\\ \;\;\;\;\frac{c \cdot -2}{\sqrt{b \cdot b - \left(c \cdot a\right) \cdot 4} + b}\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array}\]

Reproduce

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