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

Average Error: 4.5 → 1.5

Time: 17.3s

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(\frac{t}{1 - z} + \frac{-t}{1 - z}\right) \cdot x + \frac{x}{z} \cdot y\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le 4.862861552770296825237343335186305099433 \cdot 10^{206}:\\ \;\;\;\;x \cdot \left(\frac{-1}{\frac{1 - z}{t}} + \frac{y}{z}\right) + \left(\frac{t}{1 - z} + \frac{-t}{1 - z}\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{t}{1 - z} + \frac{-t}{1 - z}\right) \cdot x + \left(\frac{y \cdot x}{z} + \frac{\left(-t\right) \cdot x}{1 - z}\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r236145 = x;
        double r236146 = y;
        double r236147 = z;
        double r236148 = r236146 / r236147;
        double r236149 = t;
        double r236150 = 1.0;
        double r236151 = r236150 - r236147;
        double r236152 = r236149 / r236151;
        double r236153 = r236148 - r236152;
        double r236154 = r236145 * r236153;
        return r236154;
}

↓

double f(double x, double y, double z, double t) {
        double r236155 = y;
        double r236156 = z;
        double r236157 = r236155 / r236156;
        double r236158 = t;
        double r236159 = 1.0;
        double r236160 = r236159 - r236156;
        double r236161 = r236158 / r236160;
        double r236162 = r236157 - r236161;
        double r236163 = -inf.0;
        bool r236164 = r236162 <= r236163;
        double r236165 = -r236158;
        double r236166 = r236165 / r236160;
        double r236167 = r236161 + r236166;
        double r236168 = x;
        double r236169 = r236167 * r236168;
        double r236170 = r236168 / r236156;
        double r236171 = r236170 * r236155;
        double r236172 = r236169 + r236171;
        double r236173 = 4.862861552770297e+206;
        bool r236174 = r236162 <= r236173;
        double r236175 = -1.0;
        double r236176 = r236160 / r236158;
        double r236177 = r236175 / r236176;
        double r236178 = r236177 + r236157;
        double r236179 = r236168 * r236178;
        double r236180 = r236179 + r236169;
        double r236181 = r236155 * r236168;
        double r236182 = r236181 / r236156;
        double r236183 = r236165 * r236168;
        double r236184 = r236183 / r236160;
        double r236185 = r236182 + r236184;
        double r236186 = r236169 + r236185;
        double r236187 = r236174 ? r236180 : r236186;
        double r236188 = r236164 ? r236172 : r236187;
        return r236188;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	4.5
Target	4.2
Herbie	1.5

\[\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 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-sqr-sqrt 64.0

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

   4. Applied div-inv 64.0

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

   6. Applied distribute-lft-in 64.0

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

   7. Simplified 64.0

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

   8. Simplified 64.0

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

   9. Taylor expanded around 0 0.3

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

   10. Simplified 0.3

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

   if -inf.0 < (- (/ y z) (/ t (- 1.0 z))) < 4.862861552770297e+206

   1. Initial program 1.4

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

   3. Applied add-sqr-sqrt 26.6

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

   4. Applied div-inv 26.6

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

   5. Applied prod-diff 26.6

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

   6. Applied distribute-lft-in 26.6

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

   7. Simplified 26.5

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

   8. Simplified 1.5

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

   10. Applied fma-udef 1.5

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

   11. Simplified 1.4

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

   13. Applied clear-num 1.6

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

   if 4.862861552770297e+206 < (- (/ y z) (/ t (- 1.0 z)))

   1. Initial program 19.0

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

   3. Applied add-sqr-sqrt 53.4

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

   4. Applied div-inv 53.4

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

   5. Applied prod-diff 53.4

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

   6. Applied distribute-lft-in 53.4

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

   7. Simplified 53.4

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

   8. Simplified 19.1

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

   10. Applied fma-udef 19.1

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

   11. Simplified 19.0

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

   13. Applied distribute-rgt-in 19.0

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

   14. Simplified 0.7

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

   15. Simplified 1.2

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

4. Final simplification 1.5

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

Reproduce

herbie shell --seed 2019179 +o rules:numerics
(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)))))