Towards support for incremental sygus (#7736)

Towards support for incremental sygus (#7736)

This makes several key changes to smt::SygusSolver in preparation for incremental mode.

The key idea is to use a subsolver that:

may take multiple check-sat commands for an encoded synthesis conjecture
does not push/pop
is reconstructed when the SyGuS conjecture becomes stale.
This is motivated by 2 use cases of incremental SyGuS:

Where constraints are push/pop, in which case we should start from scratch, since the SyGuS solver uses symmetry breaking techniques that become unsound when new constraints are added.
Where multiple solutions are needed for the same set of constraints, in which the state of the subsolver should be preserved.
This functionality is still guarded by an exception.

A follow up PR will make several further changes to allow for the above use cases.