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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -1.325061842645189516831394970526279941677 \cdot 10^{154}:\\ \;\;\;\;\left(x \cdot y\right) \cdot -1\\ \mathbf{elif}\;z \le 8.769862591561264993872971347546063427107 \cdot 10^{136}:\\ \;\;\;\;\left(x \cdot y\right) \cdot \frac{1}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;z \le -1.325061842645189516831394970526279941677 \cdot 10^{154}:\\
\;\;\;\;\left(x \cdot y\right) \cdot -1\\

\mathbf{elif}\;z \le 8.769862591561264993872971347546063427107 \cdot 10^{136}:\\
\;\;\;\;\left(x \cdot y\right) \cdot \frac{1}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}\\

\mathbf{else}:\\
\;\;\;\;x \cdot y\\

\end{array}

double f(double x, double y, double z, double t, double a) {
        double r276217 = x;
        double r276218 = y;
        double r276219 = r276217 * r276218;
        double r276220 = z;
        double r276221 = r276219 * r276220;
        double r276222 = r276220 * r276220;
        double r276223 = t;
        double r276224 = a;
        double r276225 = r276223 * r276224;
        double r276226 = r276222 - r276225;
        double r276227 = sqrt(r276226);
        double r276228 = r276221 / r276227;
        return r276228;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r276229 = z;
        double r276230 = -1.3250618426451895e+154;
        bool r276231 = r276229 <= r276230;
        double r276232 = x;
        double r276233 = y;
        double r276234 = r276232 * r276233;
        double r276235 = -1.0;
        double r276236 = r276234 * r276235;
        double r276237 = 8.769862591561265e+136;
        bool r276238 = r276229 <= r276237;
        double r276239 = 1.0;
        double r276240 = r276229 * r276229;
        double r276241 = t;
        double r276242 = a;
        double r276243 = r276241 * r276242;
        double r276244 = r276240 - r276243;
        double r276245 = sqrt(r276244);
        double r276246 = r276245 / r276229;
        double r276247 = r276239 / r276246;
        double r276248 = r276234 * r276247;
        double r276249 = r276238 ? r276248 : r276234;
        double r276250 = r276231 ? r276236 : r276249;
        return r276250;
}

Original	25.0
Target	7.7
Herbie	6.3

Derivation

Split input into 3 regimes
if z < -1.3250618426451895e+154
1. Initial program 54.4
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Using strategy rm
3. Applied *-un-lft-identity54.4
  \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{1 \cdot \left(z \cdot z - t \cdot a\right)}}}\]
4. Applied sqrt-prod54.4
  \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\sqrt{1} \cdot \sqrt{z \cdot z - t \cdot a}}}\]
5. Applied times-frac54.0
  \[\leadsto \color{blue}{\frac{x \cdot y}{\sqrt{1}} \cdot \frac{z}{\sqrt{z \cdot z - t \cdot a}}}\]
6. Simplified54.0
  \[\leadsto \color{blue}{\left(x \cdot y\right)} \cdot \frac{z}{\sqrt{z \cdot z - t \cdot a}}\]
7. Taylor expanded around -inf 1.1
  \[\leadsto \left(x \cdot y\right) \cdot \color{blue}{-1}\]
if -1.3250618426451895e+154 < z < 8.769862591561265e+136
1. Initial program 11.2
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Using strategy rm
3. Applied *-un-lft-identity11.2
  \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{1 \cdot \left(z \cdot z - t \cdot a\right)}}}\]
4. Applied sqrt-prod11.2
  \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\sqrt{1} \cdot \sqrt{z \cdot z - t \cdot a}}}\]
5. Applied times-frac8.8
  \[\leadsto \color{blue}{\frac{x \cdot y}{\sqrt{1}} \cdot \frac{z}{\sqrt{z \cdot z - t \cdot a}}}\]
6. Simplified8.8
  \[\leadsto \color{blue}{\left(x \cdot y\right)} \cdot \frac{z}{\sqrt{z \cdot z - t \cdot a}}\]
7. Using strategy rm
8. Applied clear-num8.9
  \[\leadsto \left(x \cdot y\right) \cdot \color{blue}{\frac{1}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
if 8.769862591561265e+136 < z
1. Initial program 49.8
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Using strategy rm
3. Applied *-un-lft-identity49.8
  \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\sqrt{\color{blue}{1 \cdot \left(z \cdot z - t \cdot a\right)}}}\]
4. Applied sqrt-prod49.8
  \[\leadsto \frac{\left(x \cdot y\right) \cdot z}{\color{blue}{\sqrt{1} \cdot \sqrt{z \cdot z - t \cdot a}}}\]
5. Applied times-frac48.6
  \[\leadsto \color{blue}{\frac{x \cdot y}{\sqrt{1}} \cdot \frac{z}{\sqrt{z \cdot z - t \cdot a}}}\]
6. Simplified48.6
  \[\leadsto \color{blue}{\left(x \cdot y\right)} \cdot \frac{z}{\sqrt{z \cdot z - t \cdot a}}\]
7. Using strategy rm
8. Applied add-sqr-sqrt48.6
  \[\leadsto \left(x \cdot y\right) \cdot \frac{z}{\sqrt{\color{blue}{\sqrt{z \cdot z - t \cdot a} \cdot \sqrt{z \cdot z - t \cdot a}}}}\]
9. Applied sqrt-prod48.7
  \[\leadsto \left(x \cdot y\right) \cdot \frac{z}{\color{blue}{\sqrt{\sqrt{z \cdot z - t \cdot a}} \cdot \sqrt{\sqrt{z \cdot z - t \cdot a}}}}\]
10. Taylor expanded around inf 1.7
  \[\leadsto \color{blue}{x \cdot y}\]
Recombined 3 regimes into one program.
Final simplification6.3
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.325061842645189516831394970526279941677 \cdot 10^{154}:\\ \;\;\;\;\left(x \cdot y\right) \cdot -1\\ \mathbf{elif}\;z \le 8.769862591561264993872971347546063427107 \cdot 10^{136}:\\ \;\;\;\;\left(x \cdot y\right) \cdot \frac{1}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array}\]

Error

Try it out

Target

Derivation

`if z < -1.3250618426451895e+154`

`if -1.3250618426451895e+154 < z < 8.769862591561265e+136`

`if 8.769862591561265e+136 < z`

Reproduce

In
Out