在Z3中为BitVec定义特定的值范围

Question

我正在Python中使用Z3-solver。我非常感谢帮助定义具有特定范围的BitVectors。例如，我有一个问题，我想计算三个变量的总和（32位大小），这将导致溢出。变量必须仅包含A-F范围内的十六进制数字。

是否可以为数字中的每个数字设置特定范围？

谢谢！

Answer 1

我们可以将每个变量定义为BitVec，然后从向量中提取位（在我的情况下，因为它是十六进制数字，所以我一次提取了4位），然后使用BV2Int将这些位转换为整数。现在，我们可以使用大的Or表达式将约束放到每个数字中。工作代码（Python 3）：

def is_valid(x):
    x = BV2Int(x,False)
    return Or(<constraints>)

def check_digits(x):
    for i in range(0,28,4):
        hexdig = Extract(i+4,i,x)
        S.add(is_valid(hexdig))

S=Solver()
a1 = BitVec("a1", 32)
a2 = BitVec("a2", 32)
a3 = BitVec("a3", 32)
check_digits(a1)
check_digits(a2)
check_digits(a3)
S.add(a1+a2+a3==0)


print(S.check())
print(S.model())