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

Average Error: 4.7 → 4.8

Time: 13.7s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;y \le -2.249880888488687734595039382679013873129 \cdot 10^{-122} \lor \neg \left(y \le 1.764153469807286774331258966570820240811 \cdot 10^{253}\right):\\ \;\;\;\;\frac{1}{\frac{z}{x \cdot y}} + \left(-\frac{t}{1 - z}\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{\frac{z}{y}} + \left(-\frac{t}{1 - z}\right) \cdot x\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r307699 = x;
        double r307700 = y;
        double r307701 = z;
        double r307702 = r307700 / r307701;
        double r307703 = t;
        double r307704 = 1.0;
        double r307705 = r307704 - r307701;
        double r307706 = r307703 / r307705;
        double r307707 = r307702 - r307706;
        double r307708 = r307699 * r307707;
        return r307708;
}

↓

double f(double x, double y, double z, double t) {
        double r307709 = y;
        double r307710 = -2.2498808884886877e-122;
        bool r307711 = r307709 <= r307710;
        double r307712 = 1.7641534698072868e+253;
        bool r307713 = r307709 <= r307712;
        double r307714 = !r307713;
        bool r307715 = r307711 || r307714;
        double r307716 = 1.0;
        double r307717 = z;
        double r307718 = x;
        double r307719 = r307718 * r307709;
        double r307720 = r307717 / r307719;
        double r307721 = r307716 / r307720;
        double r307722 = t;
        double r307723 = 1.0;
        double r307724 = r307723 - r307717;
        double r307725 = r307722 / r307724;
        double r307726 = -r307725;
        double r307727 = r307726 * r307718;
        double r307728 = r307721 + r307727;
        double r307729 = r307717 / r307709;
        double r307730 = r307718 / r307729;
        double r307731 = r307730 + r307727;
        double r307732 = r307715 ? r307728 : r307731;
        return r307732;
}

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	4.8

\[\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 < -2.2498808884886877e-122 or 1.7641534698072868e+253 < y

   1. Initial program 6.9

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

   3. Applied sub-neg 6.9

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

   4. Applied distribute-lft-in 6.9

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

   5. Simplified 6.9

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

   6. Simplified 6.9

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

   8. Applied clear-num 7.1

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

   if -2.2498808884886877e-122 < y < 1.7641534698072868e+253

   1. Initial program 3.5

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

   3. Applied sub-neg 3.5

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

   4. Applied distribute-lft-in 3.5

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

   5. Simplified 4.8

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

   6. Simplified 4.8

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

   8. Applied associate-/l* 3.5

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

4. Final simplification 4.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -2.249880888488687734595039382679013873129 \cdot 10^{-122} \lor \neg \left(y \le 1.764153469807286774331258966570820240811 \cdot 10^{253}\right):\\ \;\;\;\;\frac{1}{\frac{z}{x \cdot y}} + \left(-\frac{t}{1 - z}\right) \cdot x\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{\frac{z}{y}} + \left(-\frac{t}{1 - z}\right) \cdot x\\ \end{array}\]

Reproduce

herbie shell --seed 2019323 
(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)))))