\[\frac{x \cdot y - z \cdot t}{a}\]

↓

\[\begin{array}{l} \mathbf{if}\;a \le -9.637778577628268 \cdot 10^{+191}:\\ \;\;\;\;x \cdot \frac{y}{a} - \frac{t \cdot z}{a}\\ \mathbf{elif}\;a \le 1.8721002625462693 \cdot 10^{-84}:\\ \;\;\;\;\frac{1}{a} \cdot \left(x \cdot y - t \cdot z\right)\\ \mathbf{elif}\;a \le 7.642381353223433 \cdot 10^{+278}:\\ \;\;\;\;\frac{x \cdot y}{a} - \frac{z}{a} \cdot t\\ \mathbf{else}:\\ \;\;\;\;x \cdot \frac{y}{a} - \frac{t \cdot z}{a}\\ \end{array}\]

\frac{x \cdot y - z \cdot t}{a}

↓

\begin{array}{l}
\mathbf{if}\;a \le -9.637778577628268 \cdot 10^{+191}:\\
\;\;\;\;x \cdot \frac{y}{a} - \frac{t \cdot z}{a}\\

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

\mathbf{elif}\;a \le 7.642381353223433 \cdot 10^{+278}:\\
\;\;\;\;\frac{x \cdot y}{a} - \frac{z}{a} \cdot t\\

\mathbf{else}:\\
\;\;\;\;x \cdot \frac{y}{a} - \frac{t \cdot z}{a}\\

\end{array}

double f(double x, double y, double z, double t, double a) {
        double r39522803 = x;
        double r39522804 = y;
        double r39522805 = r39522803 * r39522804;
        double r39522806 = z;
        double r39522807 = t;
        double r39522808 = r39522806 * r39522807;
        double r39522809 = r39522805 - r39522808;
        double r39522810 = a;
        double r39522811 = r39522809 / r39522810;
        return r39522811;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r39522812 = a;
        double r39522813 = -9.637778577628268e+191;
        bool r39522814 = r39522812 <= r39522813;
        double r39522815 = x;
        double r39522816 = y;
        double r39522817 = r39522816 / r39522812;
        double r39522818 = r39522815 * r39522817;
        double r39522819 = t;
        double r39522820 = z;
        double r39522821 = r39522819 * r39522820;
        double r39522822 = r39522821 / r39522812;
        double r39522823 = r39522818 - r39522822;
        double r39522824 = 1.8721002625462693e-84;
        bool r39522825 = r39522812 <= r39522824;
        double r39522826 = 1.0;
        double r39522827 = r39522826 / r39522812;
        double r39522828 = r39522815 * r39522816;
        double r39522829 = r39522828 - r39522821;
        double r39522830 = r39522827 * r39522829;
        double r39522831 = 7.642381353223433e+278;
        bool r39522832 = r39522812 <= r39522831;
        double r39522833 = r39522828 / r39522812;
        double r39522834 = r39522820 / r39522812;
        double r39522835 = r39522834 * r39522819;
        double r39522836 = r39522833 - r39522835;
        double r39522837 = r39522832 ? r39522836 : r39522823;
        double r39522838 = r39522825 ? r39522830 : r39522837;
        double r39522839 = r39522814 ? r39522823 : r39522838;
        return r39522839;
}

Original	7.2
Target	5.6
Herbie	6.2

Derivation

Split input into 3 regimes
if a < -9.637778577628268e+191 or 7.642381353223433e+278 < a
1. Initial program 13.6
  \[\frac{x \cdot y - z \cdot t}{a}\]
2. Using strategy rm
3. Applied div-sub13.6
  \[\leadsto \color{blue}{\frac{x \cdot y}{a} - \frac{z \cdot t}{a}}\]
4. Taylor expanded around 0 13.6
  \[\leadsto \frac{x \cdot y}{a} - \color{blue}{\frac{t \cdot z}{a}}\]
5. Using strategy rm
6. Applied *-un-lft-identity13.6
  \[\leadsto \frac{x \cdot y}{\color{blue}{1 \cdot a}} - \frac{t \cdot z}{a}\]
7. Applied times-frac10.8
  \[\leadsto \color{blue}{\frac{x}{1} \cdot \frac{y}{a}} - \frac{t \cdot z}{a}\]
8. Simplified10.8
  \[\leadsto \color{blue}{x} \cdot \frac{y}{a} - \frac{t \cdot z}{a}\]
if -9.637778577628268e+191 < a < 1.8721002625462693e-84
1. Initial program 4.1
  \[\frac{x \cdot y - z \cdot t}{a}\]
2. Using strategy rm
3. Applied div-sub4.1
  \[\leadsto \color{blue}{\frac{x \cdot y}{a} - \frac{z \cdot t}{a}}\]
4. Taylor expanded around 0 4.1
  \[\leadsto \frac{x \cdot y}{a} - \color{blue}{\frac{t \cdot z}{a}}\]
5. Using strategy rm
6. Applied div-inv4.2
  \[\leadsto \frac{x \cdot y}{a} - \color{blue}{\left(t \cdot z\right) \cdot \frac{1}{a}}\]
7. Applied div-inv4.2
  \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{1}{a}} - \left(t \cdot z\right) \cdot \frac{1}{a}\]
8. Applied distribute-rgt-out--4.2
  \[\leadsto \color{blue}{\frac{1}{a} \cdot \left(x \cdot y - t \cdot z\right)}\]
if 1.8721002625462693e-84 < a < 7.642381353223433e+278
1. Initial program 8.5
  \[\frac{x \cdot y - z \cdot t}{a}\]
2. Using strategy rm
3. Applied div-sub8.5
  \[\leadsto \color{blue}{\frac{x \cdot y}{a} - \frac{z \cdot t}{a}}\]
4. Taylor expanded around 0 8.5
  \[\leadsto \frac{x \cdot y}{a} - \color{blue}{\frac{t \cdot z}{a}}\]
5. Using strategy rm
6. Applied *-un-lft-identity8.5
  \[\leadsto \frac{x \cdot y}{a} - \frac{t \cdot z}{\color{blue}{1 \cdot a}}\]
7. Applied times-frac6.7
  \[\leadsto \frac{x \cdot y}{a} - \color{blue}{\frac{t}{1} \cdot \frac{z}{a}}\]
8. Simplified6.7
  \[\leadsto \frac{x \cdot y}{a} - \color{blue}{t} \cdot \frac{z}{a}\]
Recombined 3 regimes into one program.
Final simplification6.2
\[\leadsto \begin{array}{l} \mathbf{if}\;a \le -9.637778577628268 \cdot 10^{+191}:\\ \;\;\;\;x \cdot \frac{y}{a} - \frac{t \cdot z}{a}\\ \mathbf{elif}\;a \le 1.8721002625462693 \cdot 10^{-84}:\\ \;\;\;\;\frac{1}{a} \cdot \left(x \cdot y - t \cdot z\right)\\ \mathbf{elif}\;a \le 7.642381353223433 \cdot 10^{+278}:\\ \;\;\;\;\frac{x \cdot y}{a} - \frac{z}{a} \cdot t\\ \mathbf{else}:\\ \;\;\;\;x \cdot \frac{y}{a} - \frac{t \cdot z}{a}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if a < -9.637778577628268e+191 or 7.642381353223433e+278 < a`

`if -9.637778577628268e+191 < a < 1.8721002625462693e-84`

`if 1.8721002625462693e-84 < a < 7.642381353223433e+278`

Reproduce

In
Out