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

Average Error: 4.6 → 5.3

Time: 6.4s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -1.89141307036293912 \cdot 10^{65}:\\ \;\;\;\;1 \cdot \left(\frac{x}{\frac{z}{y}} - x \cdot \frac{t}{1 - z}\right) + x \cdot \left(\frac{t}{1 - z} \cdot \left(\left(-1\right) + 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1 \cdot \left(\frac{x \cdot y}{z} - \frac{x \cdot t}{1 - z}\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 r473470 = x;
        double r473471 = y;
        double r473472 = z;
        double r473473 = r473471 / r473472;
        double r473474 = t;
        double r473475 = 1.0;
        double r473476 = r473475 - r473472;
        double r473477 = r473474 / r473476;
        double r473478 = r473473 - r473477;
        double r473479 = r473470 * r473478;
        return r473479;
}

↓

double f(double x, double y, double z, double t) {
        double r473480 = z;
        double r473481 = -1.8914130703629391e+65;
        bool r473482 = r473480 <= r473481;
        double r473483 = 1.0;
        double r473484 = x;
        double r473485 = y;
        double r473486 = r473480 / r473485;
        double r473487 = r473484 / r473486;
        double r473488 = t;
        double r473489 = 1.0;
        double r473490 = r473489 - r473480;
        double r473491 = r473488 / r473490;
        double r473492 = r473484 * r473491;
        double r473493 = r473487 - r473492;
        double r473494 = r473483 * r473493;
        double r473495 = -r473483;
        double r473496 = r473495 + r473483;
        double r473497 = r473491 * r473496;
        double r473498 = r473484 * r473497;
        double r473499 = r473494 + r473498;
        double r473500 = r473484 * r473485;
        double r473501 = r473500 / r473480;
        double r473502 = r473484 * r473488;
        double r473503 = r473502 / r473490;
        double r473504 = r473501 - r473503;
        double r473505 = r473483 * r473504;
        double r473506 = r473505 + r473498;
        double r473507 = r473482 ? r473499 : r473506;
        return r473507;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	4.6
Target	4.4
Herbie	5.3

\[\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 2 regimes

2. if z < -1.8914130703629391e+65

   1. Initial program 2.4

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

   3. Applied add-cube-cbrt 2.9

      \[\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 add-cube-cbrt 3.2

      \[\leadsto x \cdot \left(\frac{y}{\color{blue}{\left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \sqrt[3]{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 *-un-lft-identity 3.2

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

   6. Applied times-frac 3.2

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

   7. Applied prod-diff 3.2

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

   8. Applied distribute-lft-in 3.2

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

   9. Simplified 2.8

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

   10. Simplified 2.8

       \[\leadsto x \cdot \mathsf{fma}\left(\frac{1}{\sqrt[3]{z} \cdot \sqrt[3]{z}}, \frac{y}{\sqrt[3]{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)}\]
   11. Using strategy rm

   12. Applied *-un-lft-identity 2.8

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

   13. Applied associate-*l* 2.8

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

   14. Simplified 8.4

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

   16. Applied associate-/l* 2.6

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

   if -1.8914130703629391e+65 < z

   1. Initial program 5.3

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

   3. Applied add-cube-cbrt 5.7

      \[\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 add-cube-cbrt 6.3

      \[\leadsto x \cdot \left(\frac{y}{\color{blue}{\left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \sqrt[3]{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 *-un-lft-identity 6.3

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

   6. Applied times-frac 6.3

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

   7. Applied prod-diff 6.3

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

   8. Applied distribute-lft-in 6.3

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

   9. Simplified 5.8

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

   10. Simplified 5.8

       \[\leadsto x \cdot \mathsf{fma}\left(\frac{1}{\sqrt[3]{z} \cdot \sqrt[3]{z}}, \frac{y}{\sqrt[3]{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)}\]
   11. Using strategy rm

   12. Applied *-un-lft-identity 5.8

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

   13. Applied associate-*l* 5.8

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

   14. Simplified 4.8

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

   16. Applied associate-*r/ 6.2

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

4. Final simplification 5.3

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

Reproduce

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