\[\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{x \cdot y + z \cdot \left(t - a\right)}{z \cdot \left(b - y\right) + 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{x \cdot y + z \cdot \left(t - a\right)}{z \cdot \left(b - y\right) + y}\\

\end{array}

double f(double x, double y, double z, double t, double a, double b) {
        double r896824 = x;
        double r896825 = y;
        double r896826 = r896824 * r896825;
        double r896827 = z;
        double r896828 = t;
        double r896829 = a;
        double r896830 = r896828 - r896829;
        double r896831 = r896827 * r896830;
        double r896832 = r896826 + r896831;
        double r896833 = b;
        double r896834 = r896833 - r896825;
        double r896835 = r896827 * r896834;
        double r896836 = r896825 + r896835;
        double r896837 = r896832 / r896836;
        return r896837;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r896838 = z;
        double r896839 = -7.710255796225628e+72;
        bool r896840 = r896838 <= r896839;
        double r896841 = 7.736950116967238e+43;
        bool r896842 = r896838 <= r896841;
        double r896843 = !r896842;
        bool r896844 = r896840 || r896843;
        double r896845 = t;
        double r896846 = b;
        double r896847 = r896845 / r896846;
        double r896848 = a;
        double r896849 = r896848 / r896846;
        double r896850 = r896847 - r896849;
        double r896851 = x;
        double r896852 = y;
        double r896853 = r896851 * r896852;
        double r896854 = r896845 - r896848;
        double r896855 = r896838 * r896854;
        double r896856 = r896853 + r896855;
        double r896857 = r896846 - r896852;
        double r896858 = r896838 * r896857;
        double r896859 = r896858 + r896852;
        double r896860 = r896856 / r896859;
        double r896861 = r896844 ? r896850 : r896860;
        return r896861;
}

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{x \cdot y + z \cdot \left(t - a\right)}{z \cdot \left(b - y\right) + 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{x \cdot y + z \cdot \left(t - a\right)}{z \cdot \left(b - y\right) + 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