我正在使用 Z3 3.0 版。我想为一个位向量变量赋值,如下所示。
但是 Z3 报告错误“无效的函数应用程序,对第 3 行中位置 2 的参数排序不匹配”。
我的常量#x0a 似乎有问题?我怎样才能解决这个问题?
谢谢
(set-logic QF_BV)
(declare-fun a () (_ BitVec 32))
(assert (= a #x0a))
(check-sat)
最佳答案
在 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 的位向量。
关于z3 - 为位向量(SMTLIB2,Z3)赋值?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/7165118/