Average Error: 38.2 → 24.4
Time: 4.2s
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 3.7682365661707411 \cdot 10^{-288}:\\ \;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\ \mathbf{elif}\;x \cdot x + y \cdot y \le 6.36921913743591853 \cdot 10^{78}:\\ \;\;\;\;\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z} \cdot \sqrt{\frac{1}{3}}\\ \mathbf{elif}\;x \cdot x + y \cdot y \le 9.21234681244353091 \cdot 10^{127}:\\ \;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\ \mathbf{elif}\;x \cdot x + y \cdot y \le 7.3089500670956082 \cdot 10^{304}:\\ \;\;\;\;\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|\\ \mathbf{else}:\\ \;\;\;\;\left|-1 \cdot \left(\frac{1}{\sqrt[3]{\sqrt{3}} \cdot \sqrt[3]{\sqrt{3}}} \cdot \frac{x}{\sqrt[3]{\sqrt{3}}}\right)\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 3.7682365661707411 \cdot 10^{-288}:\\
\;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\

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

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

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

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

\end{array}
double f(double x, double y, double z) {
        double r840417 = x;
        double r840418 = r840417 * r840417;
        double r840419 = y;
        double r840420 = r840419 * r840419;
        double r840421 = r840418 + r840420;
        double r840422 = z;
        double r840423 = r840422 * r840422;
        double r840424 = r840421 + r840423;
        double r840425 = 3.0;
        double r840426 = r840424 / r840425;
        double r840427 = sqrt(r840426);
        return r840427;
}
↓
double f(double x, double y, double z) {
        double r840428 = x;
        double r840429 = r840428 * r840428;
        double r840430 = y;
        double r840431 = r840430 * r840430;
        double r840432 = r840429 + r840431;
        double r840433 = 3.768236566170741e-288;
        bool r840434 = r840432 <= r840433;
        double r840435 = z;
        double r840436 = 3.0;
        double r840437 = sqrt(r840436);
        double r840438 = r840435 / r840437;
        double r840439 = fabs(r840438);
        double r840440 = 6.3692191374359185e+78;
        bool r840441 = r840432 <= r840440;
        double r840442 = r840435 * r840435;
        double r840443 = r840432 + r840442;
        double r840444 = sqrt(r840443);
        double r840445 = 1.0;
        double r840446 = r840445 / r840436;
        double r840447 = sqrt(r840446);
        double r840448 = r840444 * r840447;
        double r840449 = 9.21234681244353e+127;
        bool r840450 = r840432 <= r840449;
        double r840451 = 7.308950067095608e+304;
        bool r840452 = r840432 <= r840451;
        double r840453 = r840444 / r840437;
        double r840454 = fabs(r840453);
        double r840455 = -1.0;
        double r840456 = cbrt(r840437);
        double r840457 = r840456 * r840456;
        double r840458 = r840445 / r840457;
        double r840459 = r840428 / r840456;
        double r840460 = r840458 * r840459;
        double r840461 = r840455 * r840460;
        double r840462 = fabs(r840461);
        double r840463 = r840452 ? r840454 : r840462;
        double r840464 = r840450 ? r840439 : r840463;
        double r840465 = r840441 ? r840448 : r840464;
        double r840466 = r840434 ? r840439 : r840465;
        return r840466;
}

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.2
Target26.1
Herbie24.4
\[\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 (+ (* x x) (* y y)) < 3.768236566170741e-288 or 6.3692191374359185e+78 < (+ (* x x) (* y y)) < 9.21234681244353e+127

    1. Initial program 23.9

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

    3. Applied add-sqr-sqrt24.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-sqrt24.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-frac24.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-square24.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 0 19.1

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

    if 3.768236566170741e-288 < (+ (* x x) (* y y)) < 6.3692191374359185e+78

    1. Initial program 15.7

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

    3. Applied div-inv15.7

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

    4. Applied sqrt-prod15.9

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

    if 9.21234681244353e+127 < (+ (* x x) (* y y)) < 7.308950067095608e+304

    1. Initial program 15.6

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

    3. Applied add-sqr-sqrt15.9

      \[\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-sqrt15.9

      \[\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-frac15.8

      \[\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-square15.8

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

    if 7.308950067095608e+304 < (+ (* x x) (* y y))

    1. Initial program 63.6

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

    3. Applied add-sqr-sqrt63.6

      \[\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-sqrt63.6

      \[\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-frac63.6

      \[\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-square63.6

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

      \[\leadsto \left|\color{blue}{-1 \cdot \frac{x}{\sqrt{3}}}\right|\]
    8. Using strategy rm

    9. Applied add-cube-cbrt33.9

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

    10. Applied *-un-lft-identity33.9

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

    11. Applied times-frac34.0

      \[\leadsto \left|-1 \cdot \color{blue}{\left(\frac{1}{\sqrt[3]{\sqrt{3}} \cdot \sqrt[3]{\sqrt{3}}} \cdot \frac{x}{\sqrt[3]{\sqrt{3}}}\right)}\right|\]
  3. Recombined 4 regimes into one program.

  4. Final simplification24.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot x + y \cdot y \le 3.7682365661707411 \cdot 10^{-288}:\\ \;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\ \mathbf{elif}\;x \cdot x + y \cdot y \le 6.36921913743591853 \cdot 10^{78}:\\ \;\;\;\;\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z} \cdot \sqrt{\frac{1}{3}}\\ \mathbf{elif}\;x \cdot x + y \cdot y \le 9.21234681244353091 \cdot 10^{127}:\\ \;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\ \mathbf{elif}\;x \cdot x + y \cdot y \le 7.3089500670956082 \cdot 10^{304}:\\ \;\;\;\;\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|\\ \mathbf{else}:\\ \;\;\;\;\left|-1 \cdot \left(\frac{1}{\sqrt[3]{\sqrt{3}} \cdot \sqrt[3]{\sqrt{3}}} \cdot \frac{x}{\sqrt[3]{\sqrt{3}}}\right)\right|\\ \end{array}\]

Reproduce

herbie shell --seed 2020047 
(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)))