Z3py : how to extend and trunc variables?

Question

我有两个不同大小的变量“a”和“b”，见下文。我有几个问题:

(1) 如何将“a”的值复制到“b”？ (即扩展操作)

(2) 如何将“b”的值复制到“a”？ (即截断操作)

谢谢。

a = BitVec('a', 1)
b = BitVec('b', 32)

Answer 1

对于扩展，我们使用 ZeroExt或 SignExt . ZeroExt将添加“零”和 SignExt将“复制”符号位(即最高有效位)。对于截断，我们使用 Extract ，它可以提取比特的任何子序列。这是一个小例子(也可以在 rise4fun 在线获得)。

a = BitVec('a', 1)
b = BitVec('b', 32)
solve(ZeroExt(31, a) == b)
solve(b > 10, Extract(0,0,b) == a)

编辑 : 我们可以使用 p == (x == 1) '分配'一个 bool 变量 p具有位向量的值 x尺寸 1 ，反之亦然。公式 p == (x == 1)只是说明 p为真当且仅当 x是 1 .这是一个示例(也可在线获取 here)

x = BitVec('x', 1)
p = Bool('p')

solve(p == (x == 1), x == 0)
solve(p == (x == 1), x == 1)
solve(p == (x == 1), Not(p))
solve(p == (x == 1), p)