Linear.Projection:infinitePerspective from linear-1.19.1.3, A

Average Error: 6.7 → 1.3

Time: 12.8s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;y \cdot z - t \cdot z = -\infty:\\ \;\;\;\;\frac{2}{y - t} \cdot \frac{x}{z}\\ \mathbf{elif}\;y \cdot z - t \cdot z \le 2.166521247594354925726439343625696917212 \cdot 10^{205}:\\ \;\;\;\;\frac{x \cdot 2}{y \cdot z - t \cdot z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot 2}{y - t} \cdot \frac{1}{z}\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r349550 = x;
        double r349551 = 2.0;
        double r349552 = r349550 * r349551;
        double r349553 = y;
        double r349554 = z;
        double r349555 = r349553 * r349554;
        double r349556 = t;
        double r349557 = r349556 * r349554;
        double r349558 = r349555 - r349557;
        double r349559 = r349552 / r349558;
        return r349559;
}

↓

double f(double x, double y, double z, double t) {
        double r349560 = y;
        double r349561 = z;
        double r349562 = r349560 * r349561;
        double r349563 = t;
        double r349564 = r349563 * r349561;
        double r349565 = r349562 - r349564;
        double r349566 = -inf.0;
        bool r349567 = r349565 <= r349566;
        double r349568 = 2.0;
        double r349569 = r349560 - r349563;
        double r349570 = r349568 / r349569;
        double r349571 = x;
        double r349572 = r349571 / r349561;
        double r349573 = r349570 * r349572;
        double r349574 = 2.166521247594355e+205;
        bool r349575 = r349565 <= r349574;
        double r349576 = r349571 * r349568;
        double r349577 = r349576 / r349565;
        double r349578 = r349576 / r349569;
        double r349579 = 1.0;
        double r349580 = r349579 / r349561;
        double r349581 = r349578 * r349580;
        double r349582 = r349575 ? r349577 : r349581;
        double r349583 = r349567 ? r349573 : r349582;
        return r349583;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	6.7
Target	2.2
Herbie	1.3

\[\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)) < -inf.0

   1. Initial program 21.0

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

   2. Simplified 0.8

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

   4. Applied *-un-lft-identity 0.8

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

   5. Applied times-frac 0.2

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

   7. Applied *-un-lft-identity 0.2

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

   8. Applied *-un-lft-identity 0.2

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

   9. Applied times-frac 0.2

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

   10. Applied associate-*r* 0.2

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

   11. Simplified 0.1

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

   if -inf.0 < (- (* y z) (* t z)) < 2.166521247594355e+205

   1. Initial program 1.7

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

   if 2.166521247594355e+205 < (- (* y z) (* t z))

   1. Initial program 17.3

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

   2. Simplified 1.5

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

   4. Applied *-un-lft-identity 1.5

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

   5. Applied times-frac 0.8

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

   7. Applied div-inv 0.8

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

   8. Applied add-cube-cbrt 0.8

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

   9. Applied times-frac 0.7

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

   10. Applied associate-*l* 0.5

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

   11. Simplified 0.5

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

4. Final simplification 1.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \cdot z - t \cdot z = -\infty:\\ \;\;\;\;\frac{2}{y - t} \cdot \frac{x}{z}\\ \mathbf{elif}\;y \cdot z - t \cdot z \le 2.166521247594354925726439343625696917212 \cdot 10^{205}:\\ \;\;\;\;\frac{x \cdot 2}{y \cdot z - t \cdot z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot 2}{y - t} \cdot \frac{1}{z}\\ \end{array}\]

Reproduce

herbie shell --seed 2019179 +o rules:numerics
(FPCore (x y z t)
  :name "Linear.Projection:infinitePerspective from linear-1.19.1.3, A"

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

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