Average Error: 38.1 → 25.9
Time: 4.4s
Precision: 64
\[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
↓
\[\begin{array}{l} \mathbf{if}\;z \le -1.68678757300183878 \cdot 10^{145}:\\ \;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\ \mathbf{elif}\;z \le -4.4499930864302828 \cdot 10^{-268}:\\ \;\;\;\;\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|\\ \mathbf{elif}\;z \le 7.0122946607364459 \cdot 10^{-227}:\\ \;\;\;\;\left|-1 \cdot \frac{x}{\sqrt{3}}\right|\\ \mathbf{elif}\;z \le 4.98293636143277424 \cdot 10^{94}:\\ \;\;\;\;\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|\\ \mathbf{else}:\\ \;\;\;\;z \cdot \sqrt{0.333333333333333315}\\ \end{array}\]
\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}
↓
\begin{array}{l}
\mathbf{if}\;z \le -1.68678757300183878 \cdot 10^{145}:\\
\;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\

\mathbf{elif}\;z \le -4.4499930864302828 \cdot 10^{-268}:\\
\;\;\;\;\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|\\

\mathbf{elif}\;z \le 7.0122946607364459 \cdot 10^{-227}:\\
\;\;\;\;\left|-1 \cdot \frac{x}{\sqrt{3}}\right|\\

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

\mathbf{else}:\\
\;\;\;\;z \cdot \sqrt{0.333333333333333315}\\

\end{array}
double f(double x, double y, double z) {
        double r799294 = x;
        double r799295 = r799294 * r799294;
        double r799296 = y;
        double r799297 = r799296 * r799296;
        double r799298 = r799295 + r799297;
        double r799299 = z;
        double r799300 = r799299 * r799299;
        double r799301 = r799298 + r799300;
        double r799302 = 3.0;
        double r799303 = r799301 / r799302;
        double r799304 = sqrt(r799303);
        return r799304;
}
↓
double f(double x, double y, double z) {
        double r799305 = z;
        double r799306 = -1.6867875730018388e+145;
        bool r799307 = r799305 <= r799306;
        double r799308 = 3.0;
        double r799309 = sqrt(r799308);
        double r799310 = r799305 / r799309;
        double r799311 = fabs(r799310);
        double r799312 = -4.449993086430283e-268;
        bool r799313 = r799305 <= r799312;
        double r799314 = x;
        double r799315 = r799314 * r799314;
        double r799316 = y;
        double r799317 = r799316 * r799316;
        double r799318 = r799315 + r799317;
        double r799319 = r799305 * r799305;
        double r799320 = r799318 + r799319;
        double r799321 = sqrt(r799320);
        double r799322 = r799321 / r799309;
        double r799323 = fabs(r799322);
        double r799324 = 7.012294660736446e-227;
        bool r799325 = r799305 <= r799324;
        double r799326 = -1.0;
        double r799327 = r799314 / r799309;
        double r799328 = r799326 * r799327;
        double r799329 = fabs(r799328);
        double r799330 = 4.982936361432774e+94;
        bool r799331 = r799305 <= r799330;
        double r799332 = 0.3333333333333333;
        double r799333 = sqrt(r799332);
        double r799334 = r799305 * r799333;
        double r799335 = r799331 ? r799323 : r799334;
        double r799336 = r799325 ? r799329 : r799335;
        double r799337 = r799313 ? r799323 : r799336;
        double r799338 = r799307 ? r799311 : r799337;
        return r799338;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original38.1
Target25.9
Herbie25.9
\[\begin{array}{l} \mathbf{if}\;z \lt -6.3964793941097758 \cdot 10^{136}:\\ \;\;\;\;\frac{-z}{\sqrt{3}}\\ \mathbf{elif}\;z \lt 7.3202936944041821 \cdot 10^{117}:\\ \;\;\;\;\frac{\sqrt{\left(z \cdot z + x \cdot x\right) + y \cdot y}}{\sqrt{3}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.333333333333333315} \cdot z\\ \end{array}\]

Derivation

  1. Split input into 4 regimes

  2. if z < -1.6867875730018388e+145

    1. Initial program 62.2

      \[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
    2. Using strategy rm

    3. Applied add-sqr-sqrt62.3

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

    4. Applied add-sqr-sqrt62.3

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

    5. Applied times-frac62.3

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

    6. Applied rem-sqrt-square62.3

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

    7. Taylor expanded around 0 16.0

      \[\leadsto \left|\frac{\color{blue}{z}}{\sqrt{3}}\right|\]

    if -1.6867875730018388e+145 < z < -4.449993086430283e-268 or 7.012294660736446e-227 < z < 4.982936361432774e+94

    1. Initial program 28.9

      \[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
    2. Using strategy rm

    3. Applied add-sqr-sqrt29.1

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

    4. Applied add-sqr-sqrt29.1

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

    5. Applied times-frac29.0

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

    6. Applied rem-sqrt-square29.0

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

    if -4.449993086430283e-268 < z < 7.012294660736446e-227

    1. Initial program 33.2

      \[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
    2. Using strategy rm

    3. Applied add-sqr-sqrt33.4

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

    4. Applied add-sqr-sqrt33.4

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

    5. Applied times-frac33.3

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

    6. Applied rem-sqrt-square33.3

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

    7. Taylor expanded around -inf 32.1

      \[\leadsto \left|\color{blue}{-1 \cdot \frac{x}{\sqrt{3}}}\right|\]

    if 4.982936361432774e+94 < z

    1. Initial program 53.2

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

    2. Taylor expanded around 0 19.5

      \[\leadsto \color{blue}{z \cdot \sqrt{0.333333333333333315}}\]
  3. Recombined 4 regimes into one program.

  4. Final simplification25.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.68678757300183878 \cdot 10^{145}:\\ \;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\ \mathbf{elif}\;z \le -4.4499930864302828 \cdot 10^{-268}:\\ \;\;\;\;\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|\\ \mathbf{elif}\;z \le 7.0122946607364459 \cdot 10^{-227}:\\ \;\;\;\;\left|-1 \cdot \frac{x}{\sqrt{3}}\right|\\ \mathbf{elif}\;z \le 4.98293636143277424 \cdot 10^{94}:\\ \;\;\;\;\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|\\ \mathbf{else}:\\ \;\;\;\;z \cdot \sqrt{0.333333333333333315}\\ \end{array}\]

Reproduce

herbie shell --seed 2020081 
(FPCore (x y z)
  :name "Data.Array.Repa.Algorithms.Pixel:doubleRmsOfRGB8 from repa-algorithms-3.4.0.1"
  :precision binary64

  :herbie-target
  (if (< z -6.396479394109776e+136) (/ (- z) (sqrt 3)) (if (< z 7.320293694404182e+117) (/ (sqrt (+ (+ (* z z) (* x x)) (* y y))) (sqrt 3)) (* (sqrt 0.3333333333333333) z)))

  (sqrt (/ (+ (+ (* x x) (* y y)) (* z z)) 3)))