Average Error: 43.8 → 0.4
Time: 14.6s
Precision: binary64
Cost: 14016
\[\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} t_0 := c \cdot \left(a \cdot -3\right)\\ \frac{\frac{t_0}{b + \sqrt{\mathsf{fma}\left(b, b, t_0\right)}}}{a \cdot 3} \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
 (let* ((t_0 (* c (* a -3.0))))
   (/ (/ t_0 (+ b (sqrt (fma b b t_0)))) (* a 3.0))))
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 t_0 = c * (a * -3.0);
	return (t_0 / (b + sqrt(fma(b, b, t_0)))) / (a * 3.0);
}

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)
	t_0 = Float64(c * Float64(a * -3.0))
	return Float64(Float64(t_0 / Float64(b + sqrt(fma(b, b, t_0)))) / Float64(a * 3.0))
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_] := Block[{t$95$0 = N[(c * N[(a * -3.0), $MachinePrecision]), $MachinePrecision]}, N[(N[(t$95$0 / N[(b + N[Sqrt[N[(b * b + t$95$0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(a * 3.0), $MachinePrecision]), $MachinePrecision]]

\frac{\left(-b\right) + \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{3 \cdot a}
↓
\begin{array}{l}
t_0 := c \cdot \left(a \cdot -3\right)\\
\frac{\frac{t_0}{b + \sqrt{\mathsf{fma}\left(b, b, t_0\right)}}}{a \cdot 3}
\end{array}

Error

Derivation

  1. Initial program 43.8

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

  2. Applied egg-rr43.8

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

  3. Simplified43.8

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

  4. Applied egg-rr43.3

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

  5. Simplified0.4

    \[\leadsto \frac{\color{blue}{\frac{c \cdot \left(a \cdot -3\right)}{b + \sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -3\right)\right)}}}}{3 \cdot a} \]
    Proof
    (/.f64 (*.f64 c (*.f64 a -3)) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 c a) -3)) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 53 points increase in error, 36 points decrease in error
    (/.f64 (*.f64 (*.f64 c a) (Rewrite<= metadata-eval (neg.f64 3))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 c a) 3))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 a 3)))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 36 points increase in error, 53 points decrease in error
    (/.f64 (neg.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (*.f64 c (*.f64 a 3)))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (neg.f64 (neg.f64 (*.f64 c (Rewrite=> *-commutative_binary64 (*.f64 3 a)))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (neg.f64 (neg.f64 (*.f64 c (*.f64 (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 3) (sqrt.f64 3))) a))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 130 points increase in error, 71 points decrease in error
    (/.f64 (neg.f64 (neg.f64 (neg.f64 (*.f64 c (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (sqrt.f64 3) 2)) a))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (neg.f64 (neg.f64 (*.f64 c (Rewrite<= *-commutative_binary64 (*.f64 a (pow.f64 (sqrt.f64 3) 2))))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 c (*.f64 a (pow.f64 (sqrt.f64 3) 2))))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 -1 (*.f64 c (*.f64 a (pow.f64 (sqrt.f64 3) 2))))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (-.f64 (Rewrite<= +-inverses_binary64 (-.f64 (*.f64 b b) (*.f64 b b))) (*.f64 -1 (*.f64 c (*.f64 a (pow.f64 (sqrt.f64 3) 2)))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (-.f64 (-.f64 (*.f64 b b) (*.f64 b b)) (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 c (*.f64 a (pow.f64 (sqrt.f64 3) 2))))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (-.f64 (-.f64 (*.f64 b b) (*.f64 b b)) (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 a (pow.f64 (sqrt.f64 3) 2)) c))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (-.f64 (-.f64 (*.f64 b b) (*.f64 b b)) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 c (*.f64 a (pow.f64 (sqrt.f64 3) 2))))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (-.f64 (-.f64 (*.f64 b b) (*.f64 b b)) (neg.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 c a) (pow.f64 (sqrt.f64 3) 2)))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 44 points increase in error, 39 points decrease in error
    (/.f64 (neg.f64 (-.f64 (-.f64 (*.f64 b b) (*.f64 b b)) (neg.f64 (*.f64 (*.f64 c a) (Rewrite=> unpow2_binary64 (*.f64 (sqrt.f64 3) (sqrt.f64 3))))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (-.f64 (-.f64 (*.f64 b b) (*.f64 b b)) (neg.f64 (*.f64 (*.f64 c a) (Rewrite=> rem-square-sqrt_binary64 3))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 73 points increase in error, 129 points decrease in error
    (/.f64 (neg.f64 (-.f64 (-.f64 (*.f64 b b) (*.f64 b b)) (Rewrite=> distribute-rgt-neg-in_binary64 (*.f64 (*.f64 c a) (neg.f64 3))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (-.f64 (-.f64 (*.f64 b b) (*.f64 b b)) (*.f64 (*.f64 c a) (Rewrite=> metadata-eval -3)))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (-.f64 (-.f64 (*.f64 b b) (*.f64 b b)) (Rewrite<= associate-*r*_binary64 (*.f64 c (*.f64 a -3))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 36 points increase in error, 53 points decrease in error
    (/.f64 (neg.f64 (-.f64 (-.f64 (*.f64 b b) (*.f64 b b)) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 a -3) c)))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (neg.f64 (Rewrite<= associate--r+_binary64 (-.f64 (*.f64 b b) (+.f64 (*.f64 b b) (*.f64 (*.f64 a -3) c))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 185 points increase in error, 64 points decrease in error
    (/.f64 (neg.f64 (-.f64 (*.f64 b b) (Rewrite<= fma-udef_binary64 (fma.f64 b b (*.f64 (*.f64 a -3) c))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 16 points increase in error, 13 points decrease in error
    (/.f64 (neg.f64 (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 b b) (neg.f64 (fma.f64 b b (*.f64 (*.f64 a -3) c)))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite=> distribute-neg-in_binary64 (+.f64 (neg.f64 (*.f64 b b)) (neg.f64 (neg.f64 (fma.f64 b b (*.f64 (*.f64 a -3) c)))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (+.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (*.f64 b b))) (neg.f64 (neg.f64 (fma.f64 b b (*.f64 (*.f64 a -3) c))))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (+.f64 (*.f64 -1 (*.f64 b b)) (Rewrite=> remove-double-neg_binary64 (fma.f64 b b (*.f64 (*.f64 a -3) c)))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (fma.f64 b b (*.f64 (*.f64 a -3) c)) (*.f64 -1 (*.f64 b b)))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (+.f64 (fma.f64 b b (*.f64 (*.f64 a -3) c)) (Rewrite<= neg-mul-1_binary64 (neg.f64 (*.f64 b b)))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (fma.f64 b b (*.f64 (*.f64 a -3) c)) (*.f64 b b))) (+.f64 b (sqrt.f64 (fma.f64 b b (*.f64 c (*.f64 a -3)))))): 0 points increase in error, 0 points decrease in error
    (/.f64 (-.f64 (fma.f64 b b (*.f64 (*.f64 a -3) c)) (*.f64 b b)) (+.f64 b (sqrt.f64 (fma.f64 b b (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 a -3) c)))))): 0 points increase in error, 0 points decrease in error

  6. Final simplification0.4

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

Alternatives

Alternative 1
Error0.5
Cost14016
\[\frac{\frac{-3 \cdot \left(c \cdot a\right)}{b + \sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -3\right)\right)}}}{a \cdot 3} \]
Alternative 2
Error5.9
Cost1344
\[\frac{\frac{c \cdot \left(a \cdot -3\right)}{-1.5 \cdot \frac{c \cdot a}{b} + b \cdot 2}}{a \cdot 3} \]
Alternative 3
Error12.0
Cost320
\[-0.5 \cdot \frac{c}{b} \]

Error

Reproduce

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