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

Average Error: 4.7 → 3.0

Time: 21.7s

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} \le -6.846301356169403244877525799291254847159 \cdot 10^{184}:\\ \;\;\;\;\frac{y \cdot x}{z} + \left(-t\right) \cdot \frac{x}{1 - z}\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le 1.063507125566366594065847135998477470263 \cdot 10^{89}:\\ \;\;\;\;\frac{x}{\sqrt[3]{z}} \cdot \frac{y}{\sqrt[3]{z} \cdot \sqrt[3]{z}} + \left(-\frac{t}{1 - z}\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\frac{y \cdot x}{z} + \left(-t\right) \cdot \frac{x}{1 - z}\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r251757738 = x;
        double r251757739 = y;
        double r251757740 = z;
        double r251757741 = r251757739 / r251757740;
        double r251757742 = t;
        double r251757743 = 1.0;
        double r251757744 = r251757743 - r251757740;
        double r251757745 = r251757742 / r251757744;
        double r251757746 = r251757741 - r251757745;
        double r251757747 = r251757738 * r251757746;
        return r251757747;
}

↓

double f(double x, double y, double z, double t) {
        double r251757748 = y;
        double r251757749 = z;
        double r251757750 = r251757748 / r251757749;
        double r251757751 = t;
        double r251757752 = 1.0;
        double r251757753 = r251757752 - r251757749;
        double r251757754 = r251757751 / r251757753;
        double r251757755 = r251757750 - r251757754;
        double r251757756 = -6.846301356169403e+184;
        bool r251757757 = r251757755 <= r251757756;
        double r251757758 = x;
        double r251757759 = r251757748 * r251757758;
        double r251757760 = r251757759 / r251757749;
        double r251757761 = -r251757751;
        double r251757762 = r251757758 / r251757753;
        double r251757763 = r251757761 * r251757762;
        double r251757764 = r251757760 + r251757763;
        double r251757765 = 1.0635071255663666e+89;
        bool r251757766 = r251757755 <= r251757765;
        double r251757767 = cbrt(r251757749);
        double r251757768 = r251757758 / r251757767;
        double r251757769 = r251757767 * r251757767;
        double r251757770 = r251757748 / r251757769;
        double r251757771 = r251757768 * r251757770;
        double r251757772 = -r251757754;
        double r251757773 = r251757772 * r251757758;
        double r251757774 = r251757771 + r251757773;
        double r251757775 = r251757766 ? r251757774 : r251757764;
        double r251757776 = r251757757 ? r251757764 : r251757775;
        return r251757776;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	4.7
Target	4.5
Herbie	3.0

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

2. if (- (/ y z) (/ t (- 1.0 z))) < -6.846301356169403e+184 or 1.0635071255663666e+89 < (- (/ y z) (/ t (- 1.0 z)))

   1. Initial program 12.6

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

   3. Applied sub-neg 12.6

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

   4. Applied distribute-rgt-in 12.6

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

   6. Applied add-cube-cbrt 13.1

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

   7. Applied add-cube-cbrt 13.2

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

   8. Applied times-frac 13.2

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

   9. Applied associate-*l* 2.7

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

   11. Applied div-inv 2.8

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

   12. Applied distribute-lft-neg-in 2.8

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

   13. Applied associate-*l* 3.7

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

   14. Simplified 3.7

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

   16. Applied associate-*l/ 4.0

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

   17. Applied frac-times 4.4

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

   18. Simplified 4.2

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

   19. Simplified 3.5

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

   if -6.846301356169403e+184 < (- (/ y z) (/ t (- 1.0 z))) < 1.0635071255663666e+89

   1. Initial program 1.7

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

   3. Applied sub-neg 1.7

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

   4. Applied distribute-rgt-in 1.7

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

   6. Applied add-cube-cbrt 2.2

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

   7. Applied add-cube-cbrt 2.3

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

   8. Applied times-frac 2.3

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

   9. Applied associate-*l* 1.6

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

   11. Applied *-un-lft-identity 1.6

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

   12. Applied associate-*l* 1.6

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

   13. Simplified 2.7

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

4. Final simplification 3.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{y}{z} - \frac{t}{1 - z} \le -6.846301356169403244877525799291254847159 \cdot 10^{184}:\\ \;\;\;\;\frac{y \cdot x}{z} + \left(-t\right) \cdot \frac{x}{1 - z}\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le 1.063507125566366594065847135998477470263 \cdot 10^{89}:\\ \;\;\;\;\frac{x}{\sqrt[3]{z}} \cdot \frac{y}{\sqrt[3]{z} \cdot \sqrt[3]{z}} + \left(-\frac{t}{1 - z}\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\frac{y \cdot x}{z} + \left(-t\right) \cdot \frac{x}{1 - z}\\ \end{array}\]

Reproduce

herbie shell --seed 2019173 
(FPCore (x y z t)
  :name "Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, C"

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

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