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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.4467202670789784 \cdot 10^{138}:\\ \;\;\;\;\sqrt{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}}} \cdot \left(-1 \cdot \left(\sqrt{\frac{1}{\sqrt[3]{3}}} \cdot x\right)\right)\\ \mathbf{elif}\;x \le 1.0960437794666031 \cdot 10^{127}:\\ \;\;\;\;\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}}} \cdot \left(\sqrt{\frac{1}{\sqrt[3]{3}}} \cdot x\right)\\ \end{array}\]

\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}

↓

\begin{array}{l}
\mathbf{if}\;x \le -1.4467202670789784 \cdot 10^{138}:\\
\;\;\;\;\sqrt{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}}} \cdot \left(-1 \cdot \left(\sqrt{\frac{1}{\sqrt[3]{3}}} \cdot x\right)\right)\\

\mathbf{elif}\;x \le 1.0960437794666031 \cdot 10^{127}:\\
\;\;\;\;\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\\

\mathbf{else}:\\
\;\;\;\;\sqrt{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}}} \cdot \left(\sqrt{\frac{1}{\sqrt[3]{3}}} \cdot x\right)\\

\end{array}

double f(double x, double y, double z) {
        double r4542 = x;
        double r4543 = r4542 * r4542;
        double r4544 = y;
        double r4545 = r4544 * r4544;
        double r4546 = r4543 + r4545;
        double r4547 = z;
        double r4548 = r4547 * r4547;
        double r4549 = r4546 + r4548;
        double r4550 = 3.0;
        double r4551 = r4549 / r4550;
        double r4552 = sqrt(r4551);
        return r4552;
}

↓

double f(double x, double y, double z) {
        double r4553 = x;
        double r4554 = -1.4467202670789784e+138;
        bool r4555 = r4553 <= r4554;
        double r4556 = 1.0;
        double r4557 = 3.0;
        double r4558 = cbrt(r4557);
        double r4559 = r4558 * r4558;
        double r4560 = r4556 / r4559;
        double r4561 = sqrt(r4560);
        double r4562 = -1.0;
        double r4563 = r4556 / r4558;
        double r4564 = sqrt(r4563);
        double r4565 = r4564 * r4553;
        double r4566 = r4562 * r4565;
        double r4567 = r4561 * r4566;
        double r4568 = 1.096043779466603e+127;
        bool r4569 = r4553 <= r4568;
        double r4570 = r4553 * r4553;
        double r4571 = y;
        double r4572 = r4571 * r4571;
        double r4573 = r4570 + r4572;
        double r4574 = z;
        double r4575 = r4574 * r4574;
        double r4576 = r4573 + r4575;
        double r4577 = r4576 / r4557;
        double r4578 = sqrt(r4577);
        double r4579 = r4561 * r4565;
        double r4580 = r4569 ? r4578 : r4579;
        double r4581 = r4555 ? r4567 : r4580;
        return r4581;
}

Original	38.7
Target	26.3
Herbie	25.7

Derivation

Split input into 3 regimes
if x < -1.4467202670789784e+138
1. Initial program 61.0
  \[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
2. Using strategy rm
3. Applied add-cube-cbrt61.0
  \[\leadsto \sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{\color{blue}{\left(\sqrt[3]{3} \cdot \sqrt[3]{3}\right) \cdot \sqrt[3]{3}}}}\]
4. Applied *-un-lft-identity61.0
  \[\leadsto \sqrt{\frac{\color{blue}{1 \cdot \left(\left(x \cdot x + y \cdot y\right) + z \cdot z\right)}}{\left(\sqrt[3]{3} \cdot \sqrt[3]{3}\right) \cdot \sqrt[3]{3}}}\]
5. Applied times-frac61.0
  \[\leadsto \sqrt{\color{blue}{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}} \cdot \frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{\sqrt[3]{3}}}}\]
6. Applied sqrt-prod61.0
  \[\leadsto \color{blue}{\sqrt{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}}} \cdot \sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{\sqrt[3]{3}}}}\]
7. Taylor expanded around -inf 16.2
  \[\leadsto \sqrt{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}}} \cdot \color{blue}{\left(-1 \cdot \left(\sqrt{\frac{1}{\sqrt[3]{3}}} \cdot x\right)\right)}\]
if -1.4467202670789784e+138 < x < 1.096043779466603e+127
1. Initial program 29.8
  \[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
if 1.096043779466603e+127 < x
1. Initial program 58.4
  \[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
2. Using strategy rm
3. Applied add-cube-cbrt58.4
  \[\leadsto \sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{\color{blue}{\left(\sqrt[3]{3} \cdot \sqrt[3]{3}\right) \cdot \sqrt[3]{3}}}}\]
4. Applied *-un-lft-identity58.4
  \[\leadsto \sqrt{\frac{\color{blue}{1 \cdot \left(\left(x \cdot x + y \cdot y\right) + z \cdot z\right)}}{\left(\sqrt[3]{3} \cdot \sqrt[3]{3}\right) \cdot \sqrt[3]{3}}}\]
5. Applied times-frac58.4
  \[\leadsto \sqrt{\color{blue}{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}} \cdot \frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{\sqrt[3]{3}}}}\]
6. Applied sqrt-prod58.4
  \[\leadsto \color{blue}{\sqrt{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}}} \cdot \sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{\sqrt[3]{3}}}}\]
7. Taylor expanded around inf 16.1
  \[\leadsto \sqrt{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}}} \cdot \color{blue}{\left(\sqrt{\frac{1}{\sqrt[3]{3}}} \cdot x\right)}\]
Recombined 3 regimes into one program.
Final simplification25.7
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.4467202670789784 \cdot 10^{138}:\\ \;\;\;\;\sqrt{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}}} \cdot \left(-1 \cdot \left(\sqrt{\frac{1}{\sqrt[3]{3}}} \cdot x\right)\right)\\ \mathbf{elif}\;x \le 1.0960437794666031 \cdot 10^{127}:\\ \;\;\;\;\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{1}{\sqrt[3]{3} \cdot \sqrt[3]{3}}} \cdot \left(\sqrt{\frac{1}{\sqrt[3]{3}}} \cdot x\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if x < -1.4467202670789784e+138`

`if -1.4467202670789784e+138 < x < 1.096043779466603e+127`

`if 1.096043779466603e+127 < x`

Reproduce

In
Out