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

↓

\[\begin{array}{l} \mathbf{if}\;e^{z} \le 0.9999999353825346215529634719132445752621:\\ \;\;\;\;x - \frac{\frac{\log \left(\mathsf{fma}\left(y, e^{z}, 1 - y\right)\right)}{\sqrt[3]{t} \cdot \sqrt[3]{t}}}{\sqrt[3]{t}}\\ \mathbf{else}:\\ \;\;\;\;x - \mathsf{fma}\left(1, \frac{z}{t} \cdot y, \frac{\log 1}{t}\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;e^{z} \le 0.9999999353825346215529634719132445752621:\\
\;\;\;\;x - \frac{\frac{\log \left(\mathsf{fma}\left(y, e^{z}, 1 - y\right)\right)}{\sqrt[3]{t} \cdot \sqrt[3]{t}}}{\sqrt[3]{t}}\\

\mathbf{else}:\\
\;\;\;\;x - \mathsf{fma}\left(1, \frac{z}{t} \cdot y, \frac{\log 1}{t}\right)\\

\end{array}

double f(double x, double y, double z, double t) {
        double r23414998 = x;
        double r23414999 = 1.0;
        double r23415000 = y;
        double r23415001 = r23414999 - r23415000;
        double r23415002 = z;
        double r23415003 = exp(r23415002);
        double r23415004 = r23415000 * r23415003;
        double r23415005 = r23415001 + r23415004;
        double r23415006 = log(r23415005);
        double r23415007 = t;
        double r23415008 = r23415006 / r23415007;
        double r23415009 = r23414998 - r23415008;
        return r23415009;
}

↓

double f(double x, double y, double z, double t) {
        double r23415010 = z;
        double r23415011 = exp(r23415010);
        double r23415012 = 0.9999999353825346;
        bool r23415013 = r23415011 <= r23415012;
        double r23415014 = x;
        double r23415015 = y;
        double r23415016 = 1.0;
        double r23415017 = r23415016 - r23415015;
        double r23415018 = fma(r23415015, r23415011, r23415017);
        double r23415019 = log(r23415018);
        double r23415020 = t;
        double r23415021 = cbrt(r23415020);
        double r23415022 = r23415021 * r23415021;
        double r23415023 = r23415019 / r23415022;
        double r23415024 = r23415023 / r23415021;
        double r23415025 = r23415014 - r23415024;
        double r23415026 = r23415010 / r23415020;
        double r23415027 = r23415026 * r23415015;
        double r23415028 = log(r23415016);
        double r23415029 = r23415028 / r23415020;
        double r23415030 = fma(r23415016, r23415027, r23415029);
        double r23415031 = r23415014 - r23415030;
        double r23415032 = r23415013 ? r23415025 : r23415031;
        return r23415032;
}

Original	25.4
Target	16.4
Herbie	8.1

Derivation

Split input into 2 regimes
if (exp z) < 0.9999999353825346
1. Initial program 11.2
  \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
2. Simplified11.2
  \[\leadsto \color{blue}{x - \frac{\log \left(\mathsf{fma}\left(y, e^{z}, 1 - y\right)\right)}{t}}\]
3. Using strategy rm
4. Applied add-cube-cbrt11.4
  \[\leadsto x - \frac{\log \left(\mathsf{fma}\left(y, e^{z}, 1 - y\right)\right)}{\color{blue}{\left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) \cdot \sqrt[3]{t}}}\]
5. Applied associate-/r*11.4
  \[\leadsto x - \color{blue}{\frac{\frac{\log \left(\mathsf{fma}\left(y, e^{z}, 1 - y\right)\right)}{\sqrt[3]{t} \cdot \sqrt[3]{t}}}{\sqrt[3]{t}}}\]
if 0.9999999353825346 < (exp z)
1. Initial program 31.8
  \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
2. Simplified31.8
  \[\leadsto \color{blue}{x - \frac{\log \left(\mathsf{fma}\left(y, e^{z}, 1 - y\right)\right)}{t}}\]
3. Taylor expanded around 0 7.2
  \[\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}\]
4. Simplified7.2
  \[\leadsto x - \frac{\color{blue}{\mathsf{fma}\left(y, \mathsf{fma}\left(z, 1, 0.5 \cdot \left(z \cdot z\right)\right), \log 1\right)}}{t}\]
5. Taylor expanded around 0 7.3
  \[\leadsto \color{blue}{x - \left(1 \cdot \frac{z \cdot y}{t} + \frac{\log 1}{t}\right)}\]
6. Simplified7.3
  \[\leadsto \color{blue}{x - \mathsf{fma}\left(1, \frac{z \cdot y}{t}, \frac{\log 1}{t}\right)}\]
7. Using strategy rm
8. Applied div-inv7.3
  \[\leadsto x - \mathsf{fma}\left(1, \color{blue}{\left(z \cdot y\right) \cdot \frac{1}{t}}, \frac{\log 1}{t}\right)\]
9. Using strategy rm
10. Applied pow17.3
  \[\leadsto x - \mathsf{fma}\left(1, \left(z \cdot y\right) \cdot \color{blue}{{\left(\frac{1}{t}\right)}^{1}}, \frac{\log 1}{t}\right)\]
11. Applied pow17.3
  \[\leadsto x - \mathsf{fma}\left(1, \left(z \cdot \color{blue}{{y}^{1}}\right) \cdot {\left(\frac{1}{t}\right)}^{1}, \frac{\log 1}{t}\right)\]
12. Applied pow17.3
  \[\leadsto x - \mathsf{fma}\left(1, \left(\color{blue}{{z}^{1}} \cdot {y}^{1}\right) \cdot {\left(\frac{1}{t}\right)}^{1}, \frac{\log 1}{t}\right)\]
13. Applied pow-prod-down7.3
  \[\leadsto x - \mathsf{fma}\left(1, \color{blue}{{\left(z \cdot y\right)}^{1}} \cdot {\left(\frac{1}{t}\right)}^{1}, \frac{\log 1}{t}\right)\]
14. Applied pow-prod-down7.3
  \[\leadsto x - \mathsf{fma}\left(1, \color{blue}{{\left(\left(z \cdot y\right) \cdot \frac{1}{t}\right)}^{1}}, \frac{\log 1}{t}\right)\]
15. Simplified6.6
  \[\leadsto x - \mathsf{fma}\left(1, {\color{blue}{\left(\frac{z}{t} \cdot y\right)}}^{1}, \frac{\log 1}{t}\right)\]
Recombined 2 regimes into one program.
Final simplification8.1
\[\leadsto \begin{array}{l} \mathbf{if}\;e^{z} \le 0.9999999353825346215529634719132445752621:\\ \;\;\;\;x - \frac{\frac{\log \left(\mathsf{fma}\left(y, e^{z}, 1 - y\right)\right)}{\sqrt[3]{t} \cdot \sqrt[3]{t}}}{\sqrt[3]{t}}\\ \mathbf{else}:\\ \;\;\;\;x - \mathsf{fma}\left(1, \frac{z}{t} \cdot y, \frac{\log 1}{t}\right)\\ \end{array}\]

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

Error

Target

Derivation

`if (exp z) < 0.9999999353825346`

`if 0.9999999353825346 < (exp z)`

Reproduce