Improve the solver support by the type inference engine

[rodrigogribeiro]

Currently, the type inference algorithm just parses the output of Z3 SMT solver to build the model. While this solution is working for Z3 4.8.14, we cannot guarantee that it will work in future versions of Z3. Ideally, we should be able to use the Z3 library through FFI. The racket package list does have a package that offers a Z3 API by FFI, but it seem not to support retrieving the model found by the solver.