z3 - 为位向量（SMTLIB2，Z3）赋值？

Question

我正在使用 Z3 3.0 版。我想为位向量变量赋值，如下所示。但是 Z3 报告错误“无效的函数应用程序，第 3 行位置 2 的参数排序不匹配”。

我的常量#x0a 似乎有问题？我怎样才能解决这个问题？

谢谢

(set-logic QF_BV)
(declare-fun a () (_ BitVec 32))
(assert (= a #x0a))
(check-sat)

Answer 1

在 SMT-LIB 2.0 标准中，#x0a是大小为 8 的位向量。您会收到排序不匹配错误，因为该常量a是大小为 32 的位向量。您可以通过将示例重写为来避免类型/排序错误消息：

(set-logic QF_BV)
(declare-fun a () (_ BitVec 32))
(assert (= a #x0000000a))
(check-sat)

SMT-LIB 还支持格式为 的位向量文字(_ bv[num] [size])，其中[num]是十进制表示法，[size]是位向量的大小。因此，您也可以将位向量文字写#x0000000a为(_ bv10 32).

顺便说一句，SMT-LIB 还支持二进制表示法的位向量文字。例如，#b010是大小为 3 的位向量。