Average Error: 5.4 → 0.5
Time: 13.7s
Precision: binary64
\[[x, y, z, t]=\mathsf{sort}([x, y, z, t])\]
\[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
↓
\[\begin{array}{l} t_1 := \sqrt{1 + x}\\ t_2 := \sqrt{y + 1}\\ t_3 := t_2 - \sqrt{y}\\ t_4 := \sqrt{1 + z}\\ t_5 := \sqrt{1 + t} - \sqrt{t}\\ \mathbf{if}\;t_3 \leq 0.6460180036065553:\\ \;\;\;\;\begin{array}{l} t_6 := \sqrt{\frac{1}{t_2 + \sqrt{y}}}\\ \left(\left(\frac{1}{t_1 + \sqrt{x}} + t_6 \cdot t_6\right) + \left(t_4 - \sqrt{z}\right)\right) + t_5 \end{array}\\ \mathbf{else}:\\ \;\;\;\;t_5 + \left(\left(t_3 + \left(t_1 - \sqrt{x}\right)\right) + \frac{1}{t_4 + \sqrt{z}}\right)\\ \end{array} \]
\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)
↓
\begin{array}{l}
t_1 := \sqrt{1 + x}\\
t_2 := \sqrt{y + 1}\\
t_3 := t_2 - \sqrt{y}\\
t_4 := \sqrt{1 + z}\\
t_5 := \sqrt{1 + t} - \sqrt{t}\\
\mathbf{if}\;t_3 \leq 0.6460180036065553:\\
\;\;\;\;\begin{array}{l}
t_6 := \sqrt{\frac{1}{t_2 + \sqrt{y}}}\\
\left(\left(\frac{1}{t_1 + \sqrt{x}} + t_6 \cdot t_6\right) + \left(t_4 - \sqrt{z}\right)\right) + t_5
\end{array}\\

\mathbf{else}:\\
\;\;\;\;t_5 + \left(\left(t_3 + \left(t_1 - \sqrt{x}\right)\right) + \frac{1}{t_4 + \sqrt{z}}\right)\\


\end{array}

(FPCore (x y z t)
 :precision binary64
 (+
  (+
   (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y)))
   (- (sqrt (+ z 1.0)) (sqrt z)))
  (- (sqrt (+ t 1.0)) (sqrt t))))
↓
(FPCore (x y z t)
 :precision binary64
 (let* ((t_1 (sqrt (+ 1.0 x)))
        (t_2 (sqrt (+ y 1.0)))
        (t_3 (- t_2 (sqrt y)))
        (t_4 (sqrt (+ 1.0 z)))
        (t_5 (- (sqrt (+ 1.0 t)) (sqrt t))))
   (if (<= t_3 0.6460180036065553)
     (let* ((t_6 (sqrt (/ 1.0 (+ t_2 (sqrt y))))))
       (+ (+ (+ (/ 1.0 (+ t_1 (sqrt x))) (* t_6 t_6)) (- t_4 (sqrt z))) t_5))
     (+ t_5 (+ (+ t_3 (- t_1 (sqrt x))) (/ 1.0 (+ t_4 (sqrt z))))))))
double code(double x, double y, double z, double t) {
	return (((sqrt(x + 1.0) - sqrt(x)) + (sqrt(y + 1.0) - sqrt(y))) + (sqrt(z + 1.0) - sqrt(z))) + (sqrt(t + 1.0) - sqrt(t));
}
↓
double code(double x, double y, double z, double t) {
	double t_1 = sqrt(1.0 + x);
	double t_2 = sqrt(y + 1.0);
	double t_3 = t_2 - sqrt(y);
	double t_4 = sqrt(1.0 + z);
	double t_5 = sqrt(1.0 + t) - sqrt(t);
	double tmp;
	if (t_3 <= 0.6460180036065553) {
		double t_6_1 = sqrt(1.0 / (t_2 + sqrt(y)));
		tmp = (((1.0 / (t_1 + sqrt(x))) + (t_6_1 * t_6_1)) + (t_4 - sqrt(z))) + t_5;
	} else {
		tmp = t_5 + ((t_3 + (t_1 - sqrt(x))) + (1.0 / (t_4 + sqrt(z))));
	}
	return tmp;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original5.4
Target0.4
Herbie0.5
\[\left(\left(\frac{1}{\sqrt{x + 1} + \sqrt{x}} + \frac{1}{\sqrt{y + 1} + \sqrt{y}}\right) + \frac{1}{\sqrt{z + 1} + \sqrt{z}}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

Derivation

  1. Split input into 2 regimes

  2. if (-.f64 (sqrt.f64 (+.f64 y 1)) (sqrt.f64 y)) < 0.64601800360655526

    1. Initial program 13.4

      \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
    2. Using strategy rm

    3. Applied flip--_binary6413.2

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

    4. Simplified4.4

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

    5. Simplified4.4

      \[\leadsto \left(\left(\frac{1}{\color{blue}{\sqrt{1 + x} + \sqrt{x}}} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
    6. Using strategy rm

    7. Applied flip--_binary644.1

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

    8. Simplified0.5

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

    9. Simplified0.5

      \[\leadsto \left(\left(\frac{1}{\sqrt{1 + x} + \sqrt{x}} + \frac{1}{\color{blue}{\sqrt{1 + y} + \sqrt{y}}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
    10. Using strategy rm

    11. Applied add-sqr-sqrt_binary640.5

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

    if 0.64601800360655526 < (-.f64 (sqrt.f64 (+.f64 y 1)) (sqrt.f64 y))

    1. Initial program 1.6

      \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
    2. Using strategy rm

    3. Applied flip--_binary641.5

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

    4. Simplified0.5

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

    5. Simplified0.5

      \[\leadsto \left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \frac{1}{\color{blue}{\sqrt{1 + z} + \sqrt{z}}}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
  3. Recombined 2 regimes into one program.

  4. Final simplification0.5

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sqrt{y + 1} - \sqrt{y} \leq 0.6460180036065553:\\ \;\;\;\;\left(\left(\frac{1}{\sqrt{1 + x} + \sqrt{x}} + \sqrt{\frac{1}{\sqrt{y + 1} + \sqrt{y}}} \cdot \sqrt{\frac{1}{\sqrt{y + 1} + \sqrt{y}}}\right) + \left(\sqrt{1 + z} - \sqrt{z}\right)\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\sqrt{1 + t} - \sqrt{t}\right) + \left(\left(\left(\sqrt{y + 1} - \sqrt{y}\right) + \left(\sqrt{1 + x} - \sqrt{x}\right)\right) + \frac{1}{\sqrt{1 + z} + \sqrt{z}}\right)\\ \end{array} \]

Reproduce

herbie shell --seed 2021207 
(FPCore (x y z t)
  :name "Main:z from "
  :precision binary64

  :herbie-target
  (+ (+ (+ (/ 1.0 (+ (sqrt (+ x 1.0)) (sqrt x))) (/ 1.0 (+ (sqrt (+ y 1.0)) (sqrt y)))) (/ 1.0 (+ (sqrt (+ z 1.0)) (sqrt z)))) (- (sqrt (+ t 1.0)) (sqrt t)))

  (+ (+ (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y))) (- (sqrt (+ z 1.0)) (sqrt z))) (- (sqrt (+ t 1.0)) (sqrt t))))