Make SyGuS solver robust to non-closed enumerable sorts (#7417)

Make SyGuS solver robust to non-closed enumerable sorts (#7417)

This makes the SyGuS solver robust to variables that are not closed enumerable, e.g. arrays of uninterpreted sorts.

It corrects an issue in array's mkGroundTerm issue which would allow constants to enter into constraints for SyGuS problems with arrays. This method does not cause further issues currently since quantifiers is guarded in several places to ensure array constants are not constructed via this method.

It also makes it so that we don't add explicit CEGIS refinement lemmas unless evaluation unfolding is enabled and the counterexamples are from closed enumerable types; there is no reason to add these unless we are combining with evaluation unfolding.

This addresses several of the issues raised in #6605.