(proof-new) Minor updates to strings base solver (#4606)

(proof-new) Minor updates to strings base solver (#4606)

In preparation for proofs, this PR involves flattening AND and removing spurious true literals in conjunctions.

This also updates our policy for applying cardinality, where in some rare cases we were applying cardinality for pairs of string terms for length 0 (e.g. "there is at most 1 eqc of length 0"), which is spurious due to our term registry which always splits on emptiness.