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

Average Error: 24.6 → 8.4

Time: 21.7s

Precision: 64

• could not determine a ground truth for program body

  1. x = -1.9017384484022065e-162
  2. y = 7.770140023185365e-109
  3. z = 4.8665449650161257e+157
  4. t = -3.590079466279191e-232

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -6.310119903545574434291526250400899439411 \cdot 10^{-134}:\\ \;\;\;\;x - \frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \mathsf{fma}\left(\frac{z \cdot y}{t}, 1, \mathsf{fma}\left(\frac{{z}^{2} \cdot y}{t}, 0.5, \frac{\log 1}{t}\right)\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r146724 = x;
        double r146725 = 1.0;
        double r146726 = y;
        double r146727 = r146725 - r146726;
        double r146728 = z;
        double r146729 = exp(r146728);
        double r146730 = r146726 * r146729;
        double r146731 = r146727 + r146730;
        double r146732 = log(r146731);
        double r146733 = t;
        double r146734 = r146732 / r146733;
        double r146735 = r146724 - r146734;
        return r146735;
}

↓

double f(double x, double y, double z, double t) {
        double r146736 = z;
        double r146737 = -6.310119903545574e-134;
        bool r146738 = r146736 <= r146737;
        double r146739 = x;
        double r146740 = expm1(r146736);
        double r146741 = y;
        double r146742 = 1.0;
        double r146743 = fma(r146740, r146741, r146742);
        double r146744 = log(r146743);
        double r146745 = t;
        double r146746 = r146744 / r146745;
        double r146747 = r146739 - r146746;
        double r146748 = r146736 * r146741;
        double r146749 = r146748 / r146745;
        double r146750 = 2.0;
        double r146751 = pow(r146736, r146750);
        double r146752 = r146751 * r146741;
        double r146753 = r146752 / r146745;
        double r146754 = 0.5;
        double r146755 = log(r146742);
        double r146756 = r146755 / r146745;
        double r146757 = fma(r146753, r146754, r146756);
        double r146758 = fma(r146749, r146742, r146757);
        double r146759 = r146739 - r146758;
        double r146760 = r146738 ? r146747 : r146759;
        return r146760;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	24.6
Target	16.1
Herbie	8.4

\[\begin{array}{l} \mathbf{if}\;z \lt -2.887462308820794658905265984545350618896 \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 2 regimes

2. if z < -6.310119903545574e-134

   1. Initial program 16.9

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

   2. Simplified 11.6

      \[\leadsto \color{blue}{x - \frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{t}}\]
   3. Using strategy rm

   4. Applied div-inv 11.6

      \[\leadsto x - \color{blue}{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right) \cdot \frac{1}{t}}\]
   5. Using strategy rm

   6. Applied pow1 11.6

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

   7. Applied pow1 11.6

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

   8. Applied pow-prod-down 11.6

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

   9. Simplified 11.6

      \[\leadsto x - {\color{blue}{\left(\frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{t}\right)}}^{1}\]

   if -6.310119903545574e-134 < z

   1. Initial program 30.4

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

   2. Simplified 11.2

      \[\leadsto \color{blue}{x - \frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{t}}\]
   3. Using strategy rm

   4. Applied div-inv 11.2

      \[\leadsto x - \color{blue}{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right) \cdot \frac{1}{t}}\]
   5. Using strategy rm

   6. Applied pow1 11.2

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

   7. Applied pow1 11.2

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

   8. Applied pow-prod-down 11.2

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

   9. Simplified 11.2

      \[\leadsto x - {\color{blue}{\left(\frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{t}\right)}}^{1}\]

   10. Taylor expanded around 0 6.0

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

   11. Simplified 6.0

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

4. Final simplification 8.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -6.310119903545574434291526250400899439411 \cdot 10^{-134}:\\ \;\;\;\;x - \frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \mathsf{fma}\left(\frac{z \cdot y}{t}, 1, \mathsf{fma}\left(\frac{{z}^{2} \cdot y}{t}, 0.5, \frac{\log 1}{t}\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019323 +o rules:numerics
(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)))