\[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}:\\ \;\;\;\;\left(\frac{1}{z} + 1\right) \cdot \frac{t \cdot x}{z} + \frac{x \cdot y}{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}:\\
\;\;\;\;\left(\frac{1}{z} + 1\right) \cdot \frac{t \cdot x}{z} + \frac{x \cdot y}{z}\\

\end{array}

double f(double x, double y, double z, double t) {
        double r468216 = x;
        double r468217 = y;
        double r468218 = z;
        double r468219 = r468217 / r468218;
        double r468220 = t;
        double r468221 = 1.0;
        double r468222 = r468221 - r468218;
        double r468223 = r468220 / r468222;
        double r468224 = r468219 - r468223;
        double r468225 = r468216 * r468224;
        return r468225;
}

↓

double f(double x, double y, double z, double t) {
        double r468226 = y;
        double r468227 = z;
        double r468228 = r468226 / r468227;
        double r468229 = t;
        double r468230 = 1.0;
        double r468231 = r468230 - r468227;
        double r468232 = r468229 / r468231;
        double r468233 = r468228 - r468232;
        double r468234 = -7.71513312838218e+306;
        bool r468235 = r468233 <= r468234;
        double r468236 = x;
        double r468237 = r468236 * r468226;
        double r468238 = r468237 / r468227;
        double r468239 = r468232 * r468236;
        double r468240 = -r468239;
        double r468241 = r468238 + r468240;
        double r468242 = -9.413343469462004e-214;
        bool r468243 = r468233 <= r468242;
        double r468244 = 0.0;
        bool r468245 = r468233 <= r468244;
        double r468246 = !r468245;
        bool r468247 = r468243 || r468246;
        double r468248 = 1.0;
        double r468249 = r468248 / r468231;
        double r468250 = r468229 * r468249;
        double r468251 = r468228 - r468250;
        double r468252 = r468236 * r468251;
        double r468253 = r468230 / r468227;
        double r468254 = r468253 + r468248;
        double r468255 = r468229 * r468236;
        double r468256 = r468255 / r468227;
        double r468257 = r468254 * r468256;
        double r468258 = r468257 + r468238;
        double r468259 = r468247 ? r468252 : r468258;
        double r468260 = r468235 ? r468241 : r468259;
        return r468260;
}

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}{\left(\frac{1}{z} + 1\right) \cdot \frac{t \cdot x}{z} + \frac{x \cdot y}{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}:\\ \;\;\;\;\left(\frac{1}{z} + 1\right) \cdot \frac{t \cdot x}{z} + \frac{x \cdot y}{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