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

Average Error: 4.7 → 4.8

Time: 13.6s

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 r270082 = x;
        double r270083 = y;
        double r270084 = z;
        double r270085 = r270083 / r270084;
        double r270086 = t;
        double r270087 = 1.0;
        double r270088 = r270087 - r270084;
        double r270089 = r270086 / r270088;
        double r270090 = r270085 - r270089;
        double r270091 = r270082 * r270090;
        return r270091;
}

↓

double f(double x, double y, double z, double t) {
        double r270092 = y;
        double r270093 = -2.2498808884886877e-122;
        bool r270094 = r270092 <= r270093;
        double r270095 = 1.7641534698072868e+253;
        bool r270096 = r270092 <= r270095;
        double r270097 = !r270096;
        bool r270098 = r270094 || r270097;
        double r270099 = 1.0;
        double r270100 = z;
        double r270101 = x;
        double r270102 = r270101 * r270092;
        double r270103 = r270100 / r270102;
        double r270104 = r270099 / r270103;
        double r270105 = t;
        double r270106 = 1.0;
        double r270107 = r270106 - r270100;
        double r270108 = r270105 / r270107;
        double r270109 = -r270108;
        double r270110 = r270109 * r270101;
        double r270111 = r270104 + r270110;
        double r270112 = r270100 / r270092;
        double r270113 = r270101 / r270112;
        double r270114 = r270113 + r270110;
        double r270115 = r270098 ? r270111 : r270114;
        return r270115;
}

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