我们经常需要快速对字符进行分类。例如，考虑如何将通过电子邮件发送的二进制数据转换为由 64 个不同字符（AZ、az、0-9、+、/）组成的 ASCII 字符串。ASCII 字符存储为 7 位整数值（从 0 到 128），每个字符使用一个字节。在解码 base64 字符串期间，您可能需要识别哪些字符是 base64 字符。如果您正在逐个字符地处理来自 ASCII 或 UTF-8 流的数据，一个简单的 256 元素查找表就足够了。例如，您创建一个填充有假值的表，但与设计字符（AZ、az、0-9、+、/）的 7 位代码点值相对应的索引除外。
但是，如果您使用更高级的技术（例如单指令、多数据 (SIMD) 指令），尝试以 16 个字符或更多字符的块来处理数据，则标准查找表将失败。
我将使用 SIMD 指令对字符进行分类的过程称为矢量化分类。在矢量化分类的常见版本中，每个字符的 ASCII 值被拆分为两个 4 位半字节（低位和高位），并使用 16 字节查找表（ lut_lo和lut_hi ）通过按位与运算对字符进行分类： f(c) = lut_lo[c & 0x0F] AND lut_hi[c >> 4] 。对于 base64 解码，您可能希望f(c) = 0表示有效的 base64 字符，而f(c) > 0表示无效字符，从而允许在单个指令周期内跨字符向量进行快速验证。
如何计算出数组lut_lo和lut_hi表的内容？在“每秒解析 GB 级 JSON”（Langdale 和 Lemire，2019）以及其他论文中，我们描述了如何推导出答案。但在其他论文中，例如“使用 AVX2 指令实现更快的 Base64 编码和解码”（Muła 和 Lemire，2018） ，我们只给出了解决方案，没有进一步解释。
这些表中的常量必须经过计算才能满足所有可能输入字符的分类规则。考虑到有效字符和无效字符的重叠半字节模式，这可能是一项令人困惑的任务。我不建议使用 ChatGPT。但是，您可以使用像 Z3 这样的定理证明来自动化这项任务。Z3 可以将分类约束建模为可满足性问题，并自动计算一组满足要求的表值。
以下 Python 代码使用 Z3 来求解lut_lo和lut_hi表。首先导入 Z3 并创建一个求解器实例（ s = Solver() ）。定义两个 8 位位向量变量列表lut_lo和lut_hi来表示查找表，每个列表包含 16 个条目。base64 字符集（AZ、az、0-9、+、/）使用 ASCII 范围定义，无效字符标识为所有其他 ASCII 值（0 到 255）。向求解器添加了约束：base64 字符必须分类为 0，无效字符必须分类为大于 0 的值。求解器检查解决方案；如果找到，它将提取表值。这很简单！诚然，您必须知道如何使用 Z3。
从z3导入* s =求解器( ) lut_lo = [ BitVec （ f'lut_lo_ { i } ' ， 8 ） ， i在范围内（ 16 ） ] lut_hi = [ BitVec （ f'lut_hi_ { i } ' ， 8 ）对于范围内的i （ 16 ） ] # Base64 字符（AZ、az、0-9、+、/） base64_chars =列表（范围（ 65 , 91 ） ） +列表（范围（ 97 , 123 ） ） +列表（范围（ 48 , 58 ） ） + [ 43 , 47 ] invalid_chars = [ c对于c 在范围内（ 256 ）如果c不在base64_chars中] def分类（ c ） ： 下半字节= c & 0x0F 上半字节= c >> 4 返回lut_lo [ lower_nibble ] & lut_hi [ upper_nibble ] 对于base64_chars中的c ： s.add ( classify ( c ) == 0 ) 对于无效字符中的c ： s.add ( classify ( c ) > 0 ) 如果s.check ( ) == sat ： m = s .模型( ) 打印（ “ lut_lo = ” ， [ m [ lut_lo [ i ] ] .as_long （ ）对于i在范围内（ 16 ） ] ） 打印（ “ lut_hi = ” ， [ m [ lut_hi [ i ] ] .as_long （ ）对于i在范围内（ 16 ） ] ）
在这个例子中，它找到了以下解决方案：
lut_lo = [103, 39, 39, 39, 39, 39, 39, 39, 39, 39, 47, 31, 63, 63, 63, 31] lut_hi = [255, 255, 224, 152, 192, 144, 192, 144, 255, 255, 255, 255, 255, 255, 255, 255]
一般来说，解决方案不是唯一的。
在 Muła 和 Lemire (2018) 的论文中，我们解决了完整的 Base64 解码问题，并且至少还需要一张表。我已经在用于我博客的 GitHub 代码库中找到了关于如何进行完整计算的脚本。
如果您对矢量分类感兴趣，您可能会发现以下参考资料很有用：
- Lemire, D. (2025)。在 ARM 处理器上以每秒数十 GB 的速度扫描 HTML 。软件：实践与经验。
- Keiser, J. 和 Lemire, D. (2021)。用少于一条指令/字节验证 UTF-8 。软件：实践与经验， 51 (5)
- Koekkoek, J. 和 Lemire, D. (2025)。每秒解析数百万条 DNS 记录。软件：实践与经验， 55 (4), 778-788。
原文： https://lemire.me/blog/2025/06/01/easy-vectorized-classification-with-z3/