Average Error: 43.9 → 41.5
Time: 39.9s
Precision: binary64
Cost: 60356
\[\left(\left(1.1102230246251565 \cdot 10^{-16} < a \land a < 9007199254740992\right) \land \left(1.1102230246251565 \cdot 10^{-16} < b \land b < 9007199254740992\right)\right) \land \left(1.1102230246251565 \cdot 10^{-16} < c \land c < 9007199254740992\right)\]
\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{3 \cdot a} \]
\[\begin{array}{l} \mathbf{if}\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a} \leq -5 \cdot 10^{-22}:\\ \;\;\;\;\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot {\left(a \cdot -3\right)}^{-1}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{a}, {\left({\left(\sqrt{0.3333333333333333} \cdot {\left(\mathsf{fma}\left(-3, a \cdot c, b \cdot b\right)\right)}^{0.125}\right)}^{6}\right)}^{0.3333333333333333}, -0.3333333333333333 \cdot \frac{b}{a}\right)\\ \end{array} \]
(FPCore (a b c)
 :precision binary64
 (/ (+ (- b) (sqrt (- (* b b) (* (* 3.0 a) c)))) (* 3.0 a)))
(FPCore (a b c)
 :precision binary64
 (if (<= (/ (- (sqrt (+ (* b b) (* c (* a -3.0)))) b) (* 3.0 a)) -5e-22)
   (* (- b (sqrt (fma b b (* a (* c -3.0))))) (pow (* a -3.0) -1.0))
   (fma
    (/ (pow (fma c (* a -3.0) (* b b)) 0.25) a)
    (pow
     (pow
      (* (sqrt 0.3333333333333333) (pow (fma -3.0 (* a c) (* b b)) 0.125))
      6.0)
     0.3333333333333333)
    (* -0.3333333333333333 (/ b a)))))
double code(double a, double b, double c) {
	return (-b + sqrt(((b * b) - ((3.0 * a) * c)))) / (3.0 * a);
}
double code(double a, double b, double c) {
	double tmp;
	if (((sqrt(((b * b) + (c * (a * -3.0)))) - b) / (3.0 * a)) <= -5e-22) {
		tmp = (b - sqrt(fma(b, b, (a * (c * -3.0))))) * pow((a * -3.0), -1.0);
	} else {
		tmp = fma((pow(fma(c, (a * -3.0), (b * b)), 0.25) / a), pow(pow((sqrt(0.3333333333333333) * pow(fma(-3.0, (a * c), (b * b)), 0.125)), 6.0), 0.3333333333333333), (-0.3333333333333333 * (b / a)));
	}
	return tmp;
}
function code(a, b, c)
	return Float64(Float64(Float64(-b) + sqrt(Float64(Float64(b * b) - Float64(Float64(3.0 * a) * c)))) / Float64(3.0 * a))
end
function code(a, b, c)
	tmp = 0.0
	if (Float64(Float64(sqrt(Float64(Float64(b * b) + Float64(c * Float64(a * -3.0)))) - b) / Float64(3.0 * a)) <= -5e-22)
		tmp = Float64(Float64(b - sqrt(fma(b, b, Float64(a * Float64(c * -3.0))))) * (Float64(a * -3.0) ^ -1.0));
	else
		tmp = fma(Float64((fma(c, Float64(a * -3.0), Float64(b * b)) ^ 0.25) / a), ((Float64(sqrt(0.3333333333333333) * (fma(-3.0, Float64(a * c), Float64(b * b)) ^ 0.125)) ^ 6.0) ^ 0.3333333333333333), Float64(-0.3333333333333333 * Float64(b / a)));
	end
	return tmp
end
code[a_, b_, c_] := N[(N[((-b) + N[Sqrt[N[(N[(b * b), $MachinePrecision] - N[(N[(3.0 * a), $MachinePrecision] * c), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] / N[(3.0 * a), $MachinePrecision]), $MachinePrecision]
code[a_, b_, c_] := If[LessEqual[N[(N[(N[Sqrt[N[(N[(b * b), $MachinePrecision] + N[(c * N[(a * -3.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - b), $MachinePrecision] / N[(3.0 * a), $MachinePrecision]), $MachinePrecision], -5e-22], N[(N[(b - N[Sqrt[N[(b * b + N[(a * N[(c * -3.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] * N[Power[N[(a * -3.0), $MachinePrecision], -1.0], $MachinePrecision]), $MachinePrecision], N[(N[(N[Power[N[(c * N[(a * -3.0), $MachinePrecision] + N[(b * b), $MachinePrecision]), $MachinePrecision], 0.25], $MachinePrecision] / a), $MachinePrecision] * N[Power[N[Power[N[(N[Sqrt[0.3333333333333333], $MachinePrecision] * N[Power[N[(-3.0 * N[(a * c), $MachinePrecision] + N[(b * b), $MachinePrecision]), $MachinePrecision], 0.125], $MachinePrecision]), $MachinePrecision], 6.0], $MachinePrecision], 0.3333333333333333], $MachinePrecision] + N[(-0.3333333333333333 * N[(b / a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\frac{\left(-b\right) + \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{3 \cdot a}
\begin{array}{l}
\mathbf{if}\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a} \leq -5 \cdot 10^{-22}:\\
\;\;\;\;\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot {\left(a \cdot -3\right)}^{-1}\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{a}, {\left({\left(\sqrt{0.3333333333333333} \cdot {\left(\mathsf{fma}\left(-3, a \cdot c, b \cdot b\right)\right)}^{0.125}\right)}^{6}\right)}^{0.3333333333333333}, -0.3333333333333333 \cdot \frac{b}{a}\right)\\


\end{array}

Error

Derivation

  1. Split input into 2 regimes
  2. if (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)) < -4.99999999999999954e-22

    1. Initial program 24.0

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

      \[\leadsto \color{blue}{\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot \frac{-0.3333333333333333}{a}} \]
      Proof
      (*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c -3))))) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (*.f64 a (*.f64 c (Rewrite<= metadata-eval (neg.f64 3))))))) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a c) (neg.f64 3)))))) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 a c) 3)))))) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 3 (*.f64 a c))))))) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 b (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 3 a) c)))))) (/.f64 -1/3 a)): 1 points increase in error, 0 points decrease in error
      (*.f64 (-.f64 b (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (/.f64 -1/3 a)): 10 points increase in error, 2 points decrease in error
      (*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) 1)) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (Rewrite<= metadata-eval (/.f64 -1 -1))) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) -1)) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) -1) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) -1) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) -1) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) -1) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 b)) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (/.f64 -1/3 a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (/.f64 (Rewrite<= metadata-eval (/.f64 -1 3)) a)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (Rewrite<= associate-/r*_binary64 (/.f64 -1 (*.f64 3 a)))): 15 points increase in error, 22 points decrease in error
      (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (*.f64 -1 (*.f64 3 a)))): 16 points increase in error, 15 points decrease in error
      (/.f64 (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 3 a) -1))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> times-frac_binary64 (*.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)) (/.f64 -1 -1))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)) (Rewrite=> metadata-eval 1)): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)) (Rewrite<= metadata-eval (neg.f64 -1))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/r/_binary64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (/.f64 (*.f64 3 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 3 a) c)))) (/.f64 (*.f64 3 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 3 a) c)))) (Rewrite=> /-rgt-identity_binary64 (*.f64 3 a))): 0 points increase in error, 0 points decrease in error
    3. Applied egg-rr24.0

      \[\leadsto \left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot \color{blue}{{\left(a \cdot -3\right)}^{-1}} \]

    if -4.99999999999999954e-22 < (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a))

    1. Initial program 61.9

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

      \[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -3\right)\right)} - b}{3 \cdot a}} \]
      Proof
      (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a (Rewrite<= metadata-eval (neg.f64 3)))))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 c (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 a 3)))))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 c (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 3 a)))))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 c (*.f64 3 a)))))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 3 a) c))))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) b) (*.f64 3 a)): 10 points increase in error, 2 points decrease in error
      (/.f64 (-.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))) 1)) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (/.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))) (Rewrite<= metadata-eval (/.f64 -1 -1))) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))) -1) -1)) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) -1) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) -1) b) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (/.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (Rewrite<= /-rgt-identity_binary64 (/.f64 b 1))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (/.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (/.f64 b (Rewrite<= metadata-eval (/.f64 -1 -1)))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (/.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 b -1) -1))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (/.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 b)) -1)) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (/.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) -1) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 b)) -1)) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (neg.f64 b)) -1)) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 (Rewrite=> sub-neg_binary64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (neg.f64 (neg.f64 b)))) -1) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 (+.f64 (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (Rewrite=> remove-double-neg_binary64 b)) -1) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 b (neg.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) -1) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) -1) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/r*_binary64 (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 -1 (*.f64 3 a)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) (*.f64 -1 (*.f64 3 a))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (*.f64 -1 (*.f64 3 a))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> times-frac_binary64 (*.f64 (/.f64 (neg.f64 -1) -1) (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (Rewrite=> metadata-eval 1) -1) (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a))): 0 points increase in error, 0 points decrease in error
      (*.f64 (Rewrite=> metadata-eval -1) (/.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (*.f64 3 a))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 b (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
      (/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 b)) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c)))) (*.f64 3 a)): 0 points increase in error, 0 points decrease in error
    3. Applied egg-rr60.8

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{a}, \frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{3}, -0.3333333333333333 \cdot \frac{b}{a}\right)} \]
    4. Simplified60.8

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{a}, \frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{3}, -0.3333333333333333 \cdot \frac{b}{a}\right)} \]
      Proof
      (fma.f64 (/.f64 (pow.f64 (fma.f64 c (*.f64 a -3) (*.f64 b b)) 1/4) a) (/.f64 (pow.f64 (fma.f64 c (*.f64 a -3) (*.f64 b b)) 1/4) 3) (*.f64 -1/3 (/.f64 b a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (/.f64 (pow.f64 (fma.f64 c (*.f64 a -3) (*.f64 b b)) 1/4) a) (/.f64 (pow.f64 (fma.f64 c (*.f64 a -3) (*.f64 b b)) 1/4) 3) (*.f64 (Rewrite<= metadata-eval (neg.f64 1/3)) (/.f64 b a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (/.f64 (pow.f64 (fma.f64 c (*.f64 a -3) (*.f64 b b)) 1/4) a) (/.f64 (pow.f64 (fma.f64 c (*.f64 a -3) (*.f64 b b)) 1/4) 3) (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 1/3 (/.f64 b a))))): 0 points increase in error, 0 points decrease in error
    5. Applied egg-rr57.5

      \[\leadsto \mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{a}, \color{blue}{{\left({\left({\left(\mathsf{fma}\left(b, b, \left(c \cdot a\right) \cdot -3\right)\right)}^{0.25} \cdot 0.3333333333333333\right)}^{3}\right)}^{0.3333333333333333}}, -0.3333333333333333 \cdot \frac{b}{a}\right) \]
    6. Applied egg-rr57.3

      \[\leadsto \mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{a}, {\color{blue}{\left({\left(\sqrt{0.3333333333333333} \cdot {\left(\mathsf{fma}\left(-3, c \cdot a, b \cdot b\right)\right)}^{0.125}\right)}^{3} \cdot {\left(\sqrt{0.3333333333333333} \cdot {\left(\mathsf{fma}\left(-3, c \cdot a, b \cdot b\right)\right)}^{0.125}\right)}^{3}\right)}}^{0.3333333333333333}, -0.3333333333333333 \cdot \frac{b}{a}\right) \]
    7. Simplified57.4

      \[\leadsto \mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{a}, {\color{blue}{\left({\left(\sqrt{0.3333333333333333} \cdot {\left(\mathsf{fma}\left(-3, a \cdot c, b \cdot b\right)\right)}^{0.125}\right)}^{6}\right)}}^{0.3333333333333333}, -0.3333333333333333 \cdot \frac{b}{a}\right) \]
      Proof
      (pow.f64 (*.f64 (sqrt.f64 1/3) (pow.f64 (fma.f64 -3 (*.f64 a c) (*.f64 b b)) 1/8)) 6): 0 points increase in error, 0 points decrease in error
      (pow.f64 (*.f64 (sqrt.f64 1/3) (pow.f64 (fma.f64 -3 (Rewrite<= *-commutative_binary64 (*.f64 c a)) (*.f64 b b)) 1/8)) 6): 0 points increase in error, 0 points decrease in error
      (pow.f64 (*.f64 (sqrt.f64 1/3) (pow.f64 (fma.f64 -3 (*.f64 c a) (*.f64 b b)) 1/8)) (Rewrite<= metadata-eval (*.f64 2 3))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 (*.f64 (sqrt.f64 1/3) (pow.f64 (fma.f64 -3 (*.f64 c a) (*.f64 b b)) 1/8)) 3) (pow.f64 (*.f64 (sqrt.f64 1/3) (pow.f64 (fma.f64 -3 (*.f64 c a) (*.f64 b b)) 1/8)) 3))): 66 points increase in error, 76 points decrease in error
  3. Recombined 2 regimes into one program.
  4. Final simplification41.5

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a} \leq -5 \cdot 10^{-22}:\\ \;\;\;\;\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot {\left(a \cdot -3\right)}^{-1}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{a}, {\left({\left(\sqrt{0.3333333333333333} \cdot {\left(\mathsf{fma}\left(-3, a \cdot c, b \cdot b\right)\right)}^{0.125}\right)}^{6}\right)}^{0.3333333333333333}, -0.3333333333333333 \cdot \frac{b}{a}\right)\\ \end{array} \]

Alternatives

Alternative 1
Error41.5
Cost53956
\[\begin{array}{l} \mathbf{if}\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a} \leq -5 \cdot 10^{-22}:\\ \;\;\;\;\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot {\left(a \cdot -3\right)}^{-1}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{a}, {\left({\left(0.3333333333333333 \cdot {\left(\mathsf{fma}\left(b, b, -3 \cdot \left(a \cdot c\right)\right)\right)}^{0.25}\right)}^{3}\right)}^{0.3333333333333333}, -0.3333333333333333 \cdot \frac{b}{a}\right)\\ \end{array} \]
Alternative 2
Error41.5
Cost47492
\[\begin{array}{l} \mathbf{if}\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a} \leq -5 \cdot 10^{-22}:\\ \;\;\;\;\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot {\left(a \cdot -3\right)}^{-1}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{{\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}}{a}, {\left({\left(\mathsf{fma}\left(-3, a \cdot c, b \cdot b\right)\right)}^{0.75} \cdot 0.037037037037037035\right)}^{0.3333333333333333}, -0.3333333333333333 \cdot \frac{b}{a}\right)\\ \end{array} \]
Alternative 3
Error41.5
Cost40452
\[\begin{array}{l} \mathbf{if}\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a} \leq -5 \cdot 10^{-22}:\\ \;\;\;\;\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot {\left(a \cdot -3\right)}^{-1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{{\left({\left({\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.16666666666666666}\right)}^{2}\right)}^{3}} - b}{3 \cdot a}\\ \end{array} \]
Alternative 4
Error41.5
Cost27652
\[\begin{array}{l} \mathbf{if}\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a} \leq -5 \cdot 10^{-22}:\\ \;\;\;\;\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot {\left(a \cdot -3\right)}^{-1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(-b\right) + {\left({\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{1.5}\right)}^{0.3333333333333333}}{3 \cdot a}\\ \end{array} \]
Alternative 5
Error43.8
Cost20160
\[\frac{{\left({\left(\mathsf{fma}\left(c, a \cdot -3, b \cdot b\right)\right)}^{0.25}\right)}^{2} - b}{3 \cdot a} \]
Alternative 6
Error43.8
Cost20096
\[\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot {\left(a \cdot -3\right)}^{-1} \]
Alternative 7
Error43.8
Cost13632
\[\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot \frac{-0.3333333333333333}{a} \]
Alternative 8
Error43.8
Cost13632
\[-0.3333333333333333 \cdot \frac{b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}}{a} \]
Alternative 9
Error43.8
Cost13632
\[\frac{\sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -3\right)\right)} - b}{3 \cdot a} \]
Alternative 10
Error43.9
Cost7424
\[-0.3333333333333333 \cdot \frac{b - {\left(b \cdot b + a \cdot \left(c \cdot -3\right)\right)}^{0.5}}{a} \]
Alternative 11
Error43.9
Cost7360
\[\frac{\sqrt{b \cdot b + -3 \cdot \left(a \cdot c\right)} - b}{3 \cdot a} \]

Error

Reproduce

herbie shell --seed 2022334 
(FPCore (a b c)
  :name "Cubic critical, medium range"
  :precision binary64
  :pre (and (and (and (< 1.1102230246251565e-16 a) (< a 9007199254740992.0)) (and (< 1.1102230246251565e-16 b) (< b 9007199254740992.0))) (and (< 1.1102230246251565e-16 c) (< c 9007199254740992.0)))
  (/ (+ (- b) (sqrt (- (* b b) (* (* 3.0 a) c)))) (* 3.0 a)))