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

Average Error: 4.8 → 1.7

Time: 4.2s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\frac{y}{z} - \frac{t}{1 - z} = -\infty:\\ \;\;\;\;\left(\left(x \cdot y\right) \cdot \frac{1}{z} + \left(-x \cdot \frac{t}{1 - z}\right)\right) + x \cdot \left(\frac{t}{1 - z} \cdot \left(\left(-1\right) + 1\right)\right)\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le 2.6617172340404871 \cdot 10^{145}:\\ \;\;\;\;x \cdot \left(\frac{y}{z} - t \cdot \frac{1}{1 - z}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{x \cdot y}{z} + \left(-\left(x \cdot t\right) \cdot \frac{1}{1 - z}\right)\right) + x \cdot \left(\frac{t}{1 - z} \cdot \left(\left(-1\right) + 1\right)\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r337900 = x;
        double r337901 = y;
        double r337902 = z;
        double r337903 = r337901 / r337902;
        double r337904 = t;
        double r337905 = 1.0;
        double r337906 = r337905 - r337902;
        double r337907 = r337904 / r337906;
        double r337908 = r337903 - r337907;
        double r337909 = r337900 * r337908;
        return r337909;
}

↓

double f(double x, double y, double z, double t) {
        double r337910 = y;
        double r337911 = z;
        double r337912 = r337910 / r337911;
        double r337913 = t;
        double r337914 = 1.0;
        double r337915 = r337914 - r337911;
        double r337916 = r337913 / r337915;
        double r337917 = r337912 - r337916;
        double r337918 = -inf.0;
        bool r337919 = r337917 <= r337918;
        double r337920 = x;
        double r337921 = r337920 * r337910;
        double r337922 = 1.0;
        double r337923 = r337922 / r337911;
        double r337924 = r337921 * r337923;
        double r337925 = r337920 * r337916;
        double r337926 = -r337925;
        double r337927 = r337924 + r337926;
        double r337928 = -r337922;
        double r337929 = r337928 + r337922;
        double r337930 = r337916 * r337929;
        double r337931 = r337920 * r337930;
        double r337932 = r337927 + r337931;
        double r337933 = 2.661717234040487e+145;
        bool r337934 = r337917 <= r337933;
        double r337935 = r337922 / r337915;
        double r337936 = r337913 * r337935;
        double r337937 = r337912 - r337936;
        double r337938 = r337920 * r337937;
        double r337939 = r337921 / r337911;
        double r337940 = r337920 * r337913;
        double r337941 = r337940 * r337935;
        double r337942 = -r337941;
        double r337943 = r337939 + r337942;
        double r337944 = r337943 + r337931;
        double r337945 = r337934 ? r337938 : r337944;
        double r337946 = r337919 ? r337932 : r337945;
        return r337946;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	4.8
Target	4.3
Herbie	1.7

\[\begin{array}{l} \mathbf{if}\;x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right) \lt -7.62322630331204244 \cdot 10^{-196}:\\ \;\;\;\;x \cdot \left(\frac{y}{z} - t \cdot \frac{1}{1 - z}\right)\\ \mathbf{elif}\;x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right) \lt 1.41339449277023022 \cdot 10^{-211}:\\ \;\;\;\;\frac{y \cdot x}{z} + \left(-\frac{t \cdot x}{1 - z}\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot \left(\frac{y}{z} - t \cdot \frac{1}{1 - z}\right)\\ \end{array}\]

Derivation

1. Split input into 3 regimes

2. if (- (/ y z) (/ t (- 1.0 z))) < -inf.0

   1. Initial program 64.0

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

   3. Applied add-cube-cbrt 64.0

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

   4. Applied div-inv 64.0

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

   5. Applied prod-diff 64.0

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

   6. Applied distribute-lft-in 64.0

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

   7. Simplified 64.0

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

   8. Simplified 64.0

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

   10. Applied fma-udef 64.0

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

   11. Applied distribute-lft-in 64.0

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

   12. Simplified 0.3

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

   13. Simplified 0.3

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

   15. Applied div-inv 0.4

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

   if -inf.0 < (- (/ y z) (/ t (- 1.0 z))) < 2.661717234040487e+145

   1. Initial program 1.6

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

   3. Applied div-inv 1.6

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

   if 2.661717234040487e+145 < (- (/ y z) (/ t (- 1.0 z)))

   1. Initial program 12.8

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

   3. Applied add-cube-cbrt 13.3

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

   4. Applied div-inv 13.4

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

   5. Applied prod-diff 13.3

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

   6. Applied distribute-lft-in 13.3

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

   7. Simplified 12.9

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

   8. Simplified 12.9

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

   10. Applied fma-udef 12.9

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

   11. Applied distribute-lft-in 12.9

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

   12. Simplified 1.7

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

   13. Simplified 1.7

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

   15. Applied div-inv 1.7

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

   16. Applied associate-*r* 2.4

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

4. Final simplification 1.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{y}{z} - \frac{t}{1 - z} = -\infty:\\ \;\;\;\;\left(\left(x \cdot y\right) \cdot \frac{1}{z} + \left(-x \cdot \frac{t}{1 - z}\right)\right) + x \cdot \left(\frac{t}{1 - z} \cdot \left(\left(-1\right) + 1\right)\right)\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le 2.6617172340404871 \cdot 10^{145}:\\ \;\;\;\;x \cdot \left(\frac{y}{z} - t \cdot \frac{1}{1 - z}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{x \cdot y}{z} + \left(-\left(x \cdot t\right) \cdot \frac{1}{1 - z}\right)\right) + x \cdot \left(\frac{t}{1 - z} \cdot \left(\left(-1\right) + 1\right)\right)\\ \end{array}\]

Reproduce

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

  :herbie-target
  (if (< (* x (- (/ y z) (/ t (- 1 z)))) -7.623226303312042e-196) (* x (- (/ y z) (* t (/ 1 (- 1 z))))) (if (< (* x (- (/ y z) (/ t (- 1 z)))) 1.4133944927702302e-211) (+ (/ (* y x) z) (- (/ (* t x) (- 1 z)))) (* x (- (/ y z) (* t (/ 1 (- 1 z)))))))

  (* x (- (/ y z) (/ t (- 1 z)))))