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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -5.58639378401121532712856205181949823781 \cdot 10^{76} \lor \neg \left(z \le 1.292229734757079339613065030853168892384 \cdot 10^{133}\right):\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot y + z \cdot \left(t - a\right)}{z \cdot b + \mathsf{fma}\left(z, -y, y\right)}\\ \end{array}\]

\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}

↓

\begin{array}{l}
\mathbf{if}\;z \le -5.58639378401121532712856205181949823781 \cdot 10^{76} \lor \neg \left(z \le 1.292229734757079339613065030853168892384 \cdot 10^{133}\right):\\
\;\;\;\;\frac{t}{b} - \frac{a}{b}\\

\mathbf{else}:\\
\;\;\;\;\frac{x \cdot y + z \cdot \left(t - a\right)}{z \cdot b + \mathsf{fma}\left(z, -y, y\right)}\\

\end{array}

double f(double x, double y, double z, double t, double a, double b) {
        double r945246 = x;
        double r945247 = y;
        double r945248 = r945246 * r945247;
        double r945249 = z;
        double r945250 = t;
        double r945251 = a;
        double r945252 = r945250 - r945251;
        double r945253 = r945249 * r945252;
        double r945254 = r945248 + r945253;
        double r945255 = b;
        double r945256 = r945255 - r945247;
        double r945257 = r945249 * r945256;
        double r945258 = r945247 + r945257;
        double r945259 = r945254 / r945258;
        return r945259;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r945260 = z;
        double r945261 = -5.5863937840112153e+76;
        bool r945262 = r945260 <= r945261;
        double r945263 = 1.2922297347570793e+133;
        bool r945264 = r945260 <= r945263;
        double r945265 = !r945264;
        bool r945266 = r945262 || r945265;
        double r945267 = t;
        double r945268 = b;
        double r945269 = r945267 / r945268;
        double r945270 = a;
        double r945271 = r945270 / r945268;
        double r945272 = r945269 - r945271;
        double r945273 = x;
        double r945274 = y;
        double r945275 = r945273 * r945274;
        double r945276 = r945267 - r945270;
        double r945277 = r945260 * r945276;
        double r945278 = r945275 + r945277;
        double r945279 = r945260 * r945268;
        double r945280 = -r945274;
        double r945281 = fma(r945260, r945280, r945274);
        double r945282 = r945279 + r945281;
        double r945283 = r945278 / r945282;
        double r945284 = r945266 ? r945272 : r945283;
        return r945284;
}

Original	22.8
Target	17.6
Herbie	18.9

Derivation

Split input into 2 regimes
if z < -5.5863937840112153e+76 or 1.2922297347570793e+133 < z
1. Initial program 46.2
  \[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\]
2. Using strategy rm
3. Applied sub-neg46.2
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \color{blue}{\left(b + \left(-y\right)\right)}}\]
4. Applied distribute-lft-in46.4
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{y + \color{blue}{\left(z \cdot b + z \cdot \left(-y\right)\right)}}\]
5. Applied associate-+r+46.4
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{\color{blue}{\left(y + z \cdot b\right) + z \cdot \left(-y\right)}}\]
6. Simplified46.4
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{\color{blue}{\mathsf{fma}\left(z, b, y\right)} + z \cdot \left(-y\right)}\]
7. Using strategy rm
8. Applied clear-num46.4
  \[\leadsto \color{blue}{\frac{1}{\frac{\mathsf{fma}\left(z, b, y\right) + z \cdot \left(-y\right)}{x \cdot y + z \cdot \left(t - a\right)}}}\]
9. Simplified46.2
  \[\leadsto \frac{1}{\color{blue}{\frac{\mathsf{fma}\left(b, z, y - z \cdot y\right)}{\mathsf{fma}\left(x, y, z \cdot \left(t - a\right)\right)}}}\]
10. Taylor expanded around inf 34.0
  \[\leadsto \color{blue}{\frac{t}{b} - \frac{a}{b}}\]
if -5.5863937840112153e+76 < z < 1.2922297347570793e+133
1. Initial program 11.8
  \[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\]
2. Using strategy rm
3. Applied sub-neg11.8
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \color{blue}{\left(b + \left(-y\right)\right)}}\]
4. Applied distribute-lft-in11.8
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{y + \color{blue}{\left(z \cdot b + z \cdot \left(-y\right)\right)}}\]
5. Applied associate-+r+11.8
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{\color{blue}{\left(y + z \cdot b\right) + z \cdot \left(-y\right)}}\]
6. Simplified11.8
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{\color{blue}{\mathsf{fma}\left(z, b, y\right)} + z \cdot \left(-y\right)}\]
7. Using strategy rm
8. Applied fma-udef11.8
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{\color{blue}{\left(z \cdot b + y\right)} + z \cdot \left(-y\right)}\]
9. Applied associate-+l+11.8
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{\color{blue}{z \cdot b + \left(y + z \cdot \left(-y\right)\right)}}\]
10. Simplified11.8
  \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{z \cdot b + \color{blue}{\mathsf{fma}\left(z, -y, y\right)}}\]
Recombined 2 regimes into one program.
Final simplification18.9
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -5.58639378401121532712856205181949823781 \cdot 10^{76} \lor \neg \left(z \le 1.292229734757079339613065030853168892384 \cdot 10^{133}\right):\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot y + z \cdot \left(t - a\right)}{z \cdot b + \mathsf{fma}\left(z, -y, y\right)}\\ \end{array}\]

Error

Target

Derivation

`if z < -5.5863937840112153e+76 or 1.2922297347570793e+133 < z`

`if -5.5863937840112153e+76 < z < 1.2922297347570793e+133`

Reproduce