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

↓

\[\begin{array}{l} \mathbf{if}\;t \le -1.130766526991550831995155013766432401164 \cdot 10^{108}:\\ \;\;\;\;\left(x - \frac{y}{z} \cdot \frac{1}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \mathbf{elif}\;t \le 1.049791316749221378801639893604499862068 \cdot 10^{-26}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z} \cdot \frac{t}{3 \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot \left(3 \cdot y\right)}\\ \end{array}\]

\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}

↓

\begin{array}{l}
\mathbf{if}\;t \le -1.130766526991550831995155013766432401164 \cdot 10^{108}:\\
\;\;\;\;\left(x - \frac{y}{z} \cdot \frac{1}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\

\mathbf{elif}\;t \le 1.049791316749221378801639893604499862068 \cdot 10^{-26}:\\
\;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z} \cdot \frac{t}{3 \cdot y}\\

\mathbf{else}:\\
\;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot \left(3 \cdot y\right)}\\

\end{array}

double f(double x, double y, double z, double t) {
        double r556758 = x;
        double r556759 = y;
        double r556760 = z;
        double r556761 = 3.0;
        double r556762 = r556760 * r556761;
        double r556763 = r556759 / r556762;
        double r556764 = r556758 - r556763;
        double r556765 = t;
        double r556766 = r556762 * r556759;
        double r556767 = r556765 / r556766;
        double r556768 = r556764 + r556767;
        return r556768;
}

↓

double f(double x, double y, double z, double t) {
        double r556769 = t;
        double r556770 = -1.1307665269915508e+108;
        bool r556771 = r556769 <= r556770;
        double r556772 = x;
        double r556773 = y;
        double r556774 = z;
        double r556775 = r556773 / r556774;
        double r556776 = 1.0;
        double r556777 = 3.0;
        double r556778 = r556776 / r556777;
        double r556779 = r556775 * r556778;
        double r556780 = r556772 - r556779;
        double r556781 = r556774 * r556777;
        double r556782 = r556781 * r556773;
        double r556783 = r556769 / r556782;
        double r556784 = r556780 + r556783;
        double r556785 = 1.0497913167492214e-26;
        bool r556786 = r556769 <= r556785;
        double r556787 = r556773 / r556781;
        double r556788 = r556772 - r556787;
        double r556789 = r556776 / r556774;
        double r556790 = r556777 * r556773;
        double r556791 = r556769 / r556790;
        double r556792 = r556789 * r556791;
        double r556793 = r556788 + r556792;
        double r556794 = r556774 * r556790;
        double r556795 = r556769 / r556794;
        double r556796 = r556788 + r556795;
        double r556797 = r556786 ? r556793 : r556796;
        double r556798 = r556771 ? r556784 : r556797;
        return r556798;
}

Original	3.4
Target	2.0
Herbie	0.7

Derivation

Split input into 3 regimes
if t < -1.1307665269915508e+108
1. Initial program 1.3
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Using strategy rm
3. Applied *-un-lft-identity1.3
  \[\leadsto \left(x - \frac{\color{blue}{1 \cdot y}}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
4. Applied times-frac1.2
  \[\leadsto \left(x - \color{blue}{\frac{1}{z} \cdot \frac{y}{3}}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
5. Using strategy rm
6. Applied div-inv1.3
  \[\leadsto \left(x - \frac{1}{z} \cdot \color{blue}{\left(y \cdot \frac{1}{3}\right)}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
7. Applied associate-*r*1.3
  \[\leadsto \left(x - \color{blue}{\left(\frac{1}{z} \cdot y\right) \cdot \frac{1}{3}}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
8. Simplified1.3
  \[\leadsto \left(x - \color{blue}{\frac{y}{z}} \cdot \frac{1}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
if -1.1307665269915508e+108 < t < 1.0497913167492214e-26
1. Initial program 4.8
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Using strategy rm
3. Applied associate-*l*4.8
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\color{blue}{z \cdot \left(3 \cdot y\right)}}\]
4. Using strategy rm
5. Applied *-un-lft-identity4.8
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\color{blue}{1 \cdot t}}{z \cdot \left(3 \cdot y\right)}\]
6. Applied times-frac0.6
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{1}{z} \cdot \frac{t}{3 \cdot y}}\]
if 1.0497913167492214e-26 < t
1. Initial program 0.7
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Using strategy rm
3. Applied associate-*l*0.6
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\color{blue}{z \cdot \left(3 \cdot y\right)}}\]
Recombined 3 regimes into one program.
Final simplification0.7
\[\leadsto \begin{array}{l} \mathbf{if}\;t \le -1.130766526991550831995155013766432401164 \cdot 10^{108}:\\ \;\;\;\;\left(x - \frac{y}{z} \cdot \frac{1}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \mathbf{elif}\;t \le 1.049791316749221378801639893604499862068 \cdot 10^{-26}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z} \cdot \frac{t}{3 \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot \left(3 \cdot y\right)}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if t < -1.1307665269915508e+108`

`if -1.1307665269915508e+108 < t < 1.0497913167492214e-26`

`if 1.0497913167492214e-26 < t`

Reproduce

In
Out