\[\frac{1 - \cos x}{\sin x}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \le -0.01927343743819966842556468122893420513719:\\ \;\;\;\;\log \left(e^{\frac{\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{1 \cdot 1 + \left(1 + \cos x\right) \cdot \cos x}}{\sin x}}\right)\\ \mathbf{elif}\;x \le 0.02235098969897789805694188203233352396637:\\ \;\;\;\;x \cdot \left(\frac{1}{2} + x \cdot \left(x \cdot \frac{1}{24}\right)\right) + {x}^{5} \cdot \frac{1}{240}\\ \mathbf{else}:\\ \;\;\;\;\log \left(\sqrt{e^{\frac{1 - \cos x}{\sin x}}}\right) + \log \left(\sqrt{e^{\frac{1 - \cos x}{\sin x}}}\right)\\ \end{array}\]

\frac{1 - \cos x}{\sin x}

↓

\begin{array}{l}
\mathbf{if}\;x \le -0.01927343743819966842556468122893420513719:\\
\;\;\;\;\log \left(e^{\frac{\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{1 \cdot 1 + \left(1 + \cos x\right) \cdot \cos x}}{\sin x}}\right)\\

\mathbf{elif}\;x \le 0.02235098969897789805694188203233352396637:\\
\;\;\;\;x \cdot \left(\frac{1}{2} + x \cdot \left(x \cdot \frac{1}{24}\right)\right) + {x}^{5} \cdot \frac{1}{240}\\

\mathbf{else}:\\
\;\;\;\;\log \left(\sqrt{e^{\frac{1 - \cos x}{\sin x}}}\right) + \log \left(\sqrt{e^{\frac{1 - \cos x}{\sin x}}}\right)\\

\end{array}

double f(double x) {
        double r31163 = 1.0;
        double r31164 = x;
        double r31165 = cos(r31164);
        double r31166 = r31163 - r31165;
        double r31167 = sin(r31164);
        double r31168 = r31166 / r31167;
        return r31168;
}

↓

double f(double x) {
        double r31169 = x;
        double r31170 = -0.01927343743819967;
        bool r31171 = r31169 <= r31170;
        double r31172 = 1.0;
        double r31173 = 3.0;
        double r31174 = pow(r31172, r31173);
        double r31175 = cos(r31169);
        double r31176 = pow(r31175, r31173);
        double r31177 = r31174 - r31176;
        double r31178 = r31172 * r31172;
        double r31179 = r31172 + r31175;
        double r31180 = r31179 * r31175;
        double r31181 = r31178 + r31180;
        double r31182 = r31177 / r31181;
        double r31183 = sin(r31169);
        double r31184 = r31182 / r31183;
        double r31185 = exp(r31184);
        double r31186 = log(r31185);
        double r31187 = 0.022350989698977898;
        bool r31188 = r31169 <= r31187;
        double r31189 = 0.5;
        double r31190 = 0.041666666666666664;
        double r31191 = r31169 * r31190;
        double r31192 = r31169 * r31191;
        double r31193 = r31189 + r31192;
        double r31194 = r31169 * r31193;
        double r31195 = 5.0;
        double r31196 = pow(r31169, r31195);
        double r31197 = 0.004166666666666667;
        double r31198 = r31196 * r31197;
        double r31199 = r31194 + r31198;
        double r31200 = r31172 - r31175;
        double r31201 = r31200 / r31183;
        double r31202 = exp(r31201);
        double r31203 = sqrt(r31202);
        double r31204 = log(r31203);
        double r31205 = r31204 + r31204;
        double r31206 = r31188 ? r31199 : r31205;
        double r31207 = r31171 ? r31186 : r31206;
        return r31207;
}

Original	30.0
Target	0.0
Herbie	0.6

Derivation

Split input into 3 regimes
if x < -0.01927343743819967
1. Initial program 0.9
  \[\frac{1 - \cos x}{\sin x}\]
2. Using strategy rm
3. Applied add-log-exp1.1
  \[\leadsto \color{blue}{\log \left(e^{\frac{1 - \cos x}{\sin x}}\right)}\]
4. Using strategy rm
5. Applied flip3--1.2
  \[\leadsto \log \left(e^{\frac{\color{blue}{\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)}}}{\sin x}}\right)\]
6. Simplified1.2
  \[\leadsto \log \left(e^{\frac{\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\cos x \cdot \left(1 + \cos x\right) + 1 \cdot 1}}}{\sin x}}\right)\]
if -0.01927343743819967 < x < 0.022350989698977898
1. Initial program 59.9
  \[\frac{1 - \cos x}{\sin x}\]
2. Taylor expanded around 0 0.0
  \[\leadsto \color{blue}{\frac{1}{2} \cdot x + \left(\frac{1}{24} \cdot {x}^{3} + \frac{1}{240} \cdot {x}^{5}\right)}\]
3. Simplified0.0
  \[\leadsto \color{blue}{\frac{1}{240} \cdot {x}^{5} + x \cdot \left(x \cdot \left(x \cdot \frac{1}{24}\right) + \frac{1}{2}\right)}\]
if 0.022350989698977898 < x
1. Initial program 0.9
  \[\frac{1 - \cos x}{\sin x}\]
2. Using strategy rm
3. Applied add-log-exp1.1
  \[\leadsto \color{blue}{\log \left(e^{\frac{1 - \cos x}{\sin x}}\right)}\]
4. Using strategy rm
5. Applied add-sqr-sqrt1.3
  \[\leadsto \log \color{blue}{\left(\sqrt{e^{\frac{1 - \cos x}{\sin x}}} \cdot \sqrt{e^{\frac{1 - \cos x}{\sin x}}}\right)}\]
6. Applied log-prod1.2
  \[\leadsto \color{blue}{\log \left(\sqrt{e^{\frac{1 - \cos x}{\sin x}}}\right) + \log \left(\sqrt{e^{\frac{1 - \cos x}{\sin x}}}\right)}\]
Recombined 3 regimes into one program.
Final simplification0.6
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -0.01927343743819966842556468122893420513719:\\ \;\;\;\;\log \left(e^{\frac{\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{1 \cdot 1 + \left(1 + \cos x\right) \cdot \cos x}}{\sin x}}\right)\\ \mathbf{elif}\;x \le 0.02235098969897789805694188203233352396637:\\ \;\;\;\;x \cdot \left(\frac{1}{2} + x \cdot \left(x \cdot \frac{1}{24}\right)\right) + {x}^{5} \cdot \frac{1}{240}\\ \mathbf{else}:\\ \;\;\;\;\log \left(\sqrt{e^{\frac{1 - \cos x}{\sin x}}}\right) + \log \left(\sqrt{e^{\frac{1 - \cos x}{\sin x}}}\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if x < -0.01927343743819967`

`if -0.01927343743819967 < x < 0.022350989698977898`

`if 0.022350989698977898 < x`

Reproduce

In
Out