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

Average Error: 24.7 → 9.2

Time: 40.8s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

• could not determine a ground truth for program body

  1. x = 2.2108085494553437e+120
  2. y = 7.734281002290599e-114
  3. z = 3.1637604227072965e+33
  4. t = 1.0286577002489468e+63

Math

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

↓

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

C

double f(double x, double y, double z, double t) {
        double r323809 = x;
        double r323810 = 1.0;
        double r323811 = y;
        double r323812 = r323810 - r323811;
        double r323813 = z;
        double r323814 = exp(r323813);
        double r323815 = r323811 * r323814;
        double r323816 = r323812 + r323815;
        double r323817 = log(r323816);
        double r323818 = t;
        double r323819 = r323817 / r323818;
        double r323820 = r323809 - r323819;
        return r323820;
}

↓

double f(double x, double y, double z, double t) {
        double r323821 = z;
        double r323822 = -3.1117629263050896e+22;
        bool r323823 = r323821 <= r323822;
        double r323824 = x;
        double r323825 = 1.0;
        double r323826 = 1.0;
        double r323827 = exp(r323821);
        double r323828 = r323826 - r323827;
        double r323829 = y;
        double r323830 = r323828 * r323829;
        double r323831 = r323825 - r323830;
        double r323832 = log(r323831);
        double r323833 = t;
        double r323834 = r323832 / r323833;
        double r323835 = r323824 - r323834;
        double r323836 = cbrt(r323835);
        double r323837 = r323836 * r323836;
        double r323838 = 2.0;
        double r323839 = cbrt(r323831);
        double r323840 = log(r323839);
        double r323841 = r323838 * r323840;
        double r323842 = r323841 + r323840;
        double r323843 = r323842 / r323833;
        double r323844 = r323824 - r323843;
        double r323845 = cbrt(r323844);
        double r323846 = r323837 * r323845;
        double r323847 = r323821 * r323829;
        double r323848 = r323847 / r323833;
        double r323849 = r323825 * r323848;
        double r323850 = log(r323825);
        double r323851 = r323850 / r323833;
        double r323852 = r323849 + r323851;
        double r323853 = r323824 - r323852;
        double r323854 = r323823 ? r323846 : r323853;
        return r323854;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	24.7
Target	16.3
Herbie	9.2

\[\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 < -3.1117629263050896e+22

   1. Initial program 11.2

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

   3. Applied associate-+l- 11.2

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

   4. Simplified 11.2

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

   6. Applied add-cube-cbrt 12.2

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

   8. Applied add-cube-cbrt 12.2

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

   9. Applied log-prod 12.2

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

   10. Simplified 12.2

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

   if -3.1117629263050896e+22 < z

   1. Initial program 30.1

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

   3. Applied associate-+l- 15.8

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

   4. Simplified 15.8

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

   5. Taylor expanded around 0 7.9

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

4. Final simplification 9.2

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

Reproduce

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