Add option to limit the number of instantiation rounds (#6818)

Add option to limit the number of instantiation rounds (#6818)

This adds an option to limit the number of instantiation rounds used by quantifiers engine.

This option may be generally useful for making quantifiers terminating. It also is necessary to update the new default behavior of SyGuS + recursive functions. A followup PR will make sygus verification calls set the option added on this PR automatically, so that we use incomplete + termination strategies for (non-PBE) sygus in the presence of recursive functions.

This PR also makes minor improvements to the quantifier utility infrastructure.