Average Error: 34.5 → 12.0
Time: 25.7s
Precision: binary64
Cost: 21200
\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a} \]
\[\begin{array}{l} t_0 := \frac{\sqrt{b \cdot b + \mathsf{fma}\left(c, a \cdot -4, \mathsf{fma}\left(c, a \cdot -4, 4 \cdot \left(c \cdot a\right)\right)\right)} - b}{a \cdot 2}\\ \mathbf{if}\;b \leq -1600000000000:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \leq -2.65 \cdot 10^{-258}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;b \leq 6.6 \cdot 10^{-243}:\\ \;\;\;\;{\left(\frac{a \cdot -2}{b - \sqrt{c} \cdot \sqrt{a \cdot -4}}\right)}^{-1}\\ \mathbf{elif}\;b \leq 3.6 \cdot 10^{-64}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\frac{-c}{b}\\ \end{array} \]
(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
         (/
          (-
           (sqrt
            (+ (* b b) (fma c (* a -4.0) (fma c (* a -4.0) (* 4.0 (* c a))))))
           b)
          (* a 2.0))))
   (if (<= b -1600000000000.0)
     (- (/ c b) (/ b a))
     (if (<= b -2.65e-258)
       t_0
       (if (<= b 6.6e-243)
         (pow (/ (* a -2.0) (- b (* (sqrt c) (sqrt (* a -4.0))))) -1.0)
         (if (<= b 3.6e-64) t_0 (/ (- c) b)))))))
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 = (sqrt(((b * b) + fma(c, (a * -4.0), fma(c, (a * -4.0), (4.0 * (c * a)))))) - b) / (a * 2.0);
	double tmp;
	if (b <= -1600000000000.0) {
		tmp = (c / b) - (b / a);
	} else if (b <= -2.65e-258) {
		tmp = t_0;
	} else if (b <= 6.6e-243) {
		tmp = pow(((a * -2.0) / (b - (sqrt(c) * sqrt((a * -4.0))))), -1.0);
	} else if (b <= 3.6e-64) {
		tmp = t_0;
	} else {
		tmp = -c / b;
	}
	return tmp;
}
function code(a, b, c)
	return Float64(Float64(Float64(-b) + sqrt(Float64(Float64(b * b) - Float64(Float64(4.0 * a) * c)))) / Float64(2.0 * a))
end
function code(a, b, c)
	t_0 = Float64(Float64(sqrt(Float64(Float64(b * b) + fma(c, Float64(a * -4.0), fma(c, Float64(a * -4.0), Float64(4.0 * Float64(c * a)))))) - b) / Float64(a * 2.0))
	tmp = 0.0
	if (b <= -1600000000000.0)
		tmp = Float64(Float64(c / b) - Float64(b / a));
	elseif (b <= -2.65e-258)
		tmp = t_0;
	elseif (b <= 6.6e-243)
		tmp = Float64(Float64(a * -2.0) / Float64(b - Float64(sqrt(c) * sqrt(Float64(a * -4.0))))) ^ -1.0;
	elseif (b <= 3.6e-64)
		tmp = t_0;
	else
		tmp = Float64(Float64(-c) / b);
	end
	return tmp
end
code[a_, b_, c_] := 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]
code[a_, b_, c_] := Block[{t$95$0 = N[(N[(N[Sqrt[N[(N[(b * b), $MachinePrecision] + N[(c * N[(a * -4.0), $MachinePrecision] + N[(c * N[(a * -4.0), $MachinePrecision] + N[(4.0 * N[(c * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - b), $MachinePrecision] / N[(a * 2.0), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[b, -1600000000000.0], N[(N[(c / b), $MachinePrecision] - N[(b / a), $MachinePrecision]), $MachinePrecision], If[LessEqual[b, -2.65e-258], t$95$0, If[LessEqual[b, 6.6e-243], N[Power[N[(N[(a * -2.0), $MachinePrecision] / N[(b - N[(N[Sqrt[c], $MachinePrecision] * N[Sqrt[N[(a * -4.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], -1.0], $MachinePrecision], If[LessEqual[b, 3.6e-64], t$95$0, N[((-c) / b), $MachinePrecision]]]]]]
\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}
\begin{array}{l}
t_0 := \frac{\sqrt{b \cdot b + \mathsf{fma}\left(c, a \cdot -4, \mathsf{fma}\left(c, a \cdot -4, 4 \cdot \left(c \cdot a\right)\right)\right)} - b}{a \cdot 2}\\
\mathbf{if}\;b \leq -1600000000000:\\
\;\;\;\;\frac{c}{b} - \frac{b}{a}\\

\mathbf{elif}\;b \leq -2.65 \cdot 10^{-258}:\\
\;\;\;\;t_0\\

\mathbf{elif}\;b \leq 6.6 \cdot 10^{-243}:\\
\;\;\;\;{\left(\frac{a \cdot -2}{b - \sqrt{c} \cdot \sqrt{a \cdot -4}}\right)}^{-1}\\

\mathbf{elif}\;b \leq 3.6 \cdot 10^{-64}:\\
\;\;\;\;t_0\\

\mathbf{else}:\\
\;\;\;\;\frac{-c}{b}\\


\end{array}

Error

Target

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

Derivation

  1. Split input into 4 regimes
  2. if b < -1.6e12

    1. Initial program 33.2

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

      \[\leadsto \color{blue}{\left(\sqrt{\mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)} - b\right) \cdot \frac{0.5}{a}} \]
      Proof
      (*.f64 (-.f64 (sqrt.f64 (fma.f64 a (*.f64 c -4) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (fma.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 4))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (fma.f64 a (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 c 4))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (fma.f64 a (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 4 c))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (fma.f64 a (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 4) c)) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 a (*.f64 (neg.f64 4) c)) (*.f64 b b)))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a (neg.f64 4)) c)) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4))) c) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 a))) c) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 b b) (*.f64 (neg.f64 (*.f64 4 a)) c)))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) (neg.f64 b))) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (Rewrite<= metadata-eval (/.f64 1 2)) a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 -1)) 2) a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite<= associate-/r*_binary64 (/.f64 (neg.f64 -1) (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (neg.f64 -1)) (*.f64 2 a))): 5 points increase in error, 26 points decrease in error
      (Rewrite=> associate-/l*_binary64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (*.f64 2 a) (neg.f64 -1)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (*.f64 2 a) (Rewrite=> metadata-eval 1))): 0 points increase in error, 0 points decrease in error
      (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite=> /-rgt-identity_binary64 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    3. Applied egg-rr46.1

      \[\leadsto \left(\color{blue}{\mathsf{hypot}\left(\sqrt{a} \cdot \sqrt{c \cdot -4}, b\right)} - b\right) \cdot \frac{0.5}{a} \]
    4. Taylor expanded in b around -inf 64.0

      \[\leadsto \color{blue}{-0.25 \cdot \frac{c \cdot {\left(\sqrt{-4}\right)}^{2}}{b} + -1 \cdot \frac{b}{a}} \]
    5. Simplified6.7

      \[\leadsto \color{blue}{\frac{c}{b} - \frac{b}{a}} \]
      Proof
      (-.f64 (/.f64 c b) (/.f64 b a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 c)) b) (/.f64 b a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (*.f64 (Rewrite<= metadata-eval (*.f64 -1/4 -4)) c) b) (/.f64 b a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (*.f64 (*.f64 -1/4 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 -4) (sqrt.f64 -4)))) c) b) (/.f64 b a)): 217 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (*.f64 (*.f64 -1/4 (Rewrite<= unpow2_binary64 (pow.f64 (sqrt.f64 -4) 2))) c) b) (/.f64 b a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1/4 (*.f64 (pow.f64 (sqrt.f64 -4) 2) c))) b) (/.f64 b a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (*.f64 -1/4 (Rewrite<= *-commutative_binary64 (*.f64 c (pow.f64 (sqrt.f64 -4) 2)))) b) (/.f64 b a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1/4 (/.f64 (*.f64 c (pow.f64 (sqrt.f64 -4) 2)) b))) (/.f64 b a)): 0 points increase in error, 0 points decrease in error
      (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1/4 (/.f64 (*.f64 c (pow.f64 (sqrt.f64 -4) 2)) b)) (neg.f64 (/.f64 b a)))): 0 points increase in error, 0 points decrease in error
      (+.f64 (*.f64 -1/4 (/.f64 (*.f64 c (pow.f64 (sqrt.f64 -4) 2)) b)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 b a)))): 0 points increase in error, 0 points decrease in error

    if -1.6e12 < b < -2.65000000000000007e-258 or 6.60000000000000026e-243 < b < 3.5999999999999998e-64

    1. Initial program 14.9

      \[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a} \]
    2. Applied egg-rr15.0

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

    if -2.65000000000000007e-258 < b < 6.60000000000000026e-243

    1. Initial program 14.4

      \[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a} \]
    2. Taylor expanded in b around 0 14.5

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

      \[\leadsto \frac{\left(-b\right) + \sqrt{\color{blue}{c \cdot \left(a \cdot -4\right)}}}{2 \cdot a} \]
      Proof
      (*.f64 c (*.f64 a -4)): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c a) -4)): 1 points increase in error, 3 points decrease in error
      (Rewrite<= *-commutative_binary64 (*.f64 -4 (*.f64 c a))): 0 points increase in error, 0 points decrease in error
    4. Applied egg-rr14.6

      \[\leadsto \color{blue}{{\left(\frac{a \cdot -2}{b - \sqrt{\left(c \cdot -4\right) \cdot a}}\right)}^{-1}} \]
    5. Applied egg-rr34.3

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

    if 3.5999999999999998e-64 < b

    1. Initial program 54.2

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

      \[\leadsto \color{blue}{\left(\sqrt{\mathsf{fma}\left(a, c \cdot -4, b \cdot b\right)} - b\right) \cdot \frac{0.5}{a}} \]
      Proof
      (*.f64 (-.f64 (sqrt.f64 (fma.f64 a (*.f64 c -4) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (fma.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 4))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (fma.f64 a (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 c 4))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (fma.f64 a (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 4 c))) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (fma.f64 a (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 4) c)) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 a (*.f64 (neg.f64 4) c)) (*.f64 b b)))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a (neg.f64 4)) c)) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 4))) c) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 a))) c) (*.f64 b b))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 b b) (*.f64 (neg.f64 (*.f64 4 a)) c)))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 (sqrt.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) (neg.f64 b))) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (Rewrite<= metadata-eval (/.f64 1 2)) a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 -1)) 2) a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite<= associate-/r*_binary64 (/.f64 (neg.f64 -1) (*.f64 2 a)))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (neg.f64 -1)) (*.f64 2 a))): 5 points increase in error, 26 points decrease in error
      (Rewrite=> associate-/l*_binary64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (*.f64 2 a) (neg.f64 -1)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (*.f64 2 a) (Rewrite=> metadata-eval 1))): 0 points increase in error, 0 points decrease in error
      (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite=> /-rgt-identity_binary64 (*.f64 2 a))): 0 points increase in error, 0 points decrease in error
    3. Taylor expanded in a around 0 8.6

      \[\leadsto \color{blue}{-1 \cdot \frac{c}{b}} \]
    4. Simplified8.6

      \[\leadsto \color{blue}{\frac{-c}{b}} \]
      Proof
      (/.f64 (neg.f64 c) b): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 c)) b): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 c b))): 0 points increase in error, 0 points decrease in error
  3. Recombined 4 regimes into one program.
  4. Final simplification12.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;b \leq -1600000000000:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \leq -2.65 \cdot 10^{-258}:\\ \;\;\;\;\frac{\sqrt{b \cdot b + \mathsf{fma}\left(c, a \cdot -4, \mathsf{fma}\left(c, a \cdot -4, 4 \cdot \left(c \cdot a\right)\right)\right)} - b}{a \cdot 2}\\ \mathbf{elif}\;b \leq 6.6 \cdot 10^{-243}:\\ \;\;\;\;{\left(\frac{a \cdot -2}{b - \sqrt{c} \cdot \sqrt{a \cdot -4}}\right)}^{-1}\\ \mathbf{elif}\;b \leq 3.6 \cdot 10^{-64}:\\ \;\;\;\;\frac{\sqrt{b \cdot b + \mathsf{fma}\left(c, a \cdot -4, \mathsf{fma}\left(c, a \cdot -4, 4 \cdot \left(c \cdot a\right)\right)\right)} - b}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{-c}{b}\\ \end{array} \]

Alternatives

Alternative 1
Error12.0
Cost20364
\[\begin{array}{l} t_0 := \frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -4\right)} - b}{a \cdot 2}\\ \mathbf{if}\;b \leq -1600000000000:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \leq -2.65 \cdot 10^{-258}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;b \leq 6.6 \cdot 10^{-243}:\\ \;\;\;\;{\left(\frac{a \cdot -2}{b - \sqrt{c} \cdot \sqrt{a \cdot -4}}\right)}^{-1}\\ \mathbf{elif}\;b \leq 3.6 \cdot 10^{-64}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\frac{-c}{b}\\ \end{array} \]
Alternative 2
Error12.0
Cost13900
\[\begin{array}{l} t_0 := \frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -4\right)} - b}{a \cdot 2}\\ \mathbf{if}\;b \leq -1600000000000:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \leq -2.65 \cdot 10^{-258}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;b \leq 6.6 \cdot 10^{-243}:\\ \;\;\;\;\frac{\sqrt{c} \cdot \sqrt{a \cdot -4} - b}{a \cdot 2}\\ \mathbf{elif}\;b \leq 3.6 \cdot 10^{-64}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\frac{-c}{b}\\ \end{array} \]
Alternative 3
Error10.6
Cost7624
\[\begin{array}{l} \mathbf{if}\;b \leq -1600000000000:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \leq 3.6 \cdot 10^{-64}:\\ \;\;\;\;\left(\sqrt{b \cdot b + -4 \cdot \left(c \cdot a\right)} - b\right) \cdot \frac{0.5}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-c}{b}\\ \end{array} \]
Alternative 4
Error10.6
Cost7624
\[\begin{array}{l} \mathbf{if}\;b \leq -1600000000000:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \leq 3.6 \cdot 10^{-64}:\\ \;\;\;\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -4\right)} - b}{a \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{-c}{b}\\ \end{array} \]
Alternative 5
Error13.1
Cost7368
\[\begin{array}{l} \mathbf{if}\;b \leq -7.6 \cdot 10^{-71}:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{elif}\;b \leq 3.6 \cdot 10^{-64}:\\ \;\;\;\;\frac{\frac{b - \sqrt{c \cdot \left(a \cdot -4\right)}}{a}}{-2}\\ \mathbf{else}:\\ \;\;\;\;\frac{-c}{b}\\ \end{array} \]
Alternative 6
Error22.5
Cost708
\[\begin{array}{l} \mathbf{if}\;b \leq -4.4 \cdot 10^{-274}:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\frac{a}{b} - \frac{b}{c}}\\ \end{array} \]
Alternative 7
Error22.5
Cost580
\[\begin{array}{l} \mathbf{if}\;b \leq -1.15 \cdot 10^{-307}:\\ \;\;\;\;\frac{c}{b} - \frac{b}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-c}{b}\\ \end{array} \]
Alternative 8
Error22.5
Cost388
\[\begin{array}{l} \mathbf{if}\;b \leq 1.22 \cdot 10^{-278}:\\ \;\;\;\;-\frac{b}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{-c}{b}\\ \end{array} \]
Alternative 9
Error39.4
Cost256
\[\frac{-c}{b} \]
Alternative 10
Error56.5
Cost64
\[0 \]

Error

Reproduce

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

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

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