3

我目前正在研究通过 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 到底在使用什么逻辑。

谢谢！

4

1 回答 1

5

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 特定的扩展。

正如您所描述的，数组 sort(Array I1 I2 R)可以编码为(Array I1 (Array I2 R)).

在性能方面，Z3 3.x 和 4.x 没有针对阵列理论的性能改进。它们对位向量有很多改进，但是当问题混合数组和位向量时它们不可用。一个新的数组理论在 TODO 列表中，但 Z3 团队中目前没有人致力于此。

于 2012-11-18T19:06:31.210 回答