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

Average Error: 4.7 → 4.8

Time: 13.3s

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 r346195 = x;
        double r346196 = y;
        double r346197 = z;
        double r346198 = r346196 / r346197;
        double r346199 = t;
        double r346200 = 1.0;
        double r346201 = r346200 - r346197;
        double r346202 = r346199 / r346201;
        double r346203 = r346198 - r346202;
        double r346204 = r346195 * r346203;
        return r346204;
}

↓

double f(double x, double y, double z, double t) {
        double r346205 = y;
        double r346206 = -2.2498808884886877e-122;
        bool r346207 = r346205 <= r346206;
        double r346208 = 1.7641534698072868e+253;
        bool r346209 = r346205 <= r346208;
        double r346210 = !r346209;
        bool r346211 = r346207 || r346210;
        double r346212 = 1.0;
        double r346213 = z;
        double r346214 = x;
        double r346215 = r346214 * r346205;
        double r346216 = r346213 / r346215;
        double r346217 = r346212 / r346216;
        double r346218 = t;
        double r346219 = 1.0;
        double r346220 = r346219 - r346213;
        double r346221 = r346218 / r346220;
        double r346222 = -r346221;
        double r346223 = r346222 * r346214;
        double r346224 = r346217 + r346223;
        double r346225 = r346213 / r346205;
        double r346226 = r346214 / r346225;
        double r346227 = r346226 + r346223;
        double r346228 = r346211 ? r346224 : r346227;
        return r346228;
}

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)))))