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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -3.0286624309368284 \cdot 10^{146}:\\ \;\;\;\;x \cdot \left(-1 \cdot y\right)\\ \mathbf{elif}\;z \le 2.6367843017119099 \cdot 10^{123}:\\ \;\;\;\;x \cdot \frac{y}{\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 -3.0286624309368284 \cdot 10^{146}:\\
\;\;\;\;x \cdot \left(-1 \cdot y\right)\\

\mathbf{elif}\;z \le 2.6367843017119099 \cdot 10^{123}:\\
\;\;\;\;x \cdot \frac{y}{\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 r236228 = x;
        double r236229 = y;
        double r236230 = r236228 * r236229;
        double r236231 = z;
        double r236232 = r236230 * r236231;
        double r236233 = r236231 * r236231;
        double r236234 = t;
        double r236235 = a;
        double r236236 = r236234 * r236235;
        double r236237 = r236233 - r236236;
        double r236238 = sqrt(r236237);
        double r236239 = r236232 / r236238;
        return r236239;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r236240 = z;
        double r236241 = -3.0286624309368284e+146;
        bool r236242 = r236240 <= r236241;
        double r236243 = x;
        double r236244 = -1.0;
        double r236245 = y;
        double r236246 = r236244 * r236245;
        double r236247 = r236243 * r236246;
        double r236248 = 2.63678430171191e+123;
        bool r236249 = r236240 <= r236248;
        double r236250 = r236240 * r236240;
        double r236251 = t;
        double r236252 = a;
        double r236253 = r236251 * r236252;
        double r236254 = r236250 - r236253;
        double r236255 = sqrt(r236254);
        double r236256 = r236255 / r236240;
        double r236257 = r236245 / r236256;
        double r236258 = r236243 * r236257;
        double r236259 = r236243 * r236245;
        double r236260 = r236249 ? r236258 : r236259;
        double r236261 = r236242 ? r236247 : r236260;
        return r236261;
}

Original	25.0
Target	8.0
Herbie	6.1

Derivation

Split input into 3 regimes
if z < -3.0286624309368284e+146
1. Initial program 52.7
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Using strategy rm
3. Applied associate-/l*51.7
  \[\leadsto \color{blue}{\frac{x \cdot y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
4. Using strategy rm
5. Applied *-un-lft-identity51.7
  \[\leadsto \frac{x \cdot y}{\frac{\sqrt{z \cdot z - t \cdot a}}{\color{blue}{1 \cdot z}}}\]
6. Applied *-un-lft-identity51.7
  \[\leadsto \frac{x \cdot y}{\frac{\sqrt{\color{blue}{1 \cdot \left(z \cdot z - t \cdot a\right)}}}{1 \cdot z}}\]
7. Applied sqrt-prod51.7
  \[\leadsto \frac{x \cdot y}{\frac{\color{blue}{\sqrt{1} \cdot \sqrt{z \cdot z - t \cdot a}}}{1 \cdot z}}\]
8. Applied times-frac51.7
  \[\leadsto \frac{x \cdot y}{\color{blue}{\frac{\sqrt{1}}{1} \cdot \frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
9. Applied times-frac51.7
  \[\leadsto \color{blue}{\frac{x}{\frac{\sqrt{1}}{1}} \cdot \frac{y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
10. Simplified51.7
  \[\leadsto \color{blue}{x} \cdot \frac{y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}\]
11. Taylor expanded around -inf 1.5
  \[\leadsto x \cdot \color{blue}{\left(-1 \cdot y\right)}\]
if -3.0286624309368284e+146 < z < 2.63678430171191e+123
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 associate-/l*9.0
  \[\leadsto \color{blue}{\frac{x \cdot y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
4. Using strategy rm
5. Applied *-un-lft-identity9.0
  \[\leadsto \frac{x \cdot y}{\frac{\sqrt{z \cdot z - t \cdot a}}{\color{blue}{1 \cdot z}}}\]
6. Applied *-un-lft-identity9.0
  \[\leadsto \frac{x \cdot y}{\frac{\sqrt{\color{blue}{1 \cdot \left(z \cdot z - t \cdot a\right)}}}{1 \cdot z}}\]
7. Applied sqrt-prod9.0
  \[\leadsto \frac{x \cdot y}{\frac{\color{blue}{\sqrt{1} \cdot \sqrt{z \cdot z - t \cdot a}}}{1 \cdot z}}\]
8. Applied times-frac9.0
  \[\leadsto \frac{x \cdot y}{\color{blue}{\frac{\sqrt{1}}{1} \cdot \frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
9. Applied times-frac8.5
  \[\leadsto \color{blue}{\frac{x}{\frac{\sqrt{1}}{1}} \cdot \frac{y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
10. Simplified8.5
  \[\leadsto \color{blue}{x} \cdot \frac{y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}\]
if 2.63678430171191e+123 < z
1. Initial program 48.7
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Taylor expanded around inf 1.4
  \[\leadsto \color{blue}{x \cdot y}\]
Recombined 3 regimes into one program.
Final simplification6.1
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -3.0286624309368284 \cdot 10^{146}:\\ \;\;\;\;x \cdot \left(-1 \cdot y\right)\\ \mathbf{elif}\;z \le 2.6367843017119099 \cdot 10^{123}:\\ \;\;\;\;x \cdot \frac{y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array}\]

Error

Try it out

Target

Derivation

`if z < -3.0286624309368284e+146`

`if -3.0286624309368284e+146 < z < 2.63678430171191e+123`

`if 2.63678430171191e+123 < z`

Reproduce

In
Out