\[\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.7988374144992952 \cdot 10^{-152}:\\ \;\;\;\;\left(x - 1 \cdot \frac{\frac{y}{3}}{z}\right) + \frac{t \cdot \frac{1}{z \cdot 3}}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - 1 \cdot \frac{\frac{y}{3}}{z}\right) + 0.333333333333333315 \cdot \frac{t}{z \cdot y}\\ \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.7988374144992952 \cdot 10^{-152}:\\
\;\;\;\;\left(x - 1 \cdot \frac{\frac{y}{3}}{z}\right) + \frac{t \cdot \frac{1}{z \cdot 3}}{y}\\

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

\end{array}

double f(double x, double y, double z, double t) {
        double r759646 = x;
        double r759647 = y;
        double r759648 = z;
        double r759649 = 3.0;
        double r759650 = r759648 * r759649;
        double r759651 = r759647 / r759650;
        double r759652 = r759646 - r759651;
        double r759653 = t;
        double r759654 = r759650 * r759647;
        double r759655 = r759653 / r759654;
        double r759656 = r759652 + r759655;
        return r759656;
}

↓

double f(double x, double y, double z, double t) {
        double r759657 = t;
        double r759658 = 1.7988374144992952e-152;
        bool r759659 = r759657 <= r759658;
        double r759660 = x;
        double r759661 = 1.0;
        double r759662 = y;
        double r759663 = 3.0;
        double r759664 = r759662 / r759663;
        double r759665 = z;
        double r759666 = r759664 / r759665;
        double r759667 = r759661 * r759666;
        double r759668 = r759660 - r759667;
        double r759669 = r759665 * r759663;
        double r759670 = r759661 / r759669;
        double r759671 = r759657 * r759670;
        double r759672 = r759671 / r759662;
        double r759673 = r759668 + r759672;
        double r759674 = 0.3333333333333333;
        double r759675 = r759665 * r759662;
        double r759676 = r759657 / r759675;
        double r759677 = r759674 * r759676;
        double r759678 = r759668 + r759677;
        double r759679 = r759659 ? r759673 : r759678;
        return r759679;
}

Original	3.5
Target	1.7
Herbie	1.6

Derivation

Split input into 2 regimes
if t < 1.7988374144992952e-152
1. Initial program 4.5
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Using strategy rm
3. Applied associate-/r*1.7
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\frac{t}{z \cdot 3}}{y}}\]
4. Using strategy rm
5. Applied *-un-lft-identity1.7
  \[\leadsto \left(x - \frac{\color{blue}{1 \cdot y}}{z \cdot 3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
6. Applied times-frac1.7
  \[\leadsto \left(x - \color{blue}{\frac{1}{z} \cdot \frac{y}{3}}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
7. Using strategy rm
8. Applied *-un-lft-identity1.7
  \[\leadsto \left(x - \frac{1}{\color{blue}{1 \cdot z}} \cdot \frac{y}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
9. Applied *-un-lft-identity1.7
  \[\leadsto \left(x - \frac{\color{blue}{1 \cdot 1}}{1 \cdot z} \cdot \frac{y}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
10. Applied times-frac1.7
  \[\leadsto \left(x - \color{blue}{\left(\frac{1}{1} \cdot \frac{1}{z}\right)} \cdot \frac{y}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
11. Applied associate-*l*1.7
  \[\leadsto \left(x - \color{blue}{\frac{1}{1} \cdot \left(\frac{1}{z} \cdot \frac{y}{3}\right)}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
12. Simplified1.7
  \[\leadsto \left(x - \frac{1}{1} \cdot \color{blue}{\frac{\frac{y}{3}}{z}}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
13. Using strategy rm
14. Applied div-inv1.7
  \[\leadsto \left(x - \frac{1}{1} \cdot \frac{\frac{y}{3}}{z}\right) + \frac{\color{blue}{t \cdot \frac{1}{z \cdot 3}}}{y}\]
if 1.7988374144992952e-152 < t
1. Initial program 1.6
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Using strategy rm
3. Applied associate-/r*1.6
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\frac{t}{z \cdot 3}}{y}}\]
4. Using strategy rm
5. Applied *-un-lft-identity1.6
  \[\leadsto \left(x - \frac{\color{blue}{1 \cdot y}}{z \cdot 3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
6. Applied times-frac1.7
  \[\leadsto \left(x - \color{blue}{\frac{1}{z} \cdot \frac{y}{3}}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
7. Using strategy rm
8. Applied *-un-lft-identity1.7
  \[\leadsto \left(x - \frac{1}{\color{blue}{1 \cdot z}} \cdot \frac{y}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
9. Applied *-un-lft-identity1.7
  \[\leadsto \left(x - \frac{\color{blue}{1 \cdot 1}}{1 \cdot z} \cdot \frac{y}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
10. Applied times-frac1.7
  \[\leadsto \left(x - \color{blue}{\left(\frac{1}{1} \cdot \frac{1}{z}\right)} \cdot \frac{y}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
11. Applied associate-*l*1.7
  \[\leadsto \left(x - \color{blue}{\frac{1}{1} \cdot \left(\frac{1}{z} \cdot \frac{y}{3}\right)}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
12. Simplified1.6
  \[\leadsto \left(x - \frac{1}{1} \cdot \color{blue}{\frac{\frac{y}{3}}{z}}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
13. Taylor expanded around 0 1.6
  \[\leadsto \left(x - \frac{1}{1} \cdot \frac{\frac{y}{3}}{z}\right) + \color{blue}{0.333333333333333315 \cdot \frac{t}{z \cdot y}}\]
Recombined 2 regimes into one program.
Final simplification1.6
\[\leadsto \begin{array}{l} \mathbf{if}\;t \le 1.7988374144992952 \cdot 10^{-152}:\\ \;\;\;\;\left(x - 1 \cdot \frac{\frac{y}{3}}{z}\right) + \frac{t \cdot \frac{1}{z \cdot 3}}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - 1 \cdot \frac{\frac{y}{3}}{z}\right) + 0.333333333333333315 \cdot \frac{t}{z \cdot y}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if t < 1.7988374144992952e-152`

`if 1.7988374144992952e-152 < t`

Reproduce

In
Out