[KRRT7]

Problem

When a symbolic string method that needs Unicode data (upper, lower, casefold, title, isalpha, isspace, strip, unicodedata.digit, ...) is first used on a path, UnicodeMaskCache adds that table to the solver as a global constraint. Masks are added as a quantified axiom (ForAll c. is_<name>(c) == <ranges>), and case and numeric maps as one big conjunction of ground equations (toupper_1st(k) == v for each of ~1,550 code points).

make_default_solver builds the solver from the smt tactic, which is not incremental: every check() processes every assertion from scratch. So once a table is loaded, every later check on that path pays for it, including checks that have nothing to do with strings:

loaded into the solver	trivial linear check
nothing	0.14 ms
toupper_exists + space masks	9.44 ms
toupper_1st map	9.59 ms
toupper_exists + toupper_1st + space	28.12 ms

The slowest single queries were inverse lookups such as 97 == toupper_1st(s) (from partition/replace after .upper()), at hundreds of milliseconds each. The table above and the benchmarks below are on z3 5.3.1.

Change

• Mask predicates now expand inline at each use with CharMask.smt_matches, which builds a disjunction of ranges. Nothing is asserted globally. relib already used masks this way.
• Integer maps (case maps, decimal/digit values, numeric numerator and denominator) become IntTransforms. Sorted keys are grouped into segments where every key maps to key + offset or to a constant. Keys outside the map never reach a transform, because every call is guarded by a mask fork, so segments can span gaps between keys. toupper_1st goes from 1,552 entries to 187 segments. Each use builds a balanced If tree over segment starts (about 8 deep).
• The offset is added outside the tree (c + If(..., k1, k2)), not at each leaf (If(..., c + k1, c + k2)). With offsets at the leaves, z3's auto-config can classify a query as difference logic, and the difference-logic solver then gives up (unknown, "incomplete (theory difference-logic)") on atoms like c - (c + 205) <= 0. A 10-If reduction reproduces this, and test_int_transform_offsets_are_decidable covers it.
• The encodings no longer depend on a solver, so UnicodeMaskCache and space.extra(UnicodeMaskCache) are replaced by module-level functions (smt_is_alpha, smt_upper_1st, smt_upper_has_2nd, ...). Each builds its table lazily once and is applied directly: smt_is_alpha(smt_codepoint) instead of space.extra(UnicodeMaskCache).alpha()(smt_codepoint).
• Removed duplicate masks: decimal_exists, digit_exists and numeric_exists were the same sets as decimal, digit and numeric (isdecimal() matches unicodedata.decimal(ch, None) is not None on every code point, and likewise for digit and numeric).
• Removed CharMask.interpret_smt_function and _INTERPRETATION_CACHE.

Results

All numbers are on z3 5.3.1 (the dev pin) and Python 3.14, with PYTHONHASHSEED=0. End to end, 40 iterations, two runs each:

function	main	this PR
(s.upper() + t.strip()).replace("a", "bb")	6.48–6.75 s	1.94–1.96 s
s.lower() == s.casefold() or s.isalpha() or s.title().isupper()	58.2–62.3 s	12.2–12.4 s
s.title().isupper()	185.6 s (one run)	18.7–20.2 s
int(s) if s.isdigit() and len(s) < 4 else len(s.split())	0.22–1.33 s	1.07–1.08 s
sorted(x % 7 for x in xs) (no strings)	0.17 s	0.16–0.19 s

Every solver check in these runs returned sat or unsat. There were no unknowns on either branch.

In isolation, a trivial check after loading the upper tables drops from 28 ms back to 0.14 ms, since nothing is loaded globally any more. The inverse lookup upper(c) == 97 (given that c changes under upper) drops from 474 ms to 37 ms.

Every transform was checked against its source table on every key (z3.simplify(smt_fn(k)) == table[k]), and every mask at each range boundary plus 300 random code points.

Testing

• unicode_categories_test, unicodedatalib_test, builtinslib_test, builtinslib_ch_test, relib_test, relib_ch_test, encodings_ch_test: 820 passed, 1 failed. The failure, check_divmod, also fails on main in this environment (z3 5.3.1, Python 3.14), taking 316 s alone. On this branch it passes alone in 3 s.
• New tests: every Unicode-backed str method and unicodedata.decimal/digit/numeric leave a symbolic input symbolic (catches a method silently falling back to a realizing implementation), IntTransform segmenting and lookup, exact match against every case map, and the difference-logic regression. That test fails when offsets are moved back to the leaves.
• Full suite (-n auto, macOS, z3 5.3.1, Python 3.14): 15,011 passed, 25 xfailed, 816 skipped, 12 failed. Eleven failures were caused by my local environment and are unrelated to this change: ten fuzz_core_test turtle.* ops, and test_uncategorized_ops_probe_cleanly, which runs the same ops (it passes on main in isolation). The last is the check_divmod failure on main described above.
• pre-commit run --all-files passes (black, isort, flake8, mypy, doctest, smoke tests).

Open questions

• Masks are now expanded at each use instead of being shared through one function symbol. alpha has several hundred ranges, so a query over many symbolic characters builds larger expressions. The benchmarks above don't show a cost, but a long string run through isalpha() would be the case to watch.
• An incremental solver would remove the per-check cost of any global assertion, not just these tables. That is a larger change with determinism implications, so it isn't attempted here.

[pschanely]

@KRRT7 Amazing!