Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, G

Average Error: 6.0 → 1.5

Time: 7.2s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;z \le 1609.50674842192324831557925790548324585 \lor \neg \left(z \le 3.956447898588514434000900140654028393961 \cdot 10^{51}\right):\\ \;\;\;\;x + \frac{e^{y \cdot \left(0 + 2 \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right)}}{\frac{y}{\frac{{\left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}^{y}}{1}}}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{e^{-1 \cdot z}}{y}\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r320229 = x;
        double r320230 = y;
        double r320231 = z;
        double r320232 = r320231 + r320230;
        double r320233 = r320230 / r320232;
        double r320234 = log(r320233);
        double r320235 = r320230 * r320234;
        double r320236 = exp(r320235);
        double r320237 = r320236 / r320230;
        double r320238 = r320229 + r320237;
        return r320238;
}

↓

double f(double x, double y, double z) {
        double r320239 = z;
        double r320240 = 1609.5067484219232;
        bool r320241 = r320239 <= r320240;
        double r320242 = 3.9564478985885144e+51;
        bool r320243 = r320239 <= r320242;
        double r320244 = !r320243;
        bool r320245 = r320241 || r320244;
        double r320246 = x;
        double r320247 = y;
        double r320248 = 0.0;
        double r320249 = 2.0;
        double r320250 = cbrt(r320247);
        double r320251 = r320239 + r320247;
        double r320252 = cbrt(r320251);
        double r320253 = r320250 / r320252;
        double r320254 = log(r320253);
        double r320255 = r320249 * r320254;
        double r320256 = r320248 + r320255;
        double r320257 = r320247 * r320256;
        double r320258 = exp(r320257);
        double r320259 = pow(r320253, r320247);
        double r320260 = 1.0;
        double r320261 = r320259 / r320260;
        double r320262 = r320247 / r320261;
        double r320263 = r320258 / r320262;
        double r320264 = r320246 + r320263;
        double r320265 = -1.0;
        double r320266 = r320265 * r320239;
        double r320267 = exp(r320266);
        double r320268 = r320267 / r320247;
        double r320269 = r320246 + r320268;
        double r320270 = r320245 ? r320264 : r320269;
        return r320270;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	6.0
Target	1.1
Herbie	1.5

\[\begin{array}{l} \mathbf{if}\;\frac{y}{z + y} \lt 7.115415759790762719541517221498726780517 \cdot 10^{-315}:\\ \;\;\;\;x + \frac{e^{\frac{-1}{z}}}{y}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{e^{\log \left({\left(\frac{y}{y + z}\right)}^{y}\right)}}{y}\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if z < 1609.5067484219232 or 3.9564478985885144e+51 < z

   1. Initial program 5.8

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

   3. Applied add-cube-cbrt 19.5

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

   4. Applied add-cube-cbrt 5.8

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

   5. Applied times-frac 5.8

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

   6. Applied log-prod 1.8

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

   7. Applied distribute-lft-in 1.8

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

   8. Applied exp-sum 1.8

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

   9. Applied associate-/l* 1.8

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

   10. Simplified 1.8

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

   12. Applied *-un-lft-identity 1.8

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

   13. Applied log-prod 1.8

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

   14. Simplified 1.8

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

   15. Simplified 0.8

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

   if 1609.5067484219232 < z < 3.9564478985885144e+51

   1. Initial program 9.2

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

   2. Taylor expanded around inf 15.9

      \[\leadsto \color{blue}{x + \frac{e^{-1 \cdot z}}{y}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 1.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le 1609.50674842192324831557925790548324585 \lor \neg \left(z \le 3.956447898588514434000900140654028393961 \cdot 10^{51}\right):\\ \;\;\;\;x + \frac{e^{y \cdot \left(0 + 2 \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right)}}{\frac{y}{\frac{{\left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}^{y}}{1}}}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{e^{-1 \cdot z}}{y}\\ \end{array}\]

Reproduce

herbie shell --seed 2019354 +o rules:numerics
(FPCore (x y z)
  :name "Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, G"
  :precision binary64

  :herbie-target
  (if (< (/ y (+ z y)) 7.1154157597908e-315) (+ x (/ (exp (/ -1 z)) y)) (+ x (/ (exp (log (pow (/ y (+ y z)) y))) y)))

  (+ x (/ (exp (* y (log (/ y (+ z y))))) y)))