The quadratic formula (r2)

Average Accuracy: 46.5% → 82.8%

Time: 19.3s

Precision: binary64

Cost: 27152

Math

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

↓

\[\begin{array}{l} t_0 := \mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)\\ \mathbf{if}\;b \leq -3.35 \cdot 10^{-74}:\\ \;\;\;\;\frac{-c}{b}\\ \mathbf{elif}\;b \leq -3.8 \cdot 10^{-154}:\\ \;\;\;\;\frac{\frac{b \cdot b - t_0}{a \cdot -2}}{b - \sqrt{t_0}}\\ \mathbf{elif}\;b \leq -4.1 \cdot 10^{-171}:\\ \;\;\;\;\frac{-0.5}{0.5 \cdot \frac{b}{c} + -0.5 \cdot \frac{a}{b}}\\ \mathbf{elif}\;b \leq -1.85 \cdot 10^{-199}:\\ \;\;\;\;\frac{-0.5}{\frac{a}{b + {\left(e^{0.25 \cdot \left(\log \left(c \cdot 4\right) - \log \left(\frac{-1}{a}\right)\right)}\right)}^{2}}}\\ \mathbf{elif}\;b \leq 8.5 \cdot 10^{+35}:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + -4 \cdot \left(c \cdot a\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \end{array} \]

FPCore

(FPCore (a b c)
 :precision binary64
 (/ (- (- b) (sqrt (- (* b b) (* 4.0 (* a c))))) (* 2.0 a)))

↓

(FPCore (a b c)
 :precision binary64
 (let* ((t_0 (fma c (* a -4.0) (* b b))))
   (if (<= b -3.35e-74)
     (/ (- c) b)
     (if (<= b -3.8e-154)
       (/ (/ (- (* b b) t_0) (* a -2.0)) (- b (sqrt t_0)))
       (if (<= b -4.1e-171)
         (/ -0.5 (+ (* 0.5 (/ b c)) (* -0.5 (/ a b))))
         (if (<= b -1.85e-199)
           (/
            -0.5
            (/
             a
             (+
              b
              (pow (exp (* 0.25 (- (log (* c 4.0)) (log (/ -1.0 a))))) 2.0))))
           (if (<= b 8.5e+35)
             (/ (- (- b) (sqrt (+ (* b b) (* -4.0 (* c a))))) (* a 2.0))
             (- (/ c b) (/ b a)))))))))

C

double code(double a, double b, double c) {
	return (-b - sqrt(((b * b) - (4.0 * (a * c))))) / (2.0 * a);
}

↓

double code(double a, double b, double c) {
	double t_0 = fma(c, (a * -4.0), (b * b));
	double tmp;
	if (b <= -3.35e-74) {
		tmp = -c / b;
	} else if (b <= -3.8e-154) {
		tmp = (((b * b) - t_0) / (a * -2.0)) / (b - sqrt(t_0));
	} else if (b <= -4.1e-171) {
		tmp = -0.5 / ((0.5 * (b / c)) + (-0.5 * (a / b)));
	} else if (b <= -1.85e-199) {
		tmp = -0.5 / (a / (b + pow(exp((0.25 * (log((c * 4.0)) - log((-1.0 / a))))), 2.0)));
	} else if (b <= 8.5e+35) {
		tmp = (-b - sqrt(((b * b) + (-4.0 * (c * a))))) / (a * 2.0);
	} else {
		tmp = (c / b) - (b / a);
	}
	return tmp;
}

Julia

function code(a, b, c)
	return Float64(Float64(Float64(-b) - sqrt(Float64(Float64(b * b) - Float64(4.0 * Float64(a * c))))) / Float64(2.0 * a))
end

↓

function code(a, b, c)
	t_0 = fma(c, Float64(a * -4.0), Float64(b * b))
	tmp = 0.0
	if (b <= -3.35e-74)
		tmp = Float64(Float64(-c) / b);
	elseif (b <= -3.8e-154)
		tmp = Float64(Float64(Float64(Float64(b * b) - t_0) / Float64(a * -2.0)) / Float64(b - sqrt(t_0)));
	elseif (b <= -4.1e-171)
		tmp = Float64(-0.5 / Float64(Float64(0.5 * Float64(b / c)) + Float64(-0.5 * Float64(a / b))));
	elseif (b <= -1.85e-199)
		tmp = Float64(-0.5 / Float64(a / Float64(b + (exp(Float64(0.25 * Float64(log(Float64(c * 4.0)) - log(Float64(-1.0 / a))))) ^ 2.0))));
	elseif (b <= 8.5e+35)
		tmp = Float64(Float64(Float64(-b) - sqrt(Float64(Float64(b * b) + Float64(-4.0 * Float64(c * a))))) / Float64(a * 2.0));
	else
		tmp = Float64(Float64(c / b) - Float64(b / a));
	end
	return tmp
end

Wolfram

code[a_, b_, c_] := N[(N[((-b) - N[Sqrt[N[(N[(b * b), $MachinePrecision] - N[(4.0 * N[(a * c), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] / N[(2.0 * a), $MachinePrecision]), $MachinePrecision]

↓

code[a_, b_, c_] := Block[{t$95$0 = N[(c * N[(a * -4.0), $MachinePrecision] + N[(b * b), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[b, -3.35e-74], N[((-c) / b), $MachinePrecision], If[LessEqual[b, -3.8e-154], N[(N[(N[(N[(b * b), $MachinePrecision] - t$95$0), $MachinePrecision] / N[(a * -2.0), $MachinePrecision]), $MachinePrecision] / N[(b - N[Sqrt[t$95$0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[b, -4.1e-171], N[(-0.5 / N[(N[(0.5 * N[(b / c), $MachinePrecision]), $MachinePrecision] + N[(-0.5 * N[(a / b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[b, -1.85e-199], N[(-0.5 / N[(a / N[(b + N[Power[N[Exp[N[(0.25 * N[(N[Log[N[(c * 4.0), $MachinePrecision]], $MachinePrecision] - N[Log[N[(-1.0 / a), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[b, 8.5e+35], N[(N[((-b) - N[Sqrt[N[(N[(b * b), $MachinePrecision] + N[(-4.0 * N[(c * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] / N[(a * 2.0), $MachinePrecision]), $MachinePrecision], N[(N[(c / b), $MachinePrecision] - N[(b / a), $MachinePrecision]), $MachinePrecision]]]]]]]

Target

Original	46.5%
Target	66.6%
Herbie	82.8%

\[\begin{array}{l} \mathbf{if}\;b < 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 6 regimes

2. if b < -3.3499999999999998e-74

   1. Initial program 16.0%

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

   2. Simplified 15.9%

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

      [Start] 16.0	\[ \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      *-lft-identity [<=] 16.0	\[ \color{blue}{1 \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}} \]
      metadata-eval [<=] 16.0	\[ \color{blue}{\left(--1\right)} \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      associate-*r/ [=>] 16.0	\[ \color{blue}{\frac{\left(--1\right) \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)}{2 \cdot a}} \]
      associate-*l/ [<=] 15.9	\[ \color{blue}{\frac{--1}{2 \cdot a} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      distribute-neg-frac [<=] 15.9	\[ \color{blue}{\left(-\frac{-1}{2 \cdot a}\right)} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right) \]
      distribute-lft-neg-in [<=] 15.9	\[ \color{blue}{-\frac{-1}{2 \cdot a} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      distribute-rgt-neg-out [<=] 15.9	\[ \color{blue}{\frac{-1}{2 \cdot a} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)} \]
      associate-/r* [=>] 15.9	\[ \color{blue}{\frac{\frac{-1}{2}}{a}} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right) \]
      metadata-eval [=>] 15.9	\[ \frac{\color{blue}{-0.5}}{a} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right) \]
      sub-neg [=>] 15.9	\[ \frac{-0.5}{a} \cdot \left(-\color{blue}{\left(\left(-b\right) + \left(-\sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)}\right) \]
      distribute-neg-out [=>] 15.9	\[ \frac{-0.5}{a} \cdot \left(-\color{blue}{\left(-\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)}\right) \]
      remove-double-neg [=>] 15.9	\[ \frac{-0.5}{a} \cdot \color{blue}{\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      sub-neg [=>] 15.9	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{b \cdot b + \left(-4 \cdot \left(a \cdot c\right)\right)}}\right) \]
      +-commutative [=>] 15.9	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{\left(-4 \cdot \left(a \cdot c\right)\right) + b \cdot b}}\right) \]

   3. Taylor expanded in b around -inf 86.3%

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

   4. Simplified 86.3%

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

      [Start] 86.3	\[ -1 \cdot \frac{c}{b} \]
      mul-1-neg [=>] 86.3	\[ \color{blue}{-\frac{c}{b}} \]
      distribute-neg-frac [=>] 86.3	\[ \color{blue}{\frac{-c}{b}} \]

   if -3.3499999999999998e-74 < b < -3.8000000000000001e-154

   1. Initial program 61.4%

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

   2. Simplified 61.3%

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

      [Start] 61.4	\[ \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      *-lft-identity [<=] 61.4	\[ \color{blue}{1 \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}} \]
      metadata-eval [<=] 61.4	\[ \color{blue}{\left(--1\right)} \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      associate-*r/ [=>] 61.4	\[ \color{blue}{\frac{\left(--1\right) \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)}{2 \cdot a}} \]
      associate-*l/ [<=] 61.3	\[ \color{blue}{\frac{--1}{2 \cdot a} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      distribute-neg-frac [<=] 61.3	\[ \color{blue}{\left(-\frac{-1}{2 \cdot a}\right)} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right) \]
      distribute-lft-neg-in [<=] 61.3	\[ \color{blue}{-\frac{-1}{2 \cdot a} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      distribute-rgt-neg-out [<=] 61.3	\[ \color{blue}{\frac{-1}{2 \cdot a} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)} \]
      associate-/r* [=>] 61.3	\[ \color{blue}{\frac{\frac{-1}{2}}{a}} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right) \]
      metadata-eval [=>] 61.3	\[ \frac{\color{blue}{-0.5}}{a} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right) \]
      sub-neg [=>] 61.3	\[ \frac{-0.5}{a} \cdot \left(-\color{blue}{\left(\left(-b\right) + \left(-\sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)}\right) \]
      distribute-neg-out [=>] 61.3	\[ \frac{-0.5}{a} \cdot \left(-\color{blue}{\left(-\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)}\right) \]
      remove-double-neg [=>] 61.3	\[ \frac{-0.5}{a} \cdot \color{blue}{\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      sub-neg [=>] 61.3	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{b \cdot b + \left(-4 \cdot \left(a \cdot c\right)\right)}}\right) \]
      +-commutative [=>] 61.3	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{\left(-4 \cdot \left(a \cdot c\right)\right) + b \cdot b}}\right) \]

   3. Applied egg-rr 61.5%

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

      [Start] 61.3	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}\right) \]
      clear-num [=>] 61.3	\[ \color{blue}{\frac{1}{\frac{a}{-0.5}}} \cdot \left(b + \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}\right) \]
      flip-+ [=>] 61.3	\[ \frac{1}{\frac{a}{-0.5}} \cdot \color{blue}{\frac{b \cdot b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)} \cdot \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}} \]
      frac-times [=>] 52.9	\[ \color{blue}{\frac{1 \cdot \left(b \cdot b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)} \cdot \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}\right)}{\frac{a}{-0.5} \cdot \left(b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}\right)}} \]
      *-un-lft-identity [<=] 52.9	\[ \frac{\color{blue}{b \cdot b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)} \cdot \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}}{\frac{a}{-0.5} \cdot \left(b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}\right)} \]
      associate-/r* [=>] 61.3	\[ \color{blue}{\frac{\frac{b \cdot b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)} \cdot \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}{\frac{a}{-0.5}}}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}} \]
      add-sqr-sqrt [<=] 61.5	\[ \frac{\frac{b \cdot b - \color{blue}{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}{\frac{a}{-0.5}}}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}} \]
      div-inv [=>] 61.5	\[ \frac{\frac{b \cdot b - \mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}{\color{blue}{a \cdot \frac{1}{-0.5}}}}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}} \]
      metadata-eval [=>] 61.5	\[ \frac{\frac{b \cdot b - \mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}{a \cdot \color{blue}{-2}}}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}} \]

   if -3.8000000000000001e-154 < b < -4.1e-171

   1. Initial program 69.6%

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

   2. Simplified 69.5%

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

      [Start] 69.6	\[ \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      *-lft-identity [<=] 69.6	\[ \color{blue}{1 \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}} \]
      metadata-eval [<=] 69.6	\[ \color{blue}{\left(--1\right)} \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      associate-*r/ [=>] 69.6	\[ \color{blue}{\frac{\left(--1\right) \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)}{2 \cdot a}} \]
      associate-*l/ [<=] 69.5	\[ \color{blue}{\frac{--1}{2 \cdot a} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      distribute-neg-frac [<=] 69.5	\[ \color{blue}{\left(-\frac{-1}{2 \cdot a}\right)} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right) \]
      distribute-lft-neg-in [<=] 69.5	\[ \color{blue}{-\frac{-1}{2 \cdot a} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      distribute-rgt-neg-out [<=] 69.5	\[ \color{blue}{\frac{-1}{2 \cdot a} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)} \]
      associate-/r* [=>] 69.5	\[ \color{blue}{\frac{\frac{-1}{2}}{a}} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right) \]
      metadata-eval [=>] 69.5	\[ \frac{\color{blue}{-0.5}}{a} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right) \]
      sub-neg [=>] 69.5	\[ \frac{-0.5}{a} \cdot \left(-\color{blue}{\left(\left(-b\right) + \left(-\sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)}\right) \]
      distribute-neg-out [=>] 69.5	\[ \frac{-0.5}{a} \cdot \left(-\color{blue}{\left(-\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)}\right) \]
      remove-double-neg [=>] 69.5	\[ \frac{-0.5}{a} \cdot \color{blue}{\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      sub-neg [=>] 69.5	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{b \cdot b + \left(-4 \cdot \left(a \cdot c\right)\right)}}\right) \]
      +-commutative [=>] 69.5	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{\left(-4 \cdot \left(a \cdot c\right)\right) + b \cdot b}}\right) \]

   3. Applied egg-rr 69.7%

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

      [Start] 69.5	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}\right) \]
      associate-/r/ [<=] 69.7	\[ \color{blue}{\frac{-0.5}{\frac{a}{b + \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}}} \]

   4. Taylor expanded in b around -inf 25.0%

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

   if -4.1e-171 < b < -1.85e-199

   1. Initial program 67.7%

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

   2. Simplified 67.6%

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

      [Start] 67.7	\[ \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      *-lft-identity [<=] 67.7	\[ \color{blue}{1 \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}} \]
      metadata-eval [<=] 67.7	\[ \color{blue}{\left(--1\right)} \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      associate-*r/ [=>] 67.7	\[ \color{blue}{\frac{\left(--1\right) \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)}{2 \cdot a}} \]
      associate-*l/ [<=] 67.5	\[ \color{blue}{\frac{--1}{2 \cdot a} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      distribute-neg-frac [<=] 67.5	\[ \color{blue}{\left(-\frac{-1}{2 \cdot a}\right)} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right) \]
      distribute-lft-neg-in [<=] 67.5	\[ \color{blue}{-\frac{-1}{2 \cdot a} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      distribute-rgt-neg-out [<=] 67.5	\[ \color{blue}{\frac{-1}{2 \cdot a} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)} \]
      associate-/r* [=>] 67.5	\[ \color{blue}{\frac{\frac{-1}{2}}{a}} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right) \]
      metadata-eval [=>] 67.5	\[ \frac{\color{blue}{-0.5}}{a} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right) \]
      sub-neg [=>] 67.5	\[ \frac{-0.5}{a} \cdot \left(-\color{blue}{\left(\left(-b\right) + \left(-\sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)}\right) \]
      distribute-neg-out [=>] 67.5	\[ \frac{-0.5}{a} \cdot \left(-\color{blue}{\left(-\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)}\right) \]
      remove-double-neg [=>] 67.5	\[ \frac{-0.5}{a} \cdot \color{blue}{\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      sub-neg [=>] 67.5	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{b \cdot b + \left(-4 \cdot \left(a \cdot c\right)\right)}}\right) \]
      +-commutative [=>] 67.5	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{\left(-4 \cdot \left(a \cdot c\right)\right) + b \cdot b}}\right) \]

   3. Applied egg-rr 67.6%

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

      [Start] 67.6	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}\right) \]
      associate-/r/ [<=] 67.6	\[ \color{blue}{\frac{-0.5}{\frac{a}{b + \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}}} \]

   4. Applied egg-rr 67.3%

      \[\leadsto \frac{-0.5}{\frac{a}{b + \color{blue}{{\left({\left(\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)\right)}^{0.25}\right)}^{2}}}} \]
      Proof

      [Start] 67.6	\[ \frac{-0.5}{\frac{a}{b + \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}} \]
      add-sqr-sqrt [=>] 67.3	\[ \frac{-0.5}{\frac{a}{b + \color{blue}{\sqrt{\sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}} \cdot \sqrt{\sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}}}} \]
      pow2 [=>] 67.3	\[ \frac{-0.5}{\frac{a}{b + \color{blue}{{\left(\sqrt{\sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}\right)}^{2}}}} \]
      pow1/2 [=>] 67.3	\[ \frac{-0.5}{\frac{a}{b + {\left(\sqrt{\color{blue}{{\left(\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)\right)}^{0.5}}}\right)}^{2}}} \]
      metadata-eval [<=] 67.3	\[ \frac{-0.5}{\frac{a}{b + {\left(\sqrt{{\left(\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)\right)}^{\color{blue}{\left(--0.5\right)}}}\right)}^{2}}} \]
      sqrt-pow1 [=>] 67.3	\[ \frac{-0.5}{\frac{a}{b + {\color{blue}{\left({\left(\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)\right)}^{\left(\frac{--0.5}{2}\right)}\right)}}^{2}}} \]
      metadata-eval [=>] 67.3	\[ \frac{-0.5}{\frac{a}{b + {\left({\left(\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)\right)}^{\left(\frac{\color{blue}{0.5}}{2}\right)}\right)}^{2}}} \]
      metadata-eval [=>] 67.3	\[ \frac{-0.5}{\frac{a}{b + {\left({\left(\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)\right)}^{\color{blue}{0.25}}\right)}^{2}}} \]

   5. Taylor expanded in a around -inf 44.9%

      \[\leadsto \frac{-0.5}{\frac{a}{b + {\color{blue}{\left(e^{0.25 \cdot \left(\log \left(4 \cdot c\right) + -1 \cdot \log \left(\frac{-1}{a}\right)\right)}\right)}}^{2}}} \]

   if -1.85e-199 < b < 8.4999999999999995e35

   1. Initial program 81.4%

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

   if 8.4999999999999995e35 < b

   1. Initial program 43.1%

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

   2. Simplified 42.9%

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

      [Start] 43.1	\[ \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      *-lft-identity [<=] 43.1	\[ \color{blue}{1 \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}} \]
      metadata-eval [<=] 43.1	\[ \color{blue}{\left(--1\right)} \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      associate-*r/ [=>] 43.1	\[ \color{blue}{\frac{\left(--1\right) \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)}{2 \cdot a}} \]
      associate-*l/ [<=] 42.9	\[ \color{blue}{\frac{--1}{2 \cdot a} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      distribute-neg-frac [<=] 42.9	\[ \color{blue}{\left(-\frac{-1}{2 \cdot a}\right)} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right) \]
      distribute-lft-neg-in [<=] 42.9	\[ \color{blue}{-\frac{-1}{2 \cdot a} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      distribute-rgt-neg-out [<=] 42.9	\[ \color{blue}{\frac{-1}{2 \cdot a} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)} \]
      associate-/r* [=>] 43.0	\[ \color{blue}{\frac{\frac{-1}{2}}{a}} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right) \]
      metadata-eval [=>] 43.0	\[ \frac{\color{blue}{-0.5}}{a} \cdot \left(-\left(\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right) \]
      sub-neg [=>] 43.0	\[ \frac{-0.5}{a} \cdot \left(-\color{blue}{\left(\left(-b\right) + \left(-\sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)}\right) \]
      distribute-neg-out [=>] 43.0	\[ \frac{-0.5}{a} \cdot \left(-\color{blue}{\left(-\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)\right)}\right) \]
      remove-double-neg [=>] 43.0	\[ \frac{-0.5}{a} \cdot \color{blue}{\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      sub-neg [=>] 43.0	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{b \cdot b + \left(-4 \cdot \left(a \cdot c\right)\right)}}\right) \]
      +-commutative [=>] 43.0	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{\left(-4 \cdot \left(a \cdot c\right)\right) + b \cdot b}}\right) \]

   3. Taylor expanded in a around 0 91.0%

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

   4. Simplified 91.0%

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

      [Start] 91.0	\[ \frac{c}{b} + -1 \cdot \frac{b}{a} \]
      mul-1-neg [=>] 91.0	\[ \frac{c}{b} + \color{blue}{\left(-\frac{b}{a}\right)} \]
      unsub-neg [=>] 91.0	\[ \color{blue}{\frac{c}{b} - \frac{b}{a}} \]

3. Recombined 6 regimes into one program.

4. Final simplification 82.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \leq -3.35 \cdot 10^{-74}:\\ \;\;\;\;\frac{-c}{b}\\ \mathbf{elif}\;b \leq -3.8 \cdot 10^{-154}:\\ \;\;\;\;\frac{\frac{b \cdot b - \mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}{a \cdot -2}}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}\\ \mathbf{elif}\;b \leq -4.1 \cdot 10^{-171}:\\ \;\;\;\;\frac{-0.5}{0.5 \cdot \frac{b}{c} + -0.5 \cdot \frac{a}{b}}\\ \mathbf{elif}\;b \leq -1.85 \cdot 10^{-199}:\\ \;\;\;\;\frac{-0.5}{\frac{a}{b + {\left(e^{0.25 \cdot \left(\log \left(c \cdot 4\right) - \log \left(\frac{-1}{a}\right)\right)}\right)}^{2}}}\\ \mathbf{elif}\;b \leq 8.5 \cdot 10^{+35}:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + -4 \cdot \left(c \cdot a\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	83.7%
Cost	7688

\[\begin{array}{l} \mathbf{if}\;b \leq -4.8 \cdot 10^{-77}:\\ \;\;\;\;\frac{-c}{b}\\ \mathbf{elif}\;b \leq 8.5 \cdot 10^{+35}:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + -4 \cdot \left(c \cdot a\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \end{array} \]

Alternative 2
Accuracy	78.9%
Cost	7432

\[\begin{array}{l} \mathbf{if}\;b \leq -9.2 \cdot 10^{-105}:\\ \;\;\;\;\frac{-c}{b}\\ \mathbf{elif}\;b \leq 1.15 \cdot 10^{-98}:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{c \cdot \left(a \cdot -4\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array} \]

Alternative 3
Accuracy	38.0%
Cost	388

\[\begin{array}{l} \mathbf{if}\;b \leq -3.9 \cdot 10^{+23}:\\ \;\;\;\;\frac{c}{b}\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array} \]

Alternative 4
Accuracy	64.5%
Cost	388

\[\begin{array}{l} \mathbf{if}\;b \leq -1.48 \cdot 10^{-226}:\\ \;\;\;\;\frac{-c}{b}\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array} \]

Alternative 5
Accuracy	13.1%
Cost	324

\[\begin{array}{l} \mathbf{if}\;b \leq -3.4 \cdot 10^{+36}:\\ \;\;\;\;\frac{c}{b}\\ \mathbf{else}:\\ \;\;\;\;\frac{-0.5}{a}\\ \end{array} \]

Alternative 6
Accuracy	5.2%
Cost	192

\[\frac{-0.5}{a} \]

Reproduce

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

  :herbie-target
  (if (< b 0.0) (/ c (* a (/ (+ (- b) (sqrt (- (* b b) (* 4.0 (* a c))))) (* 2.0 a)))) (/ (- (- b) (sqrt (- (* b b) (* 4.0 (* a c))))) (* 2.0 a)))

  (/ (- (- b) (sqrt (- (* b b) (* 4.0 (* a c))))) (* 2.0 a)))