Check more preconditions for encode functions

Declare Solver in the source file instead of the header so that we
can check Sort equality of built-in binary operator arguments.