
(FPCore (a b c) :precision binary64 (/ (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)))
double code(double a, double b, double c) {
return (-b + sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a);
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = (-b + sqrt(((b * b) - ((4.0d0 * a) * c)))) / (2.0d0 * a)
end function
public static double code(double a, double b, double c) {
return (-b + Math.sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a);
}
def code(a, b, c): return (-b + math.sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a)
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 tmp = code(a, b, c) tmp = (-b + sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a); 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]
\begin{array}{l}
\\
\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}
\end{array}
Sampling outcomes in binary64 precision:
Herbie found 9 alternatives:
| Alternative | Accuracy | Speedup |
|---|
(FPCore (a b c) :precision binary64 (/ (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)))
double code(double a, double b, double c) {
return (-b + sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a);
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = (-b + sqrt(((b * b) - ((4.0d0 * a) * c)))) / (2.0d0 * a)
end function
public static double code(double a, double b, double c) {
return (-b + Math.sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a);
}
def code(a, b, c): return (-b + math.sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a)
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 tmp = code(a, b, c) tmp = (-b + sqrt(((b * b) - ((4.0 * a) * c)))) / (2.0 * a); 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]
\begin{array}{l}
\\
\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}
\end{array}
(FPCore (a b c)
:precision binary64
(-
(*
(pow c 4.0)
(-
(* -5.0 (/ (pow a 3.0) (pow b 7.0)))
(/ (+ (* 2.0 (/ (pow a 2.0) (pow b 5.0))) (/ a (* c (pow b 3.0)))) c)))
(/ c b)))
double code(double a, double b, double c) {
return (pow(c, 4.0) * ((-5.0 * (pow(a, 3.0) / pow(b, 7.0))) - (((2.0 * (pow(a, 2.0) / pow(b, 5.0))) + (a / (c * pow(b, 3.0)))) / c))) - (c / b);
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = ((c ** 4.0d0) * (((-5.0d0) * ((a ** 3.0d0) / (b ** 7.0d0))) - (((2.0d0 * ((a ** 2.0d0) / (b ** 5.0d0))) + (a / (c * (b ** 3.0d0)))) / c))) - (c / b)
end function
public static double code(double a, double b, double c) {
return (Math.pow(c, 4.0) * ((-5.0 * (Math.pow(a, 3.0) / Math.pow(b, 7.0))) - (((2.0 * (Math.pow(a, 2.0) / Math.pow(b, 5.0))) + (a / (c * Math.pow(b, 3.0)))) / c))) - (c / b);
}
def code(a, b, c): return (math.pow(c, 4.0) * ((-5.0 * (math.pow(a, 3.0) / math.pow(b, 7.0))) - (((2.0 * (math.pow(a, 2.0) / math.pow(b, 5.0))) + (a / (c * math.pow(b, 3.0)))) / c))) - (c / b)
function code(a, b, c) return Float64(Float64((c ^ 4.0) * Float64(Float64(-5.0 * Float64((a ^ 3.0) / (b ^ 7.0))) - Float64(Float64(Float64(2.0 * Float64((a ^ 2.0) / (b ^ 5.0))) + Float64(a / Float64(c * (b ^ 3.0)))) / c))) - Float64(c / b)) end
function tmp = code(a, b, c) tmp = ((c ^ 4.0) * ((-5.0 * ((a ^ 3.0) / (b ^ 7.0))) - (((2.0 * ((a ^ 2.0) / (b ^ 5.0))) + (a / (c * (b ^ 3.0)))) / c))) - (c / b); end
code[a_, b_, c_] := N[(N[(N[Power[c, 4.0], $MachinePrecision] * N[(N[(-5.0 * N[(N[Power[a, 3.0], $MachinePrecision] / N[Power[b, 7.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(N[(N[(2.0 * N[(N[Power[a, 2.0], $MachinePrecision] / N[Power[b, 5.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(a / N[(c * N[Power[b, 3.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / c), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(c / b), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
{c}^{4} \cdot \left(-5 \cdot \frac{{a}^{3}}{{b}^{7}} - \frac{2 \cdot \frac{{a}^{2}}{{b}^{5}} + \frac{a}{c \cdot {b}^{3}}}{c}\right) - \frac{c}{b}
\end{array}
Initial program 31.9%
*-commutative31.9%
+-commutative31.9%
sqr-neg31.9%
unsub-neg31.9%
sqr-neg31.9%
fma-neg32.0%
distribute-lft-neg-in32.0%
*-commutative32.0%
*-commutative32.0%
distribute-rgt-neg-in32.0%
metadata-eval32.0%
Simplified32.0%
Taylor expanded in a around 0 94.7%
Taylor expanded in c around -inf 94.7%
mul-1-neg94.7%
distribute-frac-neg94.7%
Applied egg-rr94.7%
Final simplification94.7%
(FPCore (a b c) :precision binary64 (- (* a (* (pow c 3.0) (+ (/ (* a -2.0) (pow b 5.0)) (/ -1.0 (* c (pow b 3.0)))))) (/ c b)))
double code(double a, double b, double c) {
return (a * (pow(c, 3.0) * (((a * -2.0) / pow(b, 5.0)) + (-1.0 / (c * pow(b, 3.0)))))) - (c / b);
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = (a * ((c ** 3.0d0) * (((a * (-2.0d0)) / (b ** 5.0d0)) + ((-1.0d0) / (c * (b ** 3.0d0)))))) - (c / b)
end function
public static double code(double a, double b, double c) {
return (a * (Math.pow(c, 3.0) * (((a * -2.0) / Math.pow(b, 5.0)) + (-1.0 / (c * Math.pow(b, 3.0)))))) - (c / b);
}
def code(a, b, c): return (a * (math.pow(c, 3.0) * (((a * -2.0) / math.pow(b, 5.0)) + (-1.0 / (c * math.pow(b, 3.0)))))) - (c / b)
function code(a, b, c) return Float64(Float64(a * Float64((c ^ 3.0) * Float64(Float64(Float64(a * -2.0) / (b ^ 5.0)) + Float64(-1.0 / Float64(c * (b ^ 3.0)))))) - Float64(c / b)) end
function tmp = code(a, b, c) tmp = (a * ((c ^ 3.0) * (((a * -2.0) / (b ^ 5.0)) + (-1.0 / (c * (b ^ 3.0)))))) - (c / b); end
code[a_, b_, c_] := N[(N[(a * N[(N[Power[c, 3.0], $MachinePrecision] * N[(N[(N[(a * -2.0), $MachinePrecision] / N[Power[b, 5.0], $MachinePrecision]), $MachinePrecision] + N[(-1.0 / N[(c * N[Power[b, 3.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(c / b), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
a \cdot \left({c}^{3} \cdot \left(\frac{a \cdot -2}{{b}^{5}} + \frac{-1}{c \cdot {b}^{3}}\right)\right) - \frac{c}{b}
\end{array}
Initial program 31.9%
*-commutative31.9%
+-commutative31.9%
sqr-neg31.9%
unsub-neg31.9%
sqr-neg31.9%
fma-neg32.0%
distribute-lft-neg-in32.0%
*-commutative32.0%
*-commutative32.0%
distribute-rgt-neg-in32.0%
metadata-eval32.0%
Simplified32.0%
Taylor expanded in a around 0 92.9%
Taylor expanded in c around inf 92.9%
associate-*r/92.9%
*-commutative92.9%
*-commutative92.9%
Simplified92.9%
Final simplification92.9%
(FPCore (a b c) :precision binary64 (* c (+ (* c (- (* -2.0 (/ (* c (pow a 2.0)) (pow b 5.0))) (/ a (pow b 3.0)))) (/ -1.0 b))))
double code(double a, double b, double c) {
return c * ((c * ((-2.0 * ((c * pow(a, 2.0)) / pow(b, 5.0))) - (a / pow(b, 3.0)))) + (-1.0 / b));
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = c * ((c * (((-2.0d0) * ((c * (a ** 2.0d0)) / (b ** 5.0d0))) - (a / (b ** 3.0d0)))) + ((-1.0d0) / b))
end function
public static double code(double a, double b, double c) {
return c * ((c * ((-2.0 * ((c * Math.pow(a, 2.0)) / Math.pow(b, 5.0))) - (a / Math.pow(b, 3.0)))) + (-1.0 / b));
}
def code(a, b, c): return c * ((c * ((-2.0 * ((c * math.pow(a, 2.0)) / math.pow(b, 5.0))) - (a / math.pow(b, 3.0)))) + (-1.0 / b))
function code(a, b, c) return Float64(c * Float64(Float64(c * Float64(Float64(-2.0 * Float64(Float64(c * (a ^ 2.0)) / (b ^ 5.0))) - Float64(a / (b ^ 3.0)))) + Float64(-1.0 / b))) end
function tmp = code(a, b, c) tmp = c * ((c * ((-2.0 * ((c * (a ^ 2.0)) / (b ^ 5.0))) - (a / (b ^ 3.0)))) + (-1.0 / b)); end
code[a_, b_, c_] := N[(c * N[(N[(c * N[(N[(-2.0 * N[(N[(c * N[Power[a, 2.0], $MachinePrecision]), $MachinePrecision] / N[Power[b, 5.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(a / N[Power[b, 3.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(-1.0 / b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
c \cdot \left(c \cdot \left(-2 \cdot \frac{c \cdot {a}^{2}}{{b}^{5}} - \frac{a}{{b}^{3}}\right) + \frac{-1}{b}\right)
\end{array}
Initial program 31.9%
*-commutative31.9%
+-commutative31.9%
sqr-neg31.9%
unsub-neg31.9%
sqr-neg31.9%
fma-neg32.0%
distribute-lft-neg-in32.0%
*-commutative32.0%
*-commutative32.0%
distribute-rgt-neg-in32.0%
metadata-eval32.0%
Simplified32.0%
Taylor expanded in c around 0 92.7%
Final simplification92.7%
(FPCore (a b c) :precision binary64 (- (* (/ (pow c 2.0) (pow b 3.0)) (- a)) (/ c b)))
double code(double a, double b, double c) {
return ((pow(c, 2.0) / pow(b, 3.0)) * -a) - (c / b);
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = (((c ** 2.0d0) / (b ** 3.0d0)) * -a) - (c / b)
end function
public static double code(double a, double b, double c) {
return ((Math.pow(c, 2.0) / Math.pow(b, 3.0)) * -a) - (c / b);
}
def code(a, b, c): return ((math.pow(c, 2.0) / math.pow(b, 3.0)) * -a) - (c / b)
function code(a, b, c) return Float64(Float64(Float64((c ^ 2.0) / (b ^ 3.0)) * Float64(-a)) - Float64(c / b)) end
function tmp = code(a, b, c) tmp = (((c ^ 2.0) / (b ^ 3.0)) * -a) - (c / b); end
code[a_, b_, c_] := N[(N[(N[(N[Power[c, 2.0], $MachinePrecision] / N[Power[b, 3.0], $MachinePrecision]), $MachinePrecision] * (-a)), $MachinePrecision] - N[(c / b), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
\frac{{c}^{2}}{{b}^{3}} \cdot \left(-a\right) - \frac{c}{b}
\end{array}
Initial program 31.9%
*-commutative31.9%
+-commutative31.9%
sqr-neg31.9%
unsub-neg31.9%
sqr-neg31.9%
fma-neg32.0%
distribute-lft-neg-in32.0%
*-commutative32.0%
*-commutative32.0%
distribute-rgt-neg-in32.0%
metadata-eval32.0%
Simplified32.0%
Taylor expanded in a around 0 89.5%
mul-1-neg89.5%
unsub-neg89.5%
mul-1-neg89.5%
distribute-neg-frac289.5%
associate-/l*89.5%
Simplified89.5%
Final simplification89.5%
(FPCore (a b c) :precision binary64 (/ (fma a (pow (/ c b) 2.0) c) (- b)))
double code(double a, double b, double c) {
return fma(a, pow((c / b), 2.0), c) / -b;
}
function code(a, b, c) return Float64(fma(a, (Float64(c / b) ^ 2.0), c) / Float64(-b)) end
code[a_, b_, c_] := N[(N[(a * N[Power[N[(c / b), $MachinePrecision], 2.0], $MachinePrecision] + c), $MachinePrecision] / (-b)), $MachinePrecision]
\begin{array}{l}
\\
\frac{\mathsf{fma}\left(a, {\left(\frac{c}{b}\right)}^{2}, c\right)}{-b}
\end{array}
Initial program 31.9%
*-commutative31.9%
+-commutative31.9%
sqr-neg31.9%
unsub-neg31.9%
sqr-neg31.9%
fma-neg32.0%
distribute-lft-neg-in32.0%
*-commutative32.0%
*-commutative32.0%
distribute-rgt-neg-in32.0%
metadata-eval32.0%
Simplified32.0%
Taylor expanded in c around 0 89.3%
associate-*r/89.3%
neg-mul-189.3%
distribute-rgt-neg-in89.3%
Simplified89.3%
Taylor expanded in b around inf 89.5%
distribute-lft-out89.5%
associate-*r/89.5%
mul-1-neg89.5%
distribute-neg-frac289.5%
+-commutative89.5%
associate-/l*89.5%
fma-define89.5%
unpow289.5%
unpow289.5%
times-frac89.5%
unpow289.5%
Simplified89.5%
(FPCore (a b c) :precision binary64 (* c (+ (* c (/ a (pow (- b) 3.0))) (/ -1.0 b))))
double code(double a, double b, double c) {
return c * ((c * (a / pow(-b, 3.0))) + (-1.0 / b));
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = c * ((c * (a / (-b ** 3.0d0))) + ((-1.0d0) / b))
end function
public static double code(double a, double b, double c) {
return c * ((c * (a / Math.pow(-b, 3.0))) + (-1.0 / b));
}
def code(a, b, c): return c * ((c * (a / math.pow(-b, 3.0))) + (-1.0 / b))
function code(a, b, c) return Float64(c * Float64(Float64(c * Float64(a / (Float64(-b) ^ 3.0))) + Float64(-1.0 / b))) end
function tmp = code(a, b, c) tmp = c * ((c * (a / (-b ^ 3.0))) + (-1.0 / b)); end
code[a_, b_, c_] := N[(c * N[(N[(c * N[(a / N[Power[(-b), 3.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(-1.0 / b), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
c \cdot \left(c \cdot \frac{a}{{\left(-b\right)}^{3}} + \frac{-1}{b}\right)
\end{array}
Initial program 31.9%
*-commutative31.9%
+-commutative31.9%
sqr-neg31.9%
unsub-neg31.9%
sqr-neg31.9%
fma-neg32.0%
distribute-lft-neg-in32.0%
*-commutative32.0%
*-commutative32.0%
distribute-rgt-neg-in32.0%
metadata-eval32.0%
Simplified32.0%
Taylor expanded in c around 0 89.3%
associate-*r/89.3%
neg-mul-189.3%
distribute-rgt-neg-in89.3%
Simplified89.3%
expm1-log1p-u61.1%
expm1-undefine59.9%
Applied egg-rr59.9%
sub-neg59.9%
metadata-eval59.9%
+-commutative59.9%
log1p-undefine59.9%
rem-exp-log88.1%
distribute-rgt-neg-in88.1%
unsub-neg88.1%
Simplified88.1%
Taylor expanded in a around 0 89.3%
associate-*l/89.3%
associate-*l*89.3%
*-commutative89.3%
mul-1-neg89.3%
distribute-neg-frac289.3%
cube-neg89.3%
Simplified89.3%
Final simplification89.3%
(FPCore (a b c) :precision binary64 (* c (- (/ -1.0 b) (/ (* c a) (pow b 3.0)))))
double code(double a, double b, double c) {
return c * ((-1.0 / b) - ((c * a) / pow(b, 3.0)));
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = c * (((-1.0d0) / b) - ((c * a) / (b ** 3.0d0)))
end function
public static double code(double a, double b, double c) {
return c * ((-1.0 / b) - ((c * a) / Math.pow(b, 3.0)));
}
def code(a, b, c): return c * ((-1.0 / b) - ((c * a) / math.pow(b, 3.0)))
function code(a, b, c) return Float64(c * Float64(Float64(-1.0 / b) - Float64(Float64(c * a) / (b ^ 3.0)))) end
function tmp = code(a, b, c) tmp = c * ((-1.0 / b) - ((c * a) / (b ^ 3.0))); end
code[a_, b_, c_] := N[(c * N[(N[(-1.0 / b), $MachinePrecision] - N[(N[(c * a), $MachinePrecision] / N[Power[b, 3.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
c \cdot \left(\frac{-1}{b} - \frac{c \cdot a}{{b}^{3}}\right)
\end{array}
Initial program 31.9%
*-commutative31.9%
+-commutative31.9%
sqr-neg31.9%
unsub-neg31.9%
sqr-neg31.9%
fma-neg32.0%
distribute-lft-neg-in32.0%
*-commutative32.0%
*-commutative32.0%
distribute-rgt-neg-in32.0%
metadata-eval32.0%
Simplified32.0%
Taylor expanded in c around 0 89.3%
associate-*r/89.3%
neg-mul-189.3%
distribute-rgt-neg-in89.3%
Simplified89.3%
expm1-log1p-u87.3%
expm1-undefine83.7%
associate-/l*83.7%
Applied egg-rr83.7%
sub-neg83.7%
metadata-eval83.7%
+-commutative83.7%
log1p-undefine83.7%
rem-exp-log85.8%
distribute-frac-neg85.8%
distribute-rgt-neg-in85.8%
associate-/l*85.8%
unsub-neg85.8%
associate-/l*85.8%
Simplified85.8%
Taylor expanded in c around 0 89.3%
sub-neg89.3%
neg-mul-189.3%
distribute-neg-frac89.3%
metadata-eval89.3%
+-commutative89.3%
unsub-neg89.3%
*-commutative89.3%
Simplified89.3%
(FPCore (a b c) :precision binary64 (/ c (- b)))
double code(double a, double b, double c) {
return c / -b;
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = c / -b
end function
public static double code(double a, double b, double c) {
return c / -b;
}
def code(a, b, c): return c / -b
function code(a, b, c) return Float64(c / Float64(-b)) end
function tmp = code(a, b, c) tmp = c / -b; end
code[a_, b_, c_] := N[(c / (-b)), $MachinePrecision]
\begin{array}{l}
\\
\frac{c}{-b}
\end{array}
Initial program 31.9%
*-commutative31.9%
+-commutative31.9%
sqr-neg31.9%
unsub-neg31.9%
sqr-neg31.9%
fma-neg32.0%
distribute-lft-neg-in32.0%
*-commutative32.0%
*-commutative32.0%
distribute-rgt-neg-in32.0%
metadata-eval32.0%
Simplified32.0%
Taylor expanded in b around inf 80.4%
associate-*r/80.4%
mul-1-neg80.4%
Simplified80.4%
Final simplification80.4%
(FPCore (a b c) :precision binary64 0.0)
double code(double a, double b, double c) {
return 0.0;
}
real(8) function code(a, b, c)
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8), intent (in) :: c
code = 0.0d0
end function
public static double code(double a, double b, double c) {
return 0.0;
}
def code(a, b, c): return 0.0
function code(a, b, c) return 0.0 end
function tmp = code(a, b, c) tmp = 0.0; end
code[a_, b_, c_] := 0.0
\begin{array}{l}
\\
0
\end{array}
Initial program 31.9%
*-commutative31.9%
+-commutative31.9%
sqr-neg31.9%
unsub-neg31.9%
sqr-neg31.9%
fma-neg32.0%
distribute-lft-neg-in32.0%
*-commutative32.0%
*-commutative32.0%
distribute-rgt-neg-in32.0%
metadata-eval32.0%
Simplified32.0%
Taylor expanded in c around 0 89.3%
associate-*r/89.3%
neg-mul-189.3%
distribute-rgt-neg-in89.3%
Simplified89.3%
Taylor expanded in a around 0 80.3%
expm1-log1p-u71.1%
expm1-undefine29.8%
associate-*r/29.8%
Applied egg-rr29.8%
sub-neg29.8%
log1p-undefine29.8%
*-commutative29.8%
neg-mul-129.8%
distribute-neg-frac29.8%
rem-exp-log39.0%
unsub-neg39.0%
metadata-eval39.0%
Simplified39.0%
Taylor expanded in c around 0 3.2%
Final simplification3.2%
herbie shell --seed 2024148
(FPCore (a b c)
:name "Quadratic roots, 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) (* (* 4.0 a) c)))) (* 2.0 a)))