Maksimov and Kolovsky, Equation (3)

Average Error: 18.0 → 8.9

Time: 10.2s

Precision: 64

Math

\[\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 2.8366567620949629 \cdot 10^{304}\right):\\ \;\;\;\;{\left(-2 \cdot \left(\sqrt{0.25} \cdot U\right)\right)}^{1}\\ \mathbf{else}:\\ \;\;\;\;\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}}\\ \end{array}\]

C

double f(double J, double K, double U) {
        double r238064 = -2.0;
        double r238065 = J;
        double r238066 = r238064 * r238065;
        double r238067 = K;
        double r238068 = 2.0;
        double r238069 = r238067 / r238068;
        double r238070 = cos(r238069);
        double r238071 = r238066 * r238070;
        double r238072 = 1.0;
        double r238073 = U;
        double r238074 = r238068 * r238065;
        double r238075 = r238074 * r238070;
        double r238076 = r238073 / r238075;
        double r238077 = pow(r238076, r238068);
        double r238078 = r238072 + r238077;
        double r238079 = sqrt(r238078);
        double r238080 = r238071 * r238079;
        return r238080;
}

↓

double f(double J, double K, double U) {
        double r238081 = -2.0;
        double r238082 = J;
        double r238083 = r238081 * r238082;
        double r238084 = K;
        double r238085 = 2.0;
        double r238086 = r238084 / r238085;
        double r238087 = cos(r238086);
        double r238088 = r238083 * r238087;
        double r238089 = 1.0;
        double r238090 = U;
        double r238091 = r238085 * r238082;
        double r238092 = r238091 * r238087;
        double r238093 = r238090 / r238092;
        double r238094 = pow(r238093, r238085);
        double r238095 = r238089 + r238094;
        double r238096 = sqrt(r238095);
        double r238097 = r238088 * r238096;
        double r238098 = -inf.0;
        bool r238099 = r238097 <= r238098;
        double r238100 = 2.836656762094963e+304;
        bool r238101 = r238097 <= r238100;
        double r238102 = !r238101;
        bool r238103 = r238099 || r238102;
        double r238104 = 0.25;
        double r238105 = sqrt(r238104);
        double r238106 = r238105 * r238090;
        double r238107 = r238081 * r238106;
        double r238108 = 1.0;
        double r238109 = pow(r238107, r238108);
        double r238110 = r238103 ? r238109 : r238097;
        return r238110;
}

Error

Bits error versus J

Bits error versus K

Bits error versus U

Derivation

1. Split input into 2 regimes

2. 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 2.836656762094963e+304 < (* (* (* -2.0 J) (cos (/ K 2.0))) (sqrt (+ 1.0 (pow (/ U (* (* 2.0 J) (cos (/ K 2.0)))) 2.0))))

   1. Initial program 63.0

      \[\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}}\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 63.1

      \[\leadsto \left(\left(-2 \cdot J\right) \cdot \color{blue}{\left(\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \sqrt[3]{\cos \left(\frac{K}{2}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}\right) \cdot \sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\]

   4. Applied associate-*r* 63.1

      \[\leadsto \color{blue}{\left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)\right) \cdot \sqrt[3]{\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}}\]
   5. Using strategy rm

   6. Applied add-cube-cbrt 63.1

      \[\leadsto \left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \color{blue}{\left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}\right)\right) \cdot \sqrt[3]{\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}}\]
   7. Using strategy rm

   8. Applied pow1 63.1

      \[\leadsto \left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)\right)\right) \cdot \sqrt[3]{\cos \left(\frac{K}{2}\right)}\right) \cdot \color{blue}{{\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}}\]

   9. Applied pow1 63.1

      \[\leadsto \left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)\right)\right) \cdot \color{blue}{{\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   10. Applied pow1 63.1

       \[\leadsto \left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \color{blue}{{\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{1}}\right)\right)\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   11. Applied pow1 63.1

       \[\leadsto \left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \color{blue}{{\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{1}}\right) \cdot {\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{1}\right)\right)\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   12. Applied pow1 63.1

       \[\leadsto \left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\color{blue}{{\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{1}} \cdot {\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{1}\right) \cdot {\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{1}\right)\right)\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   13. Applied pow-prod-down 63.1

       \[\leadsto \left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\color{blue}{{\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{1}} \cdot {\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{1}\right)\right)\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   14. Applied pow-prod-down 63.1

       \[\leadsto \left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \color{blue}{{\left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{1}}\right)\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   15. Applied pow1 63.1

       \[\leadsto \left(\left(\left(-2 \cdot J\right) \cdot \left(\color{blue}{{\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}} \cdot {\left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{1}\right)\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   16. Applied pow-prod-down 63.1

       \[\leadsto \left(\left(\left(-2 \cdot J\right) \cdot \color{blue}{{\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)\right)}^{1}}\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   17. Applied pow1 63.1

       \[\leadsto \left(\left(\left(-2 \cdot \color{blue}{{J}^{1}}\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)\right)}^{1}\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   18. Applied pow1 63.1

       \[\leadsto \left(\left(\left(\color{blue}{{-2}^{1}} \cdot {J}^{1}\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)\right)}^{1}\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   19. Applied pow-prod-down 63.1

       \[\leadsto \left(\left(\color{blue}{{\left(-2 \cdot J\right)}^{1}} \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)\right)}^{1}\right) \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   20. Applied pow-prod-down 63.1

       \[\leadsto \left(\color{blue}{{\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)\right)\right)}^{1}} \cdot {\left(\sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}\right) \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   21. Applied pow-prod-down 63.1

       \[\leadsto \color{blue}{{\left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)\right)\right) \cdot \sqrt[3]{\cos \left(\frac{K}{2}\right)}\right)}^{1}} \cdot {\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}}\right)}^{1}\]

   22. Applied pow-prod-down 63.1

       \[\leadsto \color{blue}{{\left(\left(\left(\left(-2 \cdot J\right) \cdot \left(\sqrt[3]{\cos \left(\frac{K}{2}\right)} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}} \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right) \cdot \sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)\right)\right) \cdot \sqrt[3]{\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}}\right)}^{1}}\]

   23. Simplified 63.1

       \[\leadsto {\color{blue}{\left(\left(\sqrt{1 + {\left(\frac{U}{\left(2 \cdot J\right) \cdot \cos \left(\frac{K}{2}\right)}\right)}^{2}} \cdot \sqrt[3]{\cos \left(\frac{K}{2}\right)}\right) \cdot \left({\left(\sqrt[3]{\sqrt[3]{\cos \left(\frac{K}{2}\right)}}\right)}^{6} \cdot \left(-2 \cdot J\right)\right)\right)}}^{1}\]

   24. Taylor expanded around inf 31.2

       \[\leadsto {\color{blue}{\left(-2 \cdot \left(\sqrt{0.25} \cdot U\right)\right)}}^{1}\]

   if -inf.0 < (* (* (* -2.0 J) (cos (/ K 2.0))) (sqrt (+ 1.0 (pow (/ U (* (* 2.0 J) (cos (/ K 2.0)))) 2.0)))) < 2.836656762094963e+304

   1. Initial program 0.1

      \[\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}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 8.9

   \[\leadsto \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 2.8366567620949629 \cdot 10^{304}\right):\\ \;\;\;\;{\left(-2 \cdot \left(\sqrt{0.25} \cdot U\right)\right)}^{1}\\ \mathbf{else}:\\ \;\;\;\;\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}}\\ \end{array}\]

Reproduce

herbie shell --seed 2020039 
(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)))))