Implement allSat for uninterpreted sorts

The idea is to use equivalence classes as identified by the backhand
solver to reject satisfying models. It was Eric Seidel who suggested
the idea, see #80. Thanks!