jeff quadratic root 1

Average Error: 19.8 → 8.6

Time: 23.7s

Precision: binary64

Cost: 50596

Math

\[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

↓

\[\begin{array}{l} t_0 := \left(a \cdot c\right) \cdot -4\\ t_1 := \sqrt{b \cdot b + t_0}\\ t_2 := \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - t_1}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{t_1 - b}\\ \end{array}\\ t_3 := \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\\ t_4 := \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - t_3}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{t_3 - b}\\ \end{array}\\ \mathbf{if}\;t_4 \leq -\infty:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array}\\ \mathbf{elif}\;t_4 \leq -1 \cdot 10^{-185}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t_4 \leq 0:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{t_0}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}\\ \end{array}\\ \mathbf{elif}\;t_4 \leq 5 \cdot 10^{+291}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;\left(b + \mathsf{hypot}\left(b, \sqrt{a \cdot -4} \cdot \sqrt{c}\right)\right) \cdot \frac{-0.5}{a}\\ \mathbf{else}:\\ \;\;\;\;-2 \cdot \frac{c}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}\\ \end{array} \]

FPCore

(FPCore (a b c)
 :precision binary64
 (if (>= b 0.0)
   (/ (- (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a))
   (/ (* 2.0 c) (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))))))

↓

(FPCore (a b c)
 :precision binary64
 (let* ((t_0 (* (* a c) -4.0))
        (t_1 (sqrt (+ (* b b) t_0)))
        (t_2
         (if (>= b 0.0) (/ (- (- b) t_1) (* a 2.0)) (/ (* c 2.0) (- t_1 b))))
        (t_3 (sqrt (- (* b b) (* (* 4.0 a) c))))
        (t_4
         (if (>= b 0.0) (/ (- (- b) t_3) (* a 2.0)) (/ (* c 2.0) (- t_3 b)))))
   (if (<= t_4 (- INFINITY))
     (if (>= b 0.0) (- (/ c b) (/ b a)) (- (/ c b)))
     (if (<= t_4 -1e-185)
       t_2
       (if (<= t_4 0.0)
         (if (>= b 0.0)
           (/ (- (- b) (sqrt t_0)) (* a 2.0))
           (/ (* c 2.0) (fma 2.0 (/ c (/ b a)) (* b -2.0))))
         (if (<= t_4 5e+291)
           t_2
           (if (>= b 0.0)
             (* (+ b (hypot b (* (sqrt (* a -4.0)) (sqrt c)))) (/ -0.5 a))
             (* -2.0 (/ c (- b (sqrt (fma c (* a -4.0) (* b b)))))))))))))

C

double code(double a, double b, double c) {
	double tmp;
	if (b >= 0.0) {
		tmp = (-b - sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a);
	} else {
		tmp = (2.0 * c) / (-b + sqrt(((b * b) - ((4.0 * a) * c))));
	}
	return tmp;
}

↓

double code(double a, double b, double c) {
	double t_0 = (a * c) * -4.0;
	double t_1 = sqrt(((b * b) + t_0));
	double tmp;
	if (b >= 0.0) {
		tmp = (-b - t_1) / (a * 2.0);
	} else {
		tmp = (c * 2.0) / (t_1 - b);
	}
	double t_2 = tmp;
	double t_3 = sqrt(((b * b) - ((4.0 * a) * c)));
	double tmp_1;
	if (b >= 0.0) {
		tmp_1 = (-b - t_3) / (a * 2.0);
	} else {
		tmp_1 = (c * 2.0) / (t_3 - b);
	}
	double t_4 = tmp_1;
	double tmp_3;
	if (t_4 <= -((double) INFINITY)) {
		double tmp_4;
		if (b >= 0.0) {
			tmp_4 = (c / b) - (b / a);
		} else {
			tmp_4 = -(c / b);
		}
		tmp_3 = tmp_4;
	} else if (t_4 <= -1e-185) {
		tmp_3 = t_2;
	} else if (t_4 <= 0.0) {
		double tmp_5;
		if (b >= 0.0) {
			tmp_5 = (-b - sqrt(t_0)) / (a * 2.0);
		} else {
			tmp_5 = (c * 2.0) / fma(2.0, (c / (b / a)), (b * -2.0));
		}
		tmp_3 = tmp_5;
	} else if (t_4 <= 5e+291) {
		tmp_3 = t_2;
	} else if (b >= 0.0) {
		tmp_3 = (b + hypot(b, (sqrt((a * -4.0)) * sqrt(c)))) * (-0.5 / a);
	} else {
		tmp_3 = -2.0 * (c / (b - sqrt(fma(c, (a * -4.0), (b * b)))));
	}
	return tmp_3;
}

Julia

function code(a, b, c)
	tmp = 0.0
	if (b >= 0.0)
		tmp = Float64(Float64(Float64(-b) - sqrt(Float64(Float64(b * b) - Float64(Float64(4.0 * a) * c)))) / Float64(2.0 * a));
	else
		tmp = Float64(Float64(2.0 * c) / Float64(Float64(-b) + sqrt(Float64(Float64(b * b) - Float64(Float64(4.0 * a) * c)))));
	end
	return tmp
end

↓

function code(a, b, c)
	t_0 = Float64(Float64(a * c) * -4.0)
	t_1 = sqrt(Float64(Float64(b * b) + t_0))
	tmp = 0.0
	if (b >= 0.0)
		tmp = Float64(Float64(Float64(-b) - t_1) / Float64(a * 2.0));
	else
		tmp = Float64(Float64(c * 2.0) / Float64(t_1 - b));
	end
	t_2 = tmp
	t_3 = sqrt(Float64(Float64(b * b) - Float64(Float64(4.0 * a) * c)))
	tmp_1 = 0.0
	if (b >= 0.0)
		tmp_1 = Float64(Float64(Float64(-b) - t_3) / Float64(a * 2.0));
	else
		tmp_1 = Float64(Float64(c * 2.0) / Float64(t_3 - b));
	end
	t_4 = tmp_1
	tmp_3 = 0.0
	if (t_4 <= Float64(-Inf))
		tmp_4 = 0.0
		if (b >= 0.0)
			tmp_4 = Float64(Float64(c / b) - Float64(b / a));
		else
			tmp_4 = Float64(-Float64(c / b));
		end
		tmp_3 = tmp_4;
	elseif (t_4 <= -1e-185)
		tmp_3 = t_2;
	elseif (t_4 <= 0.0)
		tmp_5 = 0.0
		if (b >= 0.0)
			tmp_5 = Float64(Float64(Float64(-b) - sqrt(t_0)) / Float64(a * 2.0));
		else
			tmp_5 = Float64(Float64(c * 2.0) / fma(2.0, Float64(c / Float64(b / a)), Float64(b * -2.0)));
		end
		tmp_3 = tmp_5;
	elseif (t_4 <= 5e+291)
		tmp_3 = t_2;
	elseif (b >= 0.0)
		tmp_3 = Float64(Float64(b + hypot(b, Float64(sqrt(Float64(a * -4.0)) * sqrt(c)))) * Float64(-0.5 / a));
	else
		tmp_3 = Float64(-2.0 * Float64(c / Float64(b - sqrt(fma(c, Float64(a * -4.0), Float64(b * b))))));
	end
	return tmp_3
end

Wolfram

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

↓

code[a_, b_, c_] := Block[{t$95$0 = N[(N[(a * c), $MachinePrecision] * -4.0), $MachinePrecision]}, Block[{t$95$1 = N[Sqrt[N[(N[(b * b), $MachinePrecision] + t$95$0), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$2 = If[GreaterEqual[b, 0.0], N[(N[((-b) - t$95$1), $MachinePrecision] / N[(a * 2.0), $MachinePrecision]), $MachinePrecision], N[(N[(c * 2.0), $MachinePrecision] / N[(t$95$1 - b), $MachinePrecision]), $MachinePrecision]]}, Block[{t$95$3 = N[Sqrt[N[(N[(b * b), $MachinePrecision] - N[(N[(4.0 * a), $MachinePrecision] * c), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$4 = If[GreaterEqual[b, 0.0], N[(N[((-b) - t$95$3), $MachinePrecision] / N[(a * 2.0), $MachinePrecision]), $MachinePrecision], N[(N[(c * 2.0), $MachinePrecision] / N[(t$95$3 - b), $MachinePrecision]), $MachinePrecision]]}, If[LessEqual[t$95$4, (-Infinity)], If[GreaterEqual[b, 0.0], N[(N[(c / b), $MachinePrecision] - N[(b / a), $MachinePrecision]), $MachinePrecision], (-N[(c / b), $MachinePrecision])], If[LessEqual[t$95$4, -1e-185], t$95$2, If[LessEqual[t$95$4, 0.0], If[GreaterEqual[b, 0.0], N[(N[((-b) - N[Sqrt[t$95$0], $MachinePrecision]), $MachinePrecision] / N[(a * 2.0), $MachinePrecision]), $MachinePrecision], N[(N[(c * 2.0), $MachinePrecision] / N[(2.0 * N[(c / N[(b / a), $MachinePrecision]), $MachinePrecision] + N[(b * -2.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], If[LessEqual[t$95$4, 5e+291], t$95$2, If[GreaterEqual[b, 0.0], N[(N[(b + N[Sqrt[b ^ 2 + N[(N[Sqrt[N[(a * -4.0), $MachinePrecision]], $MachinePrecision] * N[Sqrt[c], $MachinePrecision]), $MachinePrecision] ^ 2], $MachinePrecision]), $MachinePrecision] * N[(-0.5 / a), $MachinePrecision]), $MachinePrecision], N[(-2.0 * N[(c / N[(b - N[Sqrt[N[(c * N[(a * -4.0), $MachinePrecision] + N[(b * b), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]]]]]]]]

Derivation

1. Split input into 4 regimes

2. if (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (*.f64 2 c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) < -inf.0

   1. Initial program 64.0

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. Simplified 64.0

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ } \end{array}} \]
      Proof
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (*.f64 a 2)) (/.f64 (*.f64 c 2) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 a) c))))) (*.f64 a 2)) (/.f64 (*.f64 c 2) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite<= *-commutative_binary64 (*.f64 2 a))) (/.f64 (*.f64 c 2) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 c)) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (*.f64 2 c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 a) c))))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in b around -inf 64.0

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\color{blue}{\frac{c \cdot 2}{2 \cdot \frac{c \cdot a}{b} + -2 \cdot b}}\\ \end{array} \]

   4. Simplified 64.0

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\color{blue}{\frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}}\\ \end{array} \]
      Proof
      (fma.f64 2 (/.f64 c (/.f64 b a)) (*.f64 b -2)): 0 points increase in error, 0 points decrease in error
      (fma.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c a) b)) (*.f64 b -2)): 29 points increase in error, 12 points decrease in error
      (fma.f64 2 (/.f64 (*.f64 c a) b) (Rewrite<= *-commutative_binary64 (*.f64 -2 b))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 (/.f64 (*.f64 c a) b)) (*.f64 -2 b))): 0 points increase in error, 0 points decrease in error

   5. Taylor expanded in b around inf 22.0

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\left(b + -2 \cdot \frac{c \cdot a}{b}\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}\\ \end{array} \]

   6. Simplified 18.8

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \color{blue}{\left(b + -2 \cdot \frac{c}{\frac{b}{a}}\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}\\ \end{array} \]
      Proof
      (+.f64 b (*.f64 -2 (/.f64 c (/.f64 b a)))): 0 points increase in error, 0 points decrease in error
      (+.f64 b (*.f64 -2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c a) b)))): 23 points increase in error, 18 points decrease in error

   7. Taylor expanded in c around 0 18.8

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \left(b + -2 \cdot \frac{c}{\frac{b}{a}}\right)}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;-1 \cdot \frac{c}{b}\\ \end{array} \]

   8. Taylor expanded in b around 0 18.3

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\frac{c}{b} + -1 \cdot \frac{b}{a}}\\ \mathbf{else}:\\ \;\;\;\;-1 \cdot \frac{c}{b}\\ \end{array} \]

   9. Simplified 18.3

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\color{blue}{\frac{c}{b} - \frac{b}{a}}\\ \mathbf{else}:\\ \;\;\;\;-1 \cdot \frac{c}{b}\\ \end{array} \]
      Proof
      (-.f64 (/.f64 c b) (/.f64 b a)): 0 points increase in error, 0 points decrease in error
      (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 c b) (neg.f64 (/.f64 b a)))): 0 points increase in error, 0 points decrease in error
      (+.f64 (/.f64 c b) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 b a)))): 0 points increase in error, 0 points decrease in error

   if -inf.0 < (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (*.f64 2 c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) < -9.9999999999999999e-186 or -0.0 < (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (*.f64 2 c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) < 5.0000000000000001e291

   1. Initial program 3.1

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. Simplified 3.2

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ } \end{array}} \]
      Proof
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (*.f64 a 2)) (/.f64 (*.f64 c 2) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 a) c))))) (*.f64 a 2)) (/.f64 (*.f64 c 2) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite<= *-commutative_binary64 (*.f64 2 a))) (/.f64 (*.f64 c 2) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 c)) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (*.f64 2 c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 a) c))))))): 0 points increase in error, 0 points decrease in error

   if -9.9999999999999999e-186 < (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (*.f64 2 c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) < -0.0

   1. Initial program 32.0

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. Simplified 31.9

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\left(-b\right) + \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}\\ } \end{array}} \]
      Proof
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))) (*.f64 a 2)) (/.f64 (*.f64 c 2) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 a) c))))) (*.f64 a 2)) (/.f64 (*.f64 c 2) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite<= *-commutative_binary64 (*.f64 2 a))) (/.f64 (*.f64 c 2) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 c)) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (*.f64 2 c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 a) c))))))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in b around -inf 13.6

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\color{blue}{\frac{c \cdot 2}{2 \cdot \frac{c \cdot a}{b} + -2 \cdot b}}\\ \end{array} \]

   4. Simplified 11.4

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - 4 \cdot \left(a \cdot c\right)}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\color{blue}{\frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}}\\ \end{array} \]
      Proof
      (fma.f64 2 (/.f64 c (/.f64 b a)) (*.f64 b -2)): 0 points increase in error, 0 points decrease in error
      (fma.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c a) b)) (*.f64 b -2)): 29 points increase in error, 12 points decrease in error
      (fma.f64 2 (/.f64 (*.f64 c a) b) (Rewrite<= *-commutative_binary64 (*.f64 -2 b))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 (/.f64 (*.f64 c a) b)) (*.f64 -2 b))): 0 points increase in error, 0 points decrease in error

   5. Taylor expanded in b around 0 11.8

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\color{blue}{-4 \cdot \left(c \cdot a\right)}}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}\\ \end{array} \]

   if 5.0000000000000001e291 < (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (*.f64 2 c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))

   1. Initial program 62.1

      \[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot c}{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}\\ \end{array} \]

   2. Simplified 61.9

      \[\leadsto \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;b \geq 0:\\ \;\;\;\;\left(b + \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}\right) \cdot \frac{-0.5}{a}\\ \mathbf{else}:\\ \;\;\;\;-2 \cdot \frac{c}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}\\ } \end{array}} \]
      Proof
      (if (>=.f64 b 0) (*.f64 (+.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b)))) (/.f64 -1/2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (*.f64 (+.f64 b (sqrt.f64 (fma.f64 c (*.f64 a (Rewrite<= metadata-eval (neg.f64 4))) (*.f64 b b)))) (/.f64 -1/2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (*.f64 (+.f64 b (sqrt.f64 (fma.f64 c (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4))) (*.f64 b b)))) (/.f64 -1/2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (*.f64 (+.f64 b (sqrt.f64 (fma.f64 c (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 a))) (*.f64 b b)))) (/.f64 -1/2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (*.f64 (+.f64 b (sqrt.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 c (neg.f64 (*.f64 4 a))) (*.f64 b b))))) (/.f64 -1/2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (*.f64 (+.f64 b (sqrt.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 4 a)) c)) (*.f64 b b)))) (/.f64 -1/2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (*.f64 (+.f64 b (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 b b) (*.f64 (neg.f64 (*.f64 4 a)) c))))) (/.f64 -1/2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (*.f64 (+.f64 b (sqrt.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (/.f64 -1/2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (*.f64 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (Rewrite<= metadata-eval (/.f64 -1 2)) a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (*.f64 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite<= associate-/r*_binary64 (/.f64 -1 (*.f64 2 a)))) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) -1) (*.f64 2 a))) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 3 points increase in error, 22 points decrease in error
      (if (>=.f64 b 0) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (+.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (Rewrite<= distribute-neg-out_binary64 (+.f64 (neg.f64 b) (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))) (*.f64 2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (*.f64 2 a)) (*.f64 -2 (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (Rewrite<= metadata-eval (/.f64 2 -1)) (/.f64 c (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 c 1)) (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 c (Rewrite<= metadata-eval (*.f64 -1 -1))) (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 c -1) -1)) (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a -4) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 (/.f64 c -1) -1) (-.f64 b (sqrt.f64 (fma.f64 c (*.f64 a (Rewrite<= metadata-eval (neg.f64 4))) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 (/.f64 c -1) -1) (-.f64 b (sqrt.f64 (fma.f64 c (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4))) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 (/.f64 c -1) -1) (-.f64 b (sqrt.f64 (fma.f64 c (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 a))) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 (/.f64 c -1) -1) (-.f64 b (sqrt.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 c (neg.f64 (*.f64 4 a))) (*.f64 b b)))))))): 1 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 (/.f64 c -1) -1) (-.f64 b (sqrt.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 4 a)) c)) (*.f64 b b))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 (/.f64 c -1) -1) (-.f64 b (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 b b) (*.f64 (neg.f64 (*.f64 4 a)) c)))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 (/.f64 c -1) -1) (-.f64 b (sqrt.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (Rewrite=> associate-/l/_binary64 (/.f64 (/.f64 c -1) (*.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) -1))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 c -1) (Rewrite<= *-commutative_binary64 (*.f64 -1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 c -1) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 c -1) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 c -1) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 2 -1) (/.f64 (/.f64 c -1) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 b)) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 2 (/.f64 c -1)) (*.f64 -1 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 2 c) -1)) (*.f64 -1 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (Rewrite=> associate-/l*_binary64 (/.f64 2 (/.f64 -1 c))) (*.f64 -1 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))): 10 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (/.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 2 -1) c)) (*.f64 -1 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))): 0 points increase in error, 10 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (Rewrite=> times-frac_binary64 (*.f64 (/.f64 (/.f64 2 -1) -1) (/.f64 c (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (/.f64 (Rewrite=> metadata-eval -2) -1) (/.f64 c (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (*.f64 (Rewrite=> metadata-eval 2) (/.f64 c (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))): 0 points increase in error, 0 points decrease in error
      (if (>=.f64 b 0) (/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (*.f64 2 a)) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 2 c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))))): 0 points increase in error, 0 points decrease in error

   3. Applied egg-rr 29.4

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\left(b + \color{blue}{\mathsf{hypot}\left(b, \sqrt{c} \cdot \sqrt{a \cdot -4}\right)}\right) \cdot \frac{-0.5}{a}\\ \mathbf{else}:\\ \;\;\;\;-2 \cdot \frac{c}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}\\ \end{array} \]

   4. Simplified 29.4

      \[\leadsto \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\left(b + \color{blue}{\mathsf{hypot}\left(b, \sqrt{a \cdot -4} \cdot \sqrt{c}\right)}\right) \cdot \frac{-0.5}{a}\\ \mathbf{else}:\\ \;\;\;\;-2 \cdot \frac{c}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}\\ \end{array} \]
      Proof
      (hypot.f64 b (*.f64 (sqrt.f64 (*.f64 a -4)) (sqrt.f64 c))): 0 points increase in error, 0 points decrease in error
      (hypot.f64 b (Rewrite<= *-commutative_binary64 (*.f64 (sqrt.f64 c) (sqrt.f64 (*.f64 a -4))))): 0 points increase in error, 0 points decrease in error
3. Recombined 4 regimes into one program.

4. Final simplification 8.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} - b}\\ \end{array} \leq -\infty:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array}\\ \mathbf{elif}\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} - b}\\ \end{array} \leq -1 \cdot 10^{-185}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \left(a \cdot c\right) \cdot -4}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\sqrt{b \cdot b + \left(a \cdot c\right) \cdot -4} - b}\\ \end{array}\\ \mathbf{elif}\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} - b}\\ \end{array} \leq 0:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(a \cdot c\right) \cdot -4}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}\\ \end{array}\\ \mathbf{elif}\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} - b}\\ \end{array} \leq 5 \cdot 10^{+291}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{b \cdot b + \left(a \cdot c\right) \cdot -4}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\sqrt{b \cdot b + \left(a \cdot c\right) \cdot -4} - b}\\ \end{array}\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;\left(b + \mathsf{hypot}\left(b, \sqrt{a \cdot -4} \cdot \sqrt{c}\right)\right) \cdot \frac{-0.5}{a}\\ \mathbf{else}:\\ \;\;\;\;-2 \cdot \frac{c}{b - \sqrt{\mathsf{fma}\left(c, a \cdot -4, b \cdot b\right)}}\\ \end{array} \]

Alternatives

Alternative 1
Error	8.6
Cost	50596

\[\begin{array}{l} t_0 := \left(a \cdot c\right) \cdot -4\\ t_1 := \sqrt{b \cdot b + t_0}\\ t_2 := \frac{c \cdot 2}{t_1 - b}\\ t_3 := \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - t_1}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array}\\ t_4 := \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\\ t_5 := \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - t_4}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{t_4 - b}\\ \end{array}\\ \mathbf{if}\;t_5 \leq -\infty:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array}\\ \mathbf{elif}\;t_5 \leq -1 \cdot 10^{-185}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;t_5 \leq 0:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{t_0}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}\\ \end{array}\\ \mathbf{elif}\;t_5 \leq 5 \cdot 10^{+291}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;-0.5 \cdot \frac{b + \mathsf{hypot}\left(b, \sqrt{a \cdot -4} \cdot \sqrt{c}\right)}{a}\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 2
Error	7.9
Cost	38052

\[\begin{array}{l} t_0 := \left(a \cdot c\right) \cdot -4\\ t_1 := \sqrt{b \cdot b + t_0}\\ t_2 := \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}\\ t_3 := \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - t_2}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{t_2 - b}\\ \end{array}\\ t_4 := \begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - t_1}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{t_1 - b}\\ \end{array}\\ t_5 := \frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}\\ \mathbf{if}\;t_3 \leq -\infty:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array}\\ \mathbf{elif}\;t_3 \leq -1 \cdot 10^{-185}:\\ \;\;\;\;t_4\\ \mathbf{elif}\;t_3 \leq 0:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{t_0}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;t_5\\ \end{array}\\ \mathbf{elif}\;t_3 \leq 10^{+224}:\\ \;\;\;\;t_4\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;\frac{b \cdot -2}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;t_5\\ \end{array} \]

Alternative 3
Error	7.4
Cost	7952

\[\begin{array}{l} t_0 := \sqrt{b \cdot b + \left(a \cdot c\right) \cdot -4}\\ t_1 := \frac{c}{b} - \frac{b}{a}\\ \mathbf{if}\;b \leq -5 \cdot 10^{+153}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(2 \cdot \frac{c}{\frac{b}{a}} - b\right) - b}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, a \cdot \frac{c}{b}, b \cdot -2\right)}\\ \end{array}\\ \mathbf{elif}\;b \leq -5 \cdot 10^{-310}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{t_0 - b}\\ \end{array}\\ \mathbf{elif}\;b \leq 1.55 \cdot 10^{+38}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - t_0}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{b}{a} + \frac{\frac{{b}^{3}}{c}}{a \cdot a}\\ \end{array}\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array} \]

Alternative 4
Error	7.4
Cost	7952

\[\begin{array}{l} t_0 := \sqrt{b \cdot b + \left(a \cdot c\right) \cdot -4}\\ t_1 := \frac{c \cdot 2}{\mathsf{fma}\left(2, a \cdot \frac{c}{b}, b \cdot -2\right)}\\ t_2 := \frac{c}{b} - \frac{b}{a}\\ \mathbf{if}\;b \leq -2 \cdot 10^{+153}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(2 \cdot \frac{c}{\frac{b}{a}} - b\right) - b}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array}\\ \mathbf{elif}\;b \leq -5 \cdot 10^{-310}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{t_0 - b}\\ \end{array}\\ \mathbf{elif}\;b \leq 1.55 \cdot 10^{+38}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - t_0}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array}\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array} \]

Alternative 5
Error	10.3
Cost	7760

\[\begin{array}{l} t_0 := \left(a \cdot c\right) \cdot -4\\ t_1 := \frac{c}{\frac{b}{a}}\\ t_2 := \frac{c}{b} - \frac{b}{a}\\ \mathbf{if}\;b \leq -1 \cdot 10^{+154}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(2 \cdot t_1 - b\right) - b}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, a \cdot \frac{c}{b}, b \cdot -2\right)}\\ \end{array}\\ \mathbf{elif}\;b \leq -5 \cdot 10^{-310}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\sqrt{b \cdot b + t_0} - b}\\ \end{array}\\ \mathbf{elif}\;b \leq 7.8 \cdot 10^{-39}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{t_0}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, t_1, b \cdot -2\right)}\\ \end{array}\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array} \]

Alternative 6
Error	18.2
Cost	7496

\[\begin{array}{l} \mathbf{if}\;b \leq 6.6 \cdot 10^{-38}:\\ \;\;\;\;\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{\left(-b\right) - \sqrt{\left(a \cdot c\right) \cdot -4}}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}\\ \end{array}\\ \mathbf{elif}\;b \geq 0:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array} \]

Alternative 7
Error	22.9
Cost	7364

\[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{b \cdot -2}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{c \cdot 2}{\mathsf{fma}\left(2, \frac{c}{\frac{b}{a}}, b \cdot -2\right)}\\ \end{array} \]

Alternative 8
Error	39.8
Cost	388

\[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{c}{b}\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array} \]

Alternative 9
Error	23.0
Cost	388

\[\begin{array}{l} \mathbf{if}\;b \geq 0:\\ \;\;\;\;\frac{-b}{a}\\ \mathbf{else}:\\ \;\;\;\;-\frac{c}{b}\\ \end{array} \]

Reproduce

herbie shell --seed 2022296 
(FPCore (a b c)
  :name "jeff quadratic root 1"
  :precision binary64
  (if (>= b 0.0) (/ (- (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)) (/ (* 2.0 c) (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))))))