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

Average Error: 25.0 → 8.2

Time: 30.7s

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(\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(\sqrt[3]{\frac{z \cdot z}{t}} \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)\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 r18003371 = x;
        double r18003372 = 1.0;
        double r18003373 = y;
        double r18003374 = r18003372 - r18003373;
        double r18003375 = z;
        double r18003376 = exp(r18003375);
        double r18003377 = r18003373 * r18003376;
        double r18003378 = r18003374 + r18003377;
        double r18003379 = log(r18003378);
        double r18003380 = t;
        double r18003381 = r18003379 / r18003380;
        double r18003382 = r18003371 - r18003381;
        return r18003382;
}

↓

double f(double x, double y, double z, double t) {
        double r18003383 = z;
        double r18003384 = -8.054592668207058e-08;
        bool r18003385 = r18003383 <= r18003384;
        double r18003386 = x;
        double r18003387 = exp(r18003383);
        double r18003388 = y;
        double r18003389 = r18003387 * r18003388;
        double r18003390 = 1.0;
        double r18003391 = r18003390 - r18003388;
        double r18003392 = r18003389 + r18003391;
        double r18003393 = log(r18003392);
        double r18003394 = sqrt(r18003393);
        double r18003395 = t;
        double r18003396 = r18003394 / r18003395;
        double r18003397 = r18003394 * r18003396;
        double r18003398 = r18003386 - r18003397;
        double r18003399 = r18003383 * r18003383;
        double r18003400 = r18003399 / r18003395;
        double r18003401 = cbrt(r18003400);
        double r18003402 = cbrt(r18003401);
        double r18003403 = r18003402 * r18003402;
        double r18003404 = r18003403 * r18003402;
        double r18003405 = r18003401 * r18003404;
        double r18003406 = r18003404 * r18003405;
        double r18003407 = r18003406 * r18003388;
        double r18003408 = 0.5;
        double r18003409 = r18003407 * r18003408;
        double r18003410 = log(r18003390);
        double r18003411 = r18003410 / r18003395;
        double r18003412 = r18003383 / r18003395;
        double r18003413 = r18003412 * r18003388;
        double r18003414 = r18003413 * r18003390;
        double r18003415 = r18003411 + r18003414;
        double r18003416 = r18003409 + r18003415;
        double r18003417 = r18003386 - r18003416;
        double r18003418 = r18003385 ? r18003398 : r18003417;
        return r18003418;
}

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(\sqrt[3]{\frac{z \cdot z}{t}} \cdot \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 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(\sqrt[3]{\frac{z \cdot z}{t}} \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 \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 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(\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(\sqrt[3]{\frac{z \cdot z}{t}} \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)\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)))