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

Average Error: 24.7 → 14.7

Time: 13.4s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

• could not determine a ground truth for program body

  1. x = 2.2108085494553437e+120
  2. y = 7.734281002290599e-114
  3. z = 3.1637604227072965e+33
  4. t = 1.0286577002489468e+63

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;y \le -2.5270627226614018 \cdot 10^{169}:\\ \;\;\;\;x - \left(\left(\frac{\log \left(1 - e^{z}\right)}{t} - \frac{1}{\left(1 - e^{z}\right) \cdot \left(y \cdot t\right)}\right) - \frac{\log \left(\frac{-1}{y}\right)}{t}\right)\\ \mathbf{elif}\;y \le -9.549534903802116 \cdot 10^{119}:\\ \;\;\;\;x - \frac{\log \left(1 + y \cdot \left(\left(\frac{1}{6} \cdot {z}^{3} + z\right) + \frac{1}{2} \cdot {z}^{2}\right)\right)}{t}\\ \mathbf{elif}\;y \le -3.040180749931492 \cdot 10^{103}:\\ \;\;\;\;x - \frac{1}{1 \cdot \frac{t}{\left(1 - e^{z}\right) \cdot \left({\left(\log \left(1 - e^{z}\right) - \log \left(\frac{-1}{y}\right)\right)}^{2} \cdot y\right)} + \left(\frac{t}{\log \left(1 - e^{z}\right) - \log \left(\frac{-1}{y}\right)} + \left(0.5 \cdot \frac{t}{{\left(1 - e^{z}\right)}^{2} \cdot \left({\left(\log \left(1 - e^{z}\right) - \log \left(\frac{-1}{y}\right)\right)}^{2} \cdot {y}^{2}\right)} + 1 \cdot \frac{t}{{\left(1 - e^{z}\right)}^{2} \cdot \left({\left(\log \left(1 - e^{z}\right) - \log \left(\frac{-1}{y}\right)\right)}^{3} \cdot {y}^{2}\right)}\right)\right)}\\ \mathbf{elif}\;y \le 5.7372239521816668 \cdot 10^{-78}:\\ \;\;\;\;x - \frac{1}{\frac{t}{\log \left({1}^{3} + {\left(y \cdot e^{z} - y\right)}^{3}\right) - \left(\sqrt[3]{\log \left(1 \cdot 1 + \left(y \cdot e^{z} - y\right) \cdot \left(\left(y \cdot e^{z} - y\right) - 1\right)\right)} \cdot \sqrt[3]{\log \left(1 \cdot 1 + \left(y \cdot e^{z} - y\right) \cdot \left(\left(y \cdot e^{z} - y\right) - 1\right)\right)}\right) \cdot \sqrt[3]{\log \left(1 \cdot 1 + \left(y \cdot e^{z} - y\right) \cdot \left(\left(y \cdot e^{z} - y\right) - 1\right)\right)}}}\\ \mathbf{elif}\;y \le 1.3746508246750045 \cdot 10^{113}:\\ \;\;\;\;x - \frac{y \cdot \left(z \cdot \left(0.5 \cdot z + 1\right)\right) + \log 1}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{\log \left(1 + y \cdot \left(\left(\frac{1}{6} \cdot {z}^{3} + z\right) + \frac{1}{2} \cdot {z}^{2}\right)\right)}{t}\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r363637 = x;
        double r363638 = 1.0;
        double r363639 = y;
        double r363640 = r363638 - r363639;
        double r363641 = z;
        double r363642 = exp(r363641);
        double r363643 = r363639 * r363642;
        double r363644 = r363640 + r363643;
        double r363645 = log(r363644);
        double r363646 = t;
        double r363647 = r363645 / r363646;
        double r363648 = r363637 - r363647;
        return r363648;
}

↓

double f(double x, double y, double z, double t) {
        double r363649 = y;
        double r363650 = -2.5270627226614018e+169;
        bool r363651 = r363649 <= r363650;
        double r363652 = x;
        double r363653 = 1.0;
        double r363654 = z;
        double r363655 = exp(r363654);
        double r363656 = r363653 - r363655;
        double r363657 = log(r363656);
        double r363658 = t;
        double r363659 = r363657 / r363658;
        double r363660 = 1.0;
        double r363661 = r363649 * r363658;
        double r363662 = r363656 * r363661;
        double r363663 = r363660 / r363662;
        double r363664 = r363659 - r363663;
        double r363665 = -1.0;
        double r363666 = r363665 / r363649;
        double r363667 = log(r363666);
        double r363668 = r363667 / r363658;
        double r363669 = r363664 - r363668;
        double r363670 = r363652 - r363669;
        double r363671 = -9.549534903802116e+119;
        bool r363672 = r363649 <= r363671;
        double r363673 = 0.16666666666666666;
        double r363674 = 3.0;
        double r363675 = pow(r363654, r363674);
        double r363676 = r363673 * r363675;
        double r363677 = r363676 + r363654;
        double r363678 = 0.5;
        double r363679 = 2.0;
        double r363680 = pow(r363654, r363679);
        double r363681 = r363678 * r363680;
        double r363682 = r363677 + r363681;
        double r363683 = r363649 * r363682;
        double r363684 = r363660 + r363683;
        double r363685 = log(r363684);
        double r363686 = r363685 / r363658;
        double r363687 = r363652 - r363686;
        double r363688 = -3.040180749931492e+103;
        bool r363689 = r363649 <= r363688;
        double r363690 = r363657 - r363667;
        double r363691 = pow(r363690, r363679);
        double r363692 = r363691 * r363649;
        double r363693 = r363656 * r363692;
        double r363694 = r363658 / r363693;
        double r363695 = r363660 * r363694;
        double r363696 = r363658 / r363690;
        double r363697 = 0.5;
        double r363698 = pow(r363656, r363679);
        double r363699 = pow(r363649, r363679);
        double r363700 = r363691 * r363699;
        double r363701 = r363698 * r363700;
        double r363702 = r363658 / r363701;
        double r363703 = r363697 * r363702;
        double r363704 = pow(r363690, r363674);
        double r363705 = r363704 * r363699;
        double r363706 = r363698 * r363705;
        double r363707 = r363658 / r363706;
        double r363708 = r363660 * r363707;
        double r363709 = r363703 + r363708;
        double r363710 = r363696 + r363709;
        double r363711 = r363695 + r363710;
        double r363712 = r363653 / r363711;
        double r363713 = r363652 - r363712;
        double r363714 = 5.737223952181667e-78;
        bool r363715 = r363649 <= r363714;
        double r363716 = pow(r363660, r363674);
        double r363717 = r363649 * r363655;
        double r363718 = r363717 - r363649;
        double r363719 = pow(r363718, r363674);
        double r363720 = r363716 + r363719;
        double r363721 = log(r363720);
        double r363722 = r363660 * r363660;
        double r363723 = r363718 - r363660;
        double r363724 = r363718 * r363723;
        double r363725 = r363722 + r363724;
        double r363726 = log(r363725);
        double r363727 = cbrt(r363726);
        double r363728 = r363727 * r363727;
        double r363729 = r363728 * r363727;
        double r363730 = r363721 - r363729;
        double r363731 = r363658 / r363730;
        double r363732 = r363653 / r363731;
        double r363733 = r363652 - r363732;
        double r363734 = 1.3746508246750045e+113;
        bool r363735 = r363649 <= r363734;
        double r363736 = r363697 * r363654;
        double r363737 = r363736 + r363660;
        double r363738 = r363654 * r363737;
        double r363739 = r363649 * r363738;
        double r363740 = log(r363660);
        double r363741 = r363739 + r363740;
        double r363742 = r363741 / r363658;
        double r363743 = r363652 - r363742;
        double r363744 = r363735 ? r363743 : r363687;
        double r363745 = r363715 ? r363733 : r363744;
        double r363746 = r363689 ? r363713 : r363745;
        double r363747 = r363672 ? r363687 : r363746;
        double r363748 = r363651 ? r363670 : r363747;
        return r363748;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	24.7
Target	16.3
Herbie	14.7

\[\begin{array}{l} \mathbf{if}\;z \lt -2.88746230882079466 \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}{z}}{z \cdot z}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{\log \left(1 + z \cdot y\right)}{t}\\ \end{array}\]

Derivation

1. Split input into 5 regimes

2. if y < -2.5270627226614018e+169

   1. Initial program 33.5

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

   3. Applied sub-neg 33.5

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

   4. Applied associate-+l+ 16.0

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

   5. Simplified 16.0

      \[\leadsto x - \frac{\log \left(1 + \color{blue}{\left(y \cdot e^{z} - y\right)}\right)}{t}\]
   6. Using strategy rm

   7. Applied clear-num 16.0

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

   8. Taylor expanded around -inf 33.5

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

   9. Simplified 33.5

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

   if -2.5270627226614018e+169 < y < -9.549534903802116e+119 or 1.3746508246750045e+113 < y

   1. Initial program 53.7

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

   3. Applied sub-neg 53.7

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

   4. Applied associate-+l+ 22.9

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

   5. Simplified 22.9

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

   6. Taylor expanded around 0 18.3

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

   7. Simplified 18.3

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

   if -9.549534903802116e+119 < y < -3.040180749931492e+103

   1. Initial program 40.9

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

   3. Applied sub-neg 40.9

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

   4. Applied associate-+l+ 18.6

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

   5. Simplified 18.6

      \[\leadsto x - \frac{\log \left(1 + \color{blue}{\left(y \cdot e^{z} - y\right)}\right)}{t}\]
   6. Using strategy rm

   7. Applied clear-num 18.6

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

   8. Taylor expanded around -inf 41.0

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

   if -3.040180749931492e+103 < y < 5.737223952181667e-78

   1. Initial program 14.7

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

   3. Applied sub-neg 14.7

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

   4. Applied associate-+l+ 11.1

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

   5. Simplified 11.1

      \[\leadsto x - \frac{\log \left(1 + \color{blue}{\left(y \cdot e^{z} - y\right)}\right)}{t}\]
   6. Using strategy rm

   7. Applied clear-num 11.1

      \[\leadsto x - \color{blue}{\frac{1}{\frac{t}{\log \left(1 + \left(y \cdot e^{z} - y\right)\right)}}}\]
   8. Using strategy rm

   9. Applied flip3-+ 11.2

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

   10. Applied log-div 11.2

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

   11. Simplified 11.2

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

   13. Applied add-cube-cbrt 11.2

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

   if 5.737223952181667e-78 < y < 1.3746508246750045e+113

   1. Initial program 36.0

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

   2. Taylor expanded around 0 11.4

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

   3. Simplified 11.4

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

4. Final simplification 14.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -2.5270627226614018 \cdot 10^{169}:\\ \;\;\;\;x - \left(\left(\frac{\log \left(1 - e^{z}\right)}{t} - \frac{1}{\left(1 - e^{z}\right) \cdot \left(y \cdot t\right)}\right) - \frac{\log \left(\frac{-1}{y}\right)}{t}\right)\\ \mathbf{elif}\;y \le -9.549534903802116 \cdot 10^{119}:\\ \;\;\;\;x - \frac{\log \left(1 + y \cdot \left(\left(\frac{1}{6} \cdot {z}^{3} + z\right) + \frac{1}{2} \cdot {z}^{2}\right)\right)}{t}\\ \mathbf{elif}\;y \le -3.040180749931492 \cdot 10^{103}:\\ \;\;\;\;x - \frac{1}{1 \cdot \frac{t}{\left(1 - e^{z}\right) \cdot \left({\left(\log \left(1 - e^{z}\right) - \log \left(\frac{-1}{y}\right)\right)}^{2} \cdot y\right)} + \left(\frac{t}{\log \left(1 - e^{z}\right) - \log \left(\frac{-1}{y}\right)} + \left(0.5 \cdot \frac{t}{{\left(1 - e^{z}\right)}^{2} \cdot \left({\left(\log \left(1 - e^{z}\right) - \log \left(\frac{-1}{y}\right)\right)}^{2} \cdot {y}^{2}\right)} + 1 \cdot \frac{t}{{\left(1 - e^{z}\right)}^{2} \cdot \left({\left(\log \left(1 - e^{z}\right) - \log \left(\frac{-1}{y}\right)\right)}^{3} \cdot {y}^{2}\right)}\right)\right)}\\ \mathbf{elif}\;y \le 5.7372239521816668 \cdot 10^{-78}:\\ \;\;\;\;x - \frac{1}{\frac{t}{\log \left({1}^{3} + {\left(y \cdot e^{z} - y\right)}^{3}\right) - \left(\sqrt[3]{\log \left(1 \cdot 1 + \left(y \cdot e^{z} - y\right) \cdot \left(\left(y \cdot e^{z} - y\right) - 1\right)\right)} \cdot \sqrt[3]{\log \left(1 \cdot 1 + \left(y \cdot e^{z} - y\right) \cdot \left(\left(y \cdot e^{z} - y\right) - 1\right)\right)}\right) \cdot \sqrt[3]{\log \left(1 \cdot 1 + \left(y \cdot e^{z} - y\right) \cdot \left(\left(y \cdot e^{z} - y\right) - 1\right)\right)}}}\\ \mathbf{elif}\;y \le 1.3746508246750045 \cdot 10^{113}:\\ \;\;\;\;x - \frac{y \cdot \left(z \cdot \left(0.5 \cdot z + 1\right)\right) + \log 1}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{\log \left(1 + y \cdot \left(\left(\frac{1}{6} \cdot {z}^{3} + z\right) + \frac{1}{2} \cdot {z}^{2}\right)\right)}{t}\\ \end{array}\]

Reproduce

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

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

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