quad2p (problem 3.2.1, positive)

Average Error: 34.1 → 20.6

Time: 22.0s

Precision: binary64

Cost: 48464

Math

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

↓

\[\begin{array}{l} t_0 := \frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}\\ t_1 := c \cdot \left(-a\right)\\ \mathbf{if}\;t_0 \leq -\infty:\\ \;\;\;\;\frac{\mathsf{hypot}\left(\sqrt{-a} \cdot \sqrt{c}, b_2\right) - b_2}{a}\\ \mathbf{elif}\;t_0 \leq -2 \cdot 10^{-251}:\\ \;\;\;\;\frac{\sqrt{\mathsf{fma}\left(b_2, b_2, t_1\right)}}{a} - \frac{b_2}{a}\\ \mathbf{elif}\;t_0 \leq 0:\\ \;\;\;\;\frac{\frac{t_1}{b_2 + \mathsf{hypot}\left(b_2, \sqrt{t_1}\right)}}{a}\\ \mathbf{elif}\;t_0 \leq 5 \cdot 10^{+254}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{hypot}\left(\sqrt{a} \cdot \sqrt{-c}, b_2\right) - b_2}{a}\\ \end{array} \]

FPCore

(FPCore (a b_2 c)
 :precision binary64
 (/ (+ (- b_2) (sqrt (- (* b_2 b_2) (* a c)))) a))

↓

(FPCore (a b_2 c)
 :precision binary64
 (let* ((t_0 (/ (- (sqrt (- (* b_2 b_2) (* a c))) b_2) a)) (t_1 (* c (- a))))
   (if (<= t_0 (- INFINITY))
     (/ (- (hypot (* (sqrt (- a)) (sqrt c)) b_2) b_2) a)
     (if (<= t_0 -2e-251)
       (- (/ (sqrt (fma b_2 b_2 t_1)) a) (/ b_2 a))
       (if (<= t_0 0.0)
         (/ (/ t_1 (+ b_2 (hypot b_2 (sqrt t_1)))) a)
         (if (<= t_0 5e+254)
           t_0
           (/ (- (hypot (* (sqrt a) (sqrt (- c))) b_2) b_2) a)))))))

C

double code(double a, double b_2, double c) {
	return (-b_2 + sqrt(((b_2 * b_2) - (a * c)))) / a;
}

↓

double code(double a, double b_2, double c) {
	double t_0 = (sqrt(((b_2 * b_2) - (a * c))) - b_2) / a;
	double t_1 = c * -a;
	double tmp;
	if (t_0 <= -((double) INFINITY)) {
		tmp = (hypot((sqrt(-a) * sqrt(c)), b_2) - b_2) / a;
	} else if (t_0 <= -2e-251) {
		tmp = (sqrt(fma(b_2, b_2, t_1)) / a) - (b_2 / a);
	} else if (t_0 <= 0.0) {
		tmp = (t_1 / (b_2 + hypot(b_2, sqrt(t_1)))) / a;
	} else if (t_0 <= 5e+254) {
		tmp = t_0;
	} else {
		tmp = (hypot((sqrt(a) * sqrt(-c)), b_2) - b_2) / a;
	}
	return tmp;
}

Julia

function code(a, b_2, c)
	return Float64(Float64(Float64(-b_2) + sqrt(Float64(Float64(b_2 * b_2) - Float64(a * c)))) / a)
end

↓

function code(a, b_2, c)
	t_0 = Float64(Float64(sqrt(Float64(Float64(b_2 * b_2) - Float64(a * c))) - b_2) / a)
	t_1 = Float64(c * Float64(-a))
	tmp = 0.0
	if (t_0 <= Float64(-Inf))
		tmp = Float64(Float64(hypot(Float64(sqrt(Float64(-a)) * sqrt(c)), b_2) - b_2) / a);
	elseif (t_0 <= -2e-251)
		tmp = Float64(Float64(sqrt(fma(b_2, b_2, t_1)) / a) - Float64(b_2 / a));
	elseif (t_0 <= 0.0)
		tmp = Float64(Float64(t_1 / Float64(b_2 + hypot(b_2, sqrt(t_1)))) / a);
	elseif (t_0 <= 5e+254)
		tmp = t_0;
	else
		tmp = Float64(Float64(hypot(Float64(sqrt(a) * sqrt(Float64(-c))), b_2) - b_2) / a);
	end
	return tmp
end

Wolfram

code[a_, b$95$2_, c_] := N[(N[((-b$95$2) + N[Sqrt[N[(N[(b$95$2 * b$95$2), $MachinePrecision] - N[(a * c), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] / a), $MachinePrecision]

↓

code[a_, b$95$2_, c_] := Block[{t$95$0 = N[(N[(N[Sqrt[N[(N[(b$95$2 * b$95$2), $MachinePrecision] - N[(a * c), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] - b$95$2), $MachinePrecision] / a), $MachinePrecision]}, Block[{t$95$1 = N[(c * (-a)), $MachinePrecision]}, If[LessEqual[t$95$0, (-Infinity)], N[(N[(N[Sqrt[N[(N[Sqrt[(-a)], $MachinePrecision] * N[Sqrt[c], $MachinePrecision]), $MachinePrecision] ^ 2 + b$95$2 ^ 2], $MachinePrecision] - b$95$2), $MachinePrecision] / a), $MachinePrecision], If[LessEqual[t$95$0, -2e-251], N[(N[(N[Sqrt[N[(b$95$2 * b$95$2 + t$95$1), $MachinePrecision]], $MachinePrecision] / a), $MachinePrecision] - N[(b$95$2 / a), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$0, 0.0], N[(N[(t$95$1 / N[(b$95$2 + N[Sqrt[b$95$2 ^ 2 + N[Sqrt[t$95$1], $MachinePrecision] ^ 2], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / a), $MachinePrecision], If[LessEqual[t$95$0, 5e+254], t$95$0, N[(N[(N[Sqrt[N[(N[Sqrt[a], $MachinePrecision] * N[Sqrt[(-c)], $MachinePrecision]), $MachinePrecision] ^ 2 + b$95$2 ^ 2], $MachinePrecision] - b$95$2), $MachinePrecision] / a), $MachinePrecision]]]]]]]

Derivation

1. Split input into 5 regimes

2. if (/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) < -inf.0

   1. Initial program 64.0

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

   2. Simplified 64.0

      \[\leadsto \color{blue}{\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}} \]
      Proof
      (/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) b_2) a): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) (neg.f64 b_2))) a): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))))) a): 0 points increase in error, 0 points decrease in error

   3. Applied egg-rr 45.1

      \[\leadsto \frac{\color{blue}{\mathsf{hypot}\left(\sqrt{-a \cdot c}, b_2\right)} - b_2}{a} \]

   4. Applied egg-rr 31.3

      \[\leadsto \frac{\mathsf{hypot}\left(\color{blue}{\sqrt{-a} \cdot \sqrt{c}}, b_2\right) - b_2}{a} \]

   if -inf.0 < (/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) < -2.00000000000000003e-251

   1. Initial program 4.1

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

   2. Simplified 4.1

      \[\leadsto \color{blue}{\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}} \]
      Proof
      (/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) b_2) a): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) (neg.f64 b_2))) a): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))))) a): 0 points increase in error, 0 points decrease in error

   3. Applied egg-rr 63.8

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{{\left(b_2 \cdot b_2 - a \cdot c\right)}^{0.25}}{\sqrt{a}}, \frac{{\left(b_2 \cdot b_2 - a \cdot c\right)}^{0.25}}{\sqrt{a}}, -\frac{b_2}{a}\right)} \]

   4. Simplified 63.8

      \[\leadsto \color{blue}{\frac{{\left(b_2 \cdot b_2 - a \cdot c\right)}^{0.25}}{\sqrt{a}} \cdot \frac{{\left(b_2 \cdot b_2 - a \cdot c\right)}^{0.25}}{\sqrt{a}} - \frac{b_2}{a}} \]
      Proof
      (-.f64 (*.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a))) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
      (Rewrite=> fma-neg_binary64 (fma.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)) (neg.f64 (/.f64 b_2 a)))): 14 points increase in error, 25 points decrease in error

   5. Applied egg-rr 4.3

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{{\left(b_2 \cdot b_2 - a \cdot c\right)}^{0.25}}{1}, \frac{{\left(b_2 \cdot b_2 - a \cdot c\right)}^{0.25}}{a}, \frac{-b_2}{a}\right)} \]

   6. Simplified 4.1

      \[\leadsto \color{blue}{\frac{\sqrt{b_2 \cdot b_2 - a \cdot c}}{a} - \frac{b_2}{a}} \]
      Proof
      (-.f64 (/.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) a) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= unpow1/2_binary64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/2)) a) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) (Rewrite<= metadata-eval (*.f64 2 1/4))) a) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4))) a) (/.f64 b_2 a)): 52 points increase in error, 9 points decrease in error
      (-.f64 (/.f64 (Rewrite<= sqr-neg_binary64 (*.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)))) a) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (/.f64 (*.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4))) (Rewrite<= rem-square-sqrt_binary64 (*.f64 (sqrt.f64 a) (sqrt.f64 a)))) (/.f64 b_2 a)): 103 points increase in error, 14 points decrease in error
      (-.f64 (/.f64 (*.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4))) (Rewrite<= sqr-neg_binary64 (*.f64 (neg.f64 (sqrt.f64 a)) (neg.f64 (sqrt.f64 a))))) (/.f64 b_2 a)): 0 points increase in error, 0 points decrease in error
      (-.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (sqrt.f64 a))) (/.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (sqrt.f64 a))))) (/.f64 b_2 a)): 28 points increase in error, 12 points decrease in error
      (Rewrite=> fma-neg_binary64 (fma.f64 (/.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (sqrt.f64 a))) (/.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (sqrt.f64 a))) (neg.f64 (/.f64 b_2 a)))): 14 points increase in error, 25 points decrease in error
      (fma.f64 (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4))) (neg.f64 (sqrt.f64 a))) (/.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (sqrt.f64 a))) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (/.f64 (*.f64 -1 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (sqrt.f64 a)))) (/.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (sqrt.f64 a))) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 -1 -1) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)))) (/.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (sqrt.f64 a))) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (*.f64 (Rewrite=> metadata-eval 1) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a))) (/.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (sqrt.f64 a))) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (Rewrite=> *-lft-identity_binary64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a))) (/.f64 (neg.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (neg.f64 (sqrt.f64 a))) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)) (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4))) (neg.f64 (sqrt.f64 a))) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)) (/.f64 (*.f64 -1 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (sqrt.f64 a)))) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)) (Rewrite=> times-frac_binary64 (*.f64 (/.f64 -1 -1) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)))) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)) (*.f64 (Rewrite=> metadata-eval 1) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a))) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)) (Rewrite=> *-lft-identity_binary64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a))) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a)) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (sqrt.f64 a))) (/.f64 b_2 a))): 25 points increase in error, 14 points decrease in error
      (-.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (*.f64 (sqrt.f64 a) (sqrt.f64 a)))) (/.f64 b_2 a)): 12 points increase in error, 28 points decrease in error
      (-.f64 (/.f64 (*.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4)) (Rewrite=> rem-square-sqrt_binary64 a)) (/.f64 b_2 a)): 14 points increase in error, 103 points decrease in error
      (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) a))) (/.f64 b_2 a)): 30 points increase in error, 17 points decrease in error
      (Rewrite=> fma-neg_binary64 (fma.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) a) (neg.f64 (/.f64 b_2 a)))): 29 points increase in error, 43 points decrease in error
      (fma.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) 1)) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) a) (neg.f64 (/.f64 b_2 a))): 0 points increase in error, 0 points decrease in error
      (fma.f64 (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) 1) (/.f64 (pow.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)) 1/4) a) (Rewrite<= distribute-frac-neg_binary64 (/.f64 (neg.f64 b_2) a))): 0 points increase in error, 0 points decrease in error

   7. Applied egg-rr 4.1

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

   if -2.00000000000000003e-251 < (/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) < -0.0

   1. Initial program 52.4

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

   2. Simplified 52.4

      \[\leadsto \color{blue}{\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}} \]
      Proof
      (/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) b_2) a): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) (neg.f64 b_2))) a): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))))) a): 0 points increase in error, 0 points decrease in error

   3. Applied egg-rr 63.2

      \[\leadsto \frac{\sqrt{\color{blue}{\log \left(e^{b_2 \cdot b_2 - a \cdot c}\right)}} - b_2}{a} \]

   4. Applied egg-rr 53.6

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

   5. Applied egg-rr 55.6

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

   6. Simplified 37.2

      \[\leadsto \frac{\color{blue}{\frac{c \cdot \left(-a\right)}{b_2 + \mathsf{hypot}\left(b_2, \sqrt{c \cdot \left(-a\right)}\right)}}}{a} \]
      Proof
      (/.f64 (*.f64 c (neg.f64 a)) (+.f64 b_2 (hypot.f64 b_2 (sqrt.f64 (*.f64 c (neg.f64 a)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (neg.f64 a) c)) (+.f64 b_2 (hypot.f64 b_2 (sqrt.f64 (*.f64 c (neg.f64 a)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 a c))) (+.f64 b_2 (hypot.f64 b_2 (sqrt.f64 (*.f64 c (neg.f64 a)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 a c))) (+.f64 b_2 (hypot.f64 b_2 (sqrt.f64 (*.f64 c (neg.f64 a)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (Rewrite<= +-inverses_binary64 (-.f64 (*.f64 b_2 b_2) (*.f64 b_2 b_2))) (*.f64 a c)) (+.f64 b_2 (hypot.f64 b_2 (sqrt.f64 (*.f64 c (neg.f64 a)))))): 17 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= associate--r+_binary64 (-.f64 (*.f64 b_2 b_2) (+.f64 (*.f64 b_2 b_2) (*.f64 a c)))) (+.f64 b_2 (hypot.f64 b_2 (sqrt.f64 (*.f64 c (neg.f64 a)))))): 9 points increase in error, 14 points decrease in error
      (/.f64 (-.f64 (*.f64 b_2 b_2) (Rewrite<= fma-udef_binary64 (fma.f64 b_2 b_2 (*.f64 a c)))) (+.f64 b_2 (hypot.f64 b_2 (sqrt.f64 (*.f64 c (neg.f64 a)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (-.f64 (*.f64 b_2 b_2) (fma.f64 b_2 b_2 (*.f64 a c))) 1)) (+.f64 b_2 (hypot.f64 b_2 (sqrt.f64 (*.f64 c (neg.f64 a)))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*r/_binary64 (*.f64 (-.f64 (*.f64 b_2 b_2) (fma.f64 b_2 b_2 (*.f64 a c))) (/.f64 1 (+.f64 b_2 (hypot.f64 b_2 (sqrt.f64 (*.f64 c (neg.f64 a)))))))): 8 points increase in error, 8 points decrease in error

   if -0.0 < (/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a) < 4.99999999999999994e254

   1. Initial program 4.7

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

   2. Simplified 4.7

      \[\leadsto \color{blue}{\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}} \]
      Proof
      (/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) b_2) a): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) (neg.f64 b_2))) a): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))))) a): 0 points increase in error, 0 points decrease in error

   if 4.99999999999999994e254 < (/.f64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c)))) a)

   1. Initial program 59.7

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

   2. Simplified 59.7

      \[\leadsto \color{blue}{\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}} \]
      Proof
      (/.f64 (-.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) b_2) a): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))) (neg.f64 b_2))) a): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b_2) (sqrt.f64 (-.f64 (*.f64 b_2 b_2) (*.f64 a c))))) a): 0 points increase in error, 0 points decrease in error

   3. Applied egg-rr 46.8

      \[\leadsto \frac{\color{blue}{\mathsf{hypot}\left(\sqrt{-a \cdot c}, b_2\right)} - b_2}{a} \]

   4. Applied egg-rr 33.9

      \[\leadsto \frac{\mathsf{hypot}\left(\color{blue}{\sqrt{a} \cdot \sqrt{-c}}, b_2\right) - b_2}{a} \]
3. Recombined 5 regimes into one program.

4. Final simplification 20.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a} \leq -\infty:\\ \;\;\;\;\frac{\mathsf{hypot}\left(\sqrt{-a} \cdot \sqrt{c}, b_2\right) - b_2}{a}\\ \mathbf{elif}\;\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a} \leq -2 \cdot 10^{-251}:\\ \;\;\;\;\frac{\sqrt{\mathsf{fma}\left(b_2, b_2, c \cdot \left(-a\right)\right)}}{a} - \frac{b_2}{a}\\ \mathbf{elif}\;\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a} \leq 0:\\ \;\;\;\;\frac{\frac{c \cdot \left(-a\right)}{b_2 + \mathsf{hypot}\left(b_2, \sqrt{c \cdot \left(-a\right)}\right)}}{a}\\ \mathbf{elif}\;\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a} \leq 5 \cdot 10^{+254}:\\ \;\;\;\;\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{hypot}\left(\sqrt{a} \cdot \sqrt{-c}, b_2\right) - b_2}{a}\\ \end{array} \]

Alternatives

Alternative 1
Error	23.0
Cost	48464

\[\begin{array}{l} t_0 := c \cdot \left(-a\right)\\ t_1 := \sqrt{t_0}\\ t_2 := \frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}\\ \mathbf{if}\;t_2 \leq -\infty:\\ \;\;\;\;\frac{\mathsf{hypot}\left(t_1, b_2\right) - b_2}{a}\\ \mathbf{elif}\;t_2 \leq -2 \cdot 10^{-251}:\\ \;\;\;\;\frac{\sqrt{\mathsf{fma}\left(b_2, b_2, t_0\right)}}{a} - \frac{b_2}{a}\\ \mathbf{elif}\;t_2 \leq 0:\\ \;\;\;\;\frac{\frac{t_0}{b_2 + \mathsf{hypot}\left(b_2, t_1\right)}}{a}\\ \mathbf{elif}\;t_2 \leq 5 \cdot 10^{+254}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{hypot}\left(\sqrt{a} \cdot \sqrt{-c}, b_2\right) - b_2}{a}\\ \end{array} \]

Alternative 2
Error	23.5
Cost	13960

\[\begin{array}{l} t_0 := c \cdot \left(-a\right)\\ t_1 := \sqrt{t_0}\\ \mathbf{if}\;b_2 \leq -3.1 \cdot 10^{+135}:\\ \;\;\;\;\frac{\mathsf{hypot}\left(t_1, b_2\right) - b_2}{a}\\ \mathbf{elif}\;b_2 \leq 1.25 \cdot 10^{-136}:\\ \;\;\;\;\frac{\sqrt{\mathsf{fma}\left(b_2, b_2, t_0\right)}}{a} - \frac{b_2}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{t_0}{b_2 + \mathsf{hypot}\left(b_2, t_1\right)}}{a}\\ \end{array} \]

Alternative 3
Error	28.4
Cost	13576

\[\begin{array}{l} t_0 := \frac{\mathsf{hypot}\left(\sqrt{a \cdot c}, b_2\right) - b_2}{a}\\ \mathbf{if}\;b_2 \leq -1.32 \cdot 10^{+154}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;b_2 \leq 1.35 \cdot 10^{+154}:\\ \;\;\;\;\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]

Alternative 4
Error	28.0
Cost	13576

\[\begin{array}{l} \mathbf{if}\;b_2 \leq -1.25 \cdot 10^{+159}:\\ \;\;\;\;\frac{\mathsf{hypot}\left(\sqrt{c \cdot \left(-a\right)}, b_2\right) - b_2}{a}\\ \mathbf{elif}\;b_2 \leq 1.35 \cdot 10^{+154}:\\ \;\;\;\;\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{hypot}\left(\sqrt{a \cdot c}, b_2\right) - b_2}{a}\\ \end{array} \]

Alternative 5
Error	34.1
Cost	7104

\[\frac{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}{a} \]

Reproduce

herbie shell --seed 2022334 
(FPCore (a b_2 c)
  :name "quad2p (problem 3.2.1, positive)"
  :precision binary64
  (/ (+ (- b_2) (sqrt (- (* b_2 b_2) (* a c)))) a))