Escape non-ASCII characters in SMT-LIB string literals

[agusaldasoro]

Stacked on #1838.

Problem

Z3 reads an SMT-LIB string literal byte by byte, and it always prints characters outside printable ASCII as \u{X} escapes. A literal written as raw UTF-8 therefore changes on the round trip. 'ORDINÆR' was sent as 8 bytes, and the model returned "ORDIN\u{c3}\u{86}R", one escape per UTF-8 byte. SMTResultParser used that text as the value.

So a row generated to satisfy CHECK (kategori IN ('ORDINÆR', 'EØS')) broke that same CHECK, and the database rejected its INSERT. The same happened to a row for WHERE kategori = 'EØS'. Enumerations with such values are common in non-English schemas: in familie-ba-sak (EMB), 29 of the 48 CHECK constraints have one.

A backslash had a related problem. Z3 reads \u{...} inside a literal as an escape, so a value containing that text was changed too.

Fix

• SMTConditionVisitor.stringLiteral writes every code point outside printable ASCII, and the backslash, as \u{X}. Z3 then reads the literal as the same sequence of characters the query has.
• SMTResultParser.unescapeString decodes \u{X} back into the character, after turning "" into " as before (Escape quotes in SMT-LIB string literals #1838).

Tests

• StringLiteralTranslationTest: NAME = 'ORDINÆR \ 😀' is written as "ORDIN\u{c6}R \u{5c} \u{1f600}".

• SMTResultParserTest.testParseComposedTypeWithUnicodeEscapes: escapes are decoded, including a code point outside the BMP and an escaped backslash.

• New NonAsciiLiteralSolvingTest (H2, Z3 Docker): for a table with that CHECK, the solved row is inserted and satisfies the query. It covers a query that only fixes the id and one that fixes the value. On Escape quotes in SMT-LIB string literals #1838 both cases fail.

  H2 2.x reports the constraint with unicode-escaped literals (IN(U&'ORDIN\00c6R', ...)), which the CHECK parser does not read. PostgreSQL and H2 1.4 report the characters as they are, so the test gives the constraint in that form. H2 still enforces the real constraint on insertion.

All tests in core-extra/solver and under org.evomaster.core.database.sql.solver pass.