\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\begin{array}{l}
\mathbf{if}\;\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} = -\infty \lor \neg \left(\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \le 5.302399519709468445659862825023953406186 \cdot 10^{300}\right):\\
\;\;\;\;\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \frac{\sqrt{0.25} \cdot U}{J \cdot \cos \left(0.5 \cdot K\right)}\\
\mathbf{else}:\\
\;\;\;\;\left(\left(\left(-2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)\right) \cdot \sqrt{\left|\sqrt[3]{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right| \cdot \sqrt{\sqrt[3]{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}}}\right) \cdot \sqrt{\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}}\\
\end{array}double f(double J, double K, double U) {
double r123979 = -2.0;
double r123980 = J;
double r123981 = r123979 * r123980;
double r123982 = K;
double r123983 = 2.0;
double r123984 = r123982 / r123983;
double r123985 = cos(r123984);
double r123986 = r123981 * r123985;
double r123987 = 1.0;
double r123988 = U;
double r123989 = r123983 * r123980;
double r123990 = r123989 * r123985;
double r123991 = r123988 / r123990;
double r123992 = pow(r123991, r123983);
double r123993 = r123987 + r123992;
double r123994 = sqrt(r123993);
double r123995 = r123986 * r123994;
return r123995;
}
double f(double J, double K, double U) {
double r123996 = -2.0;
double r123997 = J;
double r123998 = r123996 * r123997;
double r123999 = K;
double r124000 = 2.0;
double r124001 = r123999 / r124000;
double r124002 = cos(r124001);
double r124003 = r123998 * r124002;
double r124004 = 1.0;
double r124005 = U;
double r124006 = r124000 * r123997;
double r124007 = r124006 * r124002;
double r124008 = r124005 / r124007;
double r124009 = pow(r124008, r124000);
double r124010 = r124004 + r124009;
double r124011 = sqrt(r124010);
double r124012 = r124003 * r124011;
double r124013 = -inf.0;
bool r124014 = r124012 <= r124013;
double r124015 = 5.3023995197094684e+300;
bool r124016 = r124012 <= r124015;
double r124017 = !r124016;
bool r124018 = r124014 || r124017;
double r124019 = 0.25;
double r124020 = sqrt(r124019);
double r124021 = r124020 * r124005;
double r124022 = 0.5;
double r124023 = r124022 * r123999;
double r124024 = cos(r124023);
double r124025 = r123997 * r124024;
double r124026 = r124021 / r124025;
double r124027 = r124003 * r124026;
double r124028 = cbrt(r124010);
double r124029 = fabs(r124028);
double r124030 = sqrt(r124028);
double r124031 = r124029 * r124030;
double r124032 = sqrt(r124031);
double r124033 = r124003 * r124032;
double r124034 = sqrt(r124011);
double r124035 = r124033 * r124034;
double r124036 = r124018 ? r124027 : r124035;
return r124036;
}



Bits error versus J



Bits error versus K



Bits error versus U
Results
if (* (* (* -2.0 J) (cos (/ K 2.0))) (sqrt (+ 1.0 (pow (/ U (* (* 2.0 J) (cos (/ K 2.0)))) 2.0)))) < -inf.0 or 5.3023995197094684e+300 < (* (* (* -2.0 J) (cos (/ K 2.0))) (sqrt (+ 1.0 (pow (/ U (* (* 2.0 J) (cos (/ K 2.0)))) 2.0)))) Initial program 62.3
Taylor expanded around inf 46.9
if -inf.0 < (* (* (* -2.0 J) (cos (/ K 2.0))) (sqrt (+ 1.0 (pow (/ U (* (* 2.0 J) (cos (/ K 2.0)))) 2.0)))) < 5.3023995197094684e+300Initial program 0.1
rmApplied add-sqr-sqrt0.1
Applied sqrt-prod0.3
Applied associate-*r*0.3
rmApplied add-cube-cbrt0.3
Applied sqrt-prod0.3
Simplified0.3
Final simplification13.7
herbie shell --seed 2019306
(FPCore (J K U)
:name "Maksimov and Kolovsky, Equation (3)"
:precision binary64
(* (* (* -2 J) (cos (/ K 2))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)))))