
(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 9 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 (* (sin y) (/ (tan z) (cos y))))) (tan a))))
double code(double x, double y, double z, double a) {
return x + (((tan(y) + tan(z)) / (1.0 - (sin(y) * (tan(z) / cos(y))))) - 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 - (sin(y) * (tan(z) / cos(y))))) - 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.sin(y) * (Math.tan(z) / Math.cos(y))))) - Math.tan(a));
}
def code(x, y, z, a): return x + (((math.tan(y) + math.tan(z)) / (1.0 - (math.sin(y) * (math.tan(z) / math.cos(y))))) - math.tan(a))
function code(x, y, z, a) return Float64(x + Float64(Float64(Float64(tan(y) + tan(z)) / Float64(1.0 - Float64(sin(y) * Float64(tan(z) / cos(y))))) - tan(a))) end
function tmp = code(x, y, z, a) tmp = x + (((tan(y) + tan(z)) / (1.0 - (sin(y) * (tan(z) / cos(y))))) - 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[Sin[y], $MachinePrecision] * N[(N[Tan[z], $MachinePrecision] / N[Cos[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
x + \left(\frac{\tan y + \tan z}{1 - \sin y \cdot \frac{\tan z}{\cos y}} - \tan a\right)
\end{array}
Initial program 79.6%
tan-sum99.8%
div-inv99.8%
Applied egg-rr99.8%
associate-*r/99.8%
*-rgt-identity99.8%
Simplified99.8%
*-commutative99.8%
tan-quot99.8%
associate-*r/99.8%
Applied egg-rr99.8%
*-commutative99.8%
associate-/l*99.8%
Simplified99.8%
(FPCore (x y z a) :precision binary64 (if (or (<= (tan a) -2e-13) (not (<= (tan a) 5e-41))) (+ x (- (tan (+ y z)) (tan a))) (+ x (/ (+ (tan y) (tan z)) (- 1.0 (* (tan y) (tan z)))))))
double code(double x, double y, double z, double a) {
double tmp;
if ((tan(a) <= -2e-13) || !(tan(a) <= 5e-41)) {
tmp = x + (tan((y + z)) - tan(a));
} else {
tmp = x + ((tan(y) + tan(z)) / (1.0 - (tan(y) * tan(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 ((tan(a) <= (-2d-13)) .or. (.not. (tan(a) <= 5d-41))) then
tmp = x + (tan((y + z)) - tan(a))
else
tmp = x + ((tan(y) + tan(z)) / (1.0d0 - (tan(y) * tan(z))))
end if
code = tmp
end function
public static double code(double x, double y, double z, double a) {
double tmp;
if ((Math.tan(a) <= -2e-13) || !(Math.tan(a) <= 5e-41)) {
tmp = x + (Math.tan((y + z)) - Math.tan(a));
} else {
tmp = x + ((Math.tan(y) + Math.tan(z)) / (1.0 - (Math.tan(y) * Math.tan(z))));
}
return tmp;
}
def code(x, y, z, a): tmp = 0 if (math.tan(a) <= -2e-13) or not (math.tan(a) <= 5e-41): tmp = x + (math.tan((y + z)) - math.tan(a)) else: tmp = x + ((math.tan(y) + math.tan(z)) / (1.0 - (math.tan(y) * math.tan(z)))) return tmp
function code(x, y, z, a) tmp = 0.0 if ((tan(a) <= -2e-13) || !(tan(a) <= 5e-41)) tmp = Float64(x + Float64(tan(Float64(y + z)) - tan(a))); else tmp = Float64(x + Float64(Float64(tan(y) + tan(z)) / Float64(1.0 - Float64(tan(y) * tan(z))))); end return tmp end
function tmp_2 = code(x, y, z, a) tmp = 0.0; if ((tan(a) <= -2e-13) || ~((tan(a) <= 5e-41))) tmp = x + (tan((y + z)) - tan(a)); else tmp = x + ((tan(y) + tan(z)) / (1.0 - (tan(y) * tan(z)))); end tmp_2 = tmp; end
code[x_, y_, z_, a_] := If[Or[LessEqual[N[Tan[a], $MachinePrecision], -2e-13], N[Not[LessEqual[N[Tan[a], $MachinePrecision], 5e-41]], $MachinePrecision]], N[(x + N[(N[Tan[N[(y + z), $MachinePrecision]], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x + 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]), $MachinePrecision]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;\tan a \leq -2 \cdot 10^{-13} \lor \neg \left(\tan a \leq 5 \cdot 10^{-41}\right):\\
\;\;\;\;x + \left(\tan \left(y + z\right) - \tan a\right)\\
\mathbf{else}:\\
\;\;\;\;x + \frac{\tan y + \tan z}{1 - \tan y \cdot \tan z}\\
\end{array}
\end{array}
if (tan.f64 a) < -2.0000000000000001e-13 or 4.9999999999999996e-41 < (tan.f64 a) Initial program 82.4%
if -2.0000000000000001e-13 < (tan.f64 a) < 4.9999999999999996e-41Initial program 77.0%
add-sqr-sqrt47.3%
sqrt-unprod65.3%
pow265.3%
Applied egg-rr65.3%
Taylor expanded in a around 0 65.3%
sqrt-div65.3%
sqrt-pow165.7%
metadata-eval65.7%
pow165.7%
sqrt-pow177.0%
metadata-eval77.0%
pow177.0%
tan-quot77.0%
tan-sum99.8%
+-commutative99.8%
Applied egg-rr99.8%
*-commutative99.8%
Simplified99.8%
Final simplification91.4%
(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 79.6%
tan-sum99.8%
div-inv99.8%
Applied egg-rr99.8%
associate-*r/99.8%
*-rgt-identity99.8%
Simplified99.8%
(FPCore (x y z a) :precision binary64 (if (<= (+ y z) -5e-14) (+ x (- (tan y) (tan a))) (+ x (- (tan z) (tan a)))))
double code(double x, double y, double z, double a) {
double tmp;
if ((y + z) <= -5e-14) {
tmp = x + (tan(y) - tan(a));
} 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) <= (-5d-14)) then
tmp = x + (tan(y) - tan(a))
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) <= -5e-14) {
tmp = x + (Math.tan(y) - Math.tan(a));
} else {
tmp = x + (Math.tan(z) - Math.tan(a));
}
return tmp;
}
def code(x, y, z, a): tmp = 0 if (y + z) <= -5e-14: tmp = x + (math.tan(y) - math.tan(a)) else: tmp = x + (math.tan(z) - math.tan(a)) return tmp
function code(x, y, z, a) tmp = 0.0 if (Float64(y + z) <= -5e-14) tmp = Float64(x + Float64(tan(y) - tan(a))); 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) <= -5e-14) tmp = x + (tan(y) - tan(a)); else tmp = x + (tan(z) - tan(a)); end tmp_2 = tmp; end
code[x_, y_, z_, a_] := If[LessEqual[N[(y + z), $MachinePrecision], -5e-14], N[(x + N[(N[Tan[y], $MachinePrecision] - N[Tan[a], $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 -5 \cdot 10^{-14}:\\
\;\;\;\;x + \left(\tan y - \tan a\right)\\
\mathbf{else}:\\
\;\;\;\;x + \left(\tan z - \tan a\right)\\
\end{array}
\end{array}
if (+.f64 y z) < -5.0000000000000002e-14Initial program 72.7%
Taylor expanded in z around 0 45.7%
tan-quot45.7%
tan-quot45.7%
associate--l+45.7%
Applied egg-rr45.7%
if -5.0000000000000002e-14 < (+.f64 y z) Initial program 83.7%
Taylor expanded in y around 0 70.2%
+-commutative70.2%
tan-quot70.2%
*-un-lft-identity70.2%
fma-define70.2%
Applied egg-rr70.2%
fma-undefine70.2%
*-lft-identity70.2%
Simplified70.2%
Final simplification61.0%
(FPCore (x y z a) :precision binary64 (if (<= (+ y z) 1e-19) (+ x (- (tan y) (tan a))) (+ x (tan (+ y z)))))
double code(double x, double y, double z, double a) {
double tmp;
if ((y + z) <= 1e-19) {
tmp = x + (tan(y) - tan(a));
} else {
tmp = x + tan((y + 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 ((y + z) <= 1d-19) then
tmp = x + (tan(y) - tan(a))
else
tmp = x + tan((y + z))
end if
code = tmp
end function
public static double code(double x, double y, double z, double a) {
double tmp;
if ((y + z) <= 1e-19) {
tmp = x + (Math.tan(y) - Math.tan(a));
} else {
tmp = x + Math.tan((y + z));
}
return tmp;
}
def code(x, y, z, a): tmp = 0 if (y + z) <= 1e-19: tmp = x + (math.tan(y) - math.tan(a)) else: tmp = x + math.tan((y + z)) return tmp
function code(x, y, z, a) tmp = 0.0 if (Float64(y + z) <= 1e-19) tmp = Float64(x + Float64(tan(y) - tan(a))); else tmp = Float64(x + tan(Float64(y + z))); end return tmp end
function tmp_2 = code(x, y, z, a) tmp = 0.0; if ((y + z) <= 1e-19) tmp = x + (tan(y) - tan(a)); else tmp = x + tan((y + z)); end tmp_2 = tmp; end
code[x_, y_, z_, a_] := If[LessEqual[N[(y + z), $MachinePrecision], 1e-19], N[(x + N[(N[Tan[y], $MachinePrecision] - N[Tan[a], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(x + N[Tan[N[(y + z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;y + z \leq 10^{-19}:\\
\;\;\;\;x + \left(\tan y - \tan a\right)\\
\mathbf{else}:\\
\;\;\;\;x + \tan \left(y + z\right)\\
\end{array}
\end{array}
if (+.f64 y z) < 9.9999999999999998e-20Initial program 84.3%
Taylor expanded in z around 0 68.7%
tan-quot68.7%
tan-quot68.7%
associate--l+68.8%
Applied egg-rr68.8%
if 9.9999999999999998e-20 < (+.f64 y z) Initial program 70.8%
add-sqr-sqrt45.4%
sqrt-unprod52.6%
pow252.6%
Applied egg-rr52.6%
Taylor expanded in a around 0 45.2%
sqrt-div45.2%
sqrt-pow140.8%
metadata-eval40.8%
pow140.8%
sqrt-pow153.0%
metadata-eval53.0%
pow153.0%
tan-quot53.1%
*-un-lft-identity53.1%
Applied egg-rr53.1%
*-lft-identity53.1%
Simplified53.1%
(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 79.6%
(FPCore (x y z a) :precision binary64 (if (or (<= (+ y z) -0.2) (not (<= (+ y z) 0.002))) (+ x (tan (+ y z))) (+ x (- z (tan a)))))
double code(double x, double y, double z, double a) {
double tmp;
if (((y + z) <= -0.2) || !((y + z) <= 0.002)) {
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) <= (-0.2d0)) .or. (.not. ((y + z) <= 0.002d0))) 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) <= -0.2) || !((y + z) <= 0.002)) {
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) <= -0.2) or not ((y + z) <= 0.002): 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) <= -0.2) || !(Float64(y + z) <= 0.002)) 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) <= -0.2) || ~(((y + z) <= 0.002))) 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], -0.2], N[Not[LessEqual[N[(y + z), $MachinePrecision], 0.002]], $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 -0.2 \lor \neg \left(y + z \leq 0.002\right):\\
\;\;\;\;x + \tan \left(y + z\right)\\
\mathbf{else}:\\
\;\;\;\;x + \left(z - \tan a\right)\\
\end{array}
\end{array}
if (+.f64 y z) < -0.20000000000000001 or 2e-3 < (+.f64 y z) Initial program 70.5%
add-sqr-sqrt39.8%
sqrt-unprod48.5%
pow248.5%
Applied egg-rr48.5%
Taylor expanded in a around 0 37.5%
sqrt-div37.5%
sqrt-pow137.0%
metadata-eval37.0%
pow137.0%
sqrt-pow146.8%
metadata-eval46.8%
pow146.8%
tan-quot46.8%
*-un-lft-identity46.8%
Applied egg-rr46.8%
*-lft-identity46.8%
Simplified46.8%
if -0.20000000000000001 < (+.f64 y z) < 2e-3Initial program 99.9%
Taylor expanded in y around 0 98.3%
Taylor expanded in z around 0 98.1%
Final simplification62.6%
(FPCore (x y z a) :precision binary64 (+ x (tan (+ y z))))
double code(double x, double y, double z, double a) {
return x + tan((y + 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 + tan((y + z))
end function
public static double code(double x, double y, double z, double a) {
return x + Math.tan((y + z));
}
def code(x, y, z, a): return x + math.tan((y + z))
function code(x, y, z, a) return Float64(x + tan(Float64(y + z))) end
function tmp = code(x, y, z, a) tmp = x + tan((y + z)); end
code[x_, y_, z_, a_] := N[(x + N[Tan[N[(y + z), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
x + \tan \left(y + z\right)
\end{array}
Initial program 79.6%
add-sqr-sqrt45.8%
sqrt-unprod59.9%
pow259.9%
Applied egg-rr59.9%
Taylor expanded in a around 0 45.6%
sqrt-div45.6%
sqrt-pow145.3%
metadata-eval45.3%
pow145.3%
sqrt-pow152.1%
metadata-eval52.1%
pow152.1%
tan-quot52.1%
*-un-lft-identity52.1%
Applied egg-rr52.1%
*-lft-identity52.1%
Simplified52.1%
(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 79.6%
Taylor expanded in x around inf 35.3%
herbie shell --seed 2024091
(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))))