Value classes instead of Longs in Z3 API

[Saloed]

Currently, we use long to represent all Z3 native objects: sorts, expressions, declarations. Also, all Z3.Native methods accept raw longs without any clarification whether it is sort, expr, or whatever else.

The idea is to provide wrappers for Z3.native methods with different value classes for different object kinds.