Telling an SMT solver to tell them apart

Thanks to Jacob Burnim for this post.

---

A few days back, I was trying to write a sudoku solver using an SMT solver. The idea is to express the constraints of a sudoku board in a language that an SMT solver can understand. The solver either gives a model from which the solution can be extracted or it declares the constraints to be unsatisfiable in which case no solution exists.
The SMT solver I was using was Yices. I first used the following assertion to tell Yices to make all the values in a column distinct:

(define-type single_dig (subrange 0 9))
(define board::(-> single_dig single_dig single_dig))

(assert
(forall (n1::single_dig n2::single_dig m::single_dig)
(or (= n1 n2) (/= (board n1 m) (board n2 m)))
))

Neat and compact! But wait... when you give it to Yices, it cowardly backs off, returning unknown! OK, fine, too many quantifiers... lets ask it to do it for each row separately. But no... still no luck! Notice that the subrange we are working on is finite, but somehow Yices fails to understand that. After trying many different expressions with quantifiers, I gave up (Yices is really bad with quantifiers).
And then came Jacob with a smart trick. Just define a function that maps the board values to different integers:

(define f::(-> single_dig single_dig))
(assert (and
(= (f (board 1 1)) 1)
(= (f (board 2 1)) 2)
(= (f (board 3 1)) 3)
(= (f (board 4 1)) 4)
(= (f (board 5 1)) 5)
(= (f (board 6 1)) 6)
(= (f (board 7 1)) 7)
(= (f (board 8 1)) 8)
(= (f (board 9 1)) 9)))

And voila! It automatically makes all board values distinct. Yices does not complain any more. Of course this is not too compact and the model returned by the solver becomes a bit clumsy, but it works! Looks like this is a standard trick to make a finite number of values distinct.