Z3 bitvecs 到 Int 并返回

Question

我有以下代码：

from z3 import *

a0 = Int('a0')
a1 = Int('a1')
a2 = Int('a2')
v1 = BitVec('v1',32)

s.add(v1 ==  ((a0 + a1) >> 31) >> 30)
s.add(((v1 + a2) & 3) - v1 == 1)

现在我收到以下错误：

TypeError: unsupported operand type(s) for >>: 'ArithRef' and 'int'

我明白这个问题，z3 不能像原生 python 那样处理隐式转换（即 45 >> 3 直接转换为 5）。但是，我需要我的变量 a_i 是整数。有办法实现吗？

Answer 1

您正在寻找 BV2Int 和 Int2BV。看这里：

https://z3prover.github.io/api/html/namespacez3py.html#a7954eb7ea27b3972070ac9eb6f5946a2

https://z3prover.github.io/api/html/namespacez3py.html#ac516cd29fb1da802c07a51b6be605115

Z3 bitvecs 到 Int 并返回

Z3 bitvecs to Int and back

python

z3

z3py