Average Error: 37.8 → 23.8
Time: 14.8s
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 0.0:\\ \;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\ \mathbf{elif}\;x \cdot x + y \cdot y \le 9.123040389468657471064841380531675193627 \cdot 10^{304}:\\ \;\;\;\;\sqrt{0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot x + y \cdot y\right) + z \cdot z\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 0.0:\\
\;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\

\mathbf{elif}\;x \cdot x + y \cdot y \le 9.123040389468657471064841380531675193627 \cdot 10^{304}:\\
\;\;\;\;\sqrt{0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot x + y \cdot y\right) + z \cdot z\right)}\\

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

\end{array}
double f(double x, double y, double z) {
        double r595641 = x;
        double r595642 = r595641 * r595641;
        double r595643 = y;
        double r595644 = r595643 * r595643;
        double r595645 = r595642 + r595644;
        double r595646 = z;
        double r595647 = r595646 * r595646;
        double r595648 = r595645 + r595647;
        double r595649 = 3.0;
        double r595650 = r595648 / r595649;
        double r595651 = sqrt(r595650);
        return r595651;
}
↓
double f(double x, double y, double z) {
        double r595652 = x;
        double r595653 = r595652 * r595652;
        double r595654 = y;
        double r595655 = r595654 * r595654;
        double r595656 = r595653 + r595655;
        double r595657 = 0.0;
        bool r595658 = r595656 <= r595657;
        double r595659 = z;
        double r595660 = 3.0;
        double r595661 = sqrt(r595660);
        double r595662 = r595659 / r595661;
        double r595663 = fabs(r595662);
        double r595664 = 9.123040389468657e+304;
        bool r595665 = r595656 <= r595664;
        double r595666 = 0.3333333333333333;
        double r595667 = r595659 * r595659;
        double r595668 = r595656 + r595667;
        double r595669 = r595666 * r595668;
        double r595670 = sqrt(r595669);
        double r595671 = r595652 / r595661;
        double r595672 = fabs(r595671);
        double r595673 = r595665 ? r595670 : r595672;
        double r595674 = r595658 ? r595663 : r595673;
        return r595674;
}

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.8
Target25.7
Herbie23.8
\[\begin{array}{l} \mathbf{if}\;z \lt -6.396479394109775845820908799933348003545 \cdot 10^{136}:\\ \;\;\;\;\frac{-z}{\sqrt{3}}\\ \mathbf{elif}\;z \lt 7.320293694404182125923160810847974073098 \cdot 10^{117}:\\ \;\;\;\;\frac{\sqrt{\left(z \cdot z + x \cdot x\right) + y \cdot y}}{\sqrt{3}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.3333333333333333148296162562473909929395} \cdot z\\ \end{array}\]

Derivation

  1. Split input into 3 regimes

  2. if (+ (* x x) (* y y)) < 0.0

    1. Initial program 30.8

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

    3. Applied add-sqr-sqrt31.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-sqrt31.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-frac31.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-square31.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 8.7

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

    if 0.0 < (+ (* x x) (* y y)) < 9.123040389468657e+304

    1. Initial program 15.7

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

    2. Taylor expanded around 0 15.7

      \[\leadsto \sqrt{\color{blue}{0.3333333333333333148296162562473909929395 \cdot {x}^{2} + \left(0.3333333333333333148296162562473909929395 \cdot {y}^{2} + 0.3333333333333333148296162562473909929395 \cdot {z}^{2}\right)}}\]

    3. Simplified15.7

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

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

    1. Initial program 63.7

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

    3. Applied add-sqr-sqrt63.8

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

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

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

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

  4. Final simplification23.8

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot x + y \cdot y \le 0.0:\\ \;\;\;\;\left|\frac{z}{\sqrt{3}}\right|\\ \mathbf{elif}\;x \cdot x + y \cdot y \le 9.123040389468657471064841380531675193627 \cdot 10^{304}:\\ \;\;\;\;\sqrt{0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot x + y \cdot y\right) + z \cdot z\right)}\\ \mathbf{else}:\\ \;\;\;\;\left|\frac{x}{\sqrt{3}}\right|\\ \end{array}\]

Reproduce

herbie shell --seed 2019306 
(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.3964793941097758e136) (/ (- z) (sqrt 3)) (if (< z 7.3202936944041821e117) (/ (sqrt (+ (+ (* z z) (* x x)) (* y y))) (sqrt 3)) (* (sqrt 0.333333333333333315) z)))

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