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

Average Error: 25.0 → 8.2

Time: 30.5s

Precision: 64

• could not determine a ground truth for program body

  1. x = 8.771067876955816e-28
  2. y = 1.1258782664716166e+107
  3. z = 7.706155067127394e+81
  4. t = 6.88703791615021e+280

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -8.054592668207057587662854028151548924086 \cdot 10^{-8}:\\ \;\;\;\;x - \sqrt{\log \left(e^{z} \cdot y + \left(1 - y\right)\right)} \cdot \frac{\sqrt{\log \left(e^{z} \cdot y + \left(1 - y\right)\right)}}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \left(\left(\left(\left(\left(\left(\sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}} \cdot \sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}}\right) \cdot \sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}}\right) \cdot \left(\left(\sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}} \cdot \sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}}\right) \cdot \sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}}\right)\right) \cdot \sqrt[3]{\frac{z \cdot z}{t}}\right) \cdot y\right) \cdot 0.5 + \left(\frac{\log 1}{t} + \left(\frac{z}{t} \cdot y\right) \cdot 1\right)\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r10979227 = x;
        double r10979228 = 1.0;
        double r10979229 = y;
        double r10979230 = r10979228 - r10979229;
        double r10979231 = z;
        double r10979232 = exp(r10979231);
        double r10979233 = r10979229 * r10979232;
        double r10979234 = r10979230 + r10979233;
        double r10979235 = log(r10979234);
        double r10979236 = t;
        double r10979237 = r10979235 / r10979236;
        double r10979238 = r10979227 - r10979237;
        return r10979238;
}

↓

double f(double x, double y, double z, double t) {
        double r10979239 = z;
        double r10979240 = -8.054592668207058e-08;
        bool r10979241 = r10979239 <= r10979240;
        double r10979242 = x;
        double r10979243 = exp(r10979239);
        double r10979244 = y;
        double r10979245 = r10979243 * r10979244;
        double r10979246 = 1.0;
        double r10979247 = r10979246 - r10979244;
        double r10979248 = r10979245 + r10979247;
        double r10979249 = log(r10979248);
        double r10979250 = sqrt(r10979249);
        double r10979251 = t;
        double r10979252 = r10979250 / r10979251;
        double r10979253 = r10979250 * r10979252;
        double r10979254 = r10979242 - r10979253;
        double r10979255 = r10979239 * r10979239;
        double r10979256 = r10979255 / r10979251;
        double r10979257 = cbrt(r10979256);
        double r10979258 = cbrt(r10979257);
        double r10979259 = r10979258 * r10979258;
        double r10979260 = r10979259 * r10979258;
        double r10979261 = r10979260 * r10979260;
        double r10979262 = r10979261 * r10979257;
        double r10979263 = r10979262 * r10979244;
        double r10979264 = 0.5;
        double r10979265 = r10979263 * r10979264;
        double r10979266 = log(r10979246);
        double r10979267 = r10979266 / r10979251;
        double r10979268 = r10979239 / r10979251;
        double r10979269 = r10979268 * r10979244;
        double r10979270 = r10979269 * r10979246;
        double r10979271 = r10979267 + r10979270;
        double r10979272 = r10979265 + r10979271;
        double r10979273 = r10979242 - r10979272;
        double r10979274 = r10979241 ? r10979254 : r10979273;
        return r10979274;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	25.0
Target	16.4
Herbie	8.2

\[\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 < -8.054592668207058e-08

   1. Initial program 11.9

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

   3. Applied *-un-lft-identity 11.9

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

   4. Applied add-sqr-sqrt 12.8

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

   5. Applied times-frac 12.8

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

   if -8.054592668207058e-08 < z

   1. Initial program 30.8

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

   2. Taylor expanded around 0 7.0

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

   3. Simplified 6.1

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

   5. Applied add-cube-cbrt 6.1

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

   7. Applied add-cube-cbrt 6.1

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

   9. Applied add-cube-cbrt 6.1

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

4. Final simplification 8.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -8.054592668207057587662854028151548924086 \cdot 10^{-8}:\\ \;\;\;\;x - \sqrt{\log \left(e^{z} \cdot y + \left(1 - y\right)\right)} \cdot \frac{\sqrt{\log \left(e^{z} \cdot y + \left(1 - y\right)\right)}}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \left(\left(\left(\left(\left(\left(\sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}} \cdot \sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}}\right) \cdot \sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}}\right) \cdot \left(\left(\sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}} \cdot \sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}}\right) \cdot \sqrt[3]{\sqrt[3]{\frac{z \cdot z}{t}}}\right)\right) \cdot \sqrt[3]{\frac{z \cdot z}{t}}\right) \cdot y\right) \cdot 0.5 + \left(\frac{\log 1}{t} + \left(\frac{z}{t} \cdot y\right) \cdot 1\right)\right)\\ \end{array}\]

Reproduce

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