Add type-hints to pysmt code

Python has added support for type-hints in version 3.5; which has now reached end-of-life.

In my opinion, type-hints make it easier to read the code and also enable a number of static checks.
What do you think?

If we want to go fancy, there are a number of different formats / libraries that support the definition of contracts (mostly pre-post conditions and invariants e.g. PEP 316, deal).