2

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,但随后它抱怨各种BitVecArray. (顺便说一句,无论逻辑名称如何,在线演示似乎都对调用感到满意set-logic,即使是假名,例如(set-logic blarg)。)

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

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

谢谢!

4

1 回答 1

7

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

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

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

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

关于诸如 之类的虚假命令(set-logic blarg),我添加了用于显示警告消息的代码,说明逻辑未被识别,Z3 将使用所有可用的理论。修改将在 Z3 3.2 中可用。我还在官方支持的逻辑列表中包含了 AUFBV。

于 2011-09-14T12:51:33.027 回答