Make skolem definition manager robust to definitions for already asserted skolems...

Make skolem definition manager robust to definitions for already asserted skolems (#8749)

It makes the skolem definition manager more robust so that skolem definitions can be added for skolems that have already appeared in asserted literals. This was the initial motivation for the change in ordering. As a result, fixes #8347 and fixes cvc5/cvc5-projects#512. It also optimizes this class in a few ways.

It also comments more on the change to PropEngine introduced here: #8301 which led to performance degradation on a set of string benchmarks of interest.