(FPCore (x y z t a b)
:precision binary64
(/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))))
↓
(FPCore (x y z t a b)
:precision binary64
(let* ((t_1 (/ (- t a) (- b y)))
(t_2 (+ y (* z (- b y))))
(t_3 (* z (- t a)))
(t_4 (/ (+ (* x y) t_3) t_2))
(t_5 (+ (/ t_3 t_2) (/ (* x y) t_2))))
(if (<= t_4 (- INFINITY))
x
(if (<= t_4 -5e-197)
t_5
(if (<= t_4 0.0)
t_1
(if (<= t_4 5e+287)
t_5
(if (<= t_4 INFINITY)
(/ x (- 1.0 z))
(+
t_1
(/
(- (* x (/ y (- b y))) (* y (/ (- t a) (pow (- b y) 2.0))))
z)))))))))
double code(double x, double y, double z, double t, double a, double b) {
return ((x * y) + (z * (t - a))) / (y + (z * (b - y)));
}
\[\frac{z \cdot t + y \cdot x}{y + z \cdot \left(b - y\right)} - \frac{a}{\left(b - y\right) + \frac{y}{z}}
\]
Derivation
Split input into 5 regimes
if (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < -inf.0
Initial program 64.0
\[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}
\]
Taylor expanded in z around 0 37.3
\[\leadsto \color{blue}{x}
\]
if -inf.0 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < -5.0000000000000002e-197 or 0.0 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < 5e287
Initial program 0.3
\[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}
\]
if -5.0000000000000002e-197 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < 0.0
Initial program 37.3
\[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}
\]
Taylor expanded in z around inf 18.9
\[\leadsto \color{blue}{\frac{t - a}{b - y}}
\]
if 5e287 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < +inf.0
Initial program 59.6
\[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}
\]
Taylor expanded in y around inf 34.5
\[\leadsto \color{blue}{\frac{x}{-1 \cdot z + 1}}
\]
Simplified34.5
\[\leadsto \color{blue}{\frac{x}{1 - z}}
\]
Proof
(/.f64 x (-.f64 1 z)): 0 points increase in error, 0 points decrease in error
(/.f64 x (Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 z)))): 0 points increase in error, 0 points decrease in error
(/.f64 x (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 z) 1))): 0 points increase in error, 0 points decrease in error
(/.f64 x (+.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 z)) 1)): 0 points increase in error, 0 points decrease in error
if +inf.0 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y))))
Initial program 64.0
\[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}
\]
Simplified64.0
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(x, y, z \cdot \left(t - a\right)\right)}{y + z \cdot \left(b - y\right)}}
\]
Proof
(/.f64 (fma.f64 x y (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a)))) (+.f64 y (*.f64 z (-.f64 b y)))): 1 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 1 (-.f64 (*.f64 (/.f64 y (-.f64 b y)) x) (*.f64 (/.f64 (-.f64 t a) (pow.f64 (-.f64 b y) 2)) y))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (Rewrite<= metadata-eval (*.f64 -1 -1)) (-.f64 (*.f64 (/.f64 y (-.f64 b y)) x) (*.f64 (/.f64 (-.f64 t a) (pow.f64 (-.f64 b y) 2)) y))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (*.f64 -1 -1) (-.f64 (Rewrite<= associate-/r/_binary64 (/.f64 y (/.f64 (-.f64 b y) x))) (*.f64 (/.f64 (-.f64 t a) (pow.f64 (-.f64 b y) 2)) y))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 9 points increase in error, 18 points decrease in error
(+.f64 (/.f64 (*.f64 (*.f64 -1 -1) (-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 (/.f64 (-.f64 t a) (pow.f64 (-.f64 b y) 2)) y))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 34 points increase in error, 10 points decrease in error
(+.f64 (/.f64 (*.f64 (*.f64 -1 -1) (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 t a) (/.f64 (pow.f64 (-.f64 b y) 2) y))))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 2 points increase in error, 10 points decrease in error
(+.f64 (/.f64 (*.f64 (*.f64 -1 -1) (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2))))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 42 points increase in error, 3 points decrease in error
(+.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 -1 (-.f64 (/.f64 (*.f64 y x) (-.f64 b y)) (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 -1 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))))) z) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z))) (/.f64 (-.f64 t a) (-.f64 b y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z)) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 t (-.f64 b y)) (/.f64 a (-.f64 b y))))): 3 points increase in error, 1 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z)) (/.f64 t (-.f64 b y))) (/.f64 a (-.f64 b y)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 t (-.f64 b y)) (*.f64 -1 (/.f64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y x) (-.f64 b y))) (*.f64 -1 (/.f64 (*.f64 (-.f64 t a) y) (pow.f64 (-.f64 b y) 2)))) z)))) (/.f64 a (-.f64 b y))): 0 points increase in error, 0 points decrease in error
Recombined 5 regimes into one program.
Final simplification8.0
\[\leadsto \begin{array}{l}
\mathbf{if}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq -\infty:\\
\;\;\;\;x\\
\mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq -5 \cdot 10^{-197}:\\
\;\;\;\;\frac{z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} + \frac{x \cdot y}{y + z \cdot \left(b - y\right)}\\
\mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq 0:\\
\;\;\;\;\frac{t - a}{b - y}\\
\mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq 5 \cdot 10^{+287}:\\
\;\;\;\;\frac{z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} + \frac{x \cdot y}{y + z \cdot \left(b - y\right)}\\
\mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq \infty:\\
\;\;\;\;\frac{x}{1 - z}\\
\mathbf{else}:\\
\;\;\;\;\frac{t - a}{b - y} + \frac{x \cdot \frac{y}{b - y} - y \cdot \frac{t - a}{{\left(b - y\right)}^{2}}}{z}\\
\end{array}
\]
herbie shell --seed 2022330
(FPCore (x y z t a b)
:name "Development.Shake.Progress:decay from shake-0.15.5"
:precision binary64
:herbie-target
(- (/ (+ (* z t) (* y x)) (+ y (* z (- b y)))) (/ a (+ (- b y) (/ y z))))
(/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))))