将值赋给位向量（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还支持形式(_ bv[num] [size])，其中[num]是十进制的位向量文字，和[size]是位向量的大小。 因此，您也可以将位向量文字#x0000000a写为(_ bv10 32)。

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