Allow SyGuS subsolver to be reused in incremental mode (#7785)

Allow SyGuS subsolver to be reused in incremental mode (#7785)

This allows SyGuS subsolvers to be called multiple times to produce solutions for a given set of SyGuS constraints using a new command check-synth-next.

By default, the SyGuS subsolver will generate a new solution for each successive check-synth.

This simplifies the internal SyGuS solver in several ways for this purpose. It also ensures that solutions are cached; current master may recompute solutions in the same state more than once if asked, which is no longer the case.

This completes our support for incremental SyGuS.