有没有推荐的按位向左或向右滚动的方法？
例如带有一个字节 - 0x57 rolr 3 = 0xEA。
我在 Z3py 文档中没有找到任何“滚动”操作。我正在考虑BitVec为每一位使用 s ，但这似乎效率不高/可能行不通。任何建议表示赞赏，谢谢。
编辑：感谢到目前为止的答案。这更像是一个 API 问题，因为我现在很讨厌它。这是我作为起点的内容。
def roll(bt):
count = BitVecVal(int('0x03', 16), 8)
s.add(bt == (bt << count | bt >> (8 - count)) & 0xFF)
a = BitVec('a', 8)
s = Solver()
roll(a)
s.add(a == BitVecVal(int('0xEA', 16), 8))
s.check()
这不会打印任何内容，并且模型不可用。