Linear.Projection:infinitePerspective from linear-1.19.1.3, A

Average Error: 6.8 → 2.8

Time: 23.9s

Precision: 64

Math

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

↓

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

C

double f(double x, double y, double z, double t) {
        double r561657 = x;
        double r561658 = 2.0;
        double r561659 = r561657 * r561658;
        double r561660 = y;
        double r561661 = z;
        double r561662 = r561660 * r561661;
        double r561663 = t;
        double r561664 = r561663 * r561661;
        double r561665 = r561662 - r561664;
        double r561666 = r561659 / r561665;
        return r561666;
}

↓

double f(double x, double y, double z, double t) {
        double r561667 = z;
        double r561668 = -3667224765870525.0;
        double r561669 = 6.1501577861568104e+259;
        double r561670 = r561668 / r561669;
        bool r561671 = r561667 <= r561670;
        double r561672 = 1.0;
        double r561673 = x;
        double r561674 = cbrt(r561673);
        double r561675 = cbrt(r561674);
        double r561676 = r561675 * r561675;
        double r561677 = r561672 / r561676;
        double r561678 = r561672 / r561677;
        double r561679 = r561667 / r561675;
        double r561680 = r561674 / r561679;
        double r561681 = y;
        double r561682 = t;
        double r561683 = r561681 - r561682;
        double r561684 = 2.0;
        double r561685 = r561683 / r561684;
        double r561686 = r561674 / r561685;
        double r561687 = r561680 * r561686;
        double r561688 = r561678 * r561687;
        double r561689 = 6.823904024614768e+34;
        bool r561690 = r561667 <= r561689;
        double r561691 = r561667 * r561683;
        double r561692 = pow(r561691, r561672);
        double r561693 = r561692 / r561684;
        double r561694 = r561673 / r561693;
        double r561695 = r561672 / r561667;
        double r561696 = r561673 / r561685;
        double r561697 = r561695 * r561696;
        double r561698 = r561690 ? r561694 : r561697;
        double r561699 = r561671 ? r561688 : r561698;
        return r561699;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	6.8
Target	2.0
Herbie	2.8

\[\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 z < -5.962814115314182e-245

   1. Initial program 7.0

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

   2. Simplified 5.8

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

   4. Applied *-un-lft-identity 5.8

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

   5. Applied times-frac 5.8

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

   6. Applied add-cube-cbrt 6.5

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

   7. Applied times-frac 3.5

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

   8. Simplified 3.5

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

   10. Applied add-cube-cbrt 3.8

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

   11. Applied *-un-lft-identity 3.8

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

   12. Applied times-frac 3.8

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

   13. Applied *-un-lft-identity 3.8

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

   14. Applied times-frac 3.8

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

   15. Applied associate-*l* 3.1

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

   if -5.962814115314182e-245 < z < 6.823904024614768e+34

   1. Initial program 2.8

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

   2. Simplified 2.7

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

   4. Applied pow1 2.7

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

   5. Applied pow1 2.7

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

   6. Applied pow-prod-down 2.7

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

   if 6.823904024614768e+34 < z

   1. Initial program 11.4

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

   2. Simplified 9.3

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

   4. Applied *-un-lft-identity 9.3

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

   5. Applied times-frac 9.3

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

   6. Applied *-un-lft-identity 9.3

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

   7. Applied times-frac 2.4

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

   8. Simplified 2.4

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

4. Final simplification 2.8

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

Reproduce

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