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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -6395336884503866936309996195044608815661000:\\ \;\;\;\;x \cdot \left(-y\right)\\ \mathbf{elif}\;z \le 7.643275720107879512063854532156486714456 \cdot 10^{117}:\\ \;\;\;\;\frac{x}{\sqrt{\sqrt{z \cdot z - a \cdot t}}} \cdot \frac{y \cdot z}{\sqrt{\sqrt{z \cdot z - a \cdot t}}}\\ \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 -6395336884503866936309996195044608815661000:\\
\;\;\;\;x \cdot \left(-y\right)\\

\mathbf{elif}\;z \le 7.643275720107879512063854532156486714456 \cdot 10^{117}:\\
\;\;\;\;\frac{x}{\sqrt{\sqrt{z \cdot z - a \cdot t}}} \cdot \frac{y \cdot z}{\sqrt{\sqrt{z \cdot z - a \cdot t}}}\\

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

\end{array}

double f(double x, double y, double z, double t, double a) {
        double r264521 = x;
        double r264522 = y;
        double r264523 = r264521 * r264522;
        double r264524 = z;
        double r264525 = r264523 * r264524;
        double r264526 = r264524 * r264524;
        double r264527 = t;
        double r264528 = a;
        double r264529 = r264527 * r264528;
        double r264530 = r264526 - r264529;
        double r264531 = sqrt(r264530);
        double r264532 = r264525 / r264531;
        return r264532;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r264533 = z;
        double r264534 = -6.395336884503867e+42;
        bool r264535 = r264533 <= r264534;
        double r264536 = x;
        double r264537 = y;
        double r264538 = -r264537;
        double r264539 = r264536 * r264538;
        double r264540 = 7.64327572010788e+117;
        bool r264541 = r264533 <= r264540;
        double r264542 = r264533 * r264533;
        double r264543 = a;
        double r264544 = t;
        double r264545 = r264543 * r264544;
        double r264546 = r264542 - r264545;
        double r264547 = sqrt(r264546);
        double r264548 = sqrt(r264547);
        double r264549 = r264536 / r264548;
        double r264550 = r264537 * r264533;
        double r264551 = r264550 / r264548;
        double r264552 = r264549 * r264551;
        double r264553 = r264536 * r264537;
        double r264554 = r264541 ? r264552 : r264553;
        double r264555 = r264535 ? r264539 : r264554;
        return r264555;
}

Original	24.9
Target	7.9
Herbie	7.8

Derivation

Split input into 3 regimes
if z < -6.395336884503867e+42
1. Initial program 37.0
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Simplified36.5
  \[\leadsto \color{blue}{\frac{x \cdot y}{\sqrt{z \cdot z - a \cdot t}} \cdot z}\]
3. Using strategy rm
4. Applied div-inv36.6
  \[\leadsto \color{blue}{\left(\left(x \cdot y\right) \cdot \frac{1}{\sqrt{z \cdot z - a \cdot t}}\right)} \cdot z\]
5. Applied associate-*l*34.3
  \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \left(\frac{1}{\sqrt{z \cdot z - a \cdot t}} \cdot z\right)}\]
6. Simplified34.3
  \[\leadsto \left(x \cdot y\right) \cdot \color{blue}{\frac{z}{\sqrt{z \cdot z - a \cdot t}}}\]
7. Taylor expanded around -inf 4.0
  \[\leadsto \color{blue}{-1 \cdot \left(x \cdot y\right)}\]
8. Simplified4.0
  \[\leadsto \color{blue}{x \cdot \left(-y\right)}\]
if -6.395336884503867e+42 < z < 7.64327572010788e+117
1. Initial program 11.5
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Simplified11.6
  \[\leadsto \color{blue}{\frac{x \cdot y}{\sqrt{z \cdot z - a \cdot t}} \cdot z}\]
3. Using strategy rm
4. Applied add-sqr-sqrt11.6
  \[\leadsto \frac{x \cdot y}{\sqrt{\color{blue}{\sqrt{z \cdot z - a \cdot t} \cdot \sqrt{z \cdot z - a \cdot t}}}} \cdot z\]
5. Applied sqrt-prod11.8
  \[\leadsto \frac{x \cdot y}{\color{blue}{\sqrt{\sqrt{z \cdot z - a \cdot t}} \cdot \sqrt{\sqrt{z \cdot z - a \cdot t}}}} \cdot z\]
6. Applied times-frac12.4
  \[\leadsto \color{blue}{\left(\frac{x}{\sqrt{\sqrt{z \cdot z - a \cdot t}}} \cdot \frac{y}{\sqrt{\sqrt{z \cdot z - a \cdot t}}}\right)} \cdot z\]
7. Applied associate-*l*11.4
  \[\leadsto \color{blue}{\frac{x}{\sqrt{\sqrt{z \cdot z - a \cdot t}}} \cdot \left(\frac{y}{\sqrt{\sqrt{z \cdot z - a \cdot t}}} \cdot z\right)}\]
8. Simplified11.7
  \[\leadsto \frac{x}{\sqrt{\sqrt{z \cdot z - a \cdot t}}} \cdot \color{blue}{\frac{y \cdot z}{\sqrt{\sqrt{z \cdot z - a \cdot t}}}}\]
if 7.64327572010788e+117 < z
1. Initial program 46.6
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Simplified46.2
  \[\leadsto \color{blue}{\frac{x \cdot y}{\sqrt{z \cdot z - a \cdot t}} \cdot z}\]
3. Using strategy rm
4. Applied div-inv46.2
  \[\leadsto \color{blue}{\left(\left(x \cdot y\right) \cdot \frac{1}{\sqrt{z \cdot z - a \cdot t}}\right)} \cdot z\]
5. Applied associate-*l*44.6
  \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \left(\frac{1}{\sqrt{z \cdot z - a \cdot t}} \cdot z\right)}\]
6. Simplified44.5
  \[\leadsto \left(x \cdot y\right) \cdot \color{blue}{\frac{z}{\sqrt{z \cdot z - a \cdot t}}}\]
7. Taylor expanded around inf 1.7
  \[\leadsto \left(x \cdot y\right) \cdot \color{blue}{1}\]
Recombined 3 regimes into one program.
Final simplification7.8
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -6395336884503866936309996195044608815661000:\\ \;\;\;\;x \cdot \left(-y\right)\\ \mathbf{elif}\;z \le 7.643275720107879512063854532156486714456 \cdot 10^{117}:\\ \;\;\;\;\frac{x}{\sqrt{\sqrt{z \cdot z - a \cdot t}}} \cdot \frac{y \cdot z}{\sqrt{\sqrt{z \cdot z - a \cdot t}}}\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array}\]

Error

Try it out

Target

Derivation

`if z < -6.395336884503867e+42`

`if -6.395336884503867e+42 < z < 7.64327572010788e+117`

`if 7.64327572010788e+117 < z`

Reproduce

In
Out