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

Average Error: 24.9 → 8.1

Time: 9.0s

Precision: 64

• could not determine a ground truth for program body

  1. x = -6.050923431929025e+261
  2. y = 2.472377748022429e+223
  3. z = 4.7378067628763807e+139
  4. t = 2.0449168201690372e+88

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -1.766361136059460879010885037132538855076:\\ \;\;\;\;x - \frac{2 \cdot \log \left(\sqrt[3]{\left(1 - y\right) + y \cdot e^{z}}\right) + \log \left(\sqrt[3]{\left(1 - y\right) + y \cdot e^{z}}\right)}{t}\\ \mathbf{elif}\;z \le -2.053133900874357191048429833191280385263 \cdot 10^{-126}:\\ \;\;\;\;x - \frac{\log \left(1 + y \cdot \left(\frac{1}{2} \cdot {z}^{2} + z\right)\right)}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \left(1 \cdot \left(\frac{\frac{\sqrt[3]{z} \cdot \sqrt[3]{z}}{\sqrt[3]{t}}}{1} \cdot \left(\frac{\frac{\sqrt[3]{z}}{\sqrt[3]{t}}}{\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)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r233923 = x;
        double r233924 = 1.0;
        double r233925 = y;
        double r233926 = r233924 - r233925;
        double r233927 = z;
        double r233928 = exp(r233927);
        double r233929 = r233925 * r233928;
        double r233930 = r233926 + r233929;
        double r233931 = log(r233930);
        double r233932 = t;
        double r233933 = r233931 / r233932;
        double r233934 = r233923 - r233933;
        return r233934;
}

↓

double f(double x, double y, double z, double t) {
        double r233935 = z;
        double r233936 = -1.7663611360594609;
        bool r233937 = r233935 <= r233936;
        double r233938 = x;
        double r233939 = 2.0;
        double r233940 = 1.0;
        double r233941 = y;
        double r233942 = r233940 - r233941;
        double r233943 = exp(r233935);
        double r233944 = r233941 * r233943;
        double r233945 = r233942 + r233944;
        double r233946 = cbrt(r233945);
        double r233947 = log(r233946);
        double r233948 = r233939 * r233947;
        double r233949 = r233948 + r233947;
        double r233950 = t;
        double r233951 = r233949 / r233950;
        double r233952 = r233938 - r233951;
        double r233953 = -2.0531339008743572e-126;
        bool r233954 = r233935 <= r233953;
        double r233955 = 0.5;
        double r233956 = pow(r233935, r233939);
        double r233957 = r233955 * r233956;
        double r233958 = r233957 + r233935;
        double r233959 = r233941 * r233958;
        double r233960 = r233940 + r233959;
        double r233961 = log(r233960);
        double r233962 = r233961 / r233950;
        double r233963 = r233938 - r233962;
        double r233964 = cbrt(r233935);
        double r233965 = r233964 * r233964;
        double r233966 = cbrt(r233950);
        double r233967 = r233965 / r233966;
        double r233968 = 1.0;
        double r233969 = r233967 / r233968;
        double r233970 = r233964 / r233966;
        double r233971 = r233966 * r233966;
        double r233972 = cbrt(r233971);
        double r233973 = r233970 / r233972;
        double r233974 = cbrt(r233966);
        double r233975 = r233941 / r233974;
        double r233976 = r233973 * r233975;
        double r233977 = r233969 * r233976;
        double r233978 = r233940 * r233977;
        double r233979 = log(r233940);
        double r233980 = r233979 / r233950;
        double r233981 = 0.5;
        double r233982 = r233956 * r233941;
        double r233983 = r233982 / r233950;
        double r233984 = r233981 * r233983;
        double r233985 = r233980 + r233984;
        double r233986 = r233978 + r233985;
        double r233987 = r233938 - r233986;
        double r233988 = r233954 ? r233963 : r233987;
        double r233989 = r233937 ? r233952 : r233988;
        return r233989;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	24.9
Target	15.8
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 3 regimes

2. if z < -1.7663611360594609

   1. Initial program 11.0

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

   3. Applied add-cube-cbrt 11.1

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

   4. Applied log-prod 11.1

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

   5. Simplified 11.1

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

   if -1.7663611360594609 < z < -2.0531339008743572e-126

   1. Initial program 29.1

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

   2. Taylor expanded around 0 11.7

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

   3. Simplified 11.7

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

   if -2.0531339008743572e-126 < z

   1. Initial program 30.9

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

   2. Taylor expanded around 0 6.4

      \[\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 6.6

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

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

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

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

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

       \[\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* 5.8

       \[\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 5.8

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

   14. Applied *-un-lft-identity 5.8

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

   15. Applied add-cube-cbrt 5.8

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

   16. Applied times-frac 5.8

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

   17. Applied times-frac 5.8

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

   18. Applied associate-*l* 5.8

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

4. Final simplification 8.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.766361136059460879010885037132538855076:\\ \;\;\;\;x - \frac{2 \cdot \log \left(\sqrt[3]{\left(1 - y\right) + y \cdot e^{z}}\right) + \log \left(\sqrt[3]{\left(1 - y\right) + y \cdot e^{z}}\right)}{t}\\ \mathbf{elif}\;z \le -2.053133900874357191048429833191280385263 \cdot 10^{-126}:\\ \;\;\;\;x - \frac{\log \left(1 + y \cdot \left(\frac{1}{2} \cdot {z}^{2} + z\right)\right)}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \left(1 \cdot \left(\frac{\frac{\sqrt[3]{z} \cdot \sqrt[3]{z}}{\sqrt[3]{t}}}{1} \cdot \left(\frac{\frac{\sqrt[3]{z}}{\sqrt[3]{t}}}{\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)\\ \end{array}\]

Reproduce

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