Enumerate shapes feature in fast sygus enumerator (#4742)

Enumerate shapes feature in fast sygus enumerator  (#4742)

This adds the feature of enumerating shapes in the fast sygus enumerator, which is required for a new algorithm for sygus solution reconstruction.

This also adds a builtinToSygus backwards mapping that is required for that algorithm as well.

Note this also changes the implementation of mkFreeVar in sygus term database from skolem to bound variable, which is required to do proper caching for expr::hasBoundVar.