Separate SMT declarations from expressions

This strengthens the type safety of the API. For now we keep sort::Func
even though SMT is only about first-order logic. The reason is that it
nicely annotate the C++11 template meta-programming code and it leaves
the door open for possible future extensions with higher-order logic.