\[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]

↓

\[\begin{array}{l} \mathbf{if}\;z \le -1.788149422936711126217649570543650854038 \cdot 10^{-10}:\\ \;\;\;\;x - \log \left(e^{z} \cdot y + \left(1 - y\right)\right) \cdot \frac{1}{t}\\ \mathbf{elif}\;z \le 1.548199489295338911120653686915655113605 \cdot 10^{-142} \lor \neg \left(z \le 4.70552617509855223204263570258364278042 \cdot 10^{-18}\right):\\ \;\;\;\;x - \frac{\log 1 + \left(1 \cdot z + {z}^{2} \cdot 0.5\right) \cdot y}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{\log \left(\left(\frac{1}{2} \cdot y\right) \cdot {z}^{2} + \left(y \cdot z + 1\right)\right)}{t}\\ \end{array}\]

x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}

↓

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

\mathbf{elif}\;z \le 1.548199489295338911120653686915655113605 \cdot 10^{-142} \lor \neg \left(z \le 4.70552617509855223204263570258364278042 \cdot 10^{-18}\right):\\
\;\;\;\;x - \frac{\log 1 + \left(1 \cdot z + {z}^{2} \cdot 0.5\right) \cdot y}{t}\\

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

\end{array}

double f(double x, double y, double z, double t) {
        double r233215 = x;
        double r233216 = 1.0;
        double r233217 = y;
        double r233218 = r233216 - r233217;
        double r233219 = z;
        double r233220 = exp(r233219);
        double r233221 = r233217 * r233220;
        double r233222 = r233218 + r233221;
        double r233223 = log(r233222);
        double r233224 = t;
        double r233225 = r233223 / r233224;
        double r233226 = r233215 - r233225;
        return r233226;
}

↓

double f(double x, double y, double z, double t) {
        double r233227 = z;
        double r233228 = -1.788149422936711e-10;
        bool r233229 = r233227 <= r233228;
        double r233230 = x;
        double r233231 = exp(r233227);
        double r233232 = y;
        double r233233 = r233231 * r233232;
        double r233234 = 1.0;
        double r233235 = r233234 - r233232;
        double r233236 = r233233 + r233235;
        double r233237 = log(r233236);
        double r233238 = 1.0;
        double r233239 = t;
        double r233240 = r233238 / r233239;
        double r233241 = r233237 * r233240;
        double r233242 = r233230 - r233241;
        double r233243 = 1.548199489295339e-142;
        bool r233244 = r233227 <= r233243;
        double r233245 = 4.705526175098552e-18;
        bool r233246 = r233227 <= r233245;
        double r233247 = !r233246;
        bool r233248 = r233244 || r233247;
        double r233249 = log(r233234);
        double r233250 = r233234 * r233227;
        double r233251 = 2.0;
        double r233252 = pow(r233227, r233251);
        double r233253 = 0.5;
        double r233254 = r233252 * r233253;
        double r233255 = r233250 + r233254;
        double r233256 = r233255 * r233232;
        double r233257 = r233249 + r233256;
        double r233258 = r233257 / r233239;
        double r233259 = r233230 - r233258;
        double r233260 = 0.5;
        double r233261 = r233260 * r233232;
        double r233262 = r233261 * r233252;
        double r233263 = r233232 * r233227;
        double r233264 = r233263 + r233234;
        double r233265 = r233262 + r233264;
        double r233266 = log(r233265);
        double r233267 = r233266 / r233239;
        double r233268 = r233230 - r233267;
        double r233269 = r233248 ? r233259 : r233268;
        double r233270 = r233229 ? r233242 : r233269;
        return r233270;
}

Original	25.3
Target	16.1
Herbie	8.5

Derivation

Split input into 3 regimes
if z < -1.788149422936711e-10
1. Initial program 11.1
  \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
2. Using strategy rm
3. Applied div-inv11.1
  \[\leadsto x - \color{blue}{\log \left(\left(1 - y\right) + y \cdot e^{z}\right) \cdot \frac{1}{t}}\]
if -1.788149422936711e-10 < z < 1.548199489295339e-142 or 4.705526175098552e-18 < z
1. Initial program 31.6
  \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
2. Taylor expanded around 0 6.5
  \[\leadsto x - \frac{\color{blue}{\log 1 + \left(1 \cdot \left(z \cdot y\right) + 0.5 \cdot \left({z}^{2} \cdot y\right)\right)}}{t}\]
3. Simplified6.4
  \[\leadsto x - \frac{\color{blue}{\log 1 + y \cdot \left(0.5 \cdot {z}^{2} + z \cdot 1\right)}}{t}\]
if 1.548199489295339e-142 < z < 4.705526175098552e-18
1. Initial program 31.5
  \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
2. Taylor expanded around 0 11.5
  \[\leadsto x - \frac{\log \color{blue}{\left(z \cdot y + \left(\frac{1}{2} \cdot \left({z}^{2} \cdot y\right) + 1\right)\right)}}{t}\]
3. Simplified11.5
  \[\leadsto x - \frac{\log \color{blue}{\left(\left(y \cdot z + 1\right) + \left(\frac{1}{2} \cdot y\right) \cdot {z}^{2}\right)}}{t}\]
Recombined 3 regimes into one program.
Final simplification8.5
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.788149422936711126217649570543650854038 \cdot 10^{-10}:\\ \;\;\;\;x - \log \left(e^{z} \cdot y + \left(1 - y\right)\right) \cdot \frac{1}{t}\\ \mathbf{elif}\;z \le 1.548199489295338911120653686915655113605 \cdot 10^{-142} \lor \neg \left(z \le 4.70552617509855223204263570258364278042 \cdot 10^{-18}\right):\\ \;\;\;\;x - \frac{\log 1 + \left(1 \cdot z + {z}^{2} \cdot 0.5\right) \cdot y}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{\log \left(\left(\frac{1}{2} \cdot y\right) \cdot {z}^{2} + \left(y \cdot z + 1\right)\right)}{t}\\ \end{array}\]

could not determine a ground truth for program body (more)

Error

Try it out

Target

Derivation

`if z < -1.788149422936711e-10`

`if -1.788149422936711e-10 < z < 1.548199489295339e-142 or 4.705526175098552e-18 < z`

`if 1.548199489295339e-142 < z < 4.705526175098552e-18`

Reproduce

In
Out