[FEATURE] Add support for different uninterpreted types in Rewriter

[konnov]

The type checker allows us to use uninterpreted types such as Set(RM) or Data -> Data. The model checker currently supports only strings as the only uninterpreted type. We have to add the support for different uninterpreted types in the model checker, which would translate to different uninterpreted sorts in SMT.