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 支持它。
谢谢!