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

Average Error: 3.7 → 2.8

Time: 34.6s

Precision: 64

Math

\[\frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\]

↓

\[\begin{array}{l} \mathbf{if}\;t \le -1.747646842184294811529008447013758285829 \cdot 10^{-63} \lor \neg \left(t \le 4.66119048674144283533835621815974643908 \cdot 10^{-116}\right):\\ \;\;\;\;\frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\sqrt{t + a}}{\sqrt[3]{t}} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2 \cdot \frac{\frac{z \cdot \sqrt{t + a}}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \left(\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)\right) - \sqrt[3]{t} \cdot \left(\left(b - c\right) \cdot \left(\left(a \cdot a - \frac{5}{6} \cdot \frac{5}{6}\right) \cdot \left(t \cdot 3\right) - \left(a - \frac{5}{6}\right) \cdot 2\right)\right)}{\sqrt[3]{t} \cdot \left(\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)\right)}}}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r343692 = x;
        double r343693 = y;
        double r343694 = 2.0;
        double r343695 = z;
        double r343696 = t;
        double r343697 = a;
        double r343698 = r343696 + r343697;
        double r343699 = sqrt(r343698);
        double r343700 = r343695 * r343699;
        double r343701 = r343700 / r343696;
        double r343702 = b;
        double r343703 = c;
        double r343704 = r343702 - r343703;
        double r343705 = 5.0;
        double r343706 = 6.0;
        double r343707 = r343705 / r343706;
        double r343708 = r343697 + r343707;
        double r343709 = 3.0;
        double r343710 = r343696 * r343709;
        double r343711 = r343694 / r343710;
        double r343712 = r343708 - r343711;
        double r343713 = r343704 * r343712;
        double r343714 = r343701 - r343713;
        double r343715 = r343694 * r343714;
        double r343716 = exp(r343715);
        double r343717 = r343693 * r343716;
        double r343718 = r343692 + r343717;
        double r343719 = r343692 / r343718;
        return r343719;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r343720 = t;
        double r343721 = -1.7476468421842948e-63;
        bool r343722 = r343720 <= r343721;
        double r343723 = 4.661190486741443e-116;
        bool r343724 = r343720 <= r343723;
        double r343725 = !r343724;
        bool r343726 = r343722 || r343725;
        double r343727 = x;
        double r343728 = y;
        double r343729 = 2.0;
        double r343730 = z;
        double r343731 = cbrt(r343720);
        double r343732 = r343731 * r343731;
        double r343733 = r343730 / r343732;
        double r343734 = a;
        double r343735 = r343720 + r343734;
        double r343736 = sqrt(r343735);
        double r343737 = r343736 / r343731;
        double r343738 = r343733 * r343737;
        double r343739 = b;
        double r343740 = c;
        double r343741 = r343739 - r343740;
        double r343742 = 5.0;
        double r343743 = 6.0;
        double r343744 = r343742 / r343743;
        double r343745 = r343734 + r343744;
        double r343746 = 3.0;
        double r343747 = r343720 * r343746;
        double r343748 = r343729 / r343747;
        double r343749 = r343745 - r343748;
        double r343750 = r343741 * r343749;
        double r343751 = r343738 - r343750;
        double r343752 = r343729 * r343751;
        double r343753 = exp(r343752);
        double r343754 = r343728 * r343753;
        double r343755 = r343727 + r343754;
        double r343756 = r343727 / r343755;
        double r343757 = r343730 * r343736;
        double r343758 = r343757 / r343732;
        double r343759 = r343734 - r343744;
        double r343760 = r343759 * r343747;
        double r343761 = r343758 * r343760;
        double r343762 = r343734 * r343734;
        double r343763 = r343744 * r343744;
        double r343764 = r343762 - r343763;
        double r343765 = r343764 * r343747;
        double r343766 = r343759 * r343729;
        double r343767 = r343765 - r343766;
        double r343768 = r343741 * r343767;
        double r343769 = r343731 * r343768;
        double r343770 = r343761 - r343769;
        double r343771 = r343731 * r343760;
        double r343772 = r343770 / r343771;
        double r343773 = r343729 * r343772;
        double r343774 = exp(r343773);
        double r343775 = r343728 * r343774;
        double r343776 = r343727 + r343775;
        double r343777 = r343727 / r343776;
        double r343778 = r343726 ? r343756 : r343777;
        return r343778;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Bits error versus b

Bits error versus c

Target

Original	3.7
Target	2.8
Herbie	2.8

\[\begin{array}{l} \mathbf{if}\;t \lt -2.118326644891581057561884576920117070548 \cdot 10^{-50}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2 \cdot \left(\left(a \cdot c + 0.8333333333333333703407674875052180141211 \cdot c\right) - a \cdot b\right)}}\\ \mathbf{elif}\;t \lt 5.196588770651547088010424937268931048836 \cdot 10^{-123}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2 \cdot \frac{\left(z \cdot \sqrt{t + a}\right) \cdot \left(\left(3 \cdot t\right) \cdot \left(a - \frac{5}{6}\right)\right) - \left(\left(\frac{5}{6} + a\right) \cdot \left(3 \cdot t\right) - 2\right) \cdot \left(\left(a - \frac{5}{6}\right) \cdot \left(\left(b - c\right) \cdot t\right)\right)}{\left(\left(t \cdot t\right) \cdot 3\right) \cdot \left(a - \frac{5}{6}\right)}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if t < -1.7476468421842948e-63 or 4.661190486741443e-116 < t

   1. Initial program 2.3

      \[\frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 2.3

      \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z \cdot \sqrt{t + a}}{\color{blue}{\left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) \cdot \sqrt[3]{t}}} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\]

   4. Applied times-frac 0.5

      \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \left(\color{blue}{\frac{z}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\sqrt{t + a}}{\sqrt[3]{t}}} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\]

   if -1.7476468421842948e-63 < t < 4.661190486741443e-116

   1. Initial program 6.6

      \[\frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 6.6

      \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z \cdot \sqrt{t + a}}{\color{blue}{\left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) \cdot \sqrt[3]{t}}} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\]

   4. Applied times-frac 6.8

      \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \left(\color{blue}{\frac{z}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\sqrt{t + a}}{\sqrt[3]{t}}} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\]
   5. Using strategy rm

   6. Applied add-log-exp 33.0

      \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z}{\sqrt[3]{t} \cdot \color{blue}{\log \left(e^{\sqrt[3]{t}}\right)}} \cdot \frac{\sqrt{t + a}}{\sqrt[3]{t}} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\]
   7. Using strategy rm

   8. Applied flip-+ 34.8

      \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z}{\sqrt[3]{t} \cdot \log \left(e^{\sqrt[3]{t}}\right)} \cdot \frac{\sqrt{t + a}}{\sqrt[3]{t}} - \left(b - c\right) \cdot \left(\color{blue}{\frac{a \cdot a - \frac{5}{6} \cdot \frac{5}{6}}{a - \frac{5}{6}}} - \frac{2}{t \cdot 3}\right)\right)}}\]

   9. Applied frac-sub 34.8

      \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z}{\sqrt[3]{t} \cdot \log \left(e^{\sqrt[3]{t}}\right)} \cdot \frac{\sqrt{t + a}}{\sqrt[3]{t}} - \left(b - c\right) \cdot \color{blue}{\frac{\left(a \cdot a - \frac{5}{6} \cdot \frac{5}{6}\right) \cdot \left(t \cdot 3\right) - \left(a - \frac{5}{6}\right) \cdot 2}{\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)}}\right)}}\]

   10. Applied associate-*r/ 34.8

       \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z}{\sqrt[3]{t} \cdot \log \left(e^{\sqrt[3]{t}}\right)} \cdot \frac{\sqrt{t + a}}{\sqrt[3]{t}} - \color{blue}{\frac{\left(b - c\right) \cdot \left(\left(a \cdot a - \frac{5}{6} \cdot \frac{5}{6}\right) \cdot \left(t \cdot 3\right) - \left(a - \frac{5}{6}\right) \cdot 2\right)}{\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)}}\right)}}\]

   11. Applied associate-*r/ 34.8

       \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \left(\color{blue}{\frac{\frac{z}{\sqrt[3]{t} \cdot \log \left(e^{\sqrt[3]{t}}\right)} \cdot \sqrt{t + a}}{\sqrt[3]{t}}} - \frac{\left(b - c\right) \cdot \left(\left(a \cdot a - \frac{5}{6} \cdot \frac{5}{6}\right) \cdot \left(t \cdot 3\right) - \left(a - \frac{5}{6}\right) \cdot 2\right)}{\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)}\right)}}\]

   12. Applied frac-sub 33.9

       \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \color{blue}{\frac{\left(\frac{z}{\sqrt[3]{t} \cdot \log \left(e^{\sqrt[3]{t}}\right)} \cdot \sqrt{t + a}\right) \cdot \left(\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)\right) - \sqrt[3]{t} \cdot \left(\left(b - c\right) \cdot \left(\left(a \cdot a - \frac{5}{6} \cdot \frac{5}{6}\right) \cdot \left(t \cdot 3\right) - \left(a - \frac{5}{6}\right) \cdot 2\right)\right)}{\sqrt[3]{t} \cdot \left(\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)\right)}}}}\]

   13. Simplified 7.3

       \[\leadsto \frac{x}{x + y \cdot e^{2 \cdot \frac{\color{blue}{\frac{z \cdot \sqrt{t + a}}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \left(\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)\right) - \sqrt[3]{t} \cdot \left(\left(b - c\right) \cdot \left(\left(a \cdot a - \frac{5}{6} \cdot \frac{5}{6}\right) \cdot \left(t \cdot 3\right) - \left(a - \frac{5}{6}\right) \cdot 2\right)\right)}}{\sqrt[3]{t} \cdot \left(\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)\right)}}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 2.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;t \le -1.747646842184294811529008447013758285829 \cdot 10^{-63} \lor \neg \left(t \le 4.66119048674144283533835621815974643908 \cdot 10^{-116}\right):\\ \;\;\;\;\frac{x}{x + y \cdot e^{2 \cdot \left(\frac{z}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\sqrt{t + a}}{\sqrt[3]{t}} - \left(b - c\right) \cdot \left(\left(a + \frac{5}{6}\right) - \frac{2}{t \cdot 3}\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2 \cdot \frac{\frac{z \cdot \sqrt{t + a}}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \left(\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)\right) - \sqrt[3]{t} \cdot \left(\left(b - c\right) \cdot \left(\left(a \cdot a - \frac{5}{6} \cdot \frac{5}{6}\right) \cdot \left(t \cdot 3\right) - \left(a - \frac{5}{6}\right) \cdot 2\right)\right)}{\sqrt[3]{t} \cdot \left(\left(a - \frac{5}{6}\right) \cdot \left(t \cdot 3\right)\right)}}}\\ \end{array}\]

Reproduce

herbie shell --seed 2019303 
(FPCore (x y z t a b c)
  :name "Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, I"
  :precision binary64

  :herbie-target
  (if (< t -2.1183266448915811e-50) (/ x (+ x (* y (exp (* 2 (- (+ (* a c) (* 0.83333333333333337 c)) (* a b))))))) (if (< t 5.19658877065154709e-123) (/ x (+ x (* y (exp (* 2 (/ (- (* (* z (sqrt (+ t a))) (* (* 3 t) (- a (/ 5 6)))) (* (- (* (+ (/ 5 6) a) (* 3 t)) 2) (* (- a (/ 5 6)) (* (- b c) t)))) (* (* (* t t) 3) (- a (/ 5 6))))))))) (/ x (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))))))))

  (/ x (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))))))