| Alternative 1 | |
|---|---|
| Accuracy | 97.7% |
| Cost | 91524 |

(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 x) (sqrt (+ 1.0 x))))
(t_2 (sqrt (+ y 1.0)))
(t_3 (sqrt (+ 1.0 z)))
(t_4 (sqrt (+ 1.0 t))))
(if (<= (- t_2 (sqrt y)) 0.2)
(+
(/ (/ (+ (sqrt y) (+ t_1 t_2)) (+ (sqrt y) t_2)) t_1)
(+ (- t_3 (sqrt z)) (- t_4 (sqrt t))))
(+
(- (+ 1.0 t_2) (sqrt y))
(+ (/ 1.0 (+ t_3 (sqrt z))) (/ 1.0 (+ t_4 (sqrt t))))))))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(x) + sqrt((1.0 + x));
double t_2 = sqrt((y + 1.0));
double t_3 = sqrt((1.0 + z));
double t_4 = sqrt((1.0 + t));
double tmp;
if ((t_2 - sqrt(y)) <= 0.2) {
tmp = (((sqrt(y) + (t_1 + t_2)) / (sqrt(y) + t_2)) / t_1) + ((t_3 - sqrt(z)) + (t_4 - sqrt(t)));
} else {
tmp = ((1.0 + t_2) - sqrt(y)) + ((1.0 / (t_3 + sqrt(z))) + (1.0 / (t_4 + sqrt(t))));
}
return tmp;
}
real(8) function code(x, y, z, t)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: t
code = (((sqrt((x + 1.0d0)) - sqrt(x)) + (sqrt((y + 1.0d0)) - sqrt(y))) + (sqrt((z + 1.0d0)) - sqrt(z))) + (sqrt((t + 1.0d0)) - sqrt(t))
end function
real(8) function code(x, y, z, t)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: t
real(8) :: t_1
real(8) :: t_2
real(8) :: t_3
real(8) :: t_4
real(8) :: tmp
t_1 = sqrt(x) + sqrt((1.0d0 + x))
t_2 = sqrt((y + 1.0d0))
t_3 = sqrt((1.0d0 + z))
t_4 = sqrt((1.0d0 + t))
if ((t_2 - sqrt(y)) <= 0.2d0) then
tmp = (((sqrt(y) + (t_1 + t_2)) / (sqrt(y) + t_2)) / t_1) + ((t_3 - sqrt(z)) + (t_4 - sqrt(t)))
else
tmp = ((1.0d0 + t_2) - sqrt(y)) + ((1.0d0 / (t_3 + sqrt(z))) + (1.0d0 / (t_4 + sqrt(t))))
end if
code = tmp
end function
public static double code(double x, double y, double z, double t) {
return (((Math.sqrt((x + 1.0)) - Math.sqrt(x)) + (Math.sqrt((y + 1.0)) - Math.sqrt(y))) + (Math.sqrt((z + 1.0)) - Math.sqrt(z))) + (Math.sqrt((t + 1.0)) - Math.sqrt(t));
}
public static double code(double x, double y, double z, double t) {
double t_1 = Math.sqrt(x) + Math.sqrt((1.0 + x));
double t_2 = Math.sqrt((y + 1.0));
double t_3 = Math.sqrt((1.0 + z));
double t_4 = Math.sqrt((1.0 + t));
double tmp;
if ((t_2 - Math.sqrt(y)) <= 0.2) {
tmp = (((Math.sqrt(y) + (t_1 + t_2)) / (Math.sqrt(y) + t_2)) / t_1) + ((t_3 - Math.sqrt(z)) + (t_4 - Math.sqrt(t)));
} else {
tmp = ((1.0 + t_2) - Math.sqrt(y)) + ((1.0 / (t_3 + Math.sqrt(z))) + (1.0 / (t_4 + Math.sqrt(t))));
}
return tmp;
}
def code(x, y, z, t): return (((math.sqrt((x + 1.0)) - math.sqrt(x)) + (math.sqrt((y + 1.0)) - math.sqrt(y))) + (math.sqrt((z + 1.0)) - math.sqrt(z))) + (math.sqrt((t + 1.0)) - math.sqrt(t))
def code(x, y, z, t): t_1 = math.sqrt(x) + math.sqrt((1.0 + x)) t_2 = math.sqrt((y + 1.0)) t_3 = math.sqrt((1.0 + z)) t_4 = math.sqrt((1.0 + t)) tmp = 0 if (t_2 - math.sqrt(y)) <= 0.2: tmp = (((math.sqrt(y) + (t_1 + t_2)) / (math.sqrt(y) + t_2)) / t_1) + ((t_3 - math.sqrt(z)) + (t_4 - math.sqrt(t))) else: tmp = ((1.0 + t_2) - math.sqrt(y)) + ((1.0 / (t_3 + math.sqrt(z))) + (1.0 / (t_4 + math.sqrt(t)))) return tmp
function code(x, y, z, t) return Float64(Float64(Float64(Float64(sqrt(Float64(x + 1.0)) - sqrt(x)) + Float64(sqrt(Float64(y + 1.0)) - sqrt(y))) + Float64(sqrt(Float64(z + 1.0)) - sqrt(z))) + Float64(sqrt(Float64(t + 1.0)) - sqrt(t))) end
function code(x, y, z, t) t_1 = Float64(sqrt(x) + sqrt(Float64(1.0 + x))) t_2 = sqrt(Float64(y + 1.0)) t_3 = sqrt(Float64(1.0 + z)) t_4 = sqrt(Float64(1.0 + t)) tmp = 0.0 if (Float64(t_2 - sqrt(y)) <= 0.2) tmp = Float64(Float64(Float64(Float64(sqrt(y) + Float64(t_1 + t_2)) / Float64(sqrt(y) + t_2)) / t_1) + Float64(Float64(t_3 - sqrt(z)) + Float64(t_4 - sqrt(t)))); else tmp = Float64(Float64(Float64(1.0 + t_2) - sqrt(y)) + Float64(Float64(1.0 / Float64(t_3 + sqrt(z))) + Float64(1.0 / Float64(t_4 + sqrt(t))))); end return tmp end
function tmp = code(x, y, z, t) tmp = (((sqrt((x + 1.0)) - sqrt(x)) + (sqrt((y + 1.0)) - sqrt(y))) + (sqrt((z + 1.0)) - sqrt(z))) + (sqrt((t + 1.0)) - sqrt(t)); end
function tmp_2 = code(x, y, z, t) t_1 = sqrt(x) + sqrt((1.0 + x)); t_2 = sqrt((y + 1.0)); t_3 = sqrt((1.0 + z)); t_4 = sqrt((1.0 + t)); tmp = 0.0; if ((t_2 - sqrt(y)) <= 0.2) tmp = (((sqrt(y) + (t_1 + t_2)) / (sqrt(y) + t_2)) / t_1) + ((t_3 - sqrt(z)) + (t_4 - sqrt(t))); else tmp = ((1.0 + t_2) - sqrt(y)) + ((1.0 / (t_3 + sqrt(z))) + (1.0 / (t_4 + sqrt(t)))); end tmp_2 = tmp; end
code[x_, y_, z_, t_] := N[(N[(N[(N[(N[Sqrt[N[(x + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[x], $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(z + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Sqrt[N[(t + 1.0), $MachinePrecision]], $MachinePrecision] - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
code[x_, y_, z_, t_] := Block[{t$95$1 = N[(N[Sqrt[x], $MachinePrecision] + N[Sqrt[N[(1.0 + x), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[Sqrt[N[(y + 1.0), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$3 = N[Sqrt[N[(1.0 + z), $MachinePrecision]], $MachinePrecision]}, Block[{t$95$4 = N[Sqrt[N[(1.0 + t), $MachinePrecision]], $MachinePrecision]}, If[LessEqual[N[(t$95$2 - N[Sqrt[y], $MachinePrecision]), $MachinePrecision], 0.2], N[(N[(N[(N[(N[Sqrt[y], $MachinePrecision] + N[(t$95$1 + t$95$2), $MachinePrecision]), $MachinePrecision] / N[(N[Sqrt[y], $MachinePrecision] + t$95$2), $MachinePrecision]), $MachinePrecision] / t$95$1), $MachinePrecision] + N[(N[(t$95$3 - N[Sqrt[z], $MachinePrecision]), $MachinePrecision] + N[(t$95$4 - N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(N[(1.0 + t$95$2), $MachinePrecision] - N[Sqrt[y], $MachinePrecision]), $MachinePrecision] + N[(N[(1.0 / N[(t$95$3 + N[Sqrt[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(1.0 / N[(t$95$4 + N[Sqrt[t], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]]]
\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{x} + \sqrt{1 + x}\\
t_2 := \sqrt{y + 1}\\
t_3 := \sqrt{1 + z}\\
t_4 := \sqrt{1 + t}\\
\mathbf{if}\;t_2 - \sqrt{y} \leq 0.2:\\
\;\;\;\;\frac{\frac{\sqrt{y} + \left(t_1 + t_2\right)}{\sqrt{y} + t_2}}{t_1} + \left(\left(t_3 - \sqrt{z}\right) + \left(t_4 - \sqrt{t}\right)\right)\\
\mathbf{else}:\\
\;\;\;\;\left(\left(1 + t_2\right) - \sqrt{y}\right) + \left(\frac{1}{t_3 + \sqrt{z}} + \frac{1}{t_4 + \sqrt{t}}\right)\\
\end{array}
Herbie found 18 alternatives:
| Alternative | Accuracy | Speedup |
|---|
Results
| Original | 91.8% |
|---|---|
| Target | 99.4% |
| Herbie | 99.4% |
if (-.f64 (sqrt.f64 (+.f64 y 1)) (sqrt.f64 y)) < 0.20000000000000001Initial program 86.9%
Simplified86.5%
[Start]86.9 | \[ \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)
\] |
|---|---|
associate-+l+ [=>]86.9 | \[ \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)}
\] |
associate-+l- [=>]86.5 | \[ \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)
\] |
+-commutative [=>]86.5 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)
\] |
sub-neg [=>]86.5 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} + \left(-\sqrt{z}\right)\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)
\] |
sub-neg [<=]86.5 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} - \sqrt{z}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)
\] |
+-commutative [=>]86.5 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{\color{blue}{1 + z}} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)
\] |
+-commutative [=>]86.5 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{\color{blue}{1 + t}} - \sqrt{t}\right)\right)
\] |
Applied egg-rr86.9%
[Start]86.5 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
|---|---|
add-log-exp [=>]86.5 | \[ \color{blue}{\log \left(e^{\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)}\right)} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
associate--r- [=>]86.9 | \[ \log \left(e^{\color{blue}{\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{1 + y} - \sqrt{y}\right)}}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
+-commutative [=>]86.9 | \[ \log \left(e^{\left(\sqrt{\color{blue}{1 + x}} - \sqrt{x}\right) + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
Applied egg-rr87.7%
[Start]86.9 | \[ \log \left(e^{\left(\sqrt{1 + x} - \sqrt{x}\right) + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
|---|---|
flip-- [=>]86.8 | \[ \log \left(e^{\color{blue}{\frac{\sqrt{1 + x} \cdot \sqrt{1 + x} - \sqrt{x} \cdot \sqrt{x}}{\sqrt{1 + x} + \sqrt{x}}} + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
div-inv [=>]86.8 | \[ \log \left(e^{\color{blue}{\left(\sqrt{1 + x} \cdot \sqrt{1 + x} - \sqrt{x} \cdot \sqrt{x}\right) \cdot \frac{1}{\sqrt{1 + x} + \sqrt{x}}} + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
add-sqr-sqrt [<=]72.9 | \[ \log \left(e^{\left(\color{blue}{\left(1 + x\right)} - \sqrt{x} \cdot \sqrt{x}\right) \cdot \frac{1}{\sqrt{1 + x} + \sqrt{x}} + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
add-sqr-sqrt [<=]87.3 | \[ \log \left(e^{\left(\left(1 + x\right) - \color{blue}{x}\right) \cdot \frac{1}{\sqrt{1 + x} + \sqrt{x}} + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
associate--l+ [=>]87.7 | \[ \log \left(e^{\color{blue}{\left(1 + \left(x - x\right)\right)} \cdot \frac{1}{\sqrt{1 + x} + \sqrt{x}} + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
Simplified87.7%
[Start]87.7 | \[ \log \left(e^{\left(1 + \left(x - x\right)\right) \cdot \frac{1}{\sqrt{1 + x} + \sqrt{x}} + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
|---|---|
+-inverses [=>]87.7 | \[ \log \left(e^{\left(1 + \color{blue}{0}\right) \cdot \frac{1}{\sqrt{1 + x} + \sqrt{x}} + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
metadata-eval [=>]87.7 | \[ \log \left(e^{\color{blue}{1} \cdot \frac{1}{\sqrt{1 + x} + \sqrt{x}} + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
*-lft-identity [=>]87.7 | \[ \log \left(e^{\color{blue}{\frac{1}{\sqrt{1 + x} + \sqrt{x}}} + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
Applied egg-rr91.7%
[Start]87.7 | \[ \log \left(e^{\frac{1}{\sqrt{1 + x} + \sqrt{x}} + \left(\sqrt{1 + y} - \sqrt{y}\right)}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
|---|---|
add-log-exp [<=]89.2 | \[ \color{blue}{\left(\frac{1}{\sqrt{1 + x} + \sqrt{x}} + \left(\sqrt{1 + y} - \sqrt{y}\right)\right)} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
flip-- [=>]89.1 | \[ \left(\frac{1}{\sqrt{1 + x} + \sqrt{x}} + \color{blue}{\frac{\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}}{\sqrt{1 + y} + \sqrt{y}}}\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
frac-add [=>]89.1 | \[ \color{blue}{\frac{1 \cdot \left(\sqrt{1 + y} + \sqrt{y}\right) + \left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}\right)}{\left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(\sqrt{1 + y} + \sqrt{y}\right)}} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
*-un-lft-identity [<=]89.1 | \[ \frac{\color{blue}{\left(\sqrt{1 + y} + \sqrt{y}\right)} + \left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(\sqrt{1 + y} \cdot \sqrt{1 + y} - \sqrt{y} \cdot \sqrt{y}\right)}{\left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(\sqrt{1 + y} + \sqrt{y}\right)} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
add-sqr-sqrt [<=]52.8 | \[ \frac{\left(\sqrt{1 + y} + \sqrt{y}\right) + \left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(\color{blue}{\left(1 + y\right)} - \sqrt{y} \cdot \sqrt{y}\right)}{\left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(\sqrt{1 + y} + \sqrt{y}\right)} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
add-sqr-sqrt [<=]89.3 | \[ \frac{\left(\sqrt{1 + y} + \sqrt{y}\right) + \left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(\left(1 + y\right) - \color{blue}{y}\right)}{\left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(\sqrt{1 + y} + \sqrt{y}\right)} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
associate--l+ [=>]91.7 | \[ \frac{\left(\sqrt{1 + y} + \sqrt{y}\right) + \left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \color{blue}{\left(1 + \left(y - y\right)\right)}}{\left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(\sqrt{1 + y} + \sqrt{y}\right)} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
Simplified91.7%
[Start]91.7 | \[ \frac{\left(\sqrt{1 + y} + \sqrt{y}\right) + \left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(1 + \left(y - y\right)\right)}{\left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(\sqrt{1 + y} + \sqrt{y}\right)} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
|---|---|
associate-/l/ [<=]91.7 | \[ \color{blue}{\frac{\frac{\left(\sqrt{1 + y} + \sqrt{y}\right) + \left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(1 + \left(y - y\right)\right)}{\sqrt{1 + y} + \sqrt{y}}}{\sqrt{1 + x} + \sqrt{x}}} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
+-commutative [=>]91.7 | \[ \frac{\frac{\color{blue}{\left(\sqrt{1 + x} + \sqrt{x}\right) \cdot \left(1 + \left(y - y\right)\right) + \left(\sqrt{1 + y} + \sqrt{y}\right)}}{\sqrt{1 + y} + \sqrt{y}}}{\sqrt{1 + x} + \sqrt{x}} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
*-commutative [<=]91.7 | \[ \frac{\frac{\color{blue}{\left(1 + \left(y - y\right)\right) \cdot \left(\sqrt{1 + x} + \sqrt{x}\right)} + \left(\sqrt{1 + y} + \sqrt{y}\right)}{\sqrt{1 + y} + \sqrt{y}}}{\sqrt{1 + x} + \sqrt{x}} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
*-rgt-identity [<=]91.7 | \[ \frac{\frac{\left(1 + \left(y - y\right)\right) \cdot \left(\sqrt{1 + x} + \sqrt{x}\right) + \color{blue}{\left(\sqrt{1 + y} + \sqrt{y}\right) \cdot 1}}{\sqrt{1 + y} + \sqrt{y}}}{\sqrt{1 + x} + \sqrt{x}} + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
if 0.20000000000000001 < (-.f64 (sqrt.f64 (+.f64 y 1)) (sqrt.f64 y)) Initial program 96.9%
Simplified59.9%
[Start]96.9 | \[ \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)
\] |
|---|---|
associate-+l+ [=>]96.9 | \[ \color{blue}{\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)}
\] |
associate-+l- [=>]59.9 | \[ \color{blue}{\left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{y + 1} - \sqrt{y}\right)\right)\right)} + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)
\] |
+-commutative [=>]59.9 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{\color{blue}{1 + y}} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{z + 1} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)
\] |
sub-neg [=>]59.9 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} + \left(-\sqrt{z}\right)\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)
\] |
sub-neg [<=]59.9 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{z + 1} - \sqrt{z}\right)} + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)
\] |
+-commutative [=>]59.9 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{\color{blue}{1 + z}} - \sqrt{z}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\right)
\] |
+-commutative [=>]59.9 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{\color{blue}{1 + t}} - \sqrt{t}\right)\right)
\] |
Applied egg-rr60.3%
[Start]59.9 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\sqrt{1 + z} - \sqrt{z}\right) + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
|---|---|
flip-- [=>]59.9 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\frac{\sqrt{1 + z} \cdot \sqrt{1 + z} - \sqrt{z} \cdot \sqrt{z}}{\sqrt{1 + z} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
div-inv [=>]59.9 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(\sqrt{1 + z} \cdot \sqrt{1 + z} - \sqrt{z} \cdot \sqrt{z}\right) \cdot \frac{1}{\sqrt{1 + z} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
add-sqr-sqrt [<=]48.6 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\color{blue}{\left(1 + z\right)} - \sqrt{z} \cdot \sqrt{z}\right) \cdot \frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
add-sqr-sqrt [<=]60.1 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(\left(1 + z\right) - \color{blue}{z}\right) \cdot \frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
associate--l+ [=>]60.3 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\left(1 + \left(z - z\right)\right)} \cdot \frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
Simplified60.3%
[Start]60.3 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(1 + \left(z - z\right)\right) \cdot \frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
|---|---|
+-inverses [=>]60.3 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\left(1 + \color{blue}{0}\right) \cdot \frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
metadata-eval [=>]60.3 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{1} \cdot \frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
*-lft-identity [=>]60.3 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\color{blue}{\frac{1}{\sqrt{1 + z} + \sqrt{z}}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
Applied egg-rr61.0%
[Start]60.3 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\sqrt{1 + t} - \sqrt{t}\right)\right)
\] |
|---|---|
flip-- [=>]60.4 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \color{blue}{\frac{\sqrt{1 + t} \cdot \sqrt{1 + t} - \sqrt{t} \cdot \sqrt{t}}{\sqrt{1 + t} + \sqrt{t}}}\right)
\] |
div-inv [=>]60.4 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \color{blue}{\left(\sqrt{1 + t} \cdot \sqrt{1 + t} - \sqrt{t} \cdot \sqrt{t}\right) \cdot \frac{1}{\sqrt{1 + t} + \sqrt{t}}}\right)
\] |
add-sqr-sqrt [<=]40.5 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\color{blue}{\left(1 + t\right)} - \sqrt{t} \cdot \sqrt{t}\right) \cdot \frac{1}{\sqrt{1 + t} + \sqrt{t}}\right)
\] |
add-sqr-sqrt [<=]60.4 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(\left(1 + t\right) - \color{blue}{t}\right) \cdot \frac{1}{\sqrt{1 + t} + \sqrt{t}}\right)
\] |
associate--l+ [=>]61.0 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \color{blue}{\left(1 + \left(t - t\right)\right)} \cdot \frac{1}{\sqrt{1 + t} + \sqrt{t}}\right)
\] |
Simplified61.0%
[Start]61.0 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(1 + \left(t - t\right)\right) \cdot \frac{1}{\sqrt{1 + t} + \sqrt{t}}\right)
\] |
|---|---|
+-inverses [=>]61.0 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \left(1 + \color{blue}{0}\right) \cdot \frac{1}{\sqrt{1 + t} + \sqrt{t}}\right)
\] |
metadata-eval [=>]61.0 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \color{blue}{1} \cdot \frac{1}{\sqrt{1 + t} + \sqrt{t}}\right)
\] |
*-lft-identity [=>]61.0 | \[ \left(\sqrt{x + 1} - \left(\sqrt{x} - \left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\frac{1}{\sqrt{1 + z} + \sqrt{z}} + \color{blue}{\frac{1}{\sqrt{1 + t} + \sqrt{t}}}\right)
\] |
Taylor expanded in x around 0 58.1%
Final simplification75.3%
| Alternative 1 | |
|---|---|
| Accuracy | 97.7% |
| Cost | 91524 |
| Alternative 2 | |
|---|---|
| Accuracy | 97.5% |
| Cost | 66244 |
| Alternative 3 | |
|---|---|
| Accuracy | 97.7% |
| Cost | 66116 |
| Alternative 4 | |
|---|---|
| Accuracy | 98.0% |
| Cost | 39880 |
| Alternative 5 | |
|---|---|
| Accuracy | 96.9% |
| Cost | 39876 |
| Alternative 6 | |
|---|---|
| Accuracy | 96.9% |
| Cost | 39752 |
| Alternative 7 | |
|---|---|
| Accuracy | 95.7% |
| Cost | 26692 |
| Alternative 8 | |
|---|---|
| Accuracy | 96.1% |
| Cost | 26692 |
| Alternative 9 | |
|---|---|
| Accuracy | 90.0% |
| Cost | 26568 |
| Alternative 10 | |
|---|---|
| Accuracy | 90.0% |
| Cost | 26568 |
| Alternative 11 | |
|---|---|
| Accuracy | 64.6% |
| Cost | 13384 |
| Alternative 12 | |
|---|---|
| Accuracy | 82.3% |
| Cost | 13380 |
| Alternative 13 | |
|---|---|
| Accuracy | 84.5% |
| Cost | 13380 |
| Alternative 14 | |
|---|---|
| Accuracy | 86.0% |
| Cost | 13380 |
| Alternative 15 | |
|---|---|
| Accuracy | 63.4% |
| Cost | 6856 |
| Alternative 16 | |
|---|---|
| Accuracy | 62.0% |
| Cost | 6724 |
| Alternative 17 | |
|---|---|
| Accuracy | 34.7% |
| Cost | 64 |
herbie shell --seed 2023161
(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))))