(FPCore (c0 w h D d M)
:precision binary64
(*
(/ c0 (* 2.0 w))
(+
(/ (* c0 (* d d)) (* (* w h) (* D D)))
(sqrt
(-
(*
(/ (* c0 (* d d)) (* (* w h) (* D D)))
(/ (* c0 (* d d)) (* (* w h) (* D D))))
(* M M))))))
↓
(FPCore (c0 w h D d M)
:precision binary64
(let* ((t_0 (/ (* c0 (* d d)) (* (* w h) (* D D)))))
(if (<= (* (/ c0 (* 2.0 w)) (+ t_0 (sqrt (- (* t_0 t_0) (* M M))))) 1e+240)
(* (/ (/ c0 2.0) w) (* 2.0 (* (/ (/ d D) (* w h)) (* c0 (/ d D)))))
(* 0.25 (/ (* D M) (* d (/ (/ (/ d h) M) D)))))))
if (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))) < 1.00000000000000001e240
if 1.00000000000000001e240 < (*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M)))))
(*.f64 1/4 (*.f64 (/.f64 (*.f64 D D) d) (/.f64 (*.f64 M (*.f64 M h)) d))): 0 points increase in error, 0 points decrease in error
(*.f64 1/4 (*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) d) (/.f64 (*.f64 M (*.f64 M h)) d))): 0 points increase in error, 0 points decrease in error
(*.f64 1/4 (*.f64 (/.f64 (pow.f64 D 2) d) (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 M M) h)) d))): 17 points increase in error, 2 points decrease in error
(*.f64 1/4 (*.f64 (/.f64 (pow.f64 D 2) d) (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 M 2)) h) d))): 0 points increase in error, 0 points decrease in error
(*.f64 1/4 (*.f64 (/.f64 (pow.f64 D 2) d) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 h (pow.f64 M 2))) d))): 0 points increase in error, 0 points decrease in error
(*.f64 1/4 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 d d)))): 29 points increase in error, 6 points decrease in error
(*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (Rewrite=> *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 d d))): 0 points increase in error, 0 points decrease in error
(*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (Rewrite<= unpow2_binary64 (pow.f64 d 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-lft-identity_binary64 (+.f64 0 (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= metadata-eval (*.f64 -1/2 0)) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/2 (Rewrite<= div0_binary64 (/.f64 0 (/.f64 w (pow.f64 c0 2))))) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)))): 44 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/2 (/.f64 (Rewrite<= mul0-lft_binary64 (*.f64 0 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (/.f64 w (pow.f64 c0 2)))) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)))): 87 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/2 (/.f64 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))) (/.f64 w (pow.f64 c0 2)))) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/2 (/.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))))) (/.f64 w (pow.f64 c0 2)))) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w))) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)))): 0 points increase in error, 1 points decrease in error
herbie shell --seed 2022308
(FPCore (c0 w h D d M)
:name "Henrywood and Agarwal, Equation (13)"
:precision binary64
(* (/ c0 (* 2.0 w)) (+ (/ (* c0 (* d d)) (* (* w h) (* D D))) (sqrt (- (* (/ (* c0 (* d d)) (* (* w h) (* D D))) (/ (* c0 (* d d)) (* (* w h) (* D D)))) (* M M))))))