z3 - 支持 AUFBV？

Question

Z3 会支持 AUFBV 吗？

对于以下脚本:

(set-logic AUFBV)
(declare-fun x () (_ BitVec 16))
(declare-const t (Array (_ BitVec 16) (_ BitVec 16)))
(assert (= (select t #x0000) #x0000))

在线 Z3 演示似乎对 set-logic 调用很满意，但随后它提示排序 BitVec 和 Array。 (顺便说一下，无论逻辑名称如何，在线演示似乎都对 set-logic 调用很满意，即使使用诸如 (set-logic blarg) 之类的虚假名称也是如此。)

SMT-Lib 网站既没有提到 UFBV 也没有提到 AUFBV，但考虑到它们的无量词对应项(QF_UFBV 和 QF_AUFBV)，我希望 Z3 也能支持 AUFBV。

不用说，数组在实践中起着非常重要的作用。鉴于有限性论证，我认为 AUFBV 逻辑应该保持可判定性。很高兴看到 Z3 支持它。

谢谢!

Answer 1

Z3 使用set-logic 命令来配置自身。如果 SMT 脚本不包含 set-logic，则启用所有理论求解器。如果您从脚本中删除 set-logic 命令，则 Z3 将按预期工作。

如您所说，AUFBV 逻辑是可判定的。但是，复杂度确实很高(NEXPTIME-complete)。理论上，基于模型的量词实例化 (Model Based Quantifier Instantiation, MBQI) 模块保证 Z3 是此逻辑的决策程序，但由于高度复杂，Z3 在许多脚本中会失败(在没有内存和/或时间的情况下运行)。

逻辑 AUFBV 不在官方支持的逻辑列表中。 Z3没有认出来，也没有装任何理论求解器。因此，要在 Z3 3.1 中使用此逻辑，您不应使用 set-logic 命令。

顺便说一句，你真的不需要数组。它们可以使用量词在 UFBV 中编码。在许多情况下，如果使用量词，最好避免数组理论。Z3 中的数组理论求解器针对无量词问题进行了优化。

关于(set-logic blarg)等伪命令，我添加了显示警告信息的代码，表示逻辑未被识别，Z3将使用所有可用的理论。该修改将在 Z3 3.2 中可用。我还将 AUFBV 包含在官方支持的逻辑列表中。