Added support for model values to the Theory.

The theory now internally declares function symbols of the form
(as @1234 Sort). It is as if there is a polymorphic function symbol @x
with zero arguments and arbitrary type is declared for every decimal
number x.  The function symbols are created when needed and put into
a unify hash.