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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -1.387037513954152204793629697523518119099 \cdot 10^{152}:\\ \;\;\;\;x \cdot \left(-y\right)\\ \mathbf{elif}\;z \le 2.81109844001032311849514459419925746028 \cdot 10^{123}:\\ \;\;\;\;x \cdot \left(y \cdot \frac{z}{\sqrt{{z}^{2} - a \cdot t}}\right)\\ \mathbf{else}:\\ \;\;\;\;y \cdot x\\ \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.387037513954152204793629697523518119099 \cdot 10^{152}:\\
\;\;\;\;x \cdot \left(-y\right)\\

\mathbf{elif}\;z \le 2.81109844001032311849514459419925746028 \cdot 10^{123}:\\
\;\;\;\;x \cdot \left(y \cdot \frac{z}{\sqrt{{z}^{2} - a \cdot t}}\right)\\

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

\end{array}

double f(double x, double y, double z, double t, double a) {
        double r243729 = x;
        double r243730 = y;
        double r243731 = r243729 * r243730;
        double r243732 = z;
        double r243733 = r243731 * r243732;
        double r243734 = r243732 * r243732;
        double r243735 = t;
        double r243736 = a;
        double r243737 = r243735 * r243736;
        double r243738 = r243734 - r243737;
        double r243739 = sqrt(r243738);
        double r243740 = r243733 / r243739;
        return r243740;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r243741 = z;
        double r243742 = -1.3870375139541522e+152;
        bool r243743 = r243741 <= r243742;
        double r243744 = x;
        double r243745 = y;
        double r243746 = -r243745;
        double r243747 = r243744 * r243746;
        double r243748 = 2.811098440010323e+123;
        bool r243749 = r243741 <= r243748;
        double r243750 = 2.0;
        double r243751 = pow(r243741, r243750);
        double r243752 = a;
        double r243753 = t;
        double r243754 = r243752 * r243753;
        double r243755 = r243751 - r243754;
        double r243756 = sqrt(r243755);
        double r243757 = r243741 / r243756;
        double r243758 = r243745 * r243757;
        double r243759 = r243744 * r243758;
        double r243760 = r243745 * r243744;
        double r243761 = r243749 ? r243759 : r243760;
        double r243762 = r243743 ? r243747 : r243761;
        return r243762;
}

Original	24.4
Target	7.5
Herbie	6.0

Derivation

Split input into 3 regimes
if z < -1.3870375139541522e+152
1. Initial program 52.5
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Using strategy rm
3. Applied associate-/l*52.1
  \[\leadsto \color{blue}{\frac{x \cdot y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
4. Using strategy rm
5. Applied div-inv52.1
  \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{1}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
6. Simplified52.1
  \[\leadsto \left(x \cdot y\right) \cdot \color{blue}{\frac{z}{\sqrt{{z}^{2} - a \cdot t}}}\]
7. Using strategy rm
8. Applied associate-*l*52.1
  \[\leadsto \color{blue}{x \cdot \left(y \cdot \frac{z}{\sqrt{{z}^{2} - a \cdot t}}\right)}\]
9. Taylor expanded around -inf 1.5
  \[\leadsto x \cdot \color{blue}{\left(-1 \cdot y\right)}\]
10. Simplified1.5
  \[\leadsto x \cdot \color{blue}{\left(-y\right)}\]
if -1.3870375139541522e+152 < z < 2.811098440010323e+123
1. Initial program 10.7
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Using strategy rm
3. Applied associate-/l*8.7
  \[\leadsto \color{blue}{\frac{x \cdot y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
4. Using strategy rm
5. Applied div-inv8.7
  \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{1}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
6. Simplified8.5
  \[\leadsto \left(x \cdot y\right) \cdot \color{blue}{\frac{z}{\sqrt{{z}^{2} - a \cdot t}}}\]
7. Using strategy rm
8. Applied associate-*l*8.4
  \[\leadsto \color{blue}{x \cdot \left(y \cdot \frac{z}{\sqrt{{z}^{2} - a \cdot t}}\right)}\]
if 2.811098440010323e+123 < z
1. Initial program 47.9
  \[\frac{\left(x \cdot y\right) \cdot z}{\sqrt{z \cdot z - t \cdot a}}\]
2. Using strategy rm
3. Applied associate-/l*45.9
  \[\leadsto \color{blue}{\frac{x \cdot y}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
4. Using strategy rm
5. Applied div-inv45.9
  \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{1}{\frac{\sqrt{z \cdot z - t \cdot a}}{z}}}\]
6. Simplified45.9
  \[\leadsto \left(x \cdot y\right) \cdot \color{blue}{\frac{z}{\sqrt{{z}^{2} - a \cdot t}}}\]
7. Taylor expanded around inf 1.7
  \[\leadsto \color{blue}{x \cdot y}\]
8. Simplified1.7
  \[\leadsto \color{blue}{y \cdot x}\]
Recombined 3 regimes into one program.
Final simplification6.0
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.387037513954152204793629697523518119099 \cdot 10^{152}:\\ \;\;\;\;x \cdot \left(-y\right)\\ \mathbf{elif}\;z \le 2.81109844001032311849514459419925746028 \cdot 10^{123}:\\ \;\;\;\;x \cdot \left(y \cdot \frac{z}{\sqrt{{z}^{2} - a \cdot t}}\right)\\ \mathbf{else}:\\ \;\;\;\;y \cdot x\\ \end{array}\]

Error

Try it out

Target

Derivation

`if z < -1.3870375139541522e+152`

`if -1.3870375139541522e+152 < z < 2.811098440010323e+123`

`if 2.811098440010323e+123 < z`

Reproduce

In
Out