Z3：如何从一个常数中提取（）？答案

【问题标题】：Z3: how to Extract() from a constant number?Z3：如何从一个常数中提取（）？
【发布时间】：2013-05-09 09:02:45
【问题描述】：

在 Z3 Python 中，要提取一个 BitVector V 的 8 位，我们可以这样做：

Extract(7, 0, V)

但是，有时在我的程序中，V 可以是一个常数，所以在这种情况下，代码实际上是这样的：

Extract(7, 0, 0x87654)

不幸的是，这是错误的，因为上面的代码没有指定 0x87654 是 32 位 BitVector.7

一种解决方案是创建一个临时变量，例如：

tmp = BitVec('tmp', 32)
tmp == 0x87654
Extract(7, 0, tmp)

但是，这有点麻烦，因为我必须创建一个临时的才能工作。我想知道是否有另一种方法而不必创建临时变量？有没有办法在我的代码中将 0x87654 转换为内联 BitVector？

非常感谢。

【问题讨论】：

标签： python z3

【解决方案1】：

我想你想用BitVecVal(value, bits):

Extract(7, 0, BitVecVal(0x87654, 32))

【讨论】：