Term counting: Cap size using abstract

[tnelson]

If a sort is abstract, and it contains only all-neq constants, the sort cannot contain more than #constants atoms. (This idea can probably be extended more broadly and more precisely.)