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

Average Error: 24.2 → 8.1

Time: 31.2s

Precision: 64

• could not determine a ground truth for program body

  1. x = 3.379991150789451e-273
  2. y = 5.835692568832242e+286
  3. z = 2.9416708834442995e+86
  4. t = 4.963435863499958e-264

Math

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

↓

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

C

double f(double x, double y, double z, double t) {
        double r209232 = x;
        double r209233 = 1.0;
        double r209234 = y;
        double r209235 = r209233 - r209234;
        double r209236 = z;
        double r209237 = exp(r209236);
        double r209238 = r209234 * r209237;
        double r209239 = r209235 + r209238;
        double r209240 = log(r209239);
        double r209241 = t;
        double r209242 = r209240 / r209241;
        double r209243 = r209232 - r209242;
        return r209243;
}

↓

double f(double x, double y, double z, double t) {
        double r209244 = z;
        double r209245 = -1.9853915267026948e-05;
        bool r209246 = r209244 <= r209245;
        double r209247 = x;
        double r209248 = 1.0;
        double r209249 = y;
        double r209250 = r209248 - r209249;
        double r209251 = exp(r209244);
        double r209252 = r209249 * r209251;
        double r209253 = cbrt(r209252);
        double r209254 = r209253 * r209253;
        double r209255 = r209254 * r209253;
        double r209256 = r209250 + r209255;
        double r209257 = log(r209256);
        double r209258 = t;
        double r209259 = r209257 / r209258;
        double r209260 = r209247 - r209259;
        double r209261 = cbrt(r209258);
        double r209262 = r209244 / r209261;
        double r209263 = r209262 / r209261;
        double r209264 = r209261 * r209261;
        double r209265 = cbrt(r209264);
        double r209266 = r209263 / r209265;
        double r209267 = cbrt(r209261);
        double r209268 = r209249 / r209267;
        double r209269 = r209266 * r209268;
        double r209270 = r209248 * r209269;
        double r209271 = log(r209248);
        double r209272 = r209271 / r209258;
        double r209273 = 0.5;
        double r209274 = 2.0;
        double r209275 = pow(r209244, r209274);
        double r209276 = r209275 * r209249;
        double r209277 = r209276 / r209258;
        double r209278 = r209273 * r209277;
        double r209279 = r209272 + r209278;
        double r209280 = r209270 + r209279;
        double r209281 = r209247 - r209280;
        double r209282 = r209246 ? r209260 : r209281;
        return r209282;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	24.2
Target	15.7
Herbie	8.1

\[\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 < -1.9853915267026948e-05

   1. Initial program 11.4

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

   3. Applied add-cube-cbrt 11.4

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

   if -1.9853915267026948e-05 < z

   1. Initial program 29.7

      \[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(\frac{\log 1}{t} + 0.5 \cdot \frac{{z}^{2} \cdot y}{t}\right)\right)}\]
   3. Using strategy rm

   4. Applied add-cube-cbrt 7.2

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

   5. Applied times-frac 6.7

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

   7. Applied add-cube-cbrt 6.7

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

   8. Applied cbrt-prod 6.8

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

   9. Applied *-un-lft-identity 6.8

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

   10. Applied times-frac 6.8

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

   11. Applied associate-*r* 6.6

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

   12. Simplified 6.6

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

4. Final simplification 8.1

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

Reproduce

herbie shell --seed 2019212 
(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.88746230882079466e119) (- (- 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)))