Average Error: 3.8 → 4.4
Time: 31.4s
Precision: 64
\[\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}\]
\[\begin{array}{l} \mathbf{if}\;t \le -5.347055751992442 \cdot 10^{-277}:\\ \;\;\;\;\frac{x}{x + e^{\left(\frac{\left(\left(\sqrt{t + a} \cdot z\right)\right)}{t} - \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{3.0 \cdot t}\right) \cdot \left(b - c\right)\right) \cdot 2.0} \cdot y}\\ \mathbf{elif}\;t \le 1.1946639376173716 \cdot 10^{-306}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \left(\left(\frac{z}{t} \cdot \sqrt{t + a} - \left(\frac{5.0}{6.0} + \left(a - \frac{\frac{2.0}{t}}{3.0}\right)\right) \cdot \left(b - c\right)\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \log \left(e^{\frac{z}{t} \cdot \sqrt{t + a} - \left(\frac{5.0}{6.0} + \left(a - \frac{\frac{2.0}{t}}{3.0}\right)\right) \cdot \left(b - c\right)}\right)}}\\ \end{array}\]
\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}
\begin{array}{l}
\mathbf{if}\;t \le -5.347055751992442 \cdot 10^{-277}:\\
\;\;\;\;\frac{x}{x + e^{\left(\frac{\left(\left(\sqrt{t + a} \cdot z\right)\right)}{t} - \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{3.0 \cdot t}\right) \cdot \left(b - c\right)\right) \cdot 2.0} \cdot y}\\

\mathbf{elif}\;t \le 1.1946639376173716 \cdot 10^{-306}:\\
\;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \left(\left(\frac{z}{t} \cdot \sqrt{t + a} - \left(\frac{5.0}{6.0} + \left(a - \frac{\frac{2.0}{t}}{3.0}\right)\right) \cdot \left(b - c\right)\right)\right)}}\\

\mathbf{else}:\\
\;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \log \left(e^{\frac{z}{t} \cdot \sqrt{t + a} - \left(\frac{5.0}{6.0} + \left(a - \frac{\frac{2.0}{t}}{3.0}\right)\right) \cdot \left(b - c\right)}\right)}}\\

\end{array}
double f(double x, double y, double z, double t, double a, double b, double c) {
        double r20698628 = x;
        double r20698629 = y;
        double r20698630 = 2.0;
        double r20698631 = z;
        double r20698632 = t;
        double r20698633 = a;
        double r20698634 = r20698632 + r20698633;
        double r20698635 = sqrt(r20698634);
        double r20698636 = r20698631 * r20698635;
        double r20698637 = r20698636 / r20698632;
        double r20698638 = b;
        double r20698639 = c;
        double r20698640 = r20698638 - r20698639;
        double r20698641 = 5.0;
        double r20698642 = 6.0;
        double r20698643 = r20698641 / r20698642;
        double r20698644 = r20698633 + r20698643;
        double r20698645 = 3.0;
        double r20698646 = r20698632 * r20698645;
        double r20698647 = r20698630 / r20698646;
        double r20698648 = r20698644 - r20698647;
        double r20698649 = r20698640 * r20698648;
        double r20698650 = r20698637 - r20698649;
        double r20698651 = r20698630 * r20698650;
        double r20698652 = exp(r20698651);
        double r20698653 = r20698629 * r20698652;
        double r20698654 = r20698628 + r20698653;
        double r20698655 = r20698628 / r20698654;
        return r20698655;
}

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r20698656 = t;
        double r20698657 = -5.347055751992442e-277;
        bool r20698658 = r20698656 <= r20698657;
        double r20698659 = x;
        double r20698660 = a;
        double r20698661 = r20698656 + r20698660;
        double r20698662 = sqrt(r20698661);
        double r20698663 = z;
        double r20698664 = r20698662 * r20698663;
        double r20698665 = /* ERROR: no posit support in C */;
        double r20698666 = /* ERROR: no posit support in C */;
        double r20698667 = r20698666 / r20698656;
        double r20698668 = 5.0;
        double r20698669 = 6.0;
        double r20698670 = r20698668 / r20698669;
        double r20698671 = r20698660 + r20698670;
        double r20698672 = 2.0;
        double r20698673 = 3.0;
        double r20698674 = r20698673 * r20698656;
        double r20698675 = r20698672 / r20698674;
        double r20698676 = r20698671 - r20698675;
        double r20698677 = b;
        double r20698678 = c;
        double r20698679 = r20698677 - r20698678;
        double r20698680 = r20698676 * r20698679;
        double r20698681 = r20698667 - r20698680;
        double r20698682 = r20698681 * r20698672;
        double r20698683 = exp(r20698682);
        double r20698684 = y;
        double r20698685 = r20698683 * r20698684;
        double r20698686 = r20698659 + r20698685;
        double r20698687 = r20698659 / r20698686;
        double r20698688 = 1.1946639376173716e-306;
        bool r20698689 = r20698656 <= r20698688;
        double r20698690 = r20698663 / r20698656;
        double r20698691 = r20698690 * r20698662;
        double r20698692 = r20698672 / r20698656;
        double r20698693 = r20698692 / r20698673;
        double r20698694 = r20698660 - r20698693;
        double r20698695 = r20698670 + r20698694;
        double r20698696 = r20698695 * r20698679;
        double r20698697 = r20698691 - r20698696;
        double r20698698 = /* ERROR: no posit support in C */;
        double r20698699 = /* ERROR: no posit support in C */;
        double r20698700 = r20698672 * r20698699;
        double r20698701 = exp(r20698700);
        double r20698702 = r20698684 * r20698701;
        double r20698703 = r20698659 + r20698702;
        double r20698704 = r20698659 / r20698703;
        double r20698705 = exp(r20698697);
        double r20698706 = log(r20698705);
        double r20698707 = r20698672 * r20698706;
        double r20698708 = exp(r20698707);
        double r20698709 = r20698684 * r20698708;
        double r20698710 = r20698659 + r20698709;
        double r20698711 = r20698659 / r20698710;
        double r20698712 = r20698689 ? r20698704 : r20698711;
        double r20698713 = r20698658 ? r20698687 : r20698712;
        return r20698713;
}

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

Original3.8
Target3.1
Herbie4.4
\[\begin{array}{l} \mathbf{if}\;t \lt -2.118326644891581 \cdot 10^{-50}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \left(\left(a \cdot c + 0.8333333333333334 \cdot c\right) - a \cdot b\right)}}\\ \mathbf{elif}\;t \lt 5.196588770651547 \cdot 10^{-123}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \frac{\left(z \cdot \sqrt{t + a}\right) \cdot \left(\left(3.0 \cdot t\right) \cdot \left(a - \frac{5.0}{6.0}\right)\right) - \left(\left(\frac{5.0}{6.0} + a\right) \cdot \left(3.0 \cdot t\right) - 2.0\right) \cdot \left(\left(a - \frac{5.0}{6.0}\right) \cdot \left(\left(b - c\right) \cdot t\right)\right)}{\left(\left(t \cdot t\right) \cdot 3.0\right) \cdot \left(a - \frac{5.0}{6.0}\right)}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}\\ \end{array}\]

Derivation

  1. Split input into 3 regimes
  2. if t < -5.347055751992442e-277

    1. Initial program 4.3

      \[\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}\]
    2. Using strategy rm
    3. Applied insert-posit168.8

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{\color{blue}{\left(\left(z \cdot \sqrt{t + a}\right)\right)}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}\]

    if -5.347055751992442e-277 < t < 1.1946639376173716e-306

    1. Initial program 13.5

      \[\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}\]
    2. Using strategy rm
    3. Applied add-log-exp17.1

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \color{blue}{\log \left(e^{\left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)}\right)}\right)}}\]
    4. Applied add-log-exp28.8

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \left(\color{blue}{\log \left(e^{\frac{z \cdot \sqrt{t + a}}{t}}\right)} - \log \left(e^{\left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)}\right)\right)}}\]
    5. Applied diff-log28.8

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \color{blue}{\log \left(\frac{e^{\frac{z \cdot \sqrt{t + a}}{t}}}{e^{\left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)}}\right)}}}\]
    6. Simplified15.3

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \log \color{blue}{\left(e^{\frac{z}{t} \cdot \sqrt{t + a} - \left(\frac{5.0}{6.0} + \left(a - \frac{\frac{2.0}{t}}{3.0}\right)\right) \cdot \left(b - c\right)}\right)}}}\]
    7. Using strategy rm
    8. Applied insert-posit1626.8

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \color{blue}{\left(\left(\log \left(e^{\frac{z}{t} \cdot \sqrt{t + a} - \left(\frac{5.0}{6.0} + \left(a - \frac{\frac{2.0}{t}}{3.0}\right)\right) \cdot \left(b - c\right)}\right)\right)\right)}}}\]
    9. Simplified23.7

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \color{blue}{\left(\left(\frac{z}{t} \cdot \sqrt{t + a} - \left(\frac{5.0}{6.0} + \left(a - \frac{\frac{2.0}{t}}{3.0}\right)\right) \cdot \left(b - c\right)\right)\right)}}}\]

    if 1.1946639376173716e-306 < t

    1. Initial program 3.2

      \[\frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)\right)}}\]
    2. Using strategy rm
    3. Applied add-log-exp7.4

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \left(\frac{z \cdot \sqrt{t + a}}{t} - \color{blue}{\log \left(e^{\left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)}\right)}\right)}}\]
    4. Applied add-log-exp14.3

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \left(\color{blue}{\log \left(e^{\frac{z \cdot \sqrt{t + a}}{t}}\right)} - \log \left(e^{\left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)}\right)\right)}}\]
    5. Applied diff-log14.3

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \color{blue}{\log \left(\frac{e^{\frac{z \cdot \sqrt{t + a}}{t}}}{e^{\left(b - c\right) \cdot \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{t \cdot 3.0}\right)}}\right)}}}\]
    6. Simplified2.3

      \[\leadsto \frac{x}{x + y \cdot e^{2.0 \cdot \log \color{blue}{\left(e^{\frac{z}{t} \cdot \sqrt{t + a} - \left(\frac{5.0}{6.0} + \left(a - \frac{\frac{2.0}{t}}{3.0}\right)\right) \cdot \left(b - c\right)}\right)}}}\]
  3. Recombined 3 regimes into one program.
  4. Final simplification4.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;t \le -5.347055751992442 \cdot 10^{-277}:\\ \;\;\;\;\frac{x}{x + e^{\left(\frac{\left(\left(\sqrt{t + a} \cdot z\right)\right)}{t} - \left(\left(a + \frac{5.0}{6.0}\right) - \frac{2.0}{3.0 \cdot t}\right) \cdot \left(b - c\right)\right) \cdot 2.0} \cdot y}\\ \mathbf{elif}\;t \le 1.1946639376173716 \cdot 10^{-306}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \left(\left(\frac{z}{t} \cdot \sqrt{t + a} - \left(\frac{5.0}{6.0} + \left(a - \frac{\frac{2.0}{t}}{3.0}\right)\right) \cdot \left(b - c\right)\right)\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{x + y \cdot e^{2.0 \cdot \log \left(e^{\frac{z}{t} \cdot \sqrt{t + a} - \left(\frac{5.0}{6.0} + \left(a - \frac{\frac{2.0}{t}}{3.0}\right)\right) \cdot \left(b - c\right)}\right)}}\\ \end{array}\]

Reproduce

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

  :herbie-target
  (if (< t -2.118326644891581e-50) (/ x (+ x (* y (exp (* 2.0 (- (+ (* a c) (* 0.8333333333333334 c)) (* a b))))))) (if (< t 5.196588770651547e-123) (/ x (+ x (* y (exp (* 2.0 (/ (- (* (* z (sqrt (+ t a))) (* (* 3.0 t) (- a (/ 5.0 6.0)))) (* (- (* (+ (/ 5.0 6.0) a) (* 3.0 t)) 2.0) (* (- a (/ 5.0 6.0)) (* (- b c) t)))) (* (* (* t t) 3.0) (- a (/ 5.0 6.0))))))))) (/ x (+ x (* y (exp (* 2.0 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5.0 6.0)) (/ 2.0 (* t 3.0))))))))))))

  (/ x (+ x (* y (exp (* 2.0 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5.0 6.0)) (/ 2.0 (* t 3.0)))))))))))