allow uninterpreted sorts in `allSat`.

We separate the uninterpreted sorts out from the rest of the model since
the symbolic constants that come back from the SMT solver won't be
recognized in the next run. We then partition the values into
equivalence classes and assert their negation. This prevents the SMT
solver from constructing a symmetric model, without having to refer to
specific elements of the uninterpreted sort.