(proof-new) Updates to strings skolem cache. (#4524)

(proof-new) Updates to strings skolem cache. (#4524)

This PR makes strings skolem cache call the ProofSkolemCache. This is required for proper proof checking, as it makes all skolems be associated with their formal definition, encapsulated by a witness term.

It furthermore makes skolem sharing more uniform and aggressive by noting that most string skolems correspond to purification variables (typically for some substr term). A purification variable for a term that rewrites to a constant can be replaced by the constant itself.

It also introduces an attribute IndexVarAttribute which is used to ensure reductions involving universal variables are deterministic.