The quadratic formula (r2)

Average Accuracy: 47.2% → 81.4%

Time: 20.1s

Precision: binary64

Cost: 21064

Math

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

↓

\[\begin{array}{l} t_0 := \frac{-c}{b}\\ t_1 := \mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)\\ \mathbf{if}\;b \leq -4.5 \cdot 10^{-71}:\\ \;\;\;\;t_0 - \frac{c}{\frac{\frac{{b}^{3}}{a}}{c}}\\ \mathbf{elif}\;b \leq -5.5 \cdot 10^{-137}:\\ \;\;\;\;\frac{\frac{b \cdot b - t_1}{a \cdot -2}}{b - \sqrt{t_1}}\\ \mathbf{elif}\;b \leq -4.2 \cdot 10^{-148}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;b \leq -5.6 \cdot 10^{-220}:\\ \;\;\;\;-0.5 \cdot \frac{b + \sqrt{c \cdot -4} \cdot \sqrt{a}}{a}\\ \mathbf{elif}\;b \leq 8.2 \cdot 10^{+35}:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + -4 \cdot \left(c \cdot a\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\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 (/ (- c) b)) (t_1 (fma c (* a -4.0) (* b b))))
   (if (<= b -4.5e-71)
     (- t_0 (/ c (/ (/ (pow b 3.0) a) c)))
     (if (<= b -5.5e-137)
       (/ (/ (- (* b b) t_1) (* a -2.0)) (- b (sqrt t_1)))
       (if (<= b -4.2e-148)
         t_0
         (if (<= b -5.6e-220)
           (* -0.5 (/ (+ b (* (sqrt (* c -4.0)) (sqrt a))) a))
           (if (<= b 8.2e+35)
             (/ (- (- b) (sqrt (+ (* b b) (* -4.0 (* c a))))) (* a 2.0))
             (/ (- 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 = -c / b;
	double t_1 = fma(c, (a * -4.0), (b * b));
	double tmp;
	if (b <= -4.5e-71) {
		tmp = t_0 - (c / ((pow(b, 3.0) / a) / c));
	} else if (b <= -5.5e-137) {
		tmp = (((b * b) - t_1) / (a * -2.0)) / (b - sqrt(t_1));
	} else if (b <= -4.2e-148) {
		tmp = t_0;
	} else if (b <= -5.6e-220) {
		tmp = -0.5 * ((b + (sqrt((c * -4.0)) * sqrt(a))) / a);
	} else if (b <= 8.2e+35) {
		tmp = (-b - sqrt(((b * b) + (-4.0 * (c * a))))) / (a * 2.0);
	} else {
		tmp = -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 = Float64(Float64(-c) / b)
	t_1 = fma(c, Float64(a * -4.0), Float64(b * b))
	tmp = 0.0
	if (b <= -4.5e-71)
		tmp = Float64(t_0 - Float64(c / Float64(Float64((b ^ 3.0) / a) / c)));
	elseif (b <= -5.5e-137)
		tmp = Float64(Float64(Float64(Float64(b * b) - t_1) / Float64(a * -2.0)) / Float64(b - sqrt(t_1)));
	elseif (b <= -4.2e-148)
		tmp = t_0;
	elseif (b <= -5.6e-220)
		tmp = Float64(-0.5 * Float64(Float64(b + Float64(sqrt(Float64(c * -4.0)) * sqrt(a))) / a));
	elseif (b <= 8.2e+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(-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) / b), $MachinePrecision]}, Block[{t$95$1 = N[(c * N[(a * -4.0), $MachinePrecision] + N[(b * b), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[b, -4.5e-71], N[(t$95$0 - N[(c / N[(N[(N[Power[b, 3.0], $MachinePrecision] / a), $MachinePrecision] / c), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[b, -5.5e-137], N[(N[(N[(N[(b * b), $MachinePrecision] - t$95$1), $MachinePrecision] / N[(a * -2.0), $MachinePrecision]), $MachinePrecision] / N[(b - N[Sqrt[t$95$1], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[b, -4.2e-148], t$95$0, If[LessEqual[b, -5.6e-220], N[(-0.5 * N[(N[(b + N[(N[Sqrt[N[(c * -4.0), $MachinePrecision]], $MachinePrecision] * N[Sqrt[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / a), $MachinePrecision]), $MachinePrecision], If[LessEqual[b, 8.2e+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[((-b) / a), $MachinePrecision]]]]]]]]

Target

Original	47.2%
Target	67.2%
Herbie	81.4%

\[\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 < -4.5000000000000002e-71

   1. Initial program 17.4%

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

   2. Taylor expanded in b around -inf 68.9%

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

   3. Simplified 85.6%

      \[\leadsto \color{blue}{-1 \cdot \left(\frac{c}{b} + \frac{c}{\frac{\frac{{b}^{3}}{a}}{c}}\right)} \]
      Proof

      [Start] 68.9	\[ -1 \cdot \frac{{c}^{2} \cdot a}{{b}^{3}} + -1 \cdot \frac{c}{b} \]
      distribute-lft-out [=>] 68.9	\[ \color{blue}{-1 \cdot \left(\frac{{c}^{2} \cdot a}{{b}^{3}} + \frac{c}{b}\right)} \]
      +-commutative [=>] 68.9	\[ -1 \cdot \color{blue}{\left(\frac{c}{b} + \frac{{c}^{2} \cdot a}{{b}^{3}}\right)} \]
      associate-/l* [=>] 72.0	\[ -1 \cdot \left(\frac{c}{b} + \color{blue}{\frac{{c}^{2}}{\frac{{b}^{3}}{a}}}\right) \]
      unpow2 [=>] 72.0	\[ -1 \cdot \left(\frac{c}{b} + \frac{\color{blue}{c \cdot c}}{\frac{{b}^{3}}{a}}\right) \]
      associate-/l* [=>] 85.6	\[ -1 \cdot \left(\frac{c}{b} + \color{blue}{\frac{c}{\frac{\frac{{b}^{3}}{a}}{c}}}\right) \]

   if -4.5000000000000002e-71 < b < -5.5000000000000003e-137

   1. Initial program 55.5%

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

   2. Simplified 55.1%

      \[\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] 55.5	\[ \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      *-lft-identity [<=] 55.5	\[ \color{blue}{1 \cdot \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a}} \]
      metadata-eval [<=] 55.5	\[ \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/ [=>] 55.5	\[ \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/ [<=] 55.4	\[ \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 [<=] 55.4	\[ \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 [<=] 55.4	\[ \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 [<=] 55.4	\[ \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* [=>] 55.4	\[ \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 [=>] 55.4	\[ \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 [=>] 55.4	\[ \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 [=>] 55.4	\[ \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 [=>] 55.4	\[ \frac{-0.5}{a} \cdot \color{blue}{\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      sub-neg [=>] 55.4	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\color{blue}{b \cdot b + \left(-4 \cdot \left(a \cdot c\right)\right)}}\right) \]
      +-commutative [=>] 55.4	\[ \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 55.2%

      \[\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] 55.1	\[ \frac{-0.5}{a} \cdot \left(b + \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}\right) \]
      clear-num [=>] 55.1	\[ \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-+ [=>] 55.1	\[ \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 [=>] 48.2	\[ \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 [<=] 48.2	\[ \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* [=>] 55.1	\[ \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 [<=] 55.2	\[ \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 [=>] 55.2	\[ \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 [=>] 55.2	\[ \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 -5.5000000000000003e-137 < b < -4.2e-148

   1. Initial program 72.4%

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

   2. Simplified 72.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] 72.4	\[ \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      *-lft-identity [<=] 72.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 [<=] 72.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/ [=>] 72.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/ [<=] 72.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 [<=] 72.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 [<=] 72.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 [<=] 72.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* [=>] 72.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 [=>] 72.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 [=>] 72.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 [=>] 72.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 [=>] 72.3	\[ \frac{-0.5}{a} \cdot \color{blue}{\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      sub-neg [=>] 72.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 [=>] 72.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. Taylor expanded in b around -inf 24.7%

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

   4. Simplified 24.7%

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

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

   if -4.2e-148 < b < -5.5999999999999998e-220

   1. Initial program 74.0%

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

   2. Taylor expanded in b around 0 73.5%

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

   3. Simplified 73.6%

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

      [Start] 73.5	\[ \frac{\left(-b\right) - \sqrt{-4 \cdot \left(c \cdot a\right)}}{2 \cdot a} \]
      *-commutative [=>] 73.5	\[ \frac{\left(-b\right) - \sqrt{\color{blue}{\left(c \cdot a\right) \cdot -4}}}{2 \cdot a} \]
      associate-*l* [=>] 73.6	\[ \frac{\left(-b\right) - \sqrt{\color{blue}{c \cdot \left(a \cdot -4\right)}}}{2 \cdot a} \]

   4. Applied egg-rr 73.5%

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

      [Start] 73.6	\[ \frac{\left(-b\right) - \sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a} \]
      div-sub [=>] 73.6	\[ \color{blue}{\frac{-b}{2 \cdot a} - \frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}} \]
      sub-neg [=>] 73.6	\[ \color{blue}{\frac{-b}{2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right)} \]
      frac-2neg [=>] 73.6	\[ \color{blue}{\frac{-\left(-b\right)}{-2 \cdot a}} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      add-sqr-sqrt [=>] 73.6	\[ \frac{-\color{blue}{\sqrt{-b} \cdot \sqrt{-b}}}{-2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      sqrt-unprod [=>] 73.4	\[ \frac{-\color{blue}{\sqrt{\left(-b\right) \cdot \left(-b\right)}}}{-2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      sqr-neg [=>] 73.4	\[ \frac{-\sqrt{\color{blue}{b \cdot b}}}{-2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      sqrt-unprod [<=] 0.0	\[ \frac{-\color{blue}{\sqrt{b} \cdot \sqrt{b}}}{-2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      add-sqr-sqrt [<=] 73.5	\[ \frac{-\color{blue}{b}}{-2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      add-sqr-sqrt [=>] 73.5	\[ \frac{\color{blue}{\sqrt{-b} \cdot \sqrt{-b}}}{-2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      sqrt-unprod [=>] 73.4	\[ \frac{\color{blue}{\sqrt{\left(-b\right) \cdot \left(-b\right)}}}{-2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      sqr-neg [=>] 73.4	\[ \frac{\sqrt{\color{blue}{b \cdot b}}}{-2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      sqrt-unprod [<=] 0.0	\[ \frac{\color{blue}{\sqrt{b} \cdot \sqrt{b}}}{-2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      add-sqr-sqrt [<=] 73.6	\[ \frac{\color{blue}{b}}{-2 \cdot a} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      *-commutative [=>] 73.6	\[ \frac{b}{-\color{blue}{a \cdot 2}} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      distribute-rgt-neg-in [=>] 73.6	\[ \frac{b}{\color{blue}{a \cdot \left(-2\right)}} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      metadata-eval [=>] 73.6	\[ \frac{b}{a \cdot \color{blue}{-2}} + \left(-\frac{\sqrt{c \cdot \left(a \cdot -4\right)}}{2 \cdot a}\right) \]
      div-inv [=>] 73.5	\[ \frac{b}{a \cdot -2} + \left(-\color{blue}{\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{1}{2 \cdot a}}\right) \]
      associate-/r* [=>] 73.5	\[ \frac{b}{a \cdot -2} + \left(-\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \color{blue}{\frac{\frac{1}{2}}{a}}\right) \]
      metadata-eval [=>] 73.5	\[ \frac{b}{a \cdot -2} + \left(-\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{\color{blue}{0.5}}{a}\right) \]

   5. Simplified 73.5%

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

      [Start] 73.5	\[ \frac{b}{a \cdot -2} + \left(-\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{0.5}{a}\right) \]
      *-commutative [=>] 73.5	\[ \frac{b}{\color{blue}{-2 \cdot a}} + \left(-\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{0.5}{a}\right) \]
      metadata-eval [<=] 73.5	\[ \frac{b}{\color{blue}{\frac{-2}{1}} \cdot a} + \left(-\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{0.5}{a}\right) \]
      associate-/r/ [<=] 73.5	\[ \frac{b}{\color{blue}{\frac{-2}{\frac{1}{a}}}} + \left(-\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{0.5}{a}\right) \]
      associate-/l* [<=] 73.5	\[ \color{blue}{\frac{b \cdot \frac{1}{a}}{-2}} + \left(-\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{0.5}{a}\right) \]
      associate-*r/ [<=] 73.5	\[ \color{blue}{b \cdot \frac{\frac{1}{a}}{-2}} + \left(-\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{0.5}{a}\right) \]
      associate-/r* [<=] 73.5	\[ b \cdot \color{blue}{\frac{1}{a \cdot -2}} + \left(-\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{0.5}{a}\right) \]
      distribute-rgt-neg-in [=>] 73.5	\[ b \cdot \frac{1}{a \cdot -2} + \color{blue}{\sqrt{c \cdot \left(a \cdot -4\right)} \cdot \left(-\frac{0.5}{a}\right)} \]
      distribute-neg-frac [=>] 73.5	\[ b \cdot \frac{1}{a \cdot -2} + \sqrt{c \cdot \left(a \cdot -4\right)} \cdot \color{blue}{\frac{-0.5}{a}} \]
      metadata-eval [=>] 73.5	\[ b \cdot \frac{1}{a \cdot -2} + \sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{\color{blue}{-0.5}}{a} \]
      metadata-eval [<=] 73.5	\[ b \cdot \frac{1}{a \cdot -2} + \sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{\color{blue}{\frac{1}{-2}}}{a} \]
      associate-/r* [<=] 73.5	\[ b \cdot \frac{1}{a \cdot -2} + \sqrt{c \cdot \left(a \cdot -4\right)} \cdot \color{blue}{\frac{1}{-2 \cdot a}} \]
      *-commutative [<=] 73.5	\[ b \cdot \frac{1}{a \cdot -2} + \sqrt{c \cdot \left(a \cdot -4\right)} \cdot \frac{1}{\color{blue}{a \cdot -2}} \]
      distribute-rgt-in [<=] 73.5	\[ \color{blue}{\frac{1}{a \cdot -2} \cdot \left(b + \sqrt{c \cdot \left(a \cdot -4\right)}\right)} \]
      +-commutative [<=] 73.5	\[ \frac{1}{a \cdot -2} \cdot \color{blue}{\left(\sqrt{c \cdot \left(a \cdot -4\right)} + b\right)} \]
      associate-*l/ [=>] 73.6	\[ \color{blue}{\frac{1 \cdot \left(\sqrt{c \cdot \left(a \cdot -4\right)} + b\right)}{a \cdot -2}} \]
      *-commutative [=>] 73.6	\[ \frac{1 \cdot \left(\sqrt{c \cdot \left(a \cdot -4\right)} + b\right)}{\color{blue}{-2 \cdot a}} \]
      times-frac [=>] 73.6	\[ \color{blue}{\frac{1}{-2} \cdot \frac{\sqrt{c \cdot \left(a \cdot -4\right)} + b}{a}} \]
      metadata-eval [=>] 73.6	\[ \color{blue}{-0.5} \cdot \frac{\sqrt{c \cdot \left(a \cdot -4\right)} + b}{a} \]

   6. Applied egg-rr 39.8%

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

      [Start] 73.5	\[ -0.5 \cdot \frac{b + \sqrt{-4 \cdot \left(c \cdot a\right)}}{a} \]
      associate-*r* [=>] 73.6	\[ -0.5 \cdot \frac{b + \sqrt{\color{blue}{\left(-4 \cdot c\right) \cdot a}}}{a} \]
      sqrt-prod [=>] 39.8	\[ -0.5 \cdot \frac{b + \color{blue}{\sqrt{-4 \cdot c} \cdot \sqrt{a}}}{a} \]

   if -5.5999999999999998e-220 < b < 8.1999999999999997e35

   1. Initial program 82.0%

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

   if 8.1999999999999997e35 < b

   1. Initial program 43.6%

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

   2. Simplified 43.4%

      \[\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.6	\[ \frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{2 \cdot a} \]
      *-lft-identity [<=] 43.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 [<=] 43.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/ [=>] 43.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/ [<=] 43.4	\[ \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 [<=] 43.4	\[ \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 [<=] 43.4	\[ \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 [<=] 43.4	\[ \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.4	\[ \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.4	\[ \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.4	\[ \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.4	\[ \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.4	\[ \frac{-0.5}{a} \cdot \color{blue}{\left(b + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}\right)} \]
      sub-neg [=>] 43.4	\[ \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.4	\[ \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 89.6%

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

   4. Simplified 89.6%

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

      [Start] 89.6	\[ -1 \cdot \frac{b}{a} \]
      associate-*r/ [=>] 89.6	\[ \color{blue}{\frac{-1 \cdot b}{a}} \]
      mul-1-neg [=>] 89.6	\[ \frac{\color{blue}{-b}}{a} \]

3. Recombined 6 regimes into one program.

4. Final simplification 81.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \leq -4.5 \cdot 10^{-71}:\\ \;\;\;\;\frac{-c}{b} - \frac{c}{\frac{\frac{{b}^{3}}{a}}{c}}\\ \mathbf{elif}\;b \leq -5.5 \cdot 10^{-137}:\\ \;\;\;\;\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.2 \cdot 10^{-148}:\\ \;\;\;\;\frac{-c}{b}\\ \mathbf{elif}\;b \leq -5.6 \cdot 10^{-220}:\\ \;\;\;\;-0.5 \cdot \frac{b + \sqrt{c \cdot -4} \cdot \sqrt{a}}{a}\\ \mathbf{elif}\;b \leq 8.2 \cdot 10^{+35}:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + -4 \cdot \left(c \cdot a\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	81.4%
Cost	14032

\[\begin{array}{l} t_0 := \frac{\left(-b\right) - \sqrt{b \cdot b + -4 \cdot \left(c \cdot a\right)}}{a \cdot 2}\\ t_1 := \frac{-c}{b}\\ \mathbf{if}\;b \leq -4.3 \cdot 10^{-75}:\\ \;\;\;\;t_1 - \frac{c}{\frac{\frac{{b}^{3}}{a}}{c}}\\ \mathbf{elif}\;b \leq -5.5 \cdot 10^{-137}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;b \leq -8.8 \cdot 10^{-147}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;b \leq -5.1 \cdot 10^{-220}:\\ \;\;\;\;-0.5 \cdot \frac{b + \sqrt{c \cdot -4} \cdot \sqrt{a}}{a}\\ \mathbf{elif}\;b \leq 7 \cdot 10^{+35}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array} \]

Alternative 2
Accuracy	83.4%
Cost	7688

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

Alternative 3
Accuracy	78.5%
Cost	7368

\[\begin{array}{l} \mathbf{if}\;b \leq -8.6 \cdot 10^{-89}:\\ \;\;\;\;\frac{-c}{b}\\ \mathbf{elif}\;b \leq 3.4 \cdot 10^{-118}:\\ \;\;\;\;-0.5 \cdot \frac{b + \sqrt{-4 \cdot \left(c \cdot a\right)}}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array} \]

Alternative 4
Accuracy	78.4%
Cost	7368

\[\begin{array}{l} \mathbf{if}\;b \leq -5.6 \cdot 10^{-74}:\\ \;\;\;\;\frac{-c}{b} - \frac{c}{\frac{\frac{{b}^{3}}{a}}{c}}\\ \mathbf{elif}\;b \leq 3.4 \cdot 10^{-118}:\\ \;\;\;\;-0.5 \cdot \frac{b + \sqrt{-4 \cdot \left(c \cdot a\right)}}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array} \]

Alternative 5
Accuracy	38.5%
Cost	388

\[\begin{array}{l} \mathbf{if}\;b \leq -1.95 \cdot 10^{-36}:\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\frac{-b}{a}\\ \end{array} \]

Alternative 6
Accuracy	63.9%
Cost	388

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

Alternative 7
Accuracy	12.1%
Cost	64

\[0 \]

Reproduce

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