VandenBroeck and Keller, Equation (6)

Average Error: 16.4 → 8.6

Time: 13.7s

Precision: 64

• could not determine a ground truth for program body

  1. F = 9.835650614246157e+92
  2. l = 2649526956147094.5

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\pi \cdot \ell - \frac{1}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]

↓

\[\begin{array}{l} \mathbf{if}\;\pi \cdot \ell \le -3.25877154259171114 \cdot 10^{163}:\\ \;\;\;\;\pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{\cos \left(\left(\sqrt[3]{\pi \cdot \ell} \cdot \left(\sqrt[3]{-1} \cdot \sqrt[3]{e^{\log \pi - \log \left(\frac{-1}{\ell}\right)}}\right)\right) \cdot \sqrt[3]{\pi \cdot \ell}\right) \cdot F}\\ \mathbf{elif}\;\pi \cdot \ell \le 7.52430755046992877 \cdot 10^{152}:\\ \;\;\;\;\pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{\left(\left(\frac{1}{24} \cdot \left({\pi}^{4} \cdot {\ell}^{4}\right) + 1\right) - \frac{1}{2} \cdot \left({\pi}^{2} \cdot {\ell}^{2}\right)\right) \cdot F}\\ \mathbf{else}:\\ \;\;\;\;\pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \left(\frac{\sqrt[3]{1}}{F} \cdot \tan \left(\sqrt{\pi} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)\right)\\ \end{array}\]

C

double f(double F, double l) {
        double r18987 = atan2(1.0, 0.0);
        double r18988 = l;
        double r18989 = r18987 * r18988;
        double r18990 = 1.0;
        double r18991 = F;
        double r18992 = r18991 * r18991;
        double r18993 = r18990 / r18992;
        double r18994 = tan(r18989);
        double r18995 = r18993 * r18994;
        double r18996 = r18989 - r18995;
        return r18996;
}

↓

double f(double F, double l) {
        double r18997 = atan2(1.0, 0.0);
        double r18998 = l;
        double r18999 = r18997 * r18998;
        double r19000 = -3.258771542591711e+163;
        bool r19001 = r18999 <= r19000;
        double r19002 = 1.0;
        double r19003 = cbrt(r19002);
        double r19004 = r19003 * r19003;
        double r19005 = F;
        double r19006 = r19004 / r19005;
        double r19007 = sin(r18999);
        double r19008 = r19003 * r19007;
        double r19009 = cbrt(r18999);
        double r19010 = -1.0;
        double r19011 = cbrt(r19010);
        double r19012 = log(r18997);
        double r19013 = r19010 / r18998;
        double r19014 = log(r19013);
        double r19015 = r19012 - r19014;
        double r19016 = exp(r19015);
        double r19017 = cbrt(r19016);
        double r19018 = r19011 * r19017;
        double r19019 = r19009 * r19018;
        double r19020 = r19019 * r19009;
        double r19021 = cos(r19020);
        double r19022 = r19021 * r19005;
        double r19023 = r19008 / r19022;
        double r19024 = r19006 * r19023;
        double r19025 = r18999 - r19024;
        double r19026 = 7.524307550469929e+152;
        bool r19027 = r18999 <= r19026;
        double r19028 = 0.041666666666666664;
        double r19029 = 4.0;
        double r19030 = pow(r18997, r19029);
        double r19031 = pow(r18998, r19029);
        double r19032 = r19030 * r19031;
        double r19033 = r19028 * r19032;
        double r19034 = 1.0;
        double r19035 = r19033 + r19034;
        double r19036 = 0.5;
        double r19037 = 2.0;
        double r19038 = pow(r18997, r19037);
        double r19039 = pow(r18998, r19037);
        double r19040 = r19038 * r19039;
        double r19041 = r19036 * r19040;
        double r19042 = r19035 - r19041;
        double r19043 = r19042 * r19005;
        double r19044 = r19008 / r19043;
        double r19045 = r19006 * r19044;
        double r19046 = r18999 - r19045;
        double r19047 = r19003 / r19005;
        double r19048 = sqrt(r18997);
        double r19049 = r19048 * r18998;
        double r19050 = r19048 * r19049;
        double r19051 = tan(r19050);
        double r19052 = r19047 * r19051;
        double r19053 = r19006 * r19052;
        double r19054 = r18999 - r19053;
        double r19055 = r19027 ? r19046 : r19054;
        double r19056 = r19001 ? r19025 : r19055;
        return r19056;
}

Error

Bits error versus F

Bits error versus l

Derivation

1. Split input into 3 regimes

2. if (* PI l) < -3.258771542591711e+163

   1. Initial program 19.2

      \[\pi \cdot \ell - \frac{1}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 19.2

      \[\leadsto \pi \cdot \ell - \frac{\color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{1}\right) \cdot \sqrt[3]{1}}}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]

   4. Applied times-frac 19.2

      \[\leadsto \pi \cdot \ell - \color{blue}{\left(\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1}}{F}\right)} \cdot \tan \left(\pi \cdot \ell\right)\]

   5. Applied associate-*l* 19.2

      \[\leadsto \pi \cdot \ell - \color{blue}{\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \left(\frac{\sqrt[3]{1}}{F} \cdot \tan \left(\pi \cdot \ell\right)\right)}\]
   6. Using strategy rm

   7. Applied tan-quot 19.2

      \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \left(\frac{\sqrt[3]{1}}{F} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \ell\right)}{\cos \left(\pi \cdot \ell\right)}}\right)\]

   8. Applied frac-times 19.2

      \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \color{blue}{\frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \cos \left(\pi \cdot \ell\right)}}\]

   9. Simplified 19.2

      \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{\color{blue}{\cos \left(\pi \cdot \ell\right) \cdot F}}\]
   10. Using strategy rm

   11. Applied add-cube-cbrt 19.2

       \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{\cos \color{blue}{\left(\left(\sqrt[3]{\pi \cdot \ell} \cdot \sqrt[3]{\pi \cdot \ell}\right) \cdot \sqrt[3]{\pi \cdot \ell}\right)} \cdot F}\]

   12. Taylor expanded around -inf 19.2

       \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{\cos \left(\left(\sqrt[3]{\pi \cdot \ell} \cdot \color{blue}{\left(\sqrt[3]{-1} \cdot e^{\frac{1}{3} \cdot \left(\log \pi - \log \left(\frac{-1}{\ell}\right)\right)}\right)}\right) \cdot \sqrt[3]{\pi \cdot \ell}\right) \cdot F}\]

   13. Simplified 19.2

       \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{\cos \left(\left(\sqrt[3]{\pi \cdot \ell} \cdot \color{blue}{\left(\sqrt[3]{-1} \cdot \sqrt[3]{e^{\log \pi - \log \left(\frac{-1}{\ell}\right)}}\right)}\right) \cdot \sqrt[3]{\pi \cdot \ell}\right) \cdot F}\]

   if -3.258771542591711e+163 < (* PI l) < 7.524307550469929e+152

   1. Initial program 15.2

      \[\pi \cdot \ell - \frac{1}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 15.2

      \[\leadsto \pi \cdot \ell - \frac{\color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{1}\right) \cdot \sqrt[3]{1}}}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]

   4. Applied times-frac 15.2

      \[\leadsto \pi \cdot \ell - \color{blue}{\left(\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1}}{F}\right)} \cdot \tan \left(\pi \cdot \ell\right)\]

   5. Applied associate-*l* 9.7

      \[\leadsto \pi \cdot \ell - \color{blue}{\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \left(\frac{\sqrt[3]{1}}{F} \cdot \tan \left(\pi \cdot \ell\right)\right)}\]
   6. Using strategy rm

   7. Applied tan-quot 9.7

      \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \left(\frac{\sqrt[3]{1}}{F} \cdot \color{blue}{\frac{\sin \left(\pi \cdot \ell\right)}{\cos \left(\pi \cdot \ell\right)}}\right)\]

   8. Applied frac-times 9.7

      \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \color{blue}{\frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{F \cdot \cos \left(\pi \cdot \ell\right)}}\]

   9. Simplified 9.7

      \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{\color{blue}{\cos \left(\pi \cdot \ell\right) \cdot F}}\]

   10. Taylor expanded around 0 4.4

       \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{\color{blue}{\left(\left(\frac{1}{24} \cdot \left({\pi}^{4} \cdot {\ell}^{4}\right) + 1\right) - \frac{1}{2} \cdot \left({\pi}^{2} \cdot {\ell}^{2}\right)\right)} \cdot F}\]

   if 7.524307550469929e+152 < (* PI l)

   1. Initial program 20.2

      \[\pi \cdot \ell - \frac{1}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 20.2

      \[\leadsto \pi \cdot \ell - \frac{\color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{1}\right) \cdot \sqrt[3]{1}}}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]

   4. Applied times-frac 20.2

      \[\leadsto \pi \cdot \ell - \color{blue}{\left(\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1}}{F}\right)} \cdot \tan \left(\pi \cdot \ell\right)\]

   5. Applied associate-*l* 20.2

      \[\leadsto \pi \cdot \ell - \color{blue}{\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \left(\frac{\sqrt[3]{1}}{F} \cdot \tan \left(\pi \cdot \ell\right)\right)}\]
   6. Using strategy rm

   7. Applied add-sqr-sqrt 20.2

      \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \left(\frac{\sqrt[3]{1}}{F} \cdot \tan \left(\color{blue}{\left(\sqrt{\pi} \cdot \sqrt{\pi}\right)} \cdot \ell\right)\right)\]

   8. Applied associate-*l* 20.2

      \[\leadsto \pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \left(\frac{\sqrt[3]{1}}{F} \cdot \tan \color{blue}{\left(\sqrt{\pi} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)}\right)\]
3. Recombined 3 regimes into one program.

4. Final simplification 8.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;\pi \cdot \ell \le -3.25877154259171114 \cdot 10^{163}:\\ \;\;\;\;\pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{\cos \left(\left(\sqrt[3]{\pi \cdot \ell} \cdot \left(\sqrt[3]{-1} \cdot \sqrt[3]{e^{\log \pi - \log \left(\frac{-1}{\ell}\right)}}\right)\right) \cdot \sqrt[3]{\pi \cdot \ell}\right) \cdot F}\\ \mathbf{elif}\;\pi \cdot \ell \le 7.52430755046992877 \cdot 10^{152}:\\ \;\;\;\;\pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \frac{\sqrt[3]{1} \cdot \sin \left(\pi \cdot \ell\right)}{\left(\left(\frac{1}{24} \cdot \left({\pi}^{4} \cdot {\ell}^{4}\right) + 1\right) - \frac{1}{2} \cdot \left({\pi}^{2} \cdot {\ell}^{2}\right)\right) \cdot F}\\ \mathbf{else}:\\ \;\;\;\;\pi \cdot \ell - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{F} \cdot \left(\frac{\sqrt[3]{1}}{F} \cdot \tan \left(\sqrt{\pi} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020042 
(FPCore (F l)
  :name "VandenBroeck and Keller, Equation (6)"
  :precision binary64
  (- (* PI l) (* (/ 1 (* F F)) (tan (* PI l)))))