Add new eager conflict detection in strings for integer equivalence classes (#7453)

Add new eager conflict detection in strings for integer equivalence classes (#7453)

Required to address Zelkova bottlenecks.

This generalizes the methods for eager prefix/suffix conflicts for strings to do eager lower/upper bound conflicts for integer equivalence classes based on string-specific reasoning about length terms. This avoids cases where Simplex fails to show a concise conflict due to not having access to string reasoning (e.g. strings::ArithEntail) for arithmetic bounds.

The approach can still be improved by inferring fixed length for regular expression memberships, analogous to what is done for prefix/suffix conflicts.

It also changes EqcInfo to store (str.len x) instead of x for length terms.