Linear.Projection:infinitePerspective from linear-1.19.1.3, A

Average Error: 6.6 → 1.2

Time: 10.0s

Precision: 64

Math

\[\frac{x \cdot 2}{y \cdot z - t \cdot z}\]

↓

\[\begin{array}{l} \mathbf{if}\;y \cdot z - t \cdot z \le 0.0:\\ \;\;\;\;\frac{\left(x \cdot 2\right) \cdot \left(\sqrt[3]{1} \cdot \sqrt[3]{\frac{1}{z}}\right)}{\left(\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}\right) \cdot \sqrt[3]{z}} \cdot \frac{\sqrt[3]{\frac{1}{z}}}{\sqrt[3]{y - t}}\\ \mathbf{elif}\;y \cdot z - t \cdot z \le 5.060468299900743345631957103791187978052 \cdot 10^{246}:\\ \;\;\;\;\frac{x \cdot 2}{y \cdot z - t \cdot z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot 2}{z} \cdot \frac{1}{y - t}\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r406300 = x;
        double r406301 = 2.0;
        double r406302 = r406300 * r406301;
        double r406303 = y;
        double r406304 = z;
        double r406305 = r406303 * r406304;
        double r406306 = t;
        double r406307 = r406306 * r406304;
        double r406308 = r406305 - r406307;
        double r406309 = r406302 / r406308;
        return r406309;
}

↓

double f(double x, double y, double z, double t) {
        double r406310 = y;
        double r406311 = z;
        double r406312 = r406310 * r406311;
        double r406313 = t;
        double r406314 = r406313 * r406311;
        double r406315 = r406312 - r406314;
        double r406316 = 0.0;
        bool r406317 = r406315 <= r406316;
        double r406318 = x;
        double r406319 = 2.0;
        double r406320 = r406318 * r406319;
        double r406321 = 1.0;
        double r406322 = cbrt(r406321);
        double r406323 = r406321 / r406311;
        double r406324 = cbrt(r406323);
        double r406325 = r406322 * r406324;
        double r406326 = r406320 * r406325;
        double r406327 = r406310 - r406313;
        double r406328 = cbrt(r406327);
        double r406329 = r406328 * r406328;
        double r406330 = cbrt(r406311);
        double r406331 = r406329 * r406330;
        double r406332 = r406326 / r406331;
        double r406333 = r406324 / r406328;
        double r406334 = r406332 * r406333;
        double r406335 = 5.060468299900743e+246;
        bool r406336 = r406315 <= r406335;
        double r406337 = r406320 / r406315;
        double r406338 = r406320 / r406311;
        double r406339 = r406321 / r406327;
        double r406340 = r406338 * r406339;
        double r406341 = r406336 ? r406337 : r406340;
        double r406342 = r406317 ? r406334 : r406341;
        return r406342;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	6.6
Target	1.9
Herbie	1.2

\[\begin{array}{l} \mathbf{if}\;\frac{x \cdot 2}{y \cdot z - t \cdot z} \lt -2.559141628295061113708240820439530037456 \cdot 10^{-13}:\\ \;\;\;\;\frac{x}{\left(y - t\right) \cdot z} \cdot 2\\ \mathbf{elif}\;\frac{x \cdot 2}{y \cdot z - t \cdot z} \lt 1.045027827330126029709547581125571222799 \cdot 10^{-269}:\\ \;\;\;\;\frac{\frac{x}{z} \cdot 2}{y - t}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{\left(y - t\right) \cdot z} \cdot 2\\ \end{array}\]

Derivation

1. Split input into 3 regimes

2. if (- (* y z) (* t z)) < 0.0

   1. Initial program 5.6

      \[\frac{x \cdot 2}{y \cdot z - t \cdot z}\]
   2. Using strategy rm

   3. Applied distribute-rgt-out-- 5.6

      \[\leadsto \frac{x \cdot 2}{\color{blue}{z \cdot \left(y - t\right)}}\]

   4. Applied associate-/r* 5.6

      \[\leadsto \color{blue}{\frac{\frac{x \cdot 2}{z}}{y - t}}\]
   5. Using strategy rm

   6. Applied add-cube-cbrt 6.3

      \[\leadsto \frac{\frac{x \cdot 2}{z}}{\color{blue}{\left(\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}\right) \cdot \sqrt[3]{y - t}}}\]

   7. Applied div-inv 6.3

      \[\leadsto \frac{\color{blue}{\left(x \cdot 2\right) \cdot \frac{1}{z}}}{\left(\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}\right) \cdot \sqrt[3]{y - t}}\]

   8. Applied times-frac 5.0

      \[\leadsto \color{blue}{\frac{x \cdot 2}{\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}} \cdot \frac{\frac{1}{z}}{\sqrt[3]{y - t}}}\]
   9. Using strategy rm

   10. Applied *-un-lft-identity 5.0

       \[\leadsto \frac{x \cdot 2}{\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}} \cdot \frac{\frac{1}{z}}{\color{blue}{1 \cdot \sqrt[3]{y - t}}}\]

   11. Applied add-cube-cbrt 5.2

       \[\leadsto \frac{x \cdot 2}{\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}} \cdot \frac{\color{blue}{\left(\sqrt[3]{\frac{1}{z}} \cdot \sqrt[3]{\frac{1}{z}}\right) \cdot \sqrt[3]{\frac{1}{z}}}}{1 \cdot \sqrt[3]{y - t}}\]

   12. Applied times-frac 5.2

       \[\leadsto \frac{x \cdot 2}{\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}} \cdot \color{blue}{\left(\frac{\sqrt[3]{\frac{1}{z}} \cdot \sqrt[3]{\frac{1}{z}}}{1} \cdot \frac{\sqrt[3]{\frac{1}{z}}}{\sqrt[3]{y - t}}\right)}\]

   13. Applied associate-*r* 4.0

       \[\leadsto \color{blue}{\left(\frac{x \cdot 2}{\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}} \cdot \frac{\sqrt[3]{\frac{1}{z}} \cdot \sqrt[3]{\frac{1}{z}}}{1}\right) \cdot \frac{\sqrt[3]{\frac{1}{z}}}{\sqrt[3]{y - t}}}\]

   14. Simplified 3.9

       \[\leadsto \color{blue}{\frac{\left(x \cdot 2\right) \cdot \left(\sqrt[3]{\frac{1}{z}} \cdot \sqrt[3]{\frac{1}{z}}\right)}{\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}}} \cdot \frac{\sqrt[3]{\frac{1}{z}}}{\sqrt[3]{y - t}}\]
   15. Using strategy rm

   16. Applied cbrt-div 3.8

       \[\leadsto \frac{\left(x \cdot 2\right) \cdot \left(\color{blue}{\frac{\sqrt[3]{1}}{\sqrt[3]{z}}} \cdot \sqrt[3]{\frac{1}{z}}\right)}{\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}} \cdot \frac{\sqrt[3]{\frac{1}{z}}}{\sqrt[3]{y - t}}\]

   17. Applied associate-*l/ 3.8

       \[\leadsto \frac{\left(x \cdot 2\right) \cdot \color{blue}{\frac{\sqrt[3]{1} \cdot \sqrt[3]{\frac{1}{z}}}{\sqrt[3]{z}}}}{\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}} \cdot \frac{\sqrt[3]{\frac{1}{z}}}{\sqrt[3]{y - t}}\]

   18. Applied associate-*r/ 3.8

       \[\leadsto \frac{\color{blue}{\frac{\left(x \cdot 2\right) \cdot \left(\sqrt[3]{1} \cdot \sqrt[3]{\frac{1}{z}}\right)}{\sqrt[3]{z}}}}{\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}} \cdot \frac{\sqrt[3]{\frac{1}{z}}}{\sqrt[3]{y - t}}\]

   19. Applied associate-/l/ 2.2

       \[\leadsto \color{blue}{\frac{\left(x \cdot 2\right) \cdot \left(\sqrt[3]{1} \cdot \sqrt[3]{\frac{1}{z}}\right)}{\left(\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}\right) \cdot \sqrt[3]{z}}} \cdot \frac{\sqrt[3]{\frac{1}{z}}}{\sqrt[3]{y - t}}\]

   if 0.0 < (- (* y z) (* t z)) < 5.060468299900743e+246

   1. Initial program 1.0

      \[\frac{x \cdot 2}{y \cdot z - t \cdot z}\]

   if 5.060468299900743e+246 < (- (* y z) (* t z))

   1. Initial program 20.4

      \[\frac{x \cdot 2}{y \cdot z - t \cdot z}\]
   2. Using strategy rm

   3. Applied distribute-rgt-out-- 14.2

      \[\leadsto \frac{x \cdot 2}{\color{blue}{z \cdot \left(y - t\right)}}\]

   4. Applied associate-/r* 0.2

      \[\leadsto \color{blue}{\frac{\frac{x \cdot 2}{z}}{y - t}}\]
   5. Using strategy rm

   6. Applied div-inv 0.3

      \[\leadsto \color{blue}{\frac{x \cdot 2}{z} \cdot \frac{1}{y - t}}\]
3. Recombined 3 regimes into one program.

4. Final simplification 1.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \cdot z - t \cdot z \le 0.0:\\ \;\;\;\;\frac{\left(x \cdot 2\right) \cdot \left(\sqrt[3]{1} \cdot \sqrt[3]{\frac{1}{z}}\right)}{\left(\sqrt[3]{y - t} \cdot \sqrt[3]{y - t}\right) \cdot \sqrt[3]{z}} \cdot \frac{\sqrt[3]{\frac{1}{z}}}{\sqrt[3]{y - t}}\\ \mathbf{elif}\;y \cdot z - t \cdot z \le 5.060468299900743345631957103791187978052 \cdot 10^{246}:\\ \;\;\;\;\frac{x \cdot 2}{y \cdot z - t \cdot z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot 2}{z} \cdot \frac{1}{y - t}\\ \end{array}\]

Reproduce

herbie shell --seed 2019294 
(FPCore (x y z t)
  :name "Linear.Projection:infinitePerspective from linear-1.19.1.3, A"
  :precision binary64

  :herbie-target
  (if (< (/ (* x 2) (- (* y z) (* t z))) -2.559141628295061e-13) (* (/ x (* (- y t) z)) 2) (if (< (/ (* x 2) (- (* y z) (* t z))) 1.045027827330126e-269) (/ (* (/ x z) 2) (- y t)) (* (/ x (* (- y t) z)) 2)))

  (/ (* x 2) (- (* y z) (* t z))))