Average Error: 38.2 → 24.4
Time: 11.5s
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|-\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 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|-\frac{x}{\sqrt{3}}\right|\\

\end{array}
double f(double x, double y, double z) {
        double r855750 = x;
        double r855751 = r855750 * r855750;
        double r855752 = y;
        double r855753 = r855752 * r855752;
        double r855754 = r855751 + r855753;
        double r855755 = z;
        double r855756 = r855755 * r855755;
        double r855757 = r855754 + r855756;
        double r855758 = 3.0;
        double r855759 = r855757 / r855758;
        double r855760 = sqrt(r855759);
        return r855760;
}
↓
double f(double x, double y, double z) {
        double r855761 = x;
        double r855762 = r855761 * r855761;
        double r855763 = y;
        double r855764 = r855763 * r855763;
        double r855765 = r855762 + r855764;
        double r855766 = 3.768236566170741e-288;
        bool r855767 = r855765 <= r855766;
        double r855768 = z;
        double r855769 = 3.0;
        double r855770 = sqrt(r855769);
        double r855771 = r855768 / r855770;
        double r855772 = fabs(r855771);
        double r855773 = 6.3692191374359185e+78;
        bool r855774 = r855765 <= r855773;
        double r855775 = r855768 * r855768;
        double r855776 = r855765 + r855775;
        double r855777 = sqrt(r855776);
        double r855778 = 1.0;
        double r855779 = r855778 / r855769;
        double r855780 = sqrt(r855779);
        double r855781 = r855777 * r855780;
        double r855782 = 9.21234681244353e+127;
        bool r855783 = r855765 <= r855782;
        double r855784 = 7.308950067095608e+304;
        bool r855785 = r855765 <= r855784;
        double r855786 = r855777 / r855770;
        double r855787 = fabs(r855786);
        double r855788 = r855761 / r855770;
        double r855789 = -r855788;
        double r855790 = fabs(r855789);
        double r855791 = r855785 ? r855787 : r855790;
        double r855792 = r855783 ? r855772 : r855791;
        double r855793 = r855774 ? r855781 : r855792;
        double r855794 = r855767 ? r855772 : r855793;
        return r855794;
}

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. Simplified33.9

      \[\leadsto \left|\color{blue}{-\frac{x}{\sqrt{3}}}\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|-\frac{x}{\sqrt{3}}\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)))