Linear.Projection:infinitePerspective from linear-1.19.1.3, A

Average Error: 6.8 → 2.5

Time: 11.3s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \cdot 2 \le -1797394269439569915404580548509696:\\ \;\;\;\;\frac{1}{\frac{z}{\frac{x \cdot 2}{y - t}}}\\ \mathbf{elif}\;x \cdot 2 \le 5681626209917895739607412273022943363072:\\ \;\;\;\;\frac{x \cdot 2}{z \cdot \left(y - t\right) + z \cdot \left(\left(-t\right) + t\right)}\\ \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 r336087 = x;
        double r336088 = 2.0;
        double r336089 = r336087 * r336088;
        double r336090 = y;
        double r336091 = z;
        double r336092 = r336090 * r336091;
        double r336093 = t;
        double r336094 = r336093 * r336091;
        double r336095 = r336092 - r336094;
        double r336096 = r336089 / r336095;
        return r336096;
}

↓

double f(double x, double y, double z, double t) {
        double r336097 = x;
        double r336098 = 2.0;
        double r336099 = r336097 * r336098;
        double r336100 = -1.79739426943957e+33;
        bool r336101 = r336099 <= r336100;
        double r336102 = 1.0;
        double r336103 = z;
        double r336104 = y;
        double r336105 = t;
        double r336106 = r336104 - r336105;
        double r336107 = r336099 / r336106;
        double r336108 = r336103 / r336107;
        double r336109 = r336102 / r336108;
        double r336110 = 5.681626209917896e+39;
        bool r336111 = r336099 <= r336110;
        double r336112 = r336103 * r336106;
        double r336113 = -r336105;
        double r336114 = r336113 + r336105;
        double r336115 = r336103 * r336114;
        double r336116 = r336112 + r336115;
        double r336117 = r336099 / r336116;
        double r336118 = r336102 / r336103;
        double r336119 = r336107 * r336118;
        double r336120 = r336111 ? r336117 : r336119;
        double r336121 = r336101 ? r336109 : r336120;
        return r336121;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	6.8
Target	2.2
Herbie	2.5

\[\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.045027827330125861587720199944080049996 \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 (* x 2.0) < -1.79739426943957e+33

   1. Initial program 11.2

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

   2. Simplified 10.4

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

   4. Applied add-cube-cbrt 10.8

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

   5. Applied add-sqr-sqrt 37.2

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

   6. Applied prod-diff 37.2

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

   7. Applied distribute-lft-in 37.9

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

   8. Simplified 12.1

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

   9. Simplified 10.4

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

   11. Applied clear-num 10.5

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

   12. Simplified 3.5

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

   if -1.79739426943957e+33 < (* x 2.0) < 5.681626209917896e+39

   1. Initial program 3.4

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

   2. Simplified 2.0

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

   4. Applied add-cube-cbrt 2.4

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

   5. Applied add-sqr-sqrt 33.0

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

   6. Applied prod-diff 33.0

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

   7. Applied distribute-lft-in 34.7

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

   8. Simplified 5.6

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

   9. Simplified 2.0

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

   if 5.681626209917896e+39 < (* x 2.0)

   1. Initial program 12.5

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

   2. Simplified 12.1

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

   4. Applied add-cube-cbrt 12.5

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

   5. Applied add-sqr-sqrt 39.1

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

   6. Applied prod-diff 39.1

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

   7. Applied distribute-lft-in 39.7

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

   8. Simplified 13.6

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

   9. Simplified 12.1

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

   11. Applied clear-num 12.1

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

   12. Simplified 3.4

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

   14. Applied associate-/r/ 3.0

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

4. Final simplification 2.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot 2 \le -1797394269439569915404580548509696:\\ \;\;\;\;\frac{1}{\frac{z}{\frac{x \cdot 2}{y - t}}}\\ \mathbf{elif}\;x \cdot 2 \le 5681626209917895739607412273022943363072:\\ \;\;\;\;\frac{x \cdot 2}{z \cdot \left(y - t\right) + z \cdot \left(\left(-t\right) + t\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot 2}{y - t} \cdot \frac{1}{z}\\ \end{array}\]

Reproduce

herbie shell --seed 2019347 +o rules:numerics
(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.0450278273301259e-269) (/ (* (/ x z) 2) (- y t)) (* (/ x (* (- y t) z)) 2)))

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