System.Random.MWC.Distributions:truncatedExp from mwc-random-0.13.3.2

Average Error: 24.7 → 8.9

Time: 51.4s

Precision: 64

• could not determine a ground truth for program body

  1. x = 7.658297473827752e+180
  2. y = 6.078478078877249e-301
  3. z = 5.561071419116658e+204
  4. t = 2.775116345214488e-155

Math

\[x - \frac{\log \left(\left(1.0 - y\right) + y \cdot e^{z}\right)}{t}\]

↓

\[\begin{array}{l} \mathbf{if}\;z \le -6.220564919949488 \cdot 10^{-06}:\\ \;\;\;\;x - \frac{\log \left(\sqrt[3]{e^{z} \cdot y + \left(1.0 - y\right)} \cdot \sqrt[3]{e^{z} \cdot y + \left(1.0 - y\right)}\right) + \log \left(\sqrt[3]{e^{z} \cdot y + \left(1.0 - y\right)}\right)}{t}\\ \mathbf{elif}\;z \le -7.588076395555027 \cdot 10^{-93}:\\ \;\;\;\;x - \frac{\log \left(\left(\frac{1}{2} \cdot \left(z \cdot z\right) + z\right) \cdot y + 1.0\right)}{t}\\ \mathbf{elif}\;z \le 1.6081434733570535 \cdot 10^{-109}:\\ \;\;\;\;x - \left(\frac{y \cdot z}{t} \cdot 1.0 + \frac{\left(\left(y \cdot z\right) \cdot z\right) \cdot 0.5}{t}\right)\\ \mathbf{elif}\;z \le 9.047911306874446 \cdot 10^{-17}:\\ \;\;\;\;x - \frac{\log \left(\left(\frac{1}{2} \cdot \left(z \cdot z\right) + z\right) \cdot y + 1.0\right)}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \left(\frac{y \cdot z}{t} \cdot 1.0 + \frac{\left(\left(y \cdot z\right) \cdot z\right) \cdot 0.5}{t}\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r28387645 = x;
        double r28387646 = 1.0;
        double r28387647 = y;
        double r28387648 = r28387646 - r28387647;
        double r28387649 = z;
        double r28387650 = exp(r28387649);
        double r28387651 = r28387647 * r28387650;
        double r28387652 = r28387648 + r28387651;
        double r28387653 = log(r28387652);
        double r28387654 = t;
        double r28387655 = r28387653 / r28387654;
        double r28387656 = r28387645 - r28387655;
        return r28387656;
}

↓

double f(double x, double y, double z, double t) {
        double r28387657 = z;
        double r28387658 = -6.220564919949488e-06;
        bool r28387659 = r28387657 <= r28387658;
        double r28387660 = x;
        double r28387661 = exp(r28387657);
        double r28387662 = y;
        double r28387663 = r28387661 * r28387662;
        double r28387664 = 1.0;
        double r28387665 = r28387664 - r28387662;
        double r28387666 = r28387663 + r28387665;
        double r28387667 = cbrt(r28387666);
        double r28387668 = r28387667 * r28387667;
        double r28387669 = log(r28387668);
        double r28387670 = log(r28387667);
        double r28387671 = r28387669 + r28387670;
        double r28387672 = t;
        double r28387673 = r28387671 / r28387672;
        double r28387674 = r28387660 - r28387673;
        double r28387675 = -7.588076395555027e-93;
        bool r28387676 = r28387657 <= r28387675;
        double r28387677 = 0.5;
        double r28387678 = r28387657 * r28387657;
        double r28387679 = r28387677 * r28387678;
        double r28387680 = r28387679 + r28387657;
        double r28387681 = r28387680 * r28387662;
        double r28387682 = r28387681 + r28387664;
        double r28387683 = log(r28387682);
        double r28387684 = r28387683 / r28387672;
        double r28387685 = r28387660 - r28387684;
        double r28387686 = 1.6081434733570535e-109;
        bool r28387687 = r28387657 <= r28387686;
        double r28387688 = r28387662 * r28387657;
        double r28387689 = r28387688 / r28387672;
        double r28387690 = r28387689 * r28387664;
        double r28387691 = r28387688 * r28387657;
        double r28387692 = 0.5;
        double r28387693 = r28387691 * r28387692;
        double r28387694 = r28387693 / r28387672;
        double r28387695 = r28387690 + r28387694;
        double r28387696 = r28387660 - r28387695;
        double r28387697 = 9.047911306874446e-17;
        bool r28387698 = r28387657 <= r28387697;
        double r28387699 = r28387698 ? r28387685 : r28387696;
        double r28387700 = r28387687 ? r28387696 : r28387699;
        double r28387701 = r28387676 ? r28387685 : r28387700;
        double r28387702 = r28387659 ? r28387674 : r28387701;
        return r28387702;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	24.7
Target	16.5
Herbie	8.9

\[\begin{array}{l} \mathbf{if}\;z \lt -2.8874623088207947 \cdot 10^{+119}:\\ \;\;\;\;\left(x - \frac{\frac{-0.5}{y \cdot t}}{z \cdot z}\right) - \frac{-0.5}{y \cdot t} \cdot \frac{\frac{2.0}{z}}{z \cdot z}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{\log \left(1.0 + z \cdot y\right)}{t}\\ \end{array}\]

Derivation

1. Split input into 3 regimes

2. if z < -6.220564919949488e-06

   1. Initial program 12.9

      \[x - \frac{\log \left(\left(1.0 - y\right) + y \cdot e^{z}\right)}{t}\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 13.0

      \[\leadsto x - \frac{\log \color{blue}{\left(\left(\sqrt[3]{\left(1.0 - y\right) + y \cdot e^{z}} \cdot \sqrt[3]{\left(1.0 - y\right) + y \cdot e^{z}}\right) \cdot \sqrt[3]{\left(1.0 - y\right) + y \cdot e^{z}}\right)}}{t}\]

   4. Applied log-prod 13.0

      \[\leadsto x - \frac{\color{blue}{\log \left(\sqrt[3]{\left(1.0 - y\right) + y \cdot e^{z}} \cdot \sqrt[3]{\left(1.0 - y\right) + y \cdot e^{z}}\right) + \log \left(\sqrt[3]{\left(1.0 - y\right) + y \cdot e^{z}}\right)}}{t}\]

   if -6.220564919949488e-06 < z < -7.588076395555027e-93 or 1.6081434733570535e-109 < z < 9.047911306874446e-17

   1. Initial program 30.2

      \[x - \frac{\log \left(\left(1.0 - y\right) + y \cdot e^{z}\right)}{t}\]

   2. Taylor expanded around 0 11.3

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

   3. Simplified 11.3

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

   if -7.588076395555027e-93 < z < 1.6081434733570535e-109 or 9.047911306874446e-17 < z

   1. Initial program 29.8

      \[x - \frac{\log \left(\left(1.0 - y\right) + y \cdot e^{z}\right)}{t}\]

   2. Taylor expanded around 0 5.6

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

   3. Simplified 5.6

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

   5. Applied add-cube-cbrt 5.6

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

   6. Applied associate-*l* 5.6

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

   7. Applied associate-*l* 5.6

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

   8. Applied add-cube-cbrt 5.8

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

   9. Applied associate-*l* 5.8

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

   10. Applied distribute-lft-out 5.8

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

   11. Applied associate-*r* 5.8

       \[\leadsto x - \frac{\log 1.0 + \color{blue}{\left(y \cdot \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right) \cdot \left(\sqrt[3]{z} \cdot 1.0 + \left(\sqrt[3]{z} \cdot z\right) \cdot 0.5\right)}}{t}\]
   12. Using strategy rm

   13. Applied insert-posit16 5.8

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

   14. Taylor expanded around inf 5.6

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

   15. Simplified 5.6

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

4. Final simplification 8.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -6.220564919949488 \cdot 10^{-06}:\\ \;\;\;\;x - \frac{\log \left(\sqrt[3]{e^{z} \cdot y + \left(1.0 - y\right)} \cdot \sqrt[3]{e^{z} \cdot y + \left(1.0 - y\right)}\right) + \log \left(\sqrt[3]{e^{z} \cdot y + \left(1.0 - y\right)}\right)}{t}\\ \mathbf{elif}\;z \le -7.588076395555027 \cdot 10^{-93}:\\ \;\;\;\;x - \frac{\log \left(\left(\frac{1}{2} \cdot \left(z \cdot z\right) + z\right) \cdot y + 1.0\right)}{t}\\ \mathbf{elif}\;z \le 1.6081434733570535 \cdot 10^{-109}:\\ \;\;\;\;x - \left(\frac{y \cdot z}{t} \cdot 1.0 + \frac{\left(\left(y \cdot z\right) \cdot z\right) \cdot 0.5}{t}\right)\\ \mathbf{elif}\;z \le 9.047911306874446 \cdot 10^{-17}:\\ \;\;\;\;x - \frac{\log \left(\left(\frac{1}{2} \cdot \left(z \cdot z\right) + z\right) \cdot y + 1.0\right)}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \left(\frac{y \cdot z}{t} \cdot 1.0 + \frac{\left(\left(y \cdot z\right) \cdot z\right) \cdot 0.5}{t}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019158 
(FPCore (x y z t)
  :name "System.Random.MWC.Distributions:truncatedExp from mwc-random-0.13.3.2"

  :herbie-target
  (if (< z -2.8874623088207947e+119) (- (- x (/ (/ (- 0.5) (* y t)) (* z z))) (* (/ (- 0.5) (* y t)) (/ (/ 2.0 z) (* z z)))) (- x (/ (log (+ 1.0 (* z y))) t)))

  (- x (/ (log (+ (- 1.0 y) (* y (exp z)))) t)))