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

Average Error: 4.5 → 0.2

Time: 5.6s

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:\\ \;\;\;\;1 \cdot \left(\frac{1}{\frac{z}{x \cdot y}} - x \cdot \frac{t}{1 - z}\right)\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le -2.78381369030126933781218479946675720907 \cdot 10^{-264}:\\ \;\;\;\;1 \cdot \left(\frac{x}{\frac{z}{y}} - x \cdot \frac{t}{1 - z}\right)\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le 7.010228289444063733682275068254429974158 \cdot 10^{-231}:\\ \;\;\;\;1 \cdot \left(\frac{x \cdot y}{z} - \left(x \cdot t\right) \cdot \frac{1}{1 - z}\right)\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le 1.795095217187765936797771641264103283314 \cdot 10^{286}:\\ \;\;\;\;1 \cdot \mathsf{fma}\left(\frac{x}{1}, \frac{y}{z}, -x \cdot \frac{t}{1 - z}\right)\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \left(\frac{x \cdot y}{z} - \left(x \cdot t\right) \cdot \frac{1}{1 - z}\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r356646 = x;
        double r356647 = y;
        double r356648 = z;
        double r356649 = r356647 / r356648;
        double r356650 = t;
        double r356651 = 1.0;
        double r356652 = r356651 - r356648;
        double r356653 = r356650 / r356652;
        double r356654 = r356649 - r356653;
        double r356655 = r356646 * r356654;
        return r356655;
}

↓

double f(double x, double y, double z, double t) {
        double r356656 = y;
        double r356657 = z;
        double r356658 = r356656 / r356657;
        double r356659 = t;
        double r356660 = 1.0;
        double r356661 = r356660 - r356657;
        double r356662 = r356659 / r356661;
        double r356663 = r356658 - r356662;
        double r356664 = -inf.0;
        bool r356665 = r356663 <= r356664;
        double r356666 = 1.0;
        double r356667 = x;
        double r356668 = r356667 * r356656;
        double r356669 = r356657 / r356668;
        double r356670 = r356666 / r356669;
        double r356671 = r356667 * r356662;
        double r356672 = r356670 - r356671;
        double r356673 = r356666 * r356672;
        double r356674 = -2.7838136903012693e-264;
        bool r356675 = r356663 <= r356674;
        double r356676 = r356657 / r356656;
        double r356677 = r356667 / r356676;
        double r356678 = r356677 - r356671;
        double r356679 = r356666 * r356678;
        double r356680 = 7.010228289444064e-231;
        bool r356681 = r356663 <= r356680;
        double r356682 = r356668 / r356657;
        double r356683 = r356667 * r356659;
        double r356684 = r356666 / r356661;
        double r356685 = r356683 * r356684;
        double r356686 = r356682 - r356685;
        double r356687 = r356666 * r356686;
        double r356688 = 1.795095217187766e+286;
        bool r356689 = r356663 <= r356688;
        double r356690 = r356667 / r356666;
        double r356691 = -r356671;
        double r356692 = fma(r356690, r356658, r356691);
        double r356693 = r356666 * r356692;
        double r356694 = r356689 ? r356693 : r356687;
        double r356695 = r356681 ? r356687 : r356694;
        double r356696 = r356675 ? r356679 : r356695;
        double r356697 = r356665 ? r356673 : r356696;
        return r356697;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	4.5
Target	4.1
Herbie	0.2

\[\begin{array}{l} \mathbf{if}\;x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right) \lt -7.623226303312042442144691872793570510727 \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.413394492770230216018398633584271456447 \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 4 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 *-un-lft-identity 64.0

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

   4. Applied add-cube-cbrt 64.0

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

   5. Applied times-frac 64.0

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

   6. Applied fma-neg 64.0

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

   8. Applied *-un-lft-identity 64.0

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

   9. Applied associate-*l* 64.0

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

   10. Simplified 0.2

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

   12. Applied clear-num 0.4

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

   if -inf.0 < (- (/ y z) (/ t (- 1.0 z))) < -2.7838136903012693e-264

   1. Initial program 0.2

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

   3. Applied *-un-lft-identity 0.2

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

   4. Applied add-cube-cbrt 0.8

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

   5. Applied times-frac 0.8

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

   6. Applied fma-neg 0.8

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

   8. Applied *-un-lft-identity 0.8

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

   9. Applied associate-*l* 0.8

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

   10. Simplified 5.9

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

   12. Applied associate-/l* 0.2

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

   if -2.7838136903012693e-264 < (- (/ y z) (/ t (- 1.0 z))) < 7.010228289444064e-231 or 1.795095217187766e+286 < (- (/ y z) (/ t (- 1.0 z)))

   1. Initial program 21.7

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

   3. Applied *-un-lft-identity 21.7

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

   4. Applied add-cube-cbrt 21.8

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

   5. Applied times-frac 21.8

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

   6. Applied fma-neg 21.8

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

   8. Applied *-un-lft-identity 21.8

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

   9. Applied associate-*l* 21.8

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

   10. Simplified 4.6

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

   12. Applied div-inv 4.6

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

   13. Applied associate-*r* 0.2

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

   if 7.010228289444064e-231 < (- (/ y z) (/ t (- 1.0 z))) < 1.795095217187766e+286

   1. Initial program 0.2

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

   3. Applied *-un-lft-identity 0.2

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

   4. Applied add-cube-cbrt 0.8

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

   5. Applied times-frac 0.8

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

   6. Applied fma-neg 0.8

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

   8. Applied *-un-lft-identity 0.8

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

   9. Applied associate-*l* 0.8

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

   10. Simplified 5.7

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

   12. Applied *-un-lft-identity 5.7

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

   13. Applied times-frac 0.2

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

   14. Applied fma-neg 0.2

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

4. Final simplification 0.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{y}{z} - \frac{t}{1 - z} = -\infty:\\ \;\;\;\;1 \cdot \left(\frac{1}{\frac{z}{x \cdot y}} - x \cdot \frac{t}{1 - z}\right)\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le -2.78381369030126933781218479946675720907 \cdot 10^{-264}:\\ \;\;\;\;1 \cdot \left(\frac{x}{\frac{z}{y}} - x \cdot \frac{t}{1 - z}\right)\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le 7.010228289444063733682275068254429974158 \cdot 10^{-231}:\\ \;\;\;\;1 \cdot \left(\frac{x \cdot y}{z} - \left(x \cdot t\right) \cdot \frac{1}{1 - z}\right)\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le 1.795095217187765936797771641264103283314 \cdot 10^{286}:\\ \;\;\;\;1 \cdot \mathsf{fma}\left(\frac{x}{1}, \frac{y}{z}, -x \cdot \frac{t}{1 - z}\right)\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \left(\frac{x \cdot y}{z} - \left(x \cdot t\right) \cdot \frac{1}{1 - z}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019354 +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)))))