\frac{x \cdot y - \left(z \cdot 9.0\right) \cdot t}{a \cdot 2.0}\begin{array}{l}
\mathbf{if}\;x \cdot y - \left(z \cdot 9.0\right) \cdot t = -\infty:\\
\;\;\;\;\left(\frac{y}{a} \cdot x\right) \cdot 0.5 - \frac{z}{a} \cdot \left(t \cdot 4.5\right)\\
\mathbf{elif}\;x \cdot y - \left(z \cdot 9.0\right) \cdot t \le 1.553517178096751 \cdot 10^{+221}:\\
\;\;\;\;\frac{x \cdot y}{a} \cdot 0.5 - \frac{\left(z \cdot t\right) \cdot 4.5}{a}\\
\mathbf{else}:\\
\;\;\;\;\left(\frac{y}{a} \cdot x\right) \cdot 0.5 - \frac{z}{a} \cdot \left(t \cdot 4.5\right)\\
\end{array}double f(double x, double y, double z, double t, double a) {
double r14207967 = x;
double r14207968 = y;
double r14207969 = r14207967 * r14207968;
double r14207970 = z;
double r14207971 = 9.0;
double r14207972 = r14207970 * r14207971;
double r14207973 = t;
double r14207974 = r14207972 * r14207973;
double r14207975 = r14207969 - r14207974;
double r14207976 = a;
double r14207977 = 2.0;
double r14207978 = r14207976 * r14207977;
double r14207979 = r14207975 / r14207978;
return r14207979;
}
double f(double x, double y, double z, double t, double a) {
double r14207980 = x;
double r14207981 = y;
double r14207982 = r14207980 * r14207981;
double r14207983 = z;
double r14207984 = 9.0;
double r14207985 = r14207983 * r14207984;
double r14207986 = t;
double r14207987 = r14207985 * r14207986;
double r14207988 = r14207982 - r14207987;
double r14207989 = -inf.0;
bool r14207990 = r14207988 <= r14207989;
double r14207991 = a;
double r14207992 = r14207981 / r14207991;
double r14207993 = r14207992 * r14207980;
double r14207994 = 0.5;
double r14207995 = r14207993 * r14207994;
double r14207996 = r14207983 / r14207991;
double r14207997 = 4.5;
double r14207998 = r14207986 * r14207997;
double r14207999 = r14207996 * r14207998;
double r14208000 = r14207995 - r14207999;
double r14208001 = 1.553517178096751e+221;
bool r14208002 = r14207988 <= r14208001;
double r14208003 = r14207982 / r14207991;
double r14208004 = r14208003 * r14207994;
double r14208005 = r14207983 * r14207986;
double r14208006 = r14208005 * r14207997;
double r14208007 = r14208006 / r14207991;
double r14208008 = r14208004 - r14208007;
double r14208009 = r14208002 ? r14208008 : r14208000;
double r14208010 = r14207990 ? r14208000 : r14208009;
return r14208010;
}




Bits error versus x




Bits error versus y




Bits error versus z




Bits error versus t




Bits error versus a
Results
| Original | 7.2 |
|---|---|
| Target | 5.4 |
| Herbie | 0.8 |
if (- (* x y) (* (* z 9.0) t)) < -inf.0 or 1.553517178096751e+221 < (- (* x y) (* (* z 9.0) t)) Initial program 40.7
Taylor expanded around 0 40.3
rmApplied *-un-lft-identity40.3
Applied times-frac20.4
Simplified20.4
rmApplied *-un-lft-identity20.4
Applied times-frac0.7
Applied associate-*r*0.8
Simplified0.8
if -inf.0 < (- (* x y) (* (* z 9.0) t)) < 1.553517178096751e+221Initial program 0.8
Taylor expanded around 0 0.8
rmApplied associate-*r/0.8
Final simplification0.8
herbie shell --seed 2019156 +o rules:numerics
(FPCore (x y z t a)
:name "Diagrams.Solve.Polynomial:cubForm from diagrams-solve-0.1, I"
: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)))