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

Average Error: 25.0 → 8.3

Time: 8.3s

Precision: 64

• could not determine a ground truth for program body

  1. x = 4.650088164488972e+220
  2. y = 4.289362951266288e+268
  3. z = 1.553159897592075e+232
  4. t = 4.723375383158303e-115

Math

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

↓

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

C

double code(double x, double y, double z, double t) {
	return (x - (log(((1.0 - y) + (y * exp(z)))) / t));
}

↓

double code(double x, double y, double z, double t) {
	double VAR;
	if ((z <= -89.31439750200016)) {
		VAR = (x - (1.0 / (t / log(((1.0 - y) + (y * exp(z)))))));
	} else {
		VAR = (x - ((1.0 * ((cbrt((z / (cbrt(t) * cbrt(t)))) * ((cbrt(cbrt((z / (cbrt(t) * cbrt(t))))) * cbrt(cbrt((z / (cbrt(t) * cbrt(t)))))) * cbrt(cbrt((z / (cbrt(t) * cbrt(t))))))) * (cbrt((z / (cbrt(t) * cbrt(t)))) * (y / cbrt(t))))) + ((log(1.0) / t) + (0.5 * ((pow(z, 2.0) * y) / t)))));
	}
	return VAR;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	25.0
Target	16.5
Herbie	8.3

\[\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 2 regimes

2. if z < -89.31439750200016

   1. Initial program 11.7

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

   3. Applied clear-num 11.7

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

   if -89.31439750200016 < z

   1. Initial program 31.0

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

   2. Taylor expanded around 0 7.1

      \[\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.3

      \[\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.8

      \[\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.8

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

   8. Applied associate-*l* 6.8

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

   10. Applied add-cube-cbrt 6.8

       \[\leadsto x - \left(1 \cdot \left(\left(\sqrt[3]{\frac{z}{\sqrt[3]{t} \cdot \sqrt[3]{t}}} \cdot \color{blue}{\left(\left(\sqrt[3]{\sqrt[3]{\frac{z}{\sqrt[3]{t} \cdot \sqrt[3]{t}}}} \cdot \sqrt[3]{\sqrt[3]{\frac{z}{\sqrt[3]{t} \cdot \sqrt[3]{t}}}}\right) \cdot \sqrt[3]{\sqrt[3]{\frac{z}{\sqrt[3]{t} \cdot \sqrt[3]{t}}}}\right)}\right) \cdot \left(\sqrt[3]{\frac{z}{\sqrt[3]{t} \cdot \sqrt[3]{t}}} \cdot \frac{y}{\sqrt[3]{t}}\right)\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.3

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

Reproduce

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