Average Error: 37.7 → 15.7
Time: 12.1s
Precision: 64
\[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \cdot x + y \cdot y \le 9.5571349373151974 \cdot 10^{307}:\\ \;\;\;\;\left|\frac{\mathsf{hypot}\left(\sqrt{x \cdot x + y \cdot y}, z\right)}{\sqrt{3}}\right|\\ \mathbf{else}:\\ \;\;\;\;\left|\frac{x}{\sqrt{3}}\right|\\ \end{array}\]
\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}
↓
\begin{array}{l}
\mathbf{if}\;x \cdot x + y \cdot y \le 9.5571349373151974 \cdot 10^{307}:\\
\;\;\;\;\left|\frac{\mathsf{hypot}\left(\sqrt{x \cdot x + y \cdot y}, z\right)}{\sqrt{3}}\right|\\

\mathbf{else}:\\
\;\;\;\;\left|\frac{x}{\sqrt{3}}\right|\\

\end{array}
double f(double x, double y, double z) {
        double r925276 = x;
        double r925277 = r925276 * r925276;
        double r925278 = y;
        double r925279 = r925278 * r925278;
        double r925280 = r925277 + r925279;
        double r925281 = z;
        double r925282 = r925281 * r925281;
        double r925283 = r925280 + r925282;
        double r925284 = 3.0;
        double r925285 = r925283 / r925284;
        double r925286 = sqrt(r925285);
        return r925286;
}
↓
double f(double x, double y, double z) {
        double r925287 = x;
        double r925288 = r925287 * r925287;
        double r925289 = y;
        double r925290 = r925289 * r925289;
        double r925291 = r925288 + r925290;
        double r925292 = 9.557134937315197e+307;
        bool r925293 = r925291 <= r925292;
        double r925294 = sqrt(r925291);
        double r925295 = z;
        double r925296 = hypot(r925294, r925295);
        double r925297 = 3.0;
        double r925298 = sqrt(r925297);
        double r925299 = r925296 / r925298;
        double r925300 = fabs(r925299);
        double r925301 = r925287 / r925298;
        double r925302 = fabs(r925301);
        double r925303 = r925293 ? r925300 : r925302;
        return r925303;
}

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

Original37.7
Target25.8
Herbie15.7
\[\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 2 regimes

  2. if (+ (* x x) (* y y)) < 9.557134937315197e+307

    1. Initial program 17.1

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

    3. Applied add-sqr-sqrt17.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-sqrt17.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-frac17.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-square17.3

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

    8. Applied add-sqr-sqrt17.3

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

    9. Applied hypot-def1.4

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

    if 9.557134937315197e+307 < (+ (* x x) (* y y))

    1. Initial program 64.0

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

    3. Applied add-sqr-sqrt64.0

      \[\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-sqrt64.0

      \[\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-frac64.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-square64.0

      \[\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 34.0

      \[\leadsto \left|\frac{\color{blue}{x}}{\sqrt{3}}\right|\]
  3. Recombined 2 regimes into one program.

  4. Final simplification15.7

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot x + y \cdot y \le 9.5571349373151974 \cdot 10^{307}:\\ \;\;\;\;\left|\frac{\mathsf{hypot}\left(\sqrt{x \cdot x + y \cdot y}, z\right)}{\sqrt{3}}\right|\\ \mathbf{else}:\\ \;\;\;\;\left|\frac{x}{\sqrt{3}}\right|\\ \end{array}\]

Reproduce

herbie shell --seed 2020045 +o rules:numerics
(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)))