我目前正致力于将通过C程序的“路径”转换为相应的SMT查询以测试此路径的可行性的代码 . 我有工作代码创建SMT-LIB v1.2查询，并使用Z3 2.11和QF_AUFBV逻辑来解决查询 . 我目前正在将此代码移植到Z3 4.3，以利用自那时以来可能发生的任何速度提升，特别是因为我的前代码似乎需要花费很长时间（大约22分钟）来查询仅分配24个值一个三维数组并检查数组中某个位置的值 .
但是，似乎QF_AUFBV逻辑（从SMT-LIB v2.0标准开始）不再支持多维数组，或者更确切地说，数组的值也是数组（可能更深） . 一旦我从查询中取出“（set-logic QF_AUFBV）”行，Z3 4.3就可以处理查询，但仍需要很长时间 .
我想知道是否有人知道为什么在SMT-LIB v2.0标准中停止了对多维数组的支持，以及我可以使用的替代逻辑 . 当我拿出指定QF_AUFBV理论的那条线时，我还想知道Z3究竟使用了什么逻辑 .
谢谢！
1 回答
SMT-LIB标准从未支持多维阵列 . Z3可以处理它们，但它们不是标准的一部分 . SMT-LIB 1.0是一种非常严格的格式，这就是为什么Z3有几个扩展来满足用户需求的原因 . 另一方面，SMT-LIB 2.0是一种非常丰富的输入格式，并修复了用户对SMT-LIB 1.0的主要问题 . 在Z3 4.x中，当在输入文件中指定逻辑时，Z3尝试符合SMT-LIB 2.0标准 . 删除
set-logic后，将启用所有Z3特定扩展 .如您所述，数组sorrt
(Array I1 I2 R)可以编码为(Array I1 (Array I2 R)).关于性能，Z3 3.x和4.x没有针对阵列理论的性能改进 . 它们对位向量有很多改进，但当问题混合数组和位向量时它们不可用 . 一个新的阵列理论在TODO列表中，但Z3团队中没有人正在研究这个问题 .