VandenBroeck and Keller, Equation (6)

Average Error: 16.5 → 12.1

Time: 13.2s

Precision: 64

• could not determine a ground truth for program body

  1. F = -5.743763742480061e-48
  2. l = 2591932095726941.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)\]

↓

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

C

double f(double F, double l) {
        double r13953 = atan2(1.0, 0.0);
        double r13954 = l;
        double r13955 = r13953 * r13954;
        double r13956 = 1.0;
        double r13957 = F;
        double r13958 = r13957 * r13957;
        double r13959 = r13956 / r13958;
        double r13960 = tan(r13955);
        double r13961 = r13959 * r13960;
        double r13962 = r13955 - r13961;
        return r13962;
}

↓

double f(double F, double l) {
        double r13963 = atan2(1.0, 0.0);
        double r13964 = l;
        double r13965 = r13963 * r13964;
        double r13966 = 1.0;
        double r13967 = cbrt(r13966);
        double r13968 = r13967 * r13967;
        double r13969 = F;
        double r13970 = r13968 / r13969;
        double r13971 = r13967 / r13969;
        double r13972 = sqrt(r13963);
        double r13973 = sqrt(r13972);
        double r13974 = r13973 * r13973;
        double r13975 = r13974 * r13964;
        double r13976 = r13974 * r13975;
        double r13977 = tan(r13976);
        double r13978 = r13971 * r13977;
        double r13979 = r13970 * r13978;
        double r13980 = r13965 - r13979;
        return r13980;
}

Error

Bits error versus F

Bits error versus l

Derivation

1. Initial program 16.5

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

3. Applied add-cube-cbrt 16.5

   \[\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 16.5

   \[\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* 12.1

   \[\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 12.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* 12.1

   \[\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)\]
9. Using strategy rm

10. Applied add-sqr-sqrt 12.1

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

11. Applied sqrt-prod 12.1

    \[\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{\sqrt{\pi}} \cdot \sqrt{\sqrt{\pi}}\right)} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)\right)\]
12. Using strategy rm

13. Applied add-sqr-sqrt 12.1

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

14. Applied sqrt-prod 12.1

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

15. Final simplification 12.1

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

Reproduce

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