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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -4.812224200595293507689589697171458927979 \cdot 10^{164} \lor \neg \left(z \le 1.500183368090720918883242645080141003947 \cdot 10^{85}\right):\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(b - y, z, y\right)} \cdot \left(\left(\left(-a\right) \cdot z + t \cdot z\right) + x \cdot 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 -4.812224200595293507689589697171458927979 \cdot 10^{164} \lor \neg \left(z \le 1.500183368090720918883242645080141003947 \cdot 10^{85}\right):\\
\;\;\;\;\frac{t}{b} - \frac{a}{b}\\

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

\end{array}

double f(double x, double y, double z, double t, double a, double b) {
        double r592188 = x;
        double r592189 = y;
        double r592190 = r592188 * r592189;
        double r592191 = z;
        double r592192 = t;
        double r592193 = a;
        double r592194 = r592192 - r592193;
        double r592195 = r592191 * r592194;
        double r592196 = r592190 + r592195;
        double r592197 = b;
        double r592198 = r592197 - r592189;
        double r592199 = r592191 * r592198;
        double r592200 = r592189 + r592199;
        double r592201 = r592196 / r592200;
        return r592201;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r592202 = z;
        double r592203 = -4.812224200595294e+164;
        bool r592204 = r592202 <= r592203;
        double r592205 = 1.500183368090721e+85;
        bool r592206 = r592202 <= r592205;
        double r592207 = !r592206;
        bool r592208 = r592204 || r592207;
        double r592209 = t;
        double r592210 = b;
        double r592211 = r592209 / r592210;
        double r592212 = a;
        double r592213 = r592212 / r592210;
        double r592214 = r592211 - r592213;
        double r592215 = 1.0;
        double r592216 = y;
        double r592217 = r592210 - r592216;
        double r592218 = fma(r592217, r592202, r592216);
        double r592219 = r592215 / r592218;
        double r592220 = -r592212;
        double r592221 = r592220 * r592202;
        double r592222 = r592209 * r592202;
        double r592223 = r592221 + r592222;
        double r592224 = x;
        double r592225 = r592224 * r592216;
        double r592226 = r592223 + r592225;
        double r592227 = r592219 * r592226;
        double r592228 = r592208 ? r592214 : r592227;
        return r592228;
}

Original	23.1
Target	17.9
Herbie	19.1

Derivation

Split input into 2 regimes
if z < -4.812224200595294e+164 or 1.500183368090721e+85 < z
1. Initial program 48.3
  \[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\]
2. Using strategy rm
3. Applied sub-neg48.3
  \[\leadsto \frac{x \cdot y + z \cdot \color{blue}{\left(t + \left(-a\right)\right)}}{y + z \cdot \left(b - y\right)}\]
4. Applied distribute-lft-in48.3
  \[\leadsto \frac{x \cdot y + \color{blue}{\left(z \cdot t + z \cdot \left(-a\right)\right)}}{y + z \cdot \left(b - y\right)}\]
5. Simplified48.3
  \[\leadsto \frac{x \cdot y + \left(z \cdot t + \color{blue}{\left(-a \cdot z\right)}\right)}{y + z \cdot \left(b - y\right)}\]
6. Using strategy rm
7. Applied clear-num48.3
  \[\leadsto \color{blue}{\frac{1}{\frac{y + z \cdot \left(b - y\right)}{x \cdot y + \left(z \cdot t + \left(-a \cdot z\right)\right)}}}\]
8. Simplified48.3
  \[\leadsto \frac{1}{\color{blue}{\frac{\mathsf{fma}\left(b - y, z, y\right)}{\mathsf{fma}\left(x, y, \left(t - a\right) \cdot z\right)}}}\]
9. Taylor expanded around inf 34.0
  \[\leadsto \color{blue}{\frac{t}{b} - \frac{a}{b}}\]
if -4.812224200595294e+164 < z < 1.500183368090721e+85
1. Initial program 13.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-neg13.2
  \[\leadsto \frac{x \cdot y + z \cdot \color{blue}{\left(t + \left(-a\right)\right)}}{y + z \cdot \left(b - y\right)}\]
4. Applied distribute-lft-in13.2
  \[\leadsto \frac{x \cdot y + \color{blue}{\left(z \cdot t + z \cdot \left(-a\right)\right)}}{y + z \cdot \left(b - y\right)}\]
5. Simplified13.2
  \[\leadsto \frac{x \cdot y + \left(z \cdot t + \color{blue}{\left(-a \cdot z\right)}\right)}{y + z \cdot \left(b - y\right)}\]
6. Using strategy rm
7. Applied div-inv13.3
  \[\leadsto \color{blue}{\left(x \cdot y + \left(z \cdot t + \left(-a \cdot z\right)\right)\right) \cdot \frac{1}{y + z \cdot \left(b - y\right)}}\]
8. Simplified13.3
  \[\leadsto \left(x \cdot y + \left(z \cdot t + \left(-a \cdot z\right)\right)\right) \cdot \color{blue}{\frac{1}{\mathsf{fma}\left(b - y, z, y\right)}}\]
Recombined 2 regimes into one program.
Final simplification19.1
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -4.812224200595293507689589697171458927979 \cdot 10^{164} \lor \neg \left(z \le 1.500183368090720918883242645080141003947 \cdot 10^{85}\right):\\ \;\;\;\;\frac{t}{b} - \frac{a}{b}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\mathsf{fma}\left(b - y, z, y\right)} \cdot \left(\left(\left(-a\right) \cdot z + t \cdot z\right) + x \cdot y\right)\\ \end{array}\]

Error

Target

Derivation

`if z < -4.812224200595294e+164 or 1.500183368090721e+85 < z`

`if -4.812224200595294e+164 < z < 1.500183368090721e+85`

Reproduce