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