将值赋给位向量(SMTLIB2,Z3)？

Question

我使用的是Z3 3.0版.我想为bitvector变量赋值,如下所示.但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还支持表单的bitvector文字(_ bv[num] [size]),其中[num]是十进制表示法,并且[size]是bitvector的大小.因此,您也可以将bitvector文字写#x0000000a为(_ bv10 32).

顺便说一句,SMT-LIB也支持二进制表示法中的bitvector文字.例如,#b010是一个大小为3的位向量.