Avoid redundancy in solver interface

SMT sorts can be inferred from the expression pointer and we
therefore remove sorts from the solver interface.