Quadratic roots, wide range

Average Accuracy: 17.8% → 99.4%

Time: 11.6s

Precision: binary64

Cost: 14016

\[\left(\left(4.930380657631324 \cdot 10^{-32} < a \land a < 2.028240960365167 \cdot 10^{+31}\right) \land \left(4.930380657631324 \cdot 10^{-32} < b \land b < 2.028240960365167 \cdot 10^{+31}\right)\right) \land \left(4.930380657631324 \cdot 10^{-32} < c \land c < 2.028240960365167 \cdot 10^{+31}\right)\]

Math

\[\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

↓

\[\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(-4, \mathsf{*.f64}\left(c, a\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(c, \mathsf{*.f64}\left(-4, a\right), \mathsf{*.f64}\left(b, b\right)\right)\right)\right)\right), \mathsf{*.f64}\left(a, 2\right)\right) \]

FPCore

(FPCore (a b c)
 :precision binary64
 (/.f64
  (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))
  (*.f64 2 a)))

↓

(FPCore (a b c)
 :precision binary64
 (/.f64
  (/.f64
   (*.f64 -4 (*.f64 c a))
   (+.f64 b (sqrt.f64 (fma.f64 c (*.f64 -4 a) (*.f64 b b)))))
  (*.f64 a 2)))

Derivation

1. Initial program 17.8%

   \[\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

2. Applied egg-rr 17.8%

   \[\leadsto \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)}\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   Proof

   [Start] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   sub-neg [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)}\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   flip-+ [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)}\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   pow2 [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{pow.f64}\left(b, 2\right)}, \mathsf{*.f64}\left(b, b\right)\right), \mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   pow2 [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(b, 2\right), \color{blue}{\mathsf{pow.f64}\left(b, 2\right)}\right), \mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   pow-prod-up [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{pow.f64}\left(b, \mathsf{+.f64}\left(2, 2\right)\right)}, \mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   metadata-eval [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, \color{blue}{4}\right), \mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   *-commutative [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(4, a\right)\right)}\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   distribute-rgt-neg-in [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(c, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(4, a\right)\right)\right)}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   *-commutative [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(a, 4\right)}\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   distribute-rgt-neg-in [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \color{blue}{\mathsf{*.f64}\left(a, \mathsf{neg.f64}\left(4\right)\right)}\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   metadata-eval [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, \color{blue}{-4}\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   *-commutative [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(4, a\right)\right)}\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   distribute-rgt-neg-in [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \color{blue}{\mathsf{*.f64}\left(c, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(4, a\right)\right)\right)}\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   *-commutative [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(c, \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(a, 4\right)}\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   distribute-rgt-neg-in [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(c, \color{blue}{\mathsf{*.f64}\left(a, \mathsf{neg.f64}\left(4\right)\right)}\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   metadata-eval [=>] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, \color{blue}{-4}\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(4, a\right), c\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

3. Applied egg-rr 18.2%

   \[\leadsto \mathsf{/.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right)\right)}, \mathsf{*.f64}\left(2, a\right)\right) \]
   Proof

   [Start] 17.8	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   +-commutative [=>] 17.8	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right), \mathsf{neg.f64}\left(b\right)\right)}, \mathsf{*.f64}\left(2, a\right)\right) \]
   flip-+ [=>] 17.7	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{neg.f64}\left(b\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right), \mathsf{neg.f64}\left(b\right)\right)\right)}, \mathsf{*.f64}\left(2, a\right)\right) \]

4. Simplified 18.3%

   \[\leadsto \mathsf{/.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{fma.f64}\left(c, \mathsf{*.f64}\left(a, -4\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(c, \mathsf{*.f64}\left(a, -4\right), \mathsf{*.f64}\left(b, b\right)\right)\right)\right)\right)}, \mathsf{*.f64}\left(2, a\right)\right) \]
   Proof

   [Start] 18.2	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   /-rgt-identity [<=] 18.2	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right), \mathsf{*.f64}\left(b, b\right)\right), 1\right)}, \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   /-rgt-identity [=>] 18.2	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right), \mathsf{*.f64}\left(b, b\right)\right)}, \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   fma-def [<=] 18.3	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)}, \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   +-commutative [<=] 18.3	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(b, b\right)\right)}, \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   fma-def [=>] 18.3	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{fma.f64}\left(c, \mathsf{*.f64}\left(a, -4\right), \mathsf{*.f64}\left(b, b\right)\right)}, \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   fma-def [<=] 18.3	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{fma.f64}\left(c, \mathsf{*.f64}\left(a, -4\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right)}\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   +-commutative [<=] 18.3	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{fma.f64}\left(c, \mathsf{*.f64}\left(a, -4\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right), \mathsf{*.f64}\left(b, b\right)\right)}\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
   fma-def [=>] 18.3	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{fma.f64}\left(c, \mathsf{*.f64}\left(a, -4\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{fma.f64}\left(c, \mathsf{*.f64}\left(a, -4\right), \mathsf{*.f64}\left(b, b\right)\right)}\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

5. Taylor expanded in c around 0 99.4%

   \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(-4, \mathsf{*.f64}\left(c, a\right)\right)}, \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(c, \mathsf{*.f64}\left(a, -4\right), \mathsf{*.f64}\left(b, b\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

6. Final simplification 99.4%

   \[\leadsto \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(-4, \mathsf{*.f64}\left(c, a\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(c, \mathsf{*.f64}\left(-4, a\right), \mathsf{*.f64}\left(b, b\right)\right)\right)\right)\right), \mathsf{*.f64}\left(a, 2\right)\right) \]

Alternatives

Alternative 1
Accuracy	99.4%
Cost	7744

\[\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(-4, \mathsf{*.f64}\left(c, a\right)\right), \mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(-4, a\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(a, 2\right)\right) \]

Alternative 2
Accuracy	95.2%
Cost	7232

\[\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{neg.f64}\left(c\right), b\right), \mathsf{*.f64}\left(a, \mathsf{/.f64}\left(c, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), c\right)\right)\right)\right) \]

Alternative 3
Accuracy	95.1%
Cost	576

\[\mathsf{/.f64}\left(1, \mathsf{\_.f64}\left(\mathsf{/.f64}\left(a, b\right), \mathsf{/.f64}\left(b, c\right)\right)\right) \]

Alternative 4
Accuracy	90.4%
Cost	256

\[\mathsf{/.f64}\left(\mathsf{neg.f64}\left(c\right), b\right) \]

Alternative 5
Accuracy	1.7%
Cost	192

\[\mathsf{/.f64}\left(c, b\right) \]

Reproduce

herbie shell --seed 2023144 
(FPCore (a b c)
  :name "Quadratic roots, wide range"
  :precision binary64
  :pre (and (and (and (< 4.930380657631324e-32 a) (< a 2.028240960365167e+31)) (and (< 4.930380657631324e-32 b) (< b 2.028240960365167e+31))) (and (< 4.930380657631324e-32 c) (< c 2.028240960365167e+31)))
  (/ (+ (- b) (sqrt (- (* b b) (* (* 4.0 a) c)))) (* 2.0 a)))