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

↓

\[\begin{array}{l} \mathbf{if}\;\frac{y}{z} - \frac{t}{1 - z} \le -7.7151331283821803 \cdot 10^{306}:\\ \;\;\;\;\frac{x \cdot y}{z} + \left(-\frac{t}{1 - z} \cdot x\right)\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le -9.4133434694620043 \cdot 10^{-214} \lor \neg \left(\frac{y}{z} - \frac{t}{1 - z} \le 0.0\right):\\ \;\;\;\;x \cdot \left(\frac{y}{z} - t \cdot \frac{1}{1 - z}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot y}{z} + \left(\frac{1}{z} + 1\right) \cdot \frac{t \cdot x}{z}\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\frac{y}{z} - \frac{t}{1 - z} \le -7.7151331283821803 \cdot 10^{306}:\\
\;\;\;\;\frac{x \cdot y}{z} + \left(-\frac{t}{1 - z} \cdot x\right)\\

\mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le -9.4133434694620043 \cdot 10^{-214} \lor \neg \left(\frac{y}{z} - \frac{t}{1 - z} \le 0.0\right):\\
\;\;\;\;x \cdot \left(\frac{y}{z} - t \cdot \frac{1}{1 - z}\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{x \cdot y}{z} + \left(\frac{1}{z} + 1\right) \cdot \frac{t \cdot x}{z}\\

\end{array}

double f(double x, double y, double z, double t) {
        double r477906 = x;
        double r477907 = y;
        double r477908 = z;
        double r477909 = r477907 / r477908;
        double r477910 = t;
        double r477911 = 1.0;
        double r477912 = r477911 - r477908;
        double r477913 = r477910 / r477912;
        double r477914 = r477909 - r477913;
        double r477915 = r477906 * r477914;
        return r477915;
}

↓

double f(double x, double y, double z, double t) {
        double r477916 = y;
        double r477917 = z;
        double r477918 = r477916 / r477917;
        double r477919 = t;
        double r477920 = 1.0;
        double r477921 = r477920 - r477917;
        double r477922 = r477919 / r477921;
        double r477923 = r477918 - r477922;
        double r477924 = -7.71513312838218e+306;
        bool r477925 = r477923 <= r477924;
        double r477926 = x;
        double r477927 = r477926 * r477916;
        double r477928 = r477927 / r477917;
        double r477929 = r477922 * r477926;
        double r477930 = -r477929;
        double r477931 = r477928 + r477930;
        double r477932 = -9.413343469462004e-214;
        bool r477933 = r477923 <= r477932;
        double r477934 = 0.0;
        bool r477935 = r477923 <= r477934;
        double r477936 = !r477935;
        bool r477937 = r477933 || r477936;
        double r477938 = 1.0;
        double r477939 = r477938 / r477921;
        double r477940 = r477919 * r477939;
        double r477941 = r477918 - r477940;
        double r477942 = r477926 * r477941;
        double r477943 = r477920 / r477917;
        double r477944 = r477943 + r477938;
        double r477945 = r477919 * r477926;
        double r477946 = r477945 / r477917;
        double r477947 = r477944 * r477946;
        double r477948 = r477928 + r477947;
        double r477949 = r477937 ? r477942 : r477948;
        double r477950 = r477925 ? r477931 : r477949;
        return r477950;
}

Original	4.8
Target	4.4
Herbie	2.0

Derivation

Split input into 3 regimes
if (- (/ y z) (/ t (- 1.0 z))) < -7.71513312838218e+306
1. Initial program 61.8
  \[x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right)\]
2. Using strategy rm
3. Applied div-inv61.8
  \[\leadsto x \cdot \left(\frac{y}{z} - \color{blue}{t \cdot \frac{1}{1 - z}}\right)\]
4. Using strategy rm
5. Applied sub-neg61.8
  \[\leadsto x \cdot \color{blue}{\left(\frac{y}{z} + \left(-t \cdot \frac{1}{1 - z}\right)\right)}\]
6. Applied distribute-lft-in61.8
  \[\leadsto \color{blue}{x \cdot \frac{y}{z} + x \cdot \left(-t \cdot \frac{1}{1 - z}\right)}\]
7. Simplified0.3
  \[\leadsto \color{blue}{\frac{x \cdot y}{z}} + x \cdot \left(-t \cdot \frac{1}{1 - z}\right)\]
8. Simplified0.3
  \[\leadsto \frac{x \cdot y}{z} + \color{blue}{\left(-\frac{t}{1 - z} \cdot x\right)}\]
if -7.71513312838218e+306 < (- (/ y z) (/ t (- 1.0 z))) < -9.413343469462004e-214 or 0.0 < (- (/ y z) (/ t (- 1.0 z)))
1. Initial program 2.1
  \[x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right)\]
2. Using strategy rm
3. Applied div-inv2.2
  \[\leadsto x \cdot \left(\frac{y}{z} - \color{blue}{t \cdot \frac{1}{1 - z}}\right)\]
if -9.413343469462004e-214 < (- (/ y z) (/ t (- 1.0 z))) < 0.0
1. Initial program 13.3
  \[x \cdot \left(\frac{y}{z} - \frac{t}{1 - z}\right)\]
2. Taylor expanded around inf 1.3
  \[\leadsto \color{blue}{\frac{x \cdot y}{z} + \left(1 \cdot \frac{t \cdot x}{{z}^{2}} + \frac{t \cdot x}{z}\right)}\]
3. Simplified1.3
  \[\leadsto \color{blue}{\frac{x \cdot y}{z} + \left(\frac{1}{z} + 1\right) \cdot \frac{t \cdot x}{z}}\]
Recombined 3 regimes into one program.
Final simplification2.0
\[\leadsto \begin{array}{l} \mathbf{if}\;\frac{y}{z} - \frac{t}{1 - z} \le -7.7151331283821803 \cdot 10^{306}:\\ \;\;\;\;\frac{x \cdot y}{z} + \left(-\frac{t}{1 - z} \cdot x\right)\\ \mathbf{elif}\;\frac{y}{z} - \frac{t}{1 - z} \le -9.4133434694620043 \cdot 10^{-214} \lor \neg \left(\frac{y}{z} - \frac{t}{1 - z} \le 0.0\right):\\ \;\;\;\;x \cdot \left(\frac{y}{z} - t \cdot \frac{1}{1 - z}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot y}{z} + \left(\frac{1}{z} + 1\right) \cdot \frac{t \cdot x}{z}\\ \end{array}\]

Reproduce

herbie shell --seed 2020047 
(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)))))

Falling back on racket egraph because egg-herbie package not installed (more)

Error

Try it out

Target

Derivation

`if (- (/ y z) (/ t (- 1.0 z))) < -7.71513312838218e+306`

`if -7.71513312838218e+306 < (- (/ y z) (/ t (- 1.0 z))) < -9.413343469462004e-214 or 0.0 < (- (/ y z) (/ t (- 1.0 z)))`

`if -9.413343469462004e-214 < (- (/ y z) (/ t (- 1.0 z))) < 0.0`

Reproduce

In
Out