\[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(1 \cdot \frac{t \cdot x}{{z}^{2}} + \frac{t \cdot x}{z}\right)\\ \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(1 \cdot \frac{t \cdot x}{{z}^{2}} + \frac{t \cdot x}{z}\right)\\

\end{array}

double f(double x, double y, double z, double t) {
        double r443543 = x;
        double r443544 = y;
        double r443545 = z;
        double r443546 = r443544 / r443545;
        double r443547 = t;
        double r443548 = 1.0;
        double r443549 = r443548 - r443545;
        double r443550 = r443547 / r443549;
        double r443551 = r443546 - r443550;
        double r443552 = r443543 * r443551;
        return r443552;
}

↓

double f(double x, double y, double z, double t) {
        double r443553 = y;
        double r443554 = z;
        double r443555 = r443553 / r443554;
        double r443556 = t;
        double r443557 = 1.0;
        double r443558 = r443557 - r443554;
        double r443559 = r443556 / r443558;
        double r443560 = r443555 - r443559;
        double r443561 = -7.71513312838218e+306;
        bool r443562 = r443560 <= r443561;
        double r443563 = x;
        double r443564 = r443563 * r443553;
        double r443565 = r443564 / r443554;
        double r443566 = r443559 * r443563;
        double r443567 = -r443566;
        double r443568 = r443565 + r443567;
        double r443569 = -9.413343469462004e-214;
        bool r443570 = r443560 <= r443569;
        double r443571 = 0.0;
        bool r443572 = r443560 <= r443571;
        double r443573 = !r443572;
        bool r443574 = r443570 || r443573;
        double r443575 = 1.0;
        double r443576 = r443575 / r443558;
        double r443577 = r443556 * r443576;
        double r443578 = r443555 - r443577;
        double r443579 = r443563 * r443578;
        double r443580 = r443556 * r443563;
        double r443581 = 2.0;
        double r443582 = pow(r443554, r443581);
        double r443583 = r443580 / r443582;
        double r443584 = r443557 * r443583;
        double r443585 = r443580 / r443554;
        double r443586 = r443584 + r443585;
        double r443587 = r443565 + r443586;
        double r443588 = r443574 ? r443579 : r443587;
        double r443589 = r443562 ? r443568 : r443588;
        return r443589;
}

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)}\]
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(1 \cdot \frac{t \cdot x}{{z}^{2}} + \frac{t \cdot x}{z}\right)\\ \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