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

Average Error: 25.4 → 8.1

Time: 26.9s

Precision: 64

• could not determine a ground truth for program body

  1. x = -1.1425440199203244e+248
  2. y = 2.000111729313626e+44
  3. z = 2.931459133389821e+208
  4. t = 3.625484546781197e-95

Math

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

↓

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

C

double f(double x, double y, double z, double t) {
        double r12658914 = x;
        double r12658915 = 1.0;
        double r12658916 = y;
        double r12658917 = r12658915 - r12658916;
        double r12658918 = z;
        double r12658919 = exp(r12658918);
        double r12658920 = r12658916 * r12658919;
        double r12658921 = r12658917 + r12658920;
        double r12658922 = log(r12658921);
        double r12658923 = t;
        double r12658924 = r12658922 / r12658923;
        double r12658925 = r12658914 - r12658924;
        return r12658925;
}

↓

double f(double x, double y, double z, double t) {
        double r12658926 = z;
        double r12658927 = exp(r12658926);
        double r12658928 = 0.9999999353825346;
        bool r12658929 = r12658927 <= r12658928;
        double r12658930 = x;
        double r12658931 = y;
        double r12658932 = 1.0;
        double r12658933 = r12658932 - r12658931;
        double r12658934 = fma(r12658931, r12658927, r12658933);
        double r12658935 = log(r12658934);
        double r12658936 = t;
        double r12658937 = cbrt(r12658936);
        double r12658938 = r12658937 * r12658937;
        double r12658939 = r12658935 / r12658938;
        double r12658940 = r12658939 / r12658937;
        double r12658941 = r12658930 - r12658940;
        double r12658942 = cbrt(r12658926);
        double r12658943 = r12658942 / r12658937;
        double r12658944 = r12658931 * r12658943;
        double r12658945 = r12658942 * r12658942;
        double r12658946 = r12658945 / r12658938;
        double r12658947 = r12658944 * r12658946;
        double r12658948 = r12658931 * r12658926;
        double r12658949 = r12658926 * r12658948;
        double r12658950 = r12658949 / r12658936;
        double r12658951 = 0.5;
        double r12658952 = log(r12658932);
        double r12658953 = r12658952 / r12658936;
        double r12658954 = fma(r12658950, r12658951, r12658953);
        double r12658955 = fma(r12658932, r12658947, r12658954);
        double r12658956 = cbrt(r12658955);
        double r12658957 = r12658956 * r12658956;
        double r12658958 = cbrt(r12658956);
        double r12658959 = r12658958 * r12658958;
        double r12658960 = r12658958 * r12658959;
        double r12658961 = r12658957 * r12658960;
        double r12658962 = r12658930 - r12658961;
        double r12658963 = r12658929 ? r12658941 : r12658962;
        return r12658963;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	25.4
Target	16.4
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 (exp z) < 0.9999999353825346

   1. Initial program 11.2

      \[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(y, e^{z}, 1 - y\right)\right)}{t}}\]
   3. Using strategy rm

   4. Applied add-cube-cbrt 11.4

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

   5. Applied associate-/r* 11.4

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

   if 0.9999999353825346 < (exp z)

   1. Initial program 31.8

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

   2. Simplified 31.8

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

   3. Taylor expanded around 0 7.2

      \[\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)}\]

   4. Simplified 6.5

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

   6. Applied add-cube-cbrt 6.7

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

   7. Applied add-cube-cbrt 6.8

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

   8. Applied times-frac 6.8

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

   9. Applied associate-*l* 6.5

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

   11. Applied add-cube-cbrt 6.5

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

   13. Applied add-cube-cbrt 6.6

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

4. Final simplification 8.1

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

Reproduce

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