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

Average Error: 4.9 → 5.1

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

C

double f(double x, double y, double z, double t) {
        double r355304 = x;
        double r355305 = y;
        double r355306 = z;
        double r355307 = r355305 / r355306;
        double r355308 = t;
        double r355309 = 1.0;
        double r355310 = r355309 - r355306;
        double r355311 = r355308 / r355310;
        double r355312 = r355307 - r355311;
        double r355313 = r355304 * r355312;
        return r355313;
}

↓

double f(double x, double y, double z, double t) {
        double r355314 = y;
        double r355315 = z;
        double r355316 = r355314 / r355315;
        double r355317 = t;
        double r355318 = 1.0;
        double r355319 = r355318 - r355315;
        double r355320 = r355317 / r355319;
        double r355321 = r355316 - r355320;
        double r355322 = 5.031923056387367e-36;
        bool r355323 = r355321 <= r355322;
        double r355324 = x;
        double r355325 = r355324 * r355314;
        double r355326 = 1.0;
        double r355327 = r355326 / r355315;
        double r355328 = r355325 * r355327;
        double r355329 = r355320 * r355324;
        double r355330 = -r355329;
        double r355331 = r355328 + r355330;
        double r355332 = r355315 / r355324;
        double r355333 = r355314 / r355332;
        double r355334 = r355333 - r355329;
        double r355335 = r355323 ? r355331 : r355334;
        return r355335;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	4.9
Target	4.5
Herbie	5.1

\[\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))) < 5.031923056387367e-36

   1. Initial program 4.6

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

   3. Applied div-inv 4.6

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

   5. Applied sub-neg 4.6

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

   6. Applied distribute-lft-in 4.6

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

   7. Simplified 4.6

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

   9. Applied div-inv 4.6

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

   10. Applied associate-*r* 5.2

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

   if 5.031923056387367e-36 < (- (/ y z) (/ t (- 1.0 z)))

   1. Initial program 5.7

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

   3. Applied div-inv 5.8

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

   5. Applied sub-neg 5.8

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

   6. Applied distribute-lft-in 5.8

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

   7. Simplified 5.7

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

   9. Applied div-inv 5.8

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

   10. Applied associate-*r* 5.6

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

   12. Applied neg-sub0 5.6

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

   13. Applied associate-+r- 5.6

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

   14. Simplified 5.0

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

4. Final simplification 5.1

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

Reproduce

herbie shell --seed 2019208 +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.62322630331204244e-196) (* x (- (/ y z) (* t (/ 1 (- 1 z))))) (if (< (* x (- (/ y z) (/ t (- 1 z)))) 1.41339449277023022e-211) (+ (/ (* y x) z) (- (/ (* t x) (- 1 z)))) (* x (- (/ y z) (* t (/ 1 (- 1 z)))))))

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