Keep unconstrained string models compact

[lemmy]

When a string's length is known but its contents are unconstrained, string_refinementt::get expands the backing array into one '?' per character. Large nondeterministic strings therefore produce enormous counterexample traces.

Use array_of_exprt to represent the repeated placeholder while retaining the full length in the array type. This follows expr_initializer.cpp's existing use of array_of_exprt to avoid expanding large uniform arrays. Extend string-operation evaluation and Java trace validation to handle this compact representation.

Add unit and regression coverage, including the reported reproducer with a string length of 4,194,304.

Fixes #9165

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/ (nothing to document)
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[remi-delmas-3000]

Is the semantics correct ? There’s a difference between a string that contains a different nondet character at each position and one that contains the same single nondet character at each position. An alternative would be to elide the contents using ellipsis in the rendering of that term.