\[\begin{array}{l}
t_1 := x \cdot \left(y \cdot \frac{0.5}{a}\right)\\
t_2 := x \cdot y + t \cdot \left(z \cdot -9\right)\\
\mathbf{if}\;t_2 \leq -2 \cdot 10^{+215}:\\
\;\;\;\;t_1 - \frac{z}{a \cdot \frac{0.2222222222222222}{t}}\\
\mathbf{elif}\;t_2 \leq 10^{+183}:\\
\;\;\;\;\frac{x \cdot y + z \cdot \left(t \cdot -9\right)}{a \cdot 2}\\
\mathbf{else}:\\
\;\;\;\;t_1 + \frac{z}{a} \cdot \frac{-9}{\frac{2}{t}}\\
\end{array}
\]
(FPCore (x y z t a)
:precision binary64
(/ (- (* x y) (* (* z 9.0) t)) (* a 2.0)))
↓
(FPCore (x y z t a)
:precision binary64
(let* ((t_1 (* x (* y (/ 0.5 a)))) (t_2 (+ (* x y) (* t (* z -9.0)))))
(if (<= t_2 -2e+215)
(- t_1 (/ z (* a (/ 0.2222222222222222 t))))
(if (<= t_2 1e+183)
(/ (+ (* x y) (* z (* t -9.0))) (* a 2.0))
(+ t_1 (* (/ z a) (/ -9.0 (/ 2.0 t))))))))
double code(double x, double y, double z, double t, double a) {
return ((x * y) - ((z * 9.0) * t)) / (a * 2.0);
}
↓
double code(double x, double y, double z, double t, double a) {
double t_1 = x * (y * (0.5 / a));
double t_2 = (x * y) + (t * (z * -9.0));
double tmp;
if (t_2 <= -2e+215) {
tmp = t_1 - (z / (a * (0.2222222222222222 / t)));
} else if (t_2 <= 1e+183) {
tmp = ((x * y) + (z * (t * -9.0))) / (a * 2.0);
} else {
tmp = t_1 + ((z / a) * (-9.0 / (2.0 / t)));
}
return tmp;
}
real(8) function code(x, y, z, t, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: t
real(8), intent (in) :: a
code = ((x * y) - ((z * 9.0d0) * t)) / (a * 2.0d0)
end function
↓
real(8) function code(x, y, z, t, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: t
real(8), intent (in) :: a
real(8) :: t_1
real(8) :: t_2
real(8) :: tmp
t_1 = x * (y * (0.5d0 / a))
t_2 = (x * y) + (t * (z * (-9.0d0)))
if (t_2 <= (-2d+215)) then
tmp = t_1 - (z / (a * (0.2222222222222222d0 / t)))
else if (t_2 <= 1d+183) then
tmp = ((x * y) + (z * (t * (-9.0d0)))) / (a * 2.0d0)
else
tmp = t_1 + ((z / a) * ((-9.0d0) / (2.0d0 / t)))
end if
code = tmp
end function
public static double code(double x, double y, double z, double t, double a) {
return ((x * y) - ((z * 9.0) * t)) / (a * 2.0);
}
↓
public static double code(double x, double y, double z, double t, double a) {
double t_1 = x * (y * (0.5 / a));
double t_2 = (x * y) + (t * (z * -9.0));
double tmp;
if (t_2 <= -2e+215) {
tmp = t_1 - (z / (a * (0.2222222222222222 / t)));
} else if (t_2 <= 1e+183) {
tmp = ((x * y) + (z * (t * -9.0))) / (a * 2.0);
} else {
tmp = t_1 + ((z / a) * (-9.0 / (2.0 / t)));
}
return tmp;
}
def code(x, y, z, t, a):
return ((x * y) - ((z * 9.0) * t)) / (a * 2.0)
↓
def code(x, y, z, t, a):
t_1 = x * (y * (0.5 / a))
t_2 = (x * y) + (t * (z * -9.0))
tmp = 0
if t_2 <= -2e+215:
tmp = t_1 - (z / (a * (0.2222222222222222 / t)))
elif t_2 <= 1e+183:
tmp = ((x * y) + (z * (t * -9.0))) / (a * 2.0)
else:
tmp = t_1 + ((z / a) * (-9.0 / (2.0 / t)))
return tmp
function code(x, y, z, t, a)
return Float64(Float64(Float64(x * y) - Float64(Float64(z * 9.0) * t)) / Float64(a * 2.0))
end
(-.f64 (*.f64 x (*.f64 y (/.f64 1/2 a))) (/.f64 (*.f64 (*.f64 z 9) (/.f64 t 2)) a)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 x y) (/.f64 1/2 a))) (/.f64 (*.f64 (*.f64 z 9) (/.f64 t 2)) a)): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (*.f64 x y) (/.f64 1/2 a)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (*.f64 z 9) a) (/.f64 t 2)))): 4 points increase in error, 0 points decrease in error
(Rewrite=> sub-neg_binary64 (+.f64 (*.f64 (*.f64 x y) (/.f64 1/2 a)) (neg.f64 (*.f64 (/.f64 (*.f64 z 9) a) (/.f64 t 2))))): 0 points increase in error, 4 points decrease in error
(-.f64 (*.f64 x (*.f64 y (/.f64 1/2 a))) (/.f64 z (*.f64 a (/.f64 2/9 t)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 x (*.f64 y (/.f64 1/2 a))) (/.f64 z (*.f64 a (/.f64 (Rewrite<= metadata-eval (/.f64 1 9/2)) t)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 x (*.f64 y (/.f64 1/2 a))) (/.f64 z (*.f64 a (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 9/2 t)))))): 8 points increase in error, 0 points decrease in error
(-.f64 (*.f64 x (*.f64 y (/.f64 1/2 a))) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 z (/.f64 1 (*.f64 9/2 t))) a))): 0 points increase in error, 8 points decrease in error
(-.f64 (*.f64 x (*.f64 y (/.f64 1/2 a))) (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 z (*.f64 9/2 t)) 1)) a)): 9 points increase in error, 0 points decrease in error
(-.f64 (*.f64 x (*.f64 y (/.f64 1/2 a))) (/.f64 (Rewrite=> /-rgt-identity_binary64 (*.f64 z (*.f64 9/2 t))) a)): 0 points increase in error, 3 points decrease in error
(-.f64 (*.f64 x (*.f64 y (/.f64 1/2 a))) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 9/2 t) z)) a)): 0 points increase in error, 3 points decrease in error
(-.f64 (*.f64 x (*.f64 y (/.f64 1/2 a))) (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 9/2 (*.f64 t z))) a)): 0 points increase in error, 3 points decrease in error
(-.f64 (*.f64 x (*.f64 y (/.f64 1/2 a))) (Rewrite<= associate-*r/_binary64 (*.f64 9/2 (/.f64 (*.f64 t z) a)))): 9 points increase in error, 0 points decrease in error
if -1.99999999999999981e215 < (-.f64 (*.f64 x y) (*.f64 (*.f64 z 9) t)) < 9.99999999999999947e182
\[\leadsto \color{blue}{\frac{x \cdot y - z \cdot \left(9 \cdot t\right)}{a \cdot 2}}
\]
Proof
(/.f64 (-.f64 (*.f64 x y) (*.f64 z (*.f64 9 t))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (*.f64 x y) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z 9) t))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
if 9.99999999999999947e182 < (-.f64 (*.f64 x y) (*.f64 (*.f64 z 9) t))
\[\leadsto \color{blue}{\frac{x \cdot y - z \cdot \left(9 \cdot t\right)}{a \cdot 2}}
\]
Proof
(/.f64 (-.f64 (*.f64 x y) (*.f64 z (*.f64 9 t))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (*.f64 x y) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z 9) t))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
herbie shell --seed 2022340
(FPCore (x y z t a)
:name "Diagrams.Solve.Polynomial:cubForm from diagrams-solve-0.1, I"
:precision binary64
:herbie-target
(if (< a -2.090464557976709e+86) (- (* 0.5 (/ (* y x) a)) (* 4.5 (/ t (/ a z)))) (if (< a 2.144030707833976e+99) (/ (- (* x y) (* z (* 9.0 t))) (* a 2.0)) (- (* (/ y a) (* x 0.5)) (* (/ t a) (* z 4.5)))))
(/ (- (* x y) (* (* z 9.0) t)) (* a 2.0)))