
(FPCore (x y z a) :precision binary64 (+ x (- (tan (+ y z)) (tan a))))
double code(double x, double y, double z, double a) {
return x + (tan((y + z)) - tan(a));
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
code = x + (tan((y + z)) - tan(a))
end function
public static double code(double x, double y, double z, double a) {
return x + (Math.tan((y + z)) - Math.tan(a));
}
def code(x, y, z, a): return x + (math.tan((y + z)) - math.tan(a))
function code(x, y, z, a) return Float64(x + Float64(tan(Float64(y + z)) - tan(a))) end
function tmp = code(x, y, z, a) tmp = x + (tan((y + z)) - tan(a)); end
code[x_, y_, z_, a_] := N[(x + N[(N[Tan[N[(y + z), $MachinePrecision]], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
x + \left(\tan \left(y + z\right) - \tan a\right)
\end{array}
Sampling outcomes in binary64 precision:
Herbie found 10 alternatives:
| Alternative | Accuracy | Speedup |
|---|
(FPCore (x y z a) :precision binary64 (+ x (- (tan (+ y z)) (tan a))))
double code(double x, double y, double z, double a) {
return x + (tan((y + z)) - tan(a));
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
code = x + (tan((y + z)) - tan(a))
end function
public static double code(double x, double y, double z, double a) {
return x + (Math.tan((y + z)) - Math.tan(a));
}
def code(x, y, z, a): return x + (math.tan((y + z)) - math.tan(a))
function code(x, y, z, a) return Float64(x + Float64(tan(Float64(y + z)) - tan(a))) end
function tmp = code(x, y, z, a) tmp = x + (tan((y + z)) - tan(a)); end
code[x_, y_, z_, a_] := N[(x + N[(N[Tan[N[(y + z), $MachinePrecision]], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
x + \left(\tan \left(y + z\right) - \tan a\right)
\end{array}
(FPCore (x y z a) :precision binary64 (+ x (- (/ (+ (tan y) (tan z)) (- 1.0 (+ (+ 1.0 (* (tan y) (tan z))) -1.0))) (tan a))))
double code(double x, double y, double z, double a) {
return x + (((tan(y) + tan(z)) / (1.0 - ((1.0 + (tan(y) * tan(z))) + -1.0))) - tan(a));
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
code = x + (((tan(y) + tan(z)) / (1.0d0 - ((1.0d0 + (tan(y) * tan(z))) + (-1.0d0)))) - tan(a))
end function
public static double code(double x, double y, double z, double a) {
return x + (((Math.tan(y) + Math.tan(z)) / (1.0 - ((1.0 + (Math.tan(y) * Math.tan(z))) + -1.0))) - Math.tan(a));
}
def code(x, y, z, a): return x + (((math.tan(y) + math.tan(z)) / (1.0 - ((1.0 + (math.tan(y) * math.tan(z))) + -1.0))) - math.tan(a))
function code(x, y, z, a) return Float64(x + Float64(Float64(Float64(tan(y) + tan(z)) / Float64(1.0 - Float64(Float64(1.0 + Float64(tan(y) * tan(z))) + -1.0))) - tan(a))) end
function tmp = code(x, y, z, a) tmp = x + (((tan(y) + tan(z)) / (1.0 - ((1.0 + (tan(y) * tan(z))) + -1.0))) - tan(a)); end
code[x_, y_, z_, a_] := N[(x + N[(N[(N[(N[Tan[y], $MachinePrecision] + N[Tan[z], $MachinePrecision]), $MachinePrecision] / N[(1.0 - N[(N[(1.0 + N[(N[Tan[y], $MachinePrecision] * N[Tan[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
x + \left(\frac{\tan y + \tan z}{1 - \left(\left(1 + \tan y \cdot \tan z\right) + -1\right)} - \tan a\right)
\end{array}
Initial program 76.5%
tan-sum99.7%
div-inv99.7%
Applied egg-rr99.7%
associate-*r/99.7%
*-rgt-identity99.7%
Simplified99.7%
expm1-log1p-u91.9%
expm1-udef91.9%
log1p-udef91.9%
add-exp-log99.7%
+-commutative99.7%
Applied egg-rr99.7%
Final simplification99.7%
(FPCore (x y z a) :precision binary64 (+ x (- (* (+ (tan y) (tan z)) (/ 1.0 (- 1.0 (* (tan y) (tan z))))) (tan a))))
double code(double x, double y, double z, double a) {
return x + (((tan(y) + tan(z)) * (1.0 / (1.0 - (tan(y) * tan(z))))) - tan(a));
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
code = x + (((tan(y) + tan(z)) * (1.0d0 / (1.0d0 - (tan(y) * tan(z))))) - tan(a))
end function
public static double code(double x, double y, double z, double a) {
return x + (((Math.tan(y) + Math.tan(z)) * (1.0 / (1.0 - (Math.tan(y) * Math.tan(z))))) - Math.tan(a));
}
def code(x, y, z, a): return x + (((math.tan(y) + math.tan(z)) * (1.0 / (1.0 - (math.tan(y) * math.tan(z))))) - math.tan(a))
function code(x, y, z, a) return Float64(x + Float64(Float64(Float64(tan(y) + tan(z)) * Float64(1.0 / Float64(1.0 - Float64(tan(y) * tan(z))))) - tan(a))) end
function tmp = code(x, y, z, a) tmp = x + (((tan(y) + tan(z)) * (1.0 / (1.0 - (tan(y) * tan(z))))) - tan(a)); end
code[x_, y_, z_, a_] := N[(x + N[(N[(N[(N[Tan[y], $MachinePrecision] + N[Tan[z], $MachinePrecision]), $MachinePrecision] * N[(1.0 / N[(1.0 - N[(N[Tan[y], $MachinePrecision] * N[Tan[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
x + \left(\left(\tan y + \tan z\right) \cdot \frac{1}{1 - \tan y \cdot \tan z} - \tan a\right)
\end{array}
Initial program 76.5%
tan-sum99.7%
div-inv99.7%
Applied egg-rr99.7%
Final simplification99.7%
(FPCore (x y z a) :precision binary64 (+ x (- (/ (+ (tan y) (tan z)) (- 1.0 (* (tan y) (tan z)))) (tan a))))
double code(double x, double y, double z, double a) {
return x + (((tan(y) + tan(z)) / (1.0 - (tan(y) * tan(z)))) - tan(a));
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
code = x + (((tan(y) + tan(z)) / (1.0d0 - (tan(y) * tan(z)))) - tan(a))
end function
public static double code(double x, double y, double z, double a) {
return x + (((Math.tan(y) + Math.tan(z)) / (1.0 - (Math.tan(y) * Math.tan(z)))) - Math.tan(a));
}
def code(x, y, z, a): return x + (((math.tan(y) + math.tan(z)) / (1.0 - (math.tan(y) * math.tan(z)))) - math.tan(a))
function code(x, y, z, a) return Float64(x + Float64(Float64(Float64(tan(y) + tan(z)) / Float64(1.0 - Float64(tan(y) * tan(z)))) - tan(a))) end
function tmp = code(x, y, z, a) tmp = x + (((tan(y) + tan(z)) / (1.0 - (tan(y) * tan(z)))) - tan(a)); end
code[x_, y_, z_, a_] := N[(x + N[(N[(N[(N[Tan[y], $MachinePrecision] + N[Tan[z], $MachinePrecision]), $MachinePrecision] / N[(1.0 - N[(N[Tan[y], $MachinePrecision] * N[Tan[z], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
x + \left(\frac{\tan y + \tan z}{1 - \tan y \cdot \tan z} - \tan a\right)
\end{array}
Initial program 76.5%
tan-sum99.7%
div-inv99.7%
Applied egg-rr99.7%
associate-*r/99.7%
*-rgt-identity99.7%
Simplified99.7%
Final simplification99.7%
(FPCore (x y z a) :precision binary64 (if (<= (+ y z) -2000000000000.0) (+ x (tan (+ y z))) (+ x (- (tan z) (tan a)))))
double code(double x, double y, double z, double a) {
double tmp;
if ((y + z) <= -2000000000000.0) {
tmp = x + tan((y + z));
} else {
tmp = x + (tan(z) - tan(a));
}
return tmp;
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
real(8) :: tmp
if ((y + z) <= (-2000000000000.0d0)) then
tmp = x + tan((y + z))
else
tmp = x + (tan(z) - tan(a))
end if
code = tmp
end function
public static double code(double x, double y, double z, double a) {
double tmp;
if ((y + z) <= -2000000000000.0) {
tmp = x + Math.tan((y + z));
} else {
tmp = x + (Math.tan(z) - Math.tan(a));
}
return tmp;
}
def code(x, y, z, a): tmp = 0 if (y + z) <= -2000000000000.0: tmp = x + math.tan((y + z)) else: tmp = x + (math.tan(z) - math.tan(a)) return tmp
function code(x, y, z, a) tmp = 0.0 if (Float64(y + z) <= -2000000000000.0) tmp = Float64(x + tan(Float64(y + z))); else tmp = Float64(x + Float64(tan(z) - tan(a))); end return tmp end
function tmp_2 = code(x, y, z, a) tmp = 0.0; if ((y + z) <= -2000000000000.0) tmp = x + tan((y + z)); else tmp = x + (tan(z) - tan(a)); end tmp_2 = tmp; end
code[x_, y_, z_, a_] := If[LessEqual[N[(y + z), $MachinePrecision], -2000000000000.0], N[(x + N[Tan[N[(y + z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(x + N[(N[Tan[z], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;y + z \leq -2000000000000:\\
\;\;\;\;x + \tan \left(y + z\right)\\
\mathbf{else}:\\
\;\;\;\;x + \left(\tan z - \tan a\right)\\
\end{array}
\end{array}
if (+.f64 y z) < -2e12Initial program 67.3%
add-cube-cbrt66.3%
pow366.3%
+-commutative66.3%
associate-+l-66.3%
Applied egg-rr66.3%
Taylor expanded in a around 0 42.7%
unpow1/346.8%
Simplified46.8%
rem-cube-cbrt47.4%
tan-quot47.5%
+-commutative47.5%
Applied egg-rr47.5%
if -2e12 < (+.f64 y z) Initial program 80.4%
Taylor expanded in y around 0 66.1%
tan-quot66.1%
expm1-log1p-u60.5%
expm1-udef60.5%
Applied egg-rr60.5%
expm1-def60.5%
expm1-log1p66.1%
Simplified66.1%
Final simplification60.5%
(FPCore (x y z a) :precision binary64 (if (<= y -3200000000.0) (+ x (/ (sin y) (cos y))) (+ x (- (tan z) (tan a)))))
double code(double x, double y, double z, double a) {
double tmp;
if (y <= -3200000000.0) {
tmp = x + (sin(y) / cos(y));
} else {
tmp = x + (tan(z) - tan(a));
}
return tmp;
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
real(8) :: tmp
if (y <= (-3200000000.0d0)) then
tmp = x + (sin(y) / cos(y))
else
tmp = x + (tan(z) - tan(a))
end if
code = tmp
end function
public static double code(double x, double y, double z, double a) {
double tmp;
if (y <= -3200000000.0) {
tmp = x + (Math.sin(y) / Math.cos(y));
} else {
tmp = x + (Math.tan(z) - Math.tan(a));
}
return tmp;
}
def code(x, y, z, a): tmp = 0 if y <= -3200000000.0: tmp = x + (math.sin(y) / math.cos(y)) else: tmp = x + (math.tan(z) - math.tan(a)) return tmp
function code(x, y, z, a) tmp = 0.0 if (y <= -3200000000.0) tmp = Float64(x + Float64(sin(y) / cos(y))); else tmp = Float64(x + Float64(tan(z) - tan(a))); end return tmp end
function tmp_2 = code(x, y, z, a) tmp = 0.0; if (y <= -3200000000.0) tmp = x + (sin(y) / cos(y)); else tmp = x + (tan(z) - tan(a)); end tmp_2 = tmp; end
code[x_, y_, z_, a_] := If[LessEqual[y, -3200000000.0], N[(x + N[(N[Sin[y], $MachinePrecision] / N[Cos[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x + N[(N[Tan[z], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;y \leq -3200000000:\\
\;\;\;\;x + \frac{\sin y}{\cos y}\\
\mathbf{else}:\\
\;\;\;\;x + \left(\tan z - \tan a\right)\\
\end{array}
\end{array}
if y < -3.2e9Initial program 51.7%
add-cube-cbrt50.9%
pow350.9%
+-commutative50.9%
associate-+l-50.9%
Applied egg-rr50.9%
Taylor expanded in a around 0 38.7%
unpow1/340.6%
Simplified40.6%
Taylor expanded in z around 0 40.8%
pow-base-140.8%
*-lft-identity40.8%
Simplified40.8%
if -3.2e9 < y Initial program 83.9%
Taylor expanded in y around 0 70.8%
tan-quot70.8%
expm1-log1p-u59.8%
expm1-udef59.8%
Applied egg-rr59.8%
expm1-def59.8%
expm1-log1p70.8%
Simplified70.8%
Final simplification63.9%
(FPCore (x y z a) :precision binary64 (+ x (- (tan (+ y z)) (tan a))))
double code(double x, double y, double z, double a) {
return x + (tan((y + z)) - tan(a));
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
code = x + (tan((y + z)) - tan(a))
end function
public static double code(double x, double y, double z, double a) {
return x + (Math.tan((y + z)) - Math.tan(a));
}
def code(x, y, z, a): return x + (math.tan((y + z)) - math.tan(a))
function code(x, y, z, a) return Float64(x + Float64(tan(Float64(y + z)) - tan(a))) end
function tmp = code(x, y, z, a) tmp = x + (tan((y + z)) - tan(a)); end
code[x_, y_, z_, a_] := N[(x + N[(N[Tan[N[(y + z), $MachinePrecision]], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
x + \left(\tan \left(y + z\right) - \tan a\right)
\end{array}
Initial program 76.5%
Final simplification76.5%
(FPCore (x y z a) :precision binary64 (if (or (<= (+ y z) -2000000000000.0) (not (<= (+ y z) 4e-48))) (+ x (tan (+ y z))) (+ x (- z (tan a)))))
double code(double x, double y, double z, double a) {
double tmp;
if (((y + z) <= -2000000000000.0) || !((y + z) <= 4e-48)) {
tmp = x + tan((y + z));
} else {
tmp = x + (z - tan(a));
}
return tmp;
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
real(8) :: tmp
if (((y + z) <= (-2000000000000.0d0)) .or. (.not. ((y + z) <= 4d-48))) then
tmp = x + tan((y + z))
else
tmp = x + (z - tan(a))
end if
code = tmp
end function
public static double code(double x, double y, double z, double a) {
double tmp;
if (((y + z) <= -2000000000000.0) || !((y + z) <= 4e-48)) {
tmp = x + Math.tan((y + z));
} else {
tmp = x + (z - Math.tan(a));
}
return tmp;
}
def code(x, y, z, a): tmp = 0 if ((y + z) <= -2000000000000.0) or not ((y + z) <= 4e-48): tmp = x + math.tan((y + z)) else: tmp = x + (z - math.tan(a)) return tmp
function code(x, y, z, a) tmp = 0.0 if ((Float64(y + z) <= -2000000000000.0) || !(Float64(y + z) <= 4e-48)) tmp = Float64(x + tan(Float64(y + z))); else tmp = Float64(x + Float64(z - tan(a))); end return tmp end
function tmp_2 = code(x, y, z, a) tmp = 0.0; if (((y + z) <= -2000000000000.0) || ~(((y + z) <= 4e-48))) tmp = x + tan((y + z)); else tmp = x + (z - tan(a)); end tmp_2 = tmp; end
code[x_, y_, z_, a_] := If[Or[LessEqual[N[(y + z), $MachinePrecision], -2000000000000.0], N[Not[LessEqual[N[(y + z), $MachinePrecision], 4e-48]], $MachinePrecision]], N[(x + N[Tan[N[(y + z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision], N[(x + N[(z - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;y + z \leq -2000000000000 \lor \neg \left(y + z \leq 4 \cdot 10^{-48}\right):\\
\;\;\;\;x + \tan \left(y + z\right)\\
\mathbf{else}:\\
\;\;\;\;x + \left(z - \tan a\right)\\
\end{array}
\end{array}
if (+.f64 y z) < -2e12 or 3.9999999999999999e-48 < (+.f64 y z) Initial program 68.5%
add-cube-cbrt67.5%
pow367.5%
+-commutative67.5%
associate-+l-67.5%
Applied egg-rr67.5%
Taylor expanded in a around 0 42.8%
unpow1/345.2%
Simplified45.2%
rem-cube-cbrt45.8%
tan-quot45.8%
+-commutative45.8%
Applied egg-rr45.8%
if -2e12 < (+.f64 y z) < 3.9999999999999999e-48Initial program 99.9%
Taylor expanded in y around 0 99.4%
Taylor expanded in z around 0 97.6%
Final simplification58.9%
(FPCore (x y z a) :precision binary64 (if (<= z -1.7) x (if (<= z 1.6) (+ x (- z (tan a))) (+ x (sin z)))))
double code(double x, double y, double z, double a) {
double tmp;
if (z <= -1.7) {
tmp = x;
} else if (z <= 1.6) {
tmp = x + (z - tan(a));
} else {
tmp = x + sin(z);
}
return tmp;
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
real(8) :: tmp
if (z <= (-1.7d0)) then
tmp = x
else if (z <= 1.6d0) then
tmp = x + (z - tan(a))
else
tmp = x + sin(z)
end if
code = tmp
end function
public static double code(double x, double y, double z, double a) {
double tmp;
if (z <= -1.7) {
tmp = x;
} else if (z <= 1.6) {
tmp = x + (z - Math.tan(a));
} else {
tmp = x + Math.sin(z);
}
return tmp;
}
def code(x, y, z, a): tmp = 0 if z <= -1.7: tmp = x elif z <= 1.6: tmp = x + (z - math.tan(a)) else: tmp = x + math.sin(z) return tmp
function code(x, y, z, a) tmp = 0.0 if (z <= -1.7) tmp = x; elseif (z <= 1.6) tmp = Float64(x + Float64(z - tan(a))); else tmp = Float64(x + sin(z)); end return tmp end
function tmp_2 = code(x, y, z, a) tmp = 0.0; if (z <= -1.7) tmp = x; elseif (z <= 1.6) tmp = x + (z - tan(a)); else tmp = x + sin(z); end tmp_2 = tmp; end
code[x_, y_, z_, a_] := If[LessEqual[z, -1.7], x, If[LessEqual[z, 1.6], N[(x + N[(z - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x + N[Sin[z], $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;z \leq -1.7:\\
\;\;\;\;x\\
\mathbf{elif}\;z \leq 1.6:\\
\;\;\;\;x + \left(z - \tan a\right)\\
\mathbf{else}:\\
\;\;\;\;x + \sin z\\
\end{array}
\end{array}
if z < -1.69999999999999996Initial program 51.4%
Taylor expanded in x around inf 22.1%
if -1.69999999999999996 < z < 1.6000000000000001Initial program 99.3%
Taylor expanded in y around 0 65.7%
Taylor expanded in z around 0 65.1%
if 1.6000000000000001 < z Initial program 54.3%
Taylor expanded in y around 0 55.0%
Taylor expanded in z around 0 24.0%
Taylor expanded in a around 0 23.2%
+-commutative23.2%
Simplified23.2%
Final simplification44.2%
(FPCore (x y z a) :precision binary64 (+ x (sin z)))
double code(double x, double y, double z, double a) {
return x + sin(z);
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
code = x + sin(z)
end function
public static double code(double x, double y, double z, double a) {
return x + Math.sin(z);
}
def code(x, y, z, a): return x + math.sin(z)
function code(x, y, z, a) return Float64(x + sin(z)) end
function tmp = code(x, y, z, a) tmp = x + sin(z); end
code[x_, y_, z_, a_] := N[(x + N[Sin[z], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
x + \sin z
\end{array}
Initial program 76.5%
Taylor expanded in y around 0 59.8%
Taylor expanded in z around 0 44.8%
Taylor expanded in a around 0 34.7%
+-commutative34.7%
Simplified34.7%
Final simplification34.7%
(FPCore (x y z a) :precision binary64 x)
double code(double x, double y, double z, double a) {
return x;
}
real(8) function code(x, y, z, a)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: a
code = x
end function
public static double code(double x, double y, double z, double a) {
return x;
}
def code(x, y, z, a): return x
function code(x, y, z, a) return x end
function tmp = code(x, y, z, a) tmp = x; end
code[x_, y_, z_, a_] := x
\begin{array}{l}
\\
x
\end{array}
Initial program 76.5%
Taylor expanded in x around inf 34.5%
Final simplification34.5%
herbie shell --seed 2024027
(FPCore (x y z a)
:name "tan-example (used to crash)"
:precision binary64
:pre (and (and (and (or (== x 0.0) (and (<= 0.5884142 x) (<= x 505.5909))) (or (and (<= -1.796658e+308 y) (<= y -9.425585e-310)) (and (<= 1.284938e-309 y) (<= y 1.751224e+308)))) (or (and (<= -1.776707e+308 z) (<= z -8.599796e-310)) (and (<= 3.293145e-311 z) (<= z 1.725154e+308)))) (or (and (<= -1.796658e+308 a) (<= a -9.425585e-310)) (and (<= 1.284938e-309 a) (<= a 1.751224e+308))))
(+ x (- (tan (+ y z)) (tan a))))