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

↓

\[\begin{array}{l} \mathbf{if}\;t \le -2.577022243406333944957233326176352312102 \cdot 10^{-132}:\\ \;\;\;\;\mathsf{fma}\left(0.3333333333333333148296162562473909929395, \frac{t}{z \cdot y} - \frac{y}{z}, x\right)\\ \mathbf{elif}\;t \le 1.09437522650634257873611445037935749464 \cdot 10^{-25}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{1}{z}}{\frac{y}{\frac{t}{3}}}\\ \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 -2.577022243406333944957233326176352312102 \cdot 10^{-132}:\\
\;\;\;\;\mathsf{fma}\left(0.3333333333333333148296162562473909929395, \frac{t}{z \cdot y} - \frac{y}{z}, x\right)\\

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

\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 r178182077 = x;
        double r178182078 = y;
        double r178182079 = z;
        double r178182080 = 3.0;
        double r178182081 = r178182079 * r178182080;
        double r178182082 = r178182078 / r178182081;
        double r178182083 = r178182077 - r178182082;
        double r178182084 = t;
        double r178182085 = r178182081 * r178182078;
        double r178182086 = r178182084 / r178182085;
        double r178182087 = r178182083 + r178182086;
        return r178182087;
}

↓

double f(double x, double y, double z, double t) {
        double r178182088 = t;
        double r178182089 = -2.577022243406334e-132;
        bool r178182090 = r178182088 <= r178182089;
        double r178182091 = 0.3333333333333333;
        double r178182092 = z;
        double r178182093 = y;
        double r178182094 = r178182092 * r178182093;
        double r178182095 = r178182088 / r178182094;
        double r178182096 = r178182093 / r178182092;
        double r178182097 = r178182095 - r178182096;
        double r178182098 = x;
        double r178182099 = fma(r178182091, r178182097, r178182098);
        double r178182100 = 1.0943752265063426e-25;
        bool r178182101 = r178182088 <= r178182100;
        double r178182102 = 3.0;
        double r178182103 = r178182096 / r178182102;
        double r178182104 = r178182098 - r178182103;
        double r178182105 = 1.0;
        double r178182106 = r178182105 / r178182092;
        double r178182107 = r178182088 / r178182102;
        double r178182108 = r178182093 / r178182107;
        double r178182109 = r178182106 / r178182108;
        double r178182110 = r178182104 + r178182109;
        double r178182111 = r178182092 * r178182102;
        double r178182112 = r178182093 / r178182111;
        double r178182113 = r178182098 - r178182112;
        double r178182114 = r178182102 * r178182093;
        double r178182115 = r178182092 * r178182114;
        double r178182116 = r178182088 / r178182115;
        double r178182117 = r178182113 + r178182116;
        double r178182118 = r178182101 ? r178182110 : r178182117;
        double r178182119 = r178182090 ? r178182099 : r178182118;
        return r178182119;
}

Original	3.5
Target	1.7
Herbie	0.8

Derivation

Split input into 3 regimes
if t < -2.577022243406334e-132
1. Initial program 1.7
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Taylor expanded around 0 1.8
  \[\leadsto \color{blue}{\left(x + 0.3333333333333333148296162562473909929395 \cdot \frac{t}{z \cdot y}\right) - 0.3333333333333333148296162562473909929395 \cdot \frac{y}{z}}\]
3. Simplified1.8
  \[\leadsto \color{blue}{\mathsf{fma}\left(0.3333333333333333148296162562473909929395, \frac{t}{z \cdot y} - \frac{y}{z}, x\right)}\]
if -2.577022243406334e-132 < t < 1.0943752265063426e-25
1. Initial program 6.4
  \[\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.4
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\frac{t}{z \cdot 3}}{y}}\]
4. Using strategy rm
5. Applied associate-/r*1.4
  \[\leadsto \left(x - \color{blue}{\frac{\frac{y}{z}}{3}}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
6. Using strategy rm
7. Applied *-un-lft-identity1.4
  \[\leadsto \left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{\color{blue}{1 \cdot t}}{z \cdot 3}}{y}\]
8. Applied times-frac1.4
  \[\leadsto \left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\color{blue}{\frac{1}{z} \cdot \frac{t}{3}}}{y}\]
9. Applied associate-/l*0.2
  \[\leadsto \left(x - \frac{\frac{y}{z}}{3}\right) + \color{blue}{\frac{\frac{1}{z}}{\frac{y}{\frac{t}{3}}}}\]
if 1.0943752265063426e-25 < t
1. Initial program 0.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-*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.8
\[\leadsto \begin{array}{l} \mathbf{if}\;t \le -2.577022243406333944957233326176352312102 \cdot 10^{-132}:\\ \;\;\;\;\mathsf{fma}\left(0.3333333333333333148296162562473909929395, \frac{t}{z \cdot y} - \frac{y}{z}, x\right)\\ \mathbf{elif}\;t \le 1.09437522650634257873611445037935749464 \cdot 10^{-25}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{1}{z}}{\frac{y}{\frac{t}{3}}}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot \left(3 \cdot y\right)}\\ \end{array}\]

Error

Target

Derivation

`if t < -2.577022243406334e-132`

`if -2.577022243406334e-132 < t < 1.0943752265063426e-25`

`if 1.0943752265063426e-25 < t`

Reproduce