支持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).理论上,基于模型的量化实例化(MBQI)模块保证Z3是该逻辑的决策过程,但由于高复杂性,Z3将在许多脚本中失败(在没有内存和/或时间的情况下运行).

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

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

关于虚假命令,例如(set-logic blarg),我添加了用于显示警告消息的代码,表示逻辑未被识别,并且Z3将使用所有可用的理论.修改将在Z3 3.2中提供.我还将AUFBV列入官方支持的逻辑列表中.