\[\begin{array}{l}
t_1 := \frac{y}{a} \cdot \frac{x}{2} + t \cdot \left(z \cdot \frac{-4.5}{a}\right)\\
t_2 := x \cdot y + t \cdot \left(z \cdot -9\right)\\
\mathbf{if}\;t_2 \leq -2 \cdot 10^{+285}:\\
\;\;\;\;\mathsf{fma}\left(-4.5, z \cdot \frac{t}{a}, \frac{y \cdot 0.5}{\frac{a}{x}}\right)\\
\mathbf{elif}\;t_2 \leq -1 \cdot 10^{-231}:\\
\;\;\;\;\frac{t_2}{a \cdot 2}\\
\mathbf{elif}\;t_2 \leq 10^{-321}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;t_2 \leq 10^{+245}:\\
\;\;\;\;\frac{\mathsf{fma}\left(x, y, z \cdot \left(t \cdot -9\right)\right)}{a \cdot 2}\\
\mathbf{else}:\\
\;\;\;\;t_1\\
\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 (+ (* (/ y a) (/ x 2.0)) (* t (* z (/ -4.5 a)))))
(t_2 (+ (* x y) (* t (* z -9.0)))))
(if (<= t_2 -2e+285)
(fma -4.5 (* z (/ t a)) (/ (* y 0.5) (/ a x)))
(if (<= t_2 -1e-231)
(/ t_2 (* a 2.0))
(if (<= t_2 1e-321)
t_1
(if (<= t_2 1e+245) (/ (fma x y (* z (* t -9.0))) (* a 2.0)) t_1))))))
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 = ((y / a) * (x / 2.0)) + (t * (z * (-4.5 / a)));
double t_2 = (x * y) + (t * (z * -9.0));
double tmp;
if (t_2 <= -2e+285) {
tmp = fma(-4.5, (z * (t / a)), ((y * 0.5) / (a / x)));
} else if (t_2 <= -1e-231) {
tmp = t_2 / (a * 2.0);
} else if (t_2 <= 1e-321) {
tmp = t_1;
} else if (t_2 <= 1e+245) {
tmp = fma(x, y, (z * (t * -9.0))) / (a * 2.0);
} else {
tmp = t_1;
}
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
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(x, y, z \cdot \left(t \cdot -9\right)\right)}{a \cdot 2}}
\]
Proof
(/.f64 (fma.f64 x y (*.f64 z (*.f64 t -9))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 x y (*.f64 z (*.f64 t (Rewrite<= metadata-eval (neg.f64 9))))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 x y (*.f64 z (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 t 9))))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 x y (*.f64 z (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 9 t))))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 x y (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 z (*.f64 9 t))))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 x y (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z 9) t)))) (*.f64 a 2)): 10 points increase in error, 17 points decrease in error
(/.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 x y) (*.f64 (*.f64 z 9) t))) (*.f64 a 2)): 3 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 (*.f64 x y) 0)) (*.f64 (*.f64 z 9) t)) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(Rewrite=> div-sub_binary64 (-.f64 (/.f64 (+.f64 (*.f64 x y) 0) (*.f64 a 2)) (/.f64 (*.f64 (*.f64 z 9) t) (*.f64 a 2)))): 1 points increase in error, 4 points decrease in error
(-.f64 (/.f64 (Rewrite=> +-rgt-identity_binary64 (*.f64 x y)) (*.f64 a 2)) (/.f64 (*.f64 (*.f64 z 9) t) (*.f64 a 2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= div-sub_binary64 (/.f64 (-.f64 (*.f64 x y) (*.f64 (*.f64 z 9) t)) (*.f64 a 2))): 4 points increase in error, 1 points decrease in error
(fma.f64 -9/2 (*.f64 (/.f64 t a) z) (/.f64 (*.f64 1/2 y) (/.f64 a x))): 0 points increase in error, 0 points decrease in error
(fma.f64 -9/2 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 t z) a)) (/.f64 (*.f64 1/2 y) (/.f64 a x))): 31 points increase in error, 29 points decrease in error
(fma.f64 -9/2 (/.f64 (*.f64 t z) a) (Rewrite<= associate-*r/_binary64 (*.f64 1/2 (/.f64 y (/.f64 a x))))): 0 points increase in error, 0 points decrease in error
(fma.f64 -9/2 (/.f64 (*.f64 t z) a) (*.f64 1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y x) a)))): 28 points increase in error, 33 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 -9/2 (/.f64 (*.f64 t z) a)) (*.f64 1/2 (/.f64 (*.f64 y x) a)))): 1 points increase in error, 4 points decrease in error
if -2e285 < (-.f64 (*.f64 x y) (*.f64 (*.f64 z 9) t)) < -9.9999999999999999e-232
if -9.9999999999999999e-232 < (-.f64 (*.f64 x y) (*.f64 (*.f64 z 9) t)) < 9.98013e-322 or 1.00000000000000004e245 < (-.f64 (*.f64 x y) (*.f64 (*.f64 z 9) t))
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(x, y, z \cdot \left(t \cdot -9\right)\right)}{a \cdot 2}}
\]
Proof
(/.f64 (fma.f64 x y (*.f64 z (*.f64 t -9))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 x y (*.f64 z (*.f64 t (Rewrite<= metadata-eval (neg.f64 9))))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 x y (*.f64 z (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 t 9))))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 x y (*.f64 z (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 9 t))))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 x y (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 z (*.f64 9 t))))) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 x y (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 z 9) t)))) (*.f64 a 2)): 10 points increase in error, 17 points decrease in error
(/.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 x y) (*.f64 (*.f64 z 9) t))) (*.f64 a 2)): 3 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 (*.f64 x y) 0)) (*.f64 (*.f64 z 9) t)) (*.f64 a 2)): 0 points increase in error, 0 points decrease in error
(Rewrite=> div-sub_binary64 (-.f64 (/.f64 (+.f64 (*.f64 x y) 0) (*.f64 a 2)) (/.f64 (*.f64 (*.f64 z 9) t) (*.f64 a 2)))): 1 points increase in error, 4 points decrease in error
(-.f64 (/.f64 (Rewrite=> +-rgt-identity_binary64 (*.f64 x y)) (*.f64 a 2)) (/.f64 (*.f64 (*.f64 z 9) t) (*.f64 a 2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= div-sub_binary64 (/.f64 (-.f64 (*.f64 x y) (*.f64 (*.f64 z 9) t)) (*.f64 a 2))): 4 points increase in error, 1 points decrease in error
Recombined 4 regimes into one program.
Final simplification0.4
\[\leadsto \begin{array}{l}
\mathbf{if}\;x \cdot y + t \cdot \left(z \cdot -9\right) \leq -2 \cdot 10^{+285}:\\
\;\;\;\;\mathsf{fma}\left(-4.5, z \cdot \frac{t}{a}, \frac{y \cdot 0.5}{\frac{a}{x}}\right)\\
\mathbf{elif}\;x \cdot y + t \cdot \left(z \cdot -9\right) \leq -1 \cdot 10^{-231}:\\
\;\;\;\;\frac{x \cdot y + t \cdot \left(z \cdot -9\right)}{a \cdot 2}\\
\mathbf{elif}\;x \cdot y + t \cdot \left(z \cdot -9\right) \leq 10^{-321}:\\
\;\;\;\;\frac{y}{a} \cdot \frac{x}{2} + t \cdot \left(z \cdot \frac{-4.5}{a}\right)\\
\mathbf{elif}\;x \cdot y + t \cdot \left(z \cdot -9\right) \leq 10^{+245}:\\
\;\;\;\;\frac{\mathsf{fma}\left(x, y, z \cdot \left(t \cdot -9\right)\right)}{a \cdot 2}\\
\mathbf{else}:\\
\;\;\;\;\frac{y}{a} \cdot \frac{x}{2} + t \cdot \left(z \cdot \frac{-4.5}{a}\right)\\
\end{array}
\]
Alternatives
Alternative 1
Error
0.8
Cost
9680
\[\begin{array}{l}
t_1 := \frac{y}{a} \cdot \frac{x}{2} + t \cdot \left(z \cdot \frac{-4.5}{a}\right)\\
t_2 := x \cdot y + t \cdot \left(z \cdot -9\right)\\
\mathbf{if}\;t_2 \leq -5 \cdot 10^{+297}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;t_2 \leq -1 \cdot 10^{-231}:\\
\;\;\;\;\frac{t_2}{a \cdot 2}\\
\mathbf{elif}\;t_2 \leq 10^{-321}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;t_2 \leq 2 \cdot 10^{+146}:\\
\;\;\;\;\mathsf{fma}\left(x, y, z \cdot \left(t \cdot -9\right)\right) \cdot \frac{0.5}{a}\\
\mathbf{else}:\\
\;\;\;\;t_1\\
\end{array}
\]
Alternative 2
Error
0.4
Cost
9680
\[\begin{array}{l}
t_1 := \frac{y}{a} \cdot \frac{x}{2} + t \cdot \left(z \cdot \frac{-4.5}{a}\right)\\
t_2 := x \cdot y + t \cdot \left(z \cdot -9\right)\\
\mathbf{if}\;t_2 \leq -5 \cdot 10^{+297}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;t_2 \leq -1 \cdot 10^{-231}:\\
\;\;\;\;\frac{t_2}{a \cdot 2}\\
\mathbf{elif}\;t_2 \leq 10^{-321}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;t_2 \leq 10^{+245}:\\
\;\;\;\;\frac{\mathsf{fma}\left(x, y, z \cdot \left(t \cdot -9\right)\right)}{a \cdot 2}\\
\mathbf{else}:\\
\;\;\;\;t_1\\
\end{array}
\]
herbie shell --seed 2022329
(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)))