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 的位向量。