Linear.Projection:infinitePerspective from linear-1.19.1.3, A

Average Error: 6.6 → 2.3

Time: 8.1s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -1.146577617839211770392177105389103954638 \cdot 10^{98} \lor \neg \left(z \le 1.977491692228259373608984870868524575174 \cdot 10^{-27}\right):\\ \;\;\;\;\frac{x \cdot 2}{z} \cdot \frac{1}{y - t}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot 2}{\left(y - t\right) \cdot z}\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r626789 = x;
        double r626790 = 2.0;
        double r626791 = r626789 * r626790;
        double r626792 = y;
        double r626793 = z;
        double r626794 = r626792 * r626793;
        double r626795 = t;
        double r626796 = r626795 * r626793;
        double r626797 = r626794 - r626796;
        double r626798 = r626791 / r626797;
        return r626798;
}

↓

double f(double x, double y, double z, double t) {
        double r626799 = z;
        double r626800 = -1.1465776178392118e+98;
        bool r626801 = r626799 <= r626800;
        double r626802 = 1.9774916922282594e-27;
        bool r626803 = r626799 <= r626802;
        double r626804 = !r626803;
        bool r626805 = r626801 || r626804;
        double r626806 = x;
        double r626807 = 2.0;
        double r626808 = r626806 * r626807;
        double r626809 = r626808 / r626799;
        double r626810 = 1.0;
        double r626811 = y;
        double r626812 = t;
        double r626813 = r626811 - r626812;
        double r626814 = r626810 / r626813;
        double r626815 = r626809 * r626814;
        double r626816 = r626813 * r626799;
        double r626817 = r626808 / r626816;
        double r626818 = r626805 ? r626815 : r626817;
        return r626818;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	6.6
Target	2.0
Herbie	2.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 2 regimes

2. if z < -1.1465776178392118e+98 or 1.9774916922282594e-27 < z

   1. Initial program 11.2

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

   2. Simplified 8.8

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

   4. Applied associate-/r* 2.2

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

   6. Applied div-inv 2.2

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

   if -1.1465776178392118e+98 < z < 1.9774916922282594e-27

   1. Initial program 2.5

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

   2. Simplified 2.4

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

   4. Applied associate-/r* 9.2

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

   6. Applied div-inv 9.3

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

   7. Applied associate-/l* 2.5

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

   8. Simplified 2.4

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

4. Final simplification 2.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.146577617839211770392177105389103954638 \cdot 10^{98} \lor \neg \left(z \le 1.977491692228259373608984870868524575174 \cdot 10^{-27}\right):\\ \;\;\;\;\frac{x \cdot 2}{z} \cdot \frac{1}{y - t}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot 2}{\left(y - t\right) \cdot z}\\ \end{array}\]

Reproduce

herbie shell --seed 2019209 
(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))))