pub(super) fn utf8_validity<'ctx>(
ctx: &'ctx Context,
bytes: &[Int<'ctx>],
) -> Bool<'ctx>Expand description
Build the boolean expression “bytes form a valid UTF-8 sequence”.
Encodes the UTF-8 DFA over the per-byte Z3 terms: every byte is ASCII, a
continuation byte, or a valid lead byte, and a k-byte lead must be
followed by exactly k-1 continuation bytes. Value-range refinements
reject overlong encodings, surrogates (U+D800..=U+DFFF), and code points
above U+10FFFF.