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

Average Error: 4.5 → 1.0

Time: 16.6s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\frac{y}{z} - \frac{t}{1 - z} \le -6.342310971280441367479099898482680011803 \cdot 10^{248} \lor \neg \left(\frac{y}{z} - \frac{t}{1 - z} \le -3.416216294383103464023774770379808679927 \cdot 10^{-188} \lor \neg \left(\frac{y}{z} - \frac{t}{1 - z} \le 1.924486920441284773874832647225661147178 \cdot 10^{-111}\right) \land \frac{y}{z} - \frac{t}{1 - z} \le 3.122392901089355157555263365595082273021 \cdot 10^{143}\right):\\ \;\;\;\;\left(-t\right) \cdot \frac{x}{1 - z} + \frac{y \cdot x}{z}\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{y}{z} - \frac{t}{1 - z}\right) \cdot x\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r320754 = x;
        double r320755 = y;
        double r320756 = z;
        double r320757 = r320755 / r320756;
        double r320758 = t;
        double r320759 = 1.0;
        double r320760 = r320759 - r320756;
        double r320761 = r320758 / r320760;
        double r320762 = r320757 - r320761;
        double r320763 = r320754 * r320762;
        return r320763;
}

↓

double f(double x, double y, double z, double t) {
        double r320764 = y;
        double r320765 = z;
        double r320766 = r320764 / r320765;
        double r320767 = t;
        double r320768 = 1.0;
        double r320769 = r320768 - r320765;
        double r320770 = r320767 / r320769;
        double r320771 = r320766 - r320770;
        double r320772 = -6.342310971280441e+248;
        bool r320773 = r320771 <= r320772;
        double r320774 = -3.4162162943831035e-188;
        bool r320775 = r320771 <= r320774;
        double r320776 = 1.9244869204412848e-111;
        bool r320777 = r320771 <= r320776;
        double r320778 = !r320777;
        double r320779 = 3.122392901089355e+143;
        bool r320780 = r320771 <= r320779;
        bool r320781 = r320778 && r320780;
        bool r320782 = r320775 || r320781;
        double r320783 = !r320782;
        bool r320784 = r320773 || r320783;
        double r320785 = -r320767;
        double r320786 = x;
        double r320787 = r320786 / r320769;
        double r320788 = r320785 * r320787;
        double r320789 = r320764 * r320786;
        double r320790 = r320789 / r320765;
        double r320791 = r320788 + r320790;
        double r320792 = r320771 * r320786;
        double r320793 = r320784 ? r320791 : r320792;
        return r320793;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	4.5
Target	4.2
Herbie	1.0

\[\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 z) (/ t (- 1.0 z))) < -6.342310971280441e+248 or -3.4162162943831035e-188 < (- (/ y z) (/ t (- 1.0 z))) < 1.9244869204412848e-111 or 3.122392901089355e+143 < (- (/ y z) (/ t (- 1.0 z)))

   1. Initial program 11.8

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

   3. Applied add-cube-cbrt 11.9

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

   4. Applied associate-/r* 11.9

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

   6. Applied sub-neg 11.9

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

   7. Applied distribute-lft-in 11.9

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

   8. Simplified 3.0

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

   9. Simplified 2.2

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

   if -6.342310971280441e+248 < (- (/ y z) (/ t (- 1.0 z))) < -3.4162162943831035e-188 or 1.9244869204412848e-111 < (- (/ y z) (/ t (- 1.0 z))) < 3.122392901089355e+143

   1. Initial program 0.2

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

   3. Applied add-cube-cbrt 0.5

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

   4. Applied associate-/r* 0.5

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

   6. Applied *-un-lft-identity 0.5

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

   7. Applied associate-*l* 0.5

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

   8. Simplified 0.2

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

4. Final simplification 1.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{y}{z} - \frac{t}{1 - z} \le -6.342310971280441367479099898482680011803 \cdot 10^{248} \lor \neg \left(\frac{y}{z} - \frac{t}{1 - z} \le -3.416216294383103464023774770379808679927 \cdot 10^{-188} \lor \neg \left(\frac{y}{z} - \frac{t}{1 - z} \le 1.924486920441284773874832647225661147178 \cdot 10^{-111}\right) \land \frac{y}{z} - \frac{t}{1 - z} \le 3.122392901089355157555263365595082273021 \cdot 10^{143}\right):\\ \;\;\;\;\left(-t\right) \cdot \frac{x}{1 - z} + \frac{y \cdot x}{z}\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{y}{z} - \frac{t}{1 - z}\right) \cdot x\\ \end{array}\]

Reproduce

herbie shell --seed 2019195 
(FPCore (x y z t)
  :name "Numeric.SpecFunctions:invIncompleteBetaWorker from math-functions-0.1.5.2, C"

  :herbie-target
  (if (< (* x (- (/ y z) (/ t (- 1.0 z)))) -7.623226303312042e-196) (* x (- (/ y z) (* t (/ 1.0 (- 1.0 z))))) (if (< (* x (- (/ y z) (/ t (- 1.0 z)))) 1.4133944927702302e-211) (+ (/ (* y x) z) (- (/ (* t x) (- 1.0 z)))) (* x (- (/ y z) (* t (/ 1.0 (- 1.0 z)))))))

  (* x (- (/ y z) (/ t (- 1.0 z)))))