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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -7.71025579622562754 \cdot 10^{72} \lor \neg \left(z \le 7.73695011696723767 \cdot 10^{43}\right):\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \mathbf{else}:\\ \;\;\;\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(z \cdot b + y\right) - z \cdot y}\\ \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 -7.71025579622562754 \cdot 10^{72} \lor \neg \left(z \le 7.73695011696723767 \cdot 10^{43}\right):\\
\;\;\;\;\frac{t}{b} - \frac{a}{b}\\

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

\end{array}

double f(double x, double y, double z, double t, double a, double b) {
        double r717319 = x;
        double r717320 = y;
        double r717321 = r717319 * r717320;
        double r717322 = z;
        double r717323 = t;
        double r717324 = a;
        double r717325 = r717323 - r717324;
        double r717326 = r717322 * r717325;
        double r717327 = r717321 + r717326;
        double r717328 = b;
        double r717329 = r717328 - r717320;
        double r717330 = r717322 * r717329;
        double r717331 = r717320 + r717330;
        double r717332 = r717327 / r717331;
        return r717332;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r717333 = z;
        double r717334 = -7.710255796225628e+72;
        bool r717335 = r717333 <= r717334;
        double r717336 = 7.736950116967238e+43;
        bool r717337 = r717333 <= r717336;
        double r717338 = !r717337;
        bool r717339 = r717335 || r717338;
        double r717340 = t;
        double r717341 = b;
        double r717342 = r717340 / r717341;
        double r717343 = a;
        double r717344 = r717343 / r717341;
        double r717345 = r717342 - r717344;
        double r717346 = r717340 - r717343;
        double r717347 = r717333 * r717346;
        double r717348 = x;
        double r717349 = y;
        double r717350 = r717348 * r717349;
        double r717351 = r717347 + r717350;
        double r717352 = r717333 * r717341;
        double r717353 = r717352 + r717349;
        double r717354 = r717333 * r717349;
        double r717355 = r717353 - r717354;
        double r717356 = r717351 / r717355;
        double r717357 = r717339 ? r717345 : r717356;
        return r717357;
}

Original	23.5
Target	18.1
Herbie	20.4

Derivation

Split input into 2 regimes
if z < -7.710255796225628e+72 or 7.736950116967238e+43 < z
1. Initial program 42.5
  \[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\]
2. Using strategy rm
3. Applied clear-num42.6
  \[\leadsto \color{blue}{\frac{1}{\frac{y + z \cdot \left(b - y\right)}{x \cdot y + z \cdot \left(t - a\right)}}}\]
4. Using strategy rm
5. Applied sub-neg42.6
  \[\leadsto \frac{1}{\frac{y + z \cdot \color{blue}{\left(b + \left(-y\right)\right)}}{x \cdot y + z \cdot \left(t - a\right)}}\]
6. Applied distribute-lft-in42.8
  \[\leadsto \frac{1}{\frac{y + \color{blue}{\left(z \cdot b + z \cdot \left(-y\right)\right)}}{x \cdot y + z \cdot \left(t - a\right)}}\]
7. Applied associate-+r+42.8
  \[\leadsto \frac{1}{\frac{\color{blue}{\left(y + z \cdot b\right) + z \cdot \left(-y\right)}}{x \cdot y + z \cdot \left(t - a\right)}}\]
8. Simplified42.8
  \[\leadsto \frac{1}{\frac{\color{blue}{\left(z \cdot b + y\right)} + z \cdot \left(-y\right)}{x \cdot y + z \cdot \left(t - a\right)}}\]
9. Taylor expanded around inf 34.9
  \[\leadsto \color{blue}{\frac{t}{b} - \frac{a}{b}}\]
if -7.710255796225628e+72 < z < 7.736950116967238e+43
1. Initial program 10.6
  \[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\]
2. Using strategy rm
3. Applied clear-num10.7
  \[\leadsto \color{blue}{\frac{1}{\frac{y + z \cdot \left(b - y\right)}{x \cdot y + z \cdot \left(t - a\right)}}}\]
4. Using strategy rm
5. Applied sub-neg10.7
  \[\leadsto \frac{1}{\frac{y + z \cdot \color{blue}{\left(b + \left(-y\right)\right)}}{x \cdot y + z \cdot \left(t - a\right)}}\]
6. Applied distribute-lft-in10.7
  \[\leadsto \frac{1}{\frac{y + \color{blue}{\left(z \cdot b + z \cdot \left(-y\right)\right)}}{x \cdot y + z \cdot \left(t - a\right)}}\]
7. Applied associate-+r+10.7
  \[\leadsto \frac{1}{\frac{\color{blue}{\left(y + z \cdot b\right) + z \cdot \left(-y\right)}}{x \cdot y + z \cdot \left(t - a\right)}}\]
8. Simplified10.7
  \[\leadsto \frac{1}{\frac{\color{blue}{\left(z \cdot b + y\right)} + z \cdot \left(-y\right)}{x \cdot y + z \cdot \left(t - a\right)}}\]
9. Using strategy rm
10. Applied *-un-lft-identity10.7
  \[\leadsto \frac{1}{\frac{\left(z \cdot b + y\right) + z \cdot \left(-y\right)}{\color{blue}{1 \cdot \left(x \cdot y + z \cdot \left(t - a\right)\right)}}}\]
11. Applied *-un-lft-identity10.7
  \[\leadsto \frac{1}{\frac{\color{blue}{1 \cdot \left(\left(z \cdot b + y\right) + z \cdot \left(-y\right)\right)}}{1 \cdot \left(x \cdot y + z \cdot \left(t - a\right)\right)}}\]
12. Applied times-frac10.7
  \[\leadsto \frac{1}{\color{blue}{\frac{1}{1} \cdot \frac{\left(z \cdot b + y\right) + z \cdot \left(-y\right)}{x \cdot y + z \cdot \left(t - a\right)}}}\]
13. Applied add-cube-cbrt10.7
  \[\leadsto \frac{\color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{1}\right) \cdot \sqrt[3]{1}}}{\frac{1}{1} \cdot \frac{\left(z \cdot b + y\right) + z \cdot \left(-y\right)}{x \cdot y + z \cdot \left(t - a\right)}}\]
14. Applied times-frac10.7
  \[\leadsto \color{blue}{\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{\frac{1}{1}} \cdot \frac{\sqrt[3]{1}}{\frac{\left(z \cdot b + y\right) + z \cdot \left(-y\right)}{x \cdot y + z \cdot \left(t - a\right)}}}\]
15. Simplified10.7
  \[\leadsto \color{blue}{1} \cdot \frac{\sqrt[3]{1}}{\frac{\left(z \cdot b + y\right) + z \cdot \left(-y\right)}{x \cdot y + z \cdot \left(t - a\right)}}\]
16. Simplified10.6
  \[\leadsto 1 \cdot \color{blue}{\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(z \cdot b + y\right) - z \cdot y}}\]
Recombined 2 regimes into one program.
Final simplification20.4
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -7.71025579622562754 \cdot 10^{72} \lor \neg \left(z \le 7.73695011696723767 \cdot 10^{43}\right):\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \mathbf{else}:\\ \;\;\;\;\frac{z \cdot \left(t - a\right) + x \cdot y}{\left(z \cdot b + y\right) - z \cdot y}\\ \end{array}\]

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

Error

Try it out

Target

Derivation

`if z < -7.710255796225628e+72 or 7.736950116967238e+43 < z`

`if -7.710255796225628e+72 < z < 7.736950116967238e+43`

Reproduce

In
Out